The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

> On 13 Nov 2015, at 12:49, Maxime Dénès 
> <mail AT maximedenes.fr>
>  wrote:
> 
> Hello Frédéric,
> 
> You can find the opam package for 8.5 beta 3 on the "core-dev" opam repo 
> for coq:
Thanks a lot — a new repo I did not know of.

> 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.
I was among them!


--
Frédéric

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

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail