diff options
Diffstat (limited to 'doc/sphinx/changes.rst')
| -rw-r--r-- | doc/sphinx/changes.rst | 115 |
1 files changed, 111 insertions, 4 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index e5c2056c40..0f501382e7 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -14,9 +14,9 @@ Version 8.12 Summary of changes ~~~~~~~~~~~~~~~~~~ -|Coq| version 8.12 integrates many quality-of-life improvements, +|Coq| version 8.12 integrates many usability improvements, in particular with respect to notations, scopes and implicit arguments, -along with many bug-fixes and major improvements to the reference manual. +along with many bug fixes and major improvements to the reference manual. The main changes include: - New :ref:`binder notation<812Implicit>` for non-maximal implicit arguments using :g:`[ ]` @@ -64,6 +64,23 @@ Guillaume Claret, Karl Palmskog, Matthieu Sozeau and Enrico Tassi with contributions from many users. A list of packages is available at https://coq.inria.fr/opam/www/. +Previously, most components of Coq had a single principal maintainer. +This was changed in 8.12 (`#11295 +<https://github.com/coq/coq/pull/11295>`_) so that every component now has +a team of maintainers, who are in charge of reviewing and +merging incoming pull requests. This gave us a chance to +significantly expand the pool of maintainters and provide faster +feedback to contributors. Special thanks to all our maintainers! + +Our current 31 maintainers are Yves Bertot, Frédéric Besson, Tej +Chajed, Cyril Cohen, Pierre Corbineau, Pierre Courtieu, Maxime Dénès, +Jim Fehrle, Julien Forest, Emilio Jesús Gallego Arias, Gaëtan Gilbert, +Georges Gonthier, Benjamin Grégoire, Jason Gross, Hugo Herbelin, +Vincent Laporte, Assia Mahboubi, Kenji Maillard, Guillaume Melquiond, +Pierre-Marie Pédrot, Clément Pit-Claudel, Kazuhiko Sakaguchi, Vincent +Semeria, Michael Soegtrop, Arnaud Spiwack, Matthieu Sozeau, Enrico +Tassi, Laurent Théry, Anton Trunov, Li-yao Xia, Théo Zimmermann + The 59 contributors to this version are Abhishek Anand, Yves Bertot, Frédéric Besson, Lasse Blaauwbroek, Simon Boulier, Quentin Carbonneaux, Tej Chajed, Arthur Charguéraud, Cyril Cohen, Pierre Courtieu, Matthew Dempsky, Maxime Dénès, @@ -72,8 +89,8 @@ Jesús Gallego Arias, Paolo G. Giarrusso, Gaëtan Gilbert, Jason Gross, Samuel Gruetter, Attila Gáspár, Hugo Herbelin, Jan-Oliver Kaiser, Robbert Krebbers, Vincent Laporte, Olivier Laurent, Xavier Leroy, Thomas Letan, Yishuai Li, Kenji Maillard, Erik Martin-Dorel, Guillaume Melquiond, Ike Mulder, -Guillaume Munch-Maccagnoni, Antonio Nikishaev, Karl Palmskog, Clément -Pit-Claudel, Pierre-Marie Pédrot, Ramkumar Ramachandra, Lars Rasmusson, Daniel +Guillaume Munch-Maccagnoni, Antonio Nikishaev, Karl Palmskog, Pierre-Marie +Pédrot, Clément Pit-Claudel, Ramkumar Ramachandra, Lars Rasmusson, Daniel de Rauglaudre, Talia Ringer, Pierre Roux, Kazuhiko Sakaguchi, Vincent Semeria, @scinart, Kartik Singhal, Michael Soegtrop, Matthieu Sozeau, Enrico Tassi, Laurent Théry, Ralf Treinen, Anton Trunov, Bernhard M. Wiedemann, Li-yao Xia, @@ -119,6 +136,18 @@ Specification language, type inference :cmd:`Arguments`) has been turned into an error (`#11368 <https://github.com/coq/coq/pull/11368>`_, by SimonBoulier). +- **Changed:** + Typeclass resolution, accessible through :tacn:`typeclasses eauto`, + now suspends constraints according to their modes + instead of failing. If a typeclass constraint does not match + any of the declared modes for its class, the constraint is postponed, and + the proof search continues on other goals. Proof search does a fixed point + computation to try to solve them at a later stage of resolution. It does + not fail if there remain only stuck constraints at the end of resolution. + This makes typeclasses with declared modes more robust with respect to the + order of resolution. + (`#10858 <https://github.com/coq/coq/pull/10858>`_, + fixes `#9058 <https://github.com/coq/coq/issues/9058>_`, by Matthieu Sozeau). - **Added:** Warn when manual implicit arguments are used in unexpected positions of a term (e.g. in `Check id (forall {x}, x)`) or when an implicit @@ -1109,6 +1138,84 @@ Infrastructure and dependencies (`#11245 <https://github.com/coq/coq/pull/11245>`_, by Emilio Jesus Gallego Arias). +Changes in 8.12.0 +~~~~~~~~~~~~~~~~~~~~~ + +.. contents:: + :local: + +**Notations** + +- **Added:** + Simultaneous definition of terms and notations now support custom entries. + Fixes `#11121 <https://github.com/coq/coq/pull/11121>`_. + (`#12523 <https://github.com/coq/coq/pull/11523>`_, by Maxime Dénès). +- **Fixed:** + Printing bug with notations for n-ary applications used with applied references. + (`#12683 <https://github.com/coq/coq/pull/12683>`_, + fixes `#12682 <https://github.com/coq/coq/pull/12682>`_, + by Hugo Herbelin). + +**Tactics** + +- **Fixed:** + :tacn:`typeclasses eauto` (and discriminated hint bases) now correctly + classify local variables as being unfoldable + (`#12572 <https://github.com/coq/coq/pull/12572>`_, + fixes `#12571 <https://github.com/coq/coq/issues/12571>`_, + by Pierre-Marie Pédrot). + +**Tactic language** + +- **Fixed:** + Excluding occurrences was causing an anomaly in tactics + (e.g., :g:`pattern _ at L` where :g:`L` is :g:`-2`). + (`#12541 <https://github.com/coq/coq/pull/12541>`_, + fixes `#12228 <https://github.com/coq/coq/issues/12228>`_, + by Pierre Roux). +- **Fixed:** + Parsing of multi-parameters Ltac2 types + (`#12594 <https://github.com/coq/coq/pull/12594>`_, + fixes `#12595 <https://github.com/coq/coq/issues/12595>`_, + by Pierre-Marie Pédrot). + +**SSReflect** + +- **Fixed:** + Do not store the full environment inside ssr ast_closure_term + (`#12708 <https://github.com/coq/coq/pull/12708>`_, + fixes `#12707 <https://github.com/coq/coq/issues/12707>`_, + by Pierre-Marie Pédrot). + +**Commands and options** + +- **Fixed:** + Properly report the mismatched magic number of vo files + (`#12677 <https://github.com/coq/coq/pull/12677>`_, + fixes `#12513 <https://github.com/coq/coq/issues/12513>`_, + by Pierre-Marie Pédrot). +- **Changed:** + Arbitrary hints have been undeprecated, and their definition + now triggers a standard warning instead + (`#12678 <https://github.com/coq/coq/pull/12678>`_, + fixes `#11970 <https://github.com/coq/coq/issues/11970>`_, + by Pierre-Marie Pédrot). + +**CoqIDE** + +- **Fixed:** CoqIDE no longer exits when trying to open a file whose name is not a valid identifier + (`#12562 <https://github.com/coq/coq/pull/12562>`_, + fixes `#10988 <https://github.com/coq/coq/issues/10988>`_, + by Vincent Laporte). + +**Infrastructure and dependencies** + +- **Fixed:** + Running ``make`` in ``test-suite/`` twice (or more) in a row will no longer + rebuild the ``modules/`` tests on subsequent runs, if they have not been + modified in the meantime (`#12583 <https://github.com/coq/coq/pull/12583>`_, + fixes `#12582 <https://github.com/coq/coq/issues/12582>`_, by Jason Gross). + Version 8.11 ------------ |