The Coq mailing list

[Guillaume Claret <guillaume AT claret.me>]

The 04/11/2015 16:58, Julien Narboux wrote:
> Just to add another little bit to this discussion.
> Opam seems to be the new standard way to install ocaml programs: coq,
> frama-c, etc.
> But opam does not support out of the box multi-user systems, and this is
> a problem when you want to use it in the classroom.
> We had to create a special shared directory for opam.

You mean with the root option? Like:

    mkdir /shared/opam
    opam init --root=/shared/opam
    eval `opam config env --root=/shared/opam`
    opam install ...

?

> Julien
>
>
>
> 2015-11-02 17:48 GMT+01:00 Arthur Azevedo de Amorim 
> <arthur.aa AT gmail.com
> <mailto:arthur.aa AT gmail.com>>:
>
>     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.
>
>     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