The Coq mailing list

[Michael Soegtrop <MSoegtrop AT yahoo.de>]

Dear Andrew,

> (Personally I find this a bit mysterious, as I would have thought that
> this is exactly the purpose of opam itself, but apparently opam needs
> some help.)

The issue is that the version and prerequisite dependencies given in an 
opam file are not fully tested, and probably are not feasible to test in 
their generality.

If you have an opam package with 5 dependencies, the accepted version 
set for each dependency might be say 5 versions. So testing if the 
information in an opam package is accurate would require testing 5^5 = 
3125 different combinations of package versions - each on multiple 
systems, compilers, .... Typically opam CI tests just one of these 
combinations. Some of these might not be allowed by version restrictions 
in the dependencies, but the allowed number can still be large.

Which combination of package versions you get with an "opam install" 
<some-package> might change dramatically from one day to another. There 
might be a package in your dependencies which only has an older version 
which via a chain of version requirements restricts a lot of other 
packages to an older version - opam telling you that you need Coq 8.7 is 
not that rare. An update of this one package will lead to a lot of 
packages changing their version and in the end might break things. So 
what works one day might not work a week later.

Furthermore installing two opam packages with a common dependency can 
lead to additional restrictions on the versions of dependencies which 
will lead to a combination of package versions which is tested with 
neither package. When installing 80 opam packages (as the Coq platform 
does) these effects can get very substantial.

On top of this comes the dependency on operating systems (especially the 
many Linux distributions), compiler versions and computer hardware (an 
opam install can take > 8 GB of RAM while 4 and 8 GB is still quite common).

Are there ways out of this? Well it is not that easy. One could restrict 
the dependency specification in opam packages to version combinations 
which are actually tested in CI. But this would make the dependencies so 
stiff that one could not install a larger Coq system any more because 
installing many packages would lead to unsolvable dependency conflicts. 
One would need a generic algorithms to find the sweet spot in package 
dependencies between testability and flexibility. Since already solving 
dependencies for a known set of version restrictions is a NP-complete 
problem [5][6], I have little hope that we will have this soon.

The idea behind the Coq platform [1][2][3] is to solve this problem by 
forcing at least all major dependencies in the Coq ecosystem into the 
same release cadence as Coq itself. Each author of a package provided in 
the Coq platform is expected to provide a version of the package which 
is compatible with the latest version of Coq and all other packages in 
the Coq platform in a reasonable time. This restricts the number of 
versions combinations to test to *one* while (hopefully) maintaining 
enough flexibility - or better enough structure - to not lead to 
unsolvable dependency restrictions. As you can see in the opam patch 
repository for the Coq platform 8.12 beta1 release [4] even finding this 
one set of versions requires patches to the opam database.

So yes, opam needs some help but not on its technical side - it is an 
excellent package manager - but on organizing the Coq opam package 
database in a way which makes testing it a technically feasible problem. 
Once we have this, a simple "opam install" should also work fine for 
most users and the scripts provided by the platform should just be a 
small extra to simplify the setup for beginners.

Best regards,

Michael

[1] https://github.com/coq/platform/blob/v8.12.0%2Bbeta1/charter.md
[2] https://github.com/coq/platform/blob/v8.12.0%2Bbeta1/README.md
[3] https://github.com/coq/platform/releases/tag/v8.12.0%2Bbeta1
[4] https://github.com/coq/platform/tree/master/opam/packages
[5] http://opam.ocaml.org/doc/External_solvers.html
[6] 
https://hal.archives-ouvertes.fr/file/index/docid/149566/filename/ase.pdf