The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hi Frédéric,

This is a question on which we have not been consistent over time
indeed. We don't want to overload the release manager, who does not
have to be an opam user, or have any knowledge about opam. However, it
could be said that the release manager alerts competent people and
waits for the opam package to be available before sending the
announcement. But the main opam repository, on which stable Coq
releases are published, is outside of our control, and pull requests
can take a non-predictable amount of time to get merged.

Delaying the announcement for several days because the opam package is
not available would mean delaying it for everyone, including users who
have other ways of installing Coq, such as the Windows or macOS
packages, or some package distributed in some very reactive
distribution (cf. https://repology.org/project/coq/versions).

A solution that has sometimes been used in the past is to wait at
least for a pull request to be opened on the opam repository, mention
in the announcement that opam packages will be available shortly, when
said pull request is merged, and provide the link. How does that
sound?

Théo

Le jeu. 10 oct. 2019 à 09:03, Frédéric Blanqui
<frederic.blanqui AT inria.fr>
 a écrit :
>
> Hello Théo. Why don't you announce the availability of a new version
> only when it is actually available on opam?
>
> Le 09/10/2019 à 18:25, Théo Zimmermann a écrit :
> > The opam package is actively being worked on:
> > https://github.com/ocaml/opam-repository/pull/15017
> >
> > I don't participate, so I wouldn't be able to estimate accurately, but
> > I'd say it shouldn't take long before the pull request is merged and
> > the package is available.
> >
> > Cheers,
> > Théo
> >
> > Le mer. 9 oct. 2019 à 18:24, Xuanrui Qi 
> > <xuanrui AT cs.tufts.edu>
> >  a écrit :
> >> Hi,
> >>
> >> How long do we have to wait approximately for 8.10.0 to be on opam?
> >>
> >> Thanks,
> >> Xuanrui
> >>
> >> On Wed, 2019-10-09 at 15:27 +0000, Vincent Laporte wrote:
> >>> Dear Coq users,
> >>>
> >>> The 8.10.0 release of Coq is available.
> >>>
> >>> Main changes:
> >>>
> >>> -   some quality-of-life bug fixes;
> >>> -   a critical bug fix related to template polymorphism;
> >>> -   native 63-bit machine integers;
> >>> -   a new sort of definitionally proof-irrelevant propositions:
> >>> SProp;
> >>> -   private universes for opaque polymorphic constants;
> >>> -   string notations and numeral notations;
> >>> -   a new simplex-based proof engine for the tactics lia, nia, lra
> >>> and nra;
> >>> -   new introduction patterns for SSReflect;
> >>> -   a tactic to rewrite under binders: under;
> >>> -   easy input of non-ASCII symbols in CoqIDE, which now uses GTK3.
> >>>
> >>> All details can be found in the user manual:
> >>> https://coq.inria.fr/distrib/current/refman/changes.html#version-8-10
> >>>
> >>> Pre-compiled binaries can be downloaded from the “release” page:
> >>> https://github.com/coq/coq/releases/tag/V8.10.0
> >>>
> >>> Feedback and bug reports are extremely welcome.
> >>>
> >>> --
> >>> Vincent Laporte.
> >>>