The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hello Coq-club member,

I take this opportunity to point out that the current proofgeneral dev
version is compatible with coq-8.5beta1, the current cvs fixes a few
small problems and a new dev version should be out soon.

It does not take advantage of the new fancy asynchronous edition
mechanism and it is unclear if and when it will (volunteers welcome).

Suggestions and bug reports are welcome.

Best regards,
Pierre Courtieu

Main new features:
- Asynchronous parallel compilation of required modules (nothing to do
with asynchronous edition)
- Support for _Coqproject files (sets the coq load path and options 
accordingly)
- Support for prettify-symbols-mode

Main fixes:
- indentation improved (still not perfect)
- annoying cursor jump experienced by some users seems fixed


2015-01-29 21:49 GMT+01:00 Matthieu Sozeau 
<matthieu.sozeau AT inria.fr>:
> Dear Coq-Club members,
>
> The Coq development team is pleased to announce the release of the first 
> beta
> version of Coq 8.5 at http://coq.inria.fr/. The new available features 
> include:
>
> - 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 whishes to acknowledge the many
> people which 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