The Coq mailing list

[Jeehoon Kang <jeehoon.kang AT sf.snu.ac.kr>]

It seems Coq 8.6 is in the official opam repository: https://github.com/ocaml/opam-repository/pull/8117

2016-12-17 5:19 GMT+09:00 Ralf Jung <jung AT mpi-sws.org>:

Hi all,

thanks a lot to everyone involved in this release :)
I've already been using the 8.6 branch for some weeks now because it's
so much faster than 8.5 (~30% speedup for us) -- this is a solid release
indeed.

Now I'm waiting for the new version to appear in opam so that I can
switch away from the 8.6.dev branch... ;)

Kind regards,
Ralf

On 16.12.2016 17:29, Maxime Dénès wrote:
> 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
>

--

Jeehoon Kang (Ph.D. student)

Software Foundations Laboratory

Seoul National University