coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Frédéric Besson <frederic.besson AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Coq 8.5 beta 3
- Date: Thu, 12 Nov 2015 23:41:30 +0100
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
Attachment:
signature.asc
Description: Message signed with OpenPGP using GPGMail
- [Coq-Club] Coq 8.5 beta 3, Maxime Dénès, 11/12/2015
- Re: [Coq-Club] Coq 8.5 beta 3, Frédéric Besson, 11/12/2015
- Re: [Coq-Club] Coq 8.5 beta 3, Maxime Dénès, 11/13/2015
- Re: [Coq-Club] Coq 8.5 beta 3, Frédéric Besson, 11/13/2015
- Re: [Coq-Club] Coq 8.5 beta 3, Maxime Dénès, 11/13/2015
- Re: [Coq-Club] Coq 8.5 beta 3, Frédéric Besson, 11/12/2015
Archive powered by MHonArc 2.6.18.