Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Opam & Coq 8.5 beta 2

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Opam & Coq 8.5 beta 2


Chronological Thread 
  • From: Guillaume Claret <guillaume AT claret.me>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Opam & Coq 8.5 beta 2
  • Date: Sun, 1 Nov 2015 22:54:33 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=guillaume AT claret.me; spf=Neutral smtp.mailfrom=guillaume AT claret.me; spf=None smtp.helo=postmaster AT relay3-d.mail.gandi.net
  • Ironport-phdr: 9a23:Q/ySDRFrVHU6N6wjli/BuZ1GYnF86YWxBRYc798ds5kLTJ75osmwAkXT6L1XgUPTWs2DsrQf27eQ6fyrADVfqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh730ocGYOlwXzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IZ4yhIP99FeAQTGl+cjN92Mq+vh7aCACL+3E0U2MMkxMODRKWwgv9W8Leryr+suNg3STSFsn/V70oEWCt8qZvTBb1jSovPDow6mzLzMl92vEI6Cm9rgByltaHKLqeM+BzK/6FcA==

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 ?




Archive powered by MHonArc 2.6.18.

Top of Page