The Coq mailing list

[Guillaume Claret <guillaume AT claret.me>]

The 02/11/2015 15:38, Jacques-Henri Jourdan wrote:
> > > 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.

In OPAM, the default upgrade is always the greater version number
available. Thus, this is technically not possible to both have the 8.5b2
in the `realeased` repository and a default upgrade to `8.4.6`. (Other
package managers, such as npm, interpret the version names so that the
betas and alphas are not proposed as updates by default, as you seem to
expect).

Here is an issue to discuss the inclusion of the beta of Coq in the
`released` repository:
https://github.com/coq/opam-coq-archive/issues/17

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

To me, this part is OK.

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

I agree that this is painful. The compilation time of Coq also hurts for
people doing continuous integration for example. To me, the solution 
would be
to have a smaller Coq, by having a lighter standard library for example.

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

A (possible) solution for that: to have an `opam` file at the root of your
development, with a constraint:

    "coq" {>= "8.4.5" & < "8.5~"}

This local `opam` file can be activated by a `pin`:
https://opam.ocaml.org/blog/opam-1-2-pin/
Having a local `opam` file is also useful to describe all your dependencies
to collaborators, and will serve to publish the package.

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

In my experience, a package manager for a programming language is not the
same thing as a package manager for a Linux distribution. In particular,
updates tend to be rare and painful, and many do not considered this as 
a bug.
This is probably because:

* it is hard (in practice) to enforce synchronization among all developers
so that all packages are compatible together;
* packages are made for a compiler, not for a human. You may not care if
your Firefox menu moved a little, but a change in a library will quickly be
a breaking change for your developments.

The way this is solved (in my experience) is by explicitly fixing a static
development environment for each project. Then, for each project you install
its dependencies in a "fresh" environment to avoid clashes between projects.
To illustrate these practices, I can cite:

* Ruby's Bundler: http://bundler.io/
* Python's Virtualenv: https://virtualenv.readthedocs.org/en/latest/
* JavaScript's npm: 
https://docs.npmjs.com/getting-started/installing-npm-packages-locally

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

To me, a package manager for a programming language is not supposed to work
"out of the box" for the updates.