The Coq mailing list

[Benoît Viguier <beviguier AT gmail.com>]

Hi all,

It is, however it sadly lacks CoqIde and SSreflect:

The following actions will be performed:
  ⊘  remove  coqide                 8.5.3         [conflicts with coq]
  ⊘  remove  coq-mathcomp-ssreflect 1.6           [conflicts with coq]
  ↗  upgrade coq                    8.5.3 to 8.6
===== ↗  1   ⊘  2 =====
Do you want to continue ? [Y/n] n

On 12/20/2016 04:08 AM, Jeehoon Kang wrote:

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

-- 
Kind regards,

Benoît Viguier
Software Engineer - PhD Student | Cryptography & Formal Methods
Radboud University | Mercator 1, room 03.17, Toernooiveld 212
6525 EC Nijmegen, the Netherlands | www.viguier.nl

--------------------------------------------------------------------------
This message (and any attachments) is intended solely for the addressee(s)
and may contain confidential information. If you are not the addressee, do
not copy this message (and any attachments), forward or share this message
with third parties. You are requested to notify the sender immediately and
delete this message.

Attachment: signature.asc
Description: OpenPGP digital signature