coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
>
>
>
>
>
- [Coq-Club] Coq 8.7.0 is out!, Maxime Dénès, 10/18/2017
- Re: [Coq-Club] Coq 8.7.0 is out!, Laurent Thery, 10/18/2017
- Re: [Coq-Club] Coq 8.7.0 is out!, Maxime Dénès, 10/18/2017
- Re: [Coq-Club] Coq 8.7.0 is out!, Ralf Jung, 10/18/2017
- Re: [Coq-Club] Coq 8.7.0 is out!, Laurent Thery, 10/18/2017
Archive powered by MHonArc 2.6.18.