The Coq mailing list

[Agnishom Chattopadhyay <agnishom AT cmi.ac.in>]

By the way, I re-ran the installation script after running `opam repository remove coq-released --all` and this time it worked fine.

On Mon, Sep 28, 2020 at 5:14 AM Michael Soegtrop <MSoegtrop AT yahoo.de> wrote:

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