Solver is often stumped by restrictive upper bounds

[snoyberg]

To define the term: by "restrictive upper bound" I mean an upper bound which excludes some packages available from Hackage. So if foo 1.0, 1.1, and 1.2 are available on Hackage, a bound of foo < 1.3 would not be restrictive, whereas foo < 1.2 would be restrictive.

I went to build a project I haven't touched in a few months (haskellers.com), and cabal was unable to produce a build plan. Eventually, I whittled this down to this cabal file. In this file, there is only one restrictive upper bound: http-conduit. I then ran the following command with both cabal-install 1.16 + GHC 7.6 and cabal-install 1.18 + GHC 7.8:

clear;date;cabal install --dry-run --reorder-goals --max-backjumps=-1;date

In both cases, there was no response for approximately 15 minutes, at which point I killed cabal. However, I was able to cause the dry run to succeed almost immediately (< 10 seconds) with either of the following:

1. Adding: --constraint 'http-conduit == 1.9.6'
2. Relaxing the upper bound on http-conduit to allow the newest version.

I'd like to note that these are the kinds of errors Yesod users complained about regularly in the past. The ultimate "solution" I settled on was (1) encourage usage of yesod-platform to help out the constraint solver, and (2) remove most upper bounds in cabal files. Obviously it would be better if cabal was better able to handle these situations.

[tibbe]

I would be interested to know if a proper SMT solver would come up with a solution, when fed with the constraints. It would be possible to have cabal just print all the constraints and then copy-n-paste them into an off-the-shelf constraint solver.

[NathanHowell]

I mostly hacked together a Cabal version constraint solver prototype using Z3 a while back. It works, and it is fast. Like all of Hackage in less than a second fast. There needs to be a lot more work done to produce user friendly errors, and to apply some other common sense rules.. it also needs some patches to the z3 bindings to support incremental solves. Etc etc.

https://gist.github.com/NathanHowell/5688647

[tibbe]

@NathanHowell That's really cool. Do you have an example of the kind of error messages it gives and your thoughts on how they could be improved? I would like to investigate using a real solver. It might get rid of lots of the problems we have.

Ideally the solver error message would include a minimal sense of constraints that cause a conflict to appear. Can Z3 produce such a thing?

[byorgey]

Whoops, I was writing a comment but then decided against it, and accidentally clicked "close".

[avsm]

@tibbe : we use aspcud in OPAM, which uses a format called CUDF as the interchange format to external solvers. Would probably be effective for Cabal too...

[NathanHowell]

@tibbe SAT and SMT solvers provide some tools for this but generally you need to do it yourself. If a solution is found it may not be the best one, but it is a solution. And for counterexamples they can be complex, not a simple one... So you need to do that yourself. Incremental solvers like z3 can make it faster but it's still a lot of code to write.

[snoyberg]

I'm beginning to think this is caused exclusively by --reorder-goals. I was doing some investigation into something similar the other day, and was able to get cabal to sit at "Resolving dependencies" for over an hour. Removing --reorder-goals and keeping just --max-backjumps=-1 let it complete in under a minute.