Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Coq 8.7.0 is out!

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq 8.7.0 is out!


Chronological Thread 
  • From: Ralf Jung <jung AT mpi-sws.org>
  • To: coq-club AT inria.fr, Maxime Dénès <mail AT maximedenes.fr>
  • Subject: Re: [Coq-Club] Coq 8.7.0 is out!
  • Date: Wed, 18 Oct 2017 11:26:49 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT jupiter.mpi-klsb.mpg.de
  • Ironport-phdr: 9a23:pf68jBPiVUBsCDBsVWkl6mtUPXoX/o7sNwtQ0KIMzox0K/T+rarrMEGX3/hxlliBBdydsK0UzbeO+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6a8TWO6msZHQy6Pg5oLMz0HJTThoK5zaT63pTDYgBFzBY8ZzNpZEGzpATVnswfkYpnJ6o8zBbS5HVSLbd432RtcGiamxi0xNq289Y38TlWtNok788FSrrhOaMiQuoLX3wdL2kp6Ziz5lH4RgyV6y5EXw==

Hi all,

> The Coq development team is pleased to announce the release of Coq
> 8.7.0, available at:
>
> https://coq.inria.fr/coq-87

We have been testing our developments (Iris and some of its reverse
dependencies) on the 8.7 branch for some weeks already, and this is
clearly the most compatible release I have been migrating things to.
The only change we had to make turned out to be a bug that is fixed by
now. We even got 10-12% speed improvement as a bonus :-)

Great work!

Kind regards,
Ralf

> Source, Windows and OS X packages are available at:
>
> https://github.com/coq/coq/releases/tag/V8.7.0
>
> This release includes:
>
> - A large amount of work on cleaning and speeding up the code base,
> notably the work of Pierre-Marie Pédrot on making the tactic-level
> system insensitive to existential variable expansion, providing a safer
> API to plugin writers and making the code more robust.
>
> - New tactics:
> Variants of tactics supporting existential variables eassert, eenough,
> etc. by Hugo Herbelin;
> Tactics extensionality in H and inversion_sigma by Jason Gross;
> specialize with accepting partial bindings by Pierre Courtieu.
>
> - Cumulative Polymorphic Inductive Types, allowing cumulativity of
> universes to go through applied inductive types, by Amin Timany and
> Matthieu Sozeau.
>
> - The SSReflect plugin by Georges Gonthier, Assia Mahboubi and Enrico
> Tassi was integrated (with its documentation in the reference manual) by
> Maxime Dénès, Assia Mahboubi and Enrico Tassi.
>
> - The coq_makefile tool was completely redesigned by Enrico Tassi to
> improve its maintainability and the extensibility of generated
> Makefiles, and to make _CoqProject files more palatable to IDEs.
>
> A lot of other changes are described in the CHANGES file.
>
> This is the second release of Coq developed on a time-based development
> cycle. Its development spanned 9 months from the release of Coq 8.6 and
> was based on a public road-map. It attracted many external
> contributions. Code reviews and continuous integration testing were
> systematically used before integration of new features, with an
> important focus given to compatibility and performance issues.
>
> The Coq Development Team
>
>
>
>
>



Archive powered by MHonArc 2.6.18.

Top of Page