The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hello Frédéric,

You can find the opam package for 8.5 beta 3 on the "core-dev" opam repo 
for coq:

opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev

Beta versions were moved from the "released" repo to "core-dev" because 
some users found counter-intuitive that opam was suggesting to upgrade 
stable versions of Coq to betas.

Enjoy!

Maxime.

On 11/12/15 23:41, Frédéric Besson wrote:
> Hello Maxime,
>
> Is there an opam package for coq8.5.beta3 — somewhere ?
> I have a beta1, beta2 but  beta3 does not show up…
>
> Thanks for the good work,
>
> Best,
> —
> Frédéric
>
> > On 12 Nov 2015, at 01:05, Maxime Dénès 
> > <mail AT maximedenes.fr>
> >  wrote:
> >
> > Dear Coq-Clubers,
> >
> >   The Coq development team is pleased to announce the release of the
> > third beta version of Coq 8.5 available at:
> >
> > http://coq.inria.fr/coq-85
> >
> >   This new beta version includes many bug fixes with respect to the first
> > two beta versions, and a few incompatible changes, see
> > the following file for more information:
> >
> > https://coq.inria.fr/distrib/V8.5beta3/CHANGES
> >
> > Source, Windows and OS X packages are available.
> >
> > We recall the new available features of version 8.5:
> >
> > - asynchronous edition of documents under CoqIDE to keep working on a
> >   proof while Coq checks the other proofs in the background (by Enrico
> >   Tassi);
> > - universe polymorphism making it possible to reuse the same
> >   definitions at various universe levels (by Matthieu Sozeau);
> > - primitive projections improving space and time efficiency of
> >   records, and adding eta-conversion for records (by Matthieu Sozeau);
> > - extensions of the new proof engine featuring dependent subgoals
> >   management, fully backtracking tactics, as well as tactics which can
> >   consider multiple goals together (by Arnaud Spiwack);
> > - a new reduction procedure called native_compute to evaluate terms
> >   using the OCaml native compiler, for proofs with large computational
> >   steps (by Maxime Dénès).
> >
> > The main other changes are:
> >
> > - a new fast compilation chain that skips checking of proofs (producing
> >   .vio files);
> > - a new construct $(..)$ to call tactics from term definitions;
> > - a more restrictive guard condition to recover compatibility with axioms
> >   like propositional extensionality and (some consequences of) univalence;
> > - a new option -type-in-type to collapse the universe hierarchy (makes
> >   the logic inconsistent but useful for exploration);
> > - a better-behaved alternative to simpl, called cbn;
> > - various improvements to the tactic language, like a new introduction
> >   pattern [= x1 ... xn] which applies injection on the fly (inspired
> >   by SSReflect); new constructs uconstr:c and type_term c to build
> >   untyped terms in Ltac;
> > - significant improvements of general efficiency.
> >
> > See http://coq.inria.fr/  for more details, and the CHANGES file in the
> > distribution for a comprehensive list.
> >
> > The Coq development team wishes to acknowledge the many
> > people who made Coq 8.5 possible: Pierre Boutillier,
> > Pierre Courtieu, Maxime Dénès, Hugo Herbelin, Pierre Letouzey,
> > Pierre-Marie Pédrot, Yann Régis-Gianas, Matthieu Sozeau, Arnaud
> > Spiwack, Enrico Tassi with contributions also from Bruno Barras, Yves
> > Bertot, Frédéric Besson, Xavier Clerc, Pierre Corbineau,
> > Jean-Christophe Filliâtre, Julien Forest, Sébastien Hinderer, Assia
> > Mahboubi, Guillaume Melquiond, Jean-Marc Notin, François Ripault,
> > Carst Tankink as well as many external contributors.
> >
> > The Coq Development Team