The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

>> 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.

What was proposed? If this is about releasing the beta on opam, then I
agree. But this is not what I am saying here: today, 8.5b2 is the
*default* upgrade from 8.4.6.

>
>> 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.

So, the result is going to be that people using an library incompatible
with 8.5 will be stuck in 8.4.6 (=> useless upgrade).

For other people (like me), they will loose 20minutes installing the new
version then downgrading to 8.4.6 because obviously their developments
won't be compatible. Then, the result is that my current version of Coq
is pinned, so that a future pl of the 8.4 branch won't install.

From my point of view, an automatic upgrade using opam should be
(mostly) transparent to the user: opam upgrade is something you execute
without looking into the details of what's going to happen, because you
trust the packagers for maintaining reasonable compatibility.

>
>> 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.
>

And you pin the coq packages on your 8.4 switches? Even if this works,
how are you going to explain that to users? The good thing about opam is
that it works "out of the box", and no complicated setting is needed.
This does seem like a hack, so let's please do not make it the idiomatic
way of using opam for Coq.


-- 
JH

Attachment: signature.asc
Description: OpenPGP digital signature