Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Coq 8.5 is out!

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq 8.5 is out!


Chronological Thread 
  • From: Maxime Dénès <mail AT maximedenes.fr>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Coq 8.5 is out!
  • Date: Fri, 22 Jan 2016 01:22:13 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mail AT maximedenes.fr; spf=Pass smtp.mailfrom=mail AT maximedenes.fr; spf=None smtp.helo=postmaster AT 11.mo1.mail-out.ovh.net
  • Ironport-phdr: 9a23:4SNebBAC0IgdvfEHEbfwUyQJP3N1i/DPJgcQr6AfoPdwSP74oMbcNUDSrc9gkEXOFd2CrakU1ayP6/yrAzdIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/niabro8GYOV4ArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8/VPlTCCksG2Ez/szi8xfZHiWV4X5Jd2wGkx9FSyRE6pHhFsP0uyr+nu90yCifMMH7S70vHzq4ufQ4ACT0gTsKYmZquFrcjdZ92fpW

Dear Coq-Clubers,

The Coq development team is pleased to announce the final release
of Coq 8.5 available at:

http://coq.inria.fr/coq-85

This release includes many bug fixes with respect to the previous
versions, and a few incompatible changes, see the following file for
more information:

https://coq.inria.fr/distrib/V8.5/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 ltac:(..) 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




Archive powered by MHonArc 2.6.18.

Top of Page