[question] Howto debug/fix slow constraint solving

[gares]

This takes minutes to propose a solution.

opam switch create 4.05.0
opam repo add coq https://coq.inria.fr/opam/released
OPAMSOLVERTIMEOUT=3400 opam install coq-monae

It works fine with a 4.07 or 4.09 switch, see also: coq/opam#1572

How can we debug the issue?

It's not a big deal this time, since it seems tied to an old OCaml compiler we may drop soonish, but for the future, I'd like to understand the issue.

[AltGr]

Thanks for reporting. Indeed, with the growth of the repository, the solver sometimes struggles... Here are a few things you can try:

• are you on the latest 2.1 beta ? We added some pre-processing which helps a lot, although not in all cases
• you can try alternate solvers; z3 has much fewer worst cases than the built-in mccs+glpk, but you will need to recompile opam with support (opam install z3 opam-devel) — it's to heavy to be included by default. Then run with --solver=builtin-z3
• the 0install solver is another alternative; it's more limited in terms of features (e.g. it may force upgrades), but more reliable in terms of solving time. Compile support with (opam install opam-0install-cudf opam-devel), then run with --solver=builtin-0install.

As for your question proper ("how to debug/fix"), this is quite hard since solvers are black boxes. They tend, however, to struggle with disjunctions (many versions of a package available and compatible, with lots of choices of dependencies), so multiple levels of dependencies with many possibilities should be avoided.

If you want to dig deeper, you can fine-tune the preprocessing with (see src/solver/opamCudf.ml for details):

• OPAMCUDFTRIM=false|simple|true controls if the pre-processing is done; --debug will add info about how many package it could trim.
• OPAMDIGDEPTH=2 controls the number of trimming iterations
• OPAMVERSIONLAGPOWER=1 not to be used in production, this is unreliable and dangerous, but setting it to 2 or 3 biases the solvers in ways that sometimes make it find a solution much more quickly.

Note that this is still being worked on, and we have a few other ideas for improving further :)

[gares]

The very great news is that 2.1~beta4 takes 10 seconds to answer, rather than minutes.

[AltGr]

Additional note: the Z3 backend, in the newer versions, has the added benefit that even if it times out, it will still provide a correct solution. Although not proved optimal, in practice these solution are pretty good already, and the difference does not matter in general.

[dra27]

Looks like this was solved with 2.1.0 - please feel free to re-open as necessary!