OPAM: try out coq as a compiler

[gares]

When #587 is fixed, we can then experiment with what opam2 promises, that is to handle coq as a compiler.
This should make it possible to "root" an entire switch around a coq version, and automatically reomcpile things when coq is updated.

[Zimmi48]

What would be really awesome then would be to support Coq as a system compiler, e.g. when installed through the distribution's package manager. I don't know if that's a supported use case.

[gares]

Nice idea. I was planning to wait the opam2.0 transition and then study the possibilities... I don't know if system is special...

[Zimmi48]

(The point being that the Coq packages specify a dependency on Coq but it should be supported to satisfy this dependency with a system-wide install of Coq, like it is possible to do with the OCaml compiler.)

[ejgallego]

Umm, as far as I know the concept of compiler is less special in OPAM2 than in OPAM1, already, if the packages properly depend on Coq in runtime fashion [which they must] they will get rebuilt], so I am not sure what this would change.

My impression also is that system compilers are discouraged, as they tend to create many problems due to opam not being notified of upgrades in the package-manager side. So even if I am not sure they are deprecated yet, they are certainly to be avoided.

[gares]

A switch is created using opam switch create <switch> (<compiler>|--empty).
[cut]
If a compiler is selected, opam will install the corresponding packages and their dependencies in the new switch. These packages will be marked as base, protected against removal and unaffected by upgrade commands. compiler can be selected among packages which have the compiler flag set, or their versions. Use opam switch list-available to list them.

So it seems we can just flag the coq package as being a compiler, then opam switch would list it as such and one can the initialize the switch by choosing a coq version (rather than an ocaml one)

[ejgallego]

Yup so indeed what this does is to pin the package , however setting the flag would mean that coq is not upgraded, so it'd be great for some users , not so for others, I dunno.

[gares]

available: [ <filter> ]: can be used to add constraints on the OS and other global 
variables. In case the filter doesn't evaluate to true, the package is disabled.

And we should be able to use available to express hard dependency on Coq

This field is evaluated before request solving or any actions take place ; it can only refer to global variables, since it shouldn't depend on the current switch state. An unavailable package won't generally be seen on the system, except with opam list -A.

That is, unavailable package are not even listed, rather than listed but uninstallable

[gares]

Yup so indeed what this does is to pin the package , however setting the flag would mean that coq is not upgraded, so it'd be great for some users , not so for others, I dunno.

Right. IIRC there is a way to say "build a new switch X on compiler C and put in all packages I've in switch Y (on compiler D)". So I think "upgrading" is still possible, but will not erase the old switch. This seems a feature to me.

[gares]

Here it is:

Ability to export a compiler universe into another one

This means “replicate the state (installed packages, etc.) from one compiler to another one”. It is useful if you want to have the ability to fork a given compiler. The syntax is

opam switch <version>
opam switch export universe_for_<version>
opam switch <other-version>
opam switch import universe_for_<version>

The import installs all packages from the file into the currently selected compiler. The above sequence of commands will install all packages installed in the compiler <version> into the compiler <other-version>.