diff options
| author | Matthieu Sozeau | 2016-11-06 11:22:31 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-11-06 11:43:50 +0100 |
| commit | ceaafcde70e0ba536cae03baa740563aff47f6e8 (patch) | |
| tree | dc3bbb34b1bc45eeec40693994c2c7aa7bc25bf1 | |
| parent | 25fc9919c6d86fa8119b1f0c8e5ddba156055c9d (diff) | |
Maxime's comments
| -rw-r--r-- | doc/refman/RefMan-pre.tex | 36 |
1 files changed, 20 insertions, 16 deletions
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 669ba11e81..944cd48481 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -1087,7 +1087,7 @@ Paris, January 2015, revised December 2015,\\ Hugo Herbelin, Matthieu Sozeau and the {\Coq} development team\\ \end{flushright} -\section*{Credits: version 8.6 (Stronger, Better, Faster Rooster)} +\section*{Credits: version 8.6} {\Coq} version 8.6 contains the result of refinements, stabilization of 8.5's features and cleanups of the internals of the system. Over the @@ -1098,7 +1098,8 @@ over 100 contributions integrated. The main user visible changes are: can outperform the previous version by an order of magnitude, by Jacques-Henri Jourdan. \item In CoqIDE and other asynchronous interfaces, more fine-grained - asynchronous processing and error reporting by Enrico Tassi. + asynchronous processing and error reporting by Enrico Tassi (ability + to jump to any error in the document). \item More access to the proof engine features from Ltac: goal management primitives, range selectors and a {\tt typeclasses eauto} engine handling multiple goals and multiple successes, by @@ -1170,22 +1171,25 @@ The OPAM repository for {\Coq} packages has been maintained by Guillaume Claret, Guillaume Melquiond, Matthieu Sozeau, Enrico Tassi and others. A list of packages is now available at \url{https://coq.inria.fr/opam/www/}. -Packaging tools and software development kits were prepared by Maxime -Dénès, Michael Soegtrop and Enrico Tassi for Windows, and Maxime Dénès -and Matthieu Sozeau for MacOS X. Packages are now regularly built on the -continuous integration server. +Packaging tools and software development kits were prepared by Michael +Soegtrop with the help of Maxime Dénès and Enrico Tassi for Windows, and +Maxime Dénès and Matthieu Sozeau for MacOS X. Packages are now regularly +built on the continuous integration server. Matej Košík maintained and greatly improved the continuous integration setup and the testing of {\Coq} contributions. He also contributed many API improvement and code cleanups throughout the system. -General maintenance during part or whole of this period has been done by -Pierre Boutillier, Pierre Courtieu, Maxime Dénès, Hugo Herbelin, Pierre -Letouzey, Guillaume Melquiond, Pierre-Marie Pédrot, Matthieu Sozeau, -Arnaud Spiwack, Enrico Tassi, Bruno Barras, Yves Bertot, -Frédéric Besson, Assia Mahboubi and Yann Régis-Gianas. The development -process was coordinated by Matthieu Sozeau with the help of Maxime -Dénès, who was also in charge of the release process. +The contributors for this version are C.J. Bell, Yves Bertot, Frédéric +Besson, Tej Chajed, Pierre Courtieu, Maxime Dénès, Ricky Elrod, Jason +Gross, Hugo Herbelin, Emilio Jesus Gallego Arias, Jacques-Henri Jourdan, +Matej Košík, Xavier Leroy, Pierre Letouzey, Gregory Malecha, Cyprien +Mangin, Erik Martin-Dorel, Guillaume Melquiond, Pierre-Marie Pédrot, +Lionel Rieg, Gabriel Scherer, Matthieu Sozeau, Arnaud Spiwack, Paul +Steckler, Laurent Théry, Enrico Tassi, Nickolai Zeldovich, Théo +Zimmermann and Daniel de Rauglaudre. The development process was +coordinated by Hugo Herbelin and Matthieu Sozeau with the help of +Maxime Dénès, who was also in charge of the release process. Many power users helped to improve the design of the new features via the bug tracker, the pull request system, the {\Coq} development mailing @@ -1193,8 +1197,8 @@ list or the coq-club mailing list. Special thanks to the users who contributed patches and intensive brain-storming and code reviews, starting with Cyril Cohen, Jason Gross, Robbert Krebbers, Jonathan Leivent, Xavier Leroy, Gregory Malecha, Clément Pit-Claudel, Gabriel -Sherer and Beta Ziliani. It would however be impossible to mention with -precision all the names of people who to some extent influenced the +Sherer and Beta Ziliani. It would however be impossible to mention +exhaustively the names of everybody who to some extent influenced the development. Version 8.6 is the first release of {\Coq} developed on a time-based @@ -1203,7 +1207,7 @@ development cycle. Its development spanned 10 months from the release of external contributions than any previous {\Coq} system. Code reviews were systematically done before integration of new features, with an important focus given to compatibility and performance issues, resulting -in a hopefully much more robust release than previous ones. +in a hopefully more robust release than {\Coq} 8.5. Coq Enhancement Proposals (CEPs for short) were introduced by Enrico Tassi to provide more visibility and a discussion period on new |
