coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Matthieu Sozeau <matthieu.sozeau AT inria.fr>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Coq 8.5 beta 1
- Date: Thu, 29 Jan 2015 21:49:53 +0100
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
- [Coq-Club] Coq 8.5 beta 1, Matthieu Sozeau, 01/29/2015
- Re: [Coq-Club] Coq 8.5 beta 1, Jonathan Leivent, 01/29/2015
- Re: [Coq-Club] Coq 8.5 beta 1, John Wiegley, 01/30/2015
- Re: [Coq-Club] Coq 8.5 beta 1, Pierre Courtieu, 01/30/2015
- [Coq-Club] Ssreflect and MathComp 1.5 for Coq 8.5beta1 available, Enrico Tassi, 01/30/2015
Archive powered by MHonArc 2.6.18.