The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Dear Coq Clubbers,

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

  http://coq.inria.fr/download

You may need to refresh the page if your browser has a previous version
in cache.

Source, Windows and OS X packages are available.

This release includes:

- A new, faster state-of-the-art universe constraint checker by
  Jacques-Henri Jourdan.
- In CoqIDE and other asynchronous interfaces, more fine-grained
  asynchronous processing and error reporting by Enrico Tassi, making
  Coq capable of recovering from errors and continuing to process the
  document.
- Better access to the proof engine features from Ltac: goal management
  primitives, range selectors and a typeclasses eauto engine handling
  multiple goals and multiple successes, by Cyprien Mangin, Matthieu
  Sozeau and Arnaud Spiwack.
- Tactic behavior uniformization and specification, generalization of
  intro-patterns by Hugo Herbelin and others.
- A brand new warning system allowing to control warnings, turn them
  into errors or ignore them selectively by Maxime Dénès, Guillaume
  Melquiond, Pierre-Marie Pédrot and others.
- Irrefutable patterns in abstractions, by Daniel de Rauglaudre.
- The ssreflect subterm selection algorithm by Georges Gonthier and
  Enrico Tassi, now accessible to tactic writers through the
  ssrmatching plugin.
- LtacProf, a profiler for Ltac by Jason Gross, Paul Steckler, Enrico
  Tassi and Tobias Tebbi.

A short demo of some of these new features can be run in your browser,
thanks to Emilio Gallego's JsCoq, at:

  https://x80.org/rhino-coq/examples/Coq86.html

See http://coq.inria.fr/ and the CHANGES file in the distribution for
for more details.

Coq 8.6 initiates a time-based release cycle, with a major version being
released every 10 months. The roadmap is also made public.

To date, Coq 8.6 contains more external contributions than any previous
Coq version. Code reviews were systematically done before integrating
new features, with an important focus given to compatibility and
performance issues.

The Coq Development Team