The Coq mailing list

[Guillaume Claret <guillaume AT claret.me>]

Hi,

The 01/11/2015 21:43, Jacques-Henri Jourdan wrote:
> Hi coq-club,
>
> Coq 8.5 beta 2 has been released, and now my opam wants to update my
> 8.4.6 to 8.5. My Coq developments are not compatible to 8.5, so I do not
> want this upgrade to happen on my computer.
>
> It seems to me that:
> 1- It is not a good idea to make a beta available as a default upgrade
> in opam

As far as I remember, this was proposed to motivate people to try the beta.

> 2- It is not a good idea to release 8.5 as an update to 8.4.6, since
> mast developments wont compile on both versions. I'd rather publish it
> as a different package that needs to be installed separately

In my opinion:
This problem of incompatibility between successive versions will also occur
for libraries. Thus, we should start using the versions numbers + 
dependencies
constraints mechanism for Coq, to promote practices which will scale for the
libraries. And on the long term, if Coq releases become more frequent, there
should be less compatibility issues between Coq versions. Even today, *some*
packages are compatible with both 8.4 and 8.5, like Coquelicot.

> Am I the only user of Coq in this situation?

I am in this situation too :). I have one OPAM folder per version of Coq 
(the
OPAM folder can be set with the `--root=` option). Alternatively, the switch
mechanism offers the same possibility.

> Are the Coq developers sure that all the packages in the opam repo are
> compatible with 8.5 (AFAIK, the opam package in opam for CompCert is not) ?

The meta-data of the OPAM packages precise whether a package is 
compatible with
Coq 8.5 or not. If a package is not compatible with Coq 8.5, OPAM will 
propose
to downgrade Coq to 8.4. The OPAM bench helps us to check the 
compatibility of
the packages:
https://coq-bench.github.io/clean/Linux-x86_64-4.02.2-1.2.2/released/
(45 compatible and 35 not compatible with Coq 8.5~beta2)

> What is the easiest way to forbid opam doing this upgrade ?