The Coq mailing list

[Guillaume Claret <guillaume AT claret.me>]

The 02/11/2015 17:48, Arthur Azevedo de Amorim wrote:
> Just to add a little bit to this discussion. I held a Coq tutorial a few
> days ago and proposed opam as a good way of installing Coq. When people
> arrived, most of them had installation problems because of this issue,
> in particular because of coqide if I remember correctly. In the end, we
> ended up spending 45 minutes just on installation issues...
>
> It would be nice if people could use opam to install 8.5, while ensuring
> that 8.4 is installed by default.

Yes. We should probably move the beta from the `released` repository to the
`core-dev` repository. See this issue:
https://github.com/coq/opam-coq-archive/issues/17

In general, I agree that there are problems with the installation of Coq
through OPAM and that this is not totally ready.

> Em seg, 2 de nov de 2015 às 09:39, Jacques-Henri Jourdan
> <jacques-henri.jourdan AT inria.fr
>  
> <mailto:jacques-henri.jourdan AT inria.fr>>
> escreveu:
>
>
>     >> 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