WIP release summary for 8.19

doc/sphinx/changes.rst

@@ -14,7 +14,91 @@ Version 8.19
 Summary of changes
 ~~~~~~~~~~~~~~~~~~
 
-TODO
+Coq version 8.19 extends the kernel universe polymorphism to
+polymorphism over sorts (e.g. `Prop`, `SProp`) along with a few new
+features, a host of improvements to the notation system, the Ltac2
+standard library, and the removal of some standard library files after
+a long deprecation period.
+
+We highlight some of the most impactful changes here:
+
+  - :ref:`sort-polymorphism` makes it possible to share common constructs
+    over `Type` `Prop` and `SProp`.
+
+  - The notation :g:`term%_scope` to set a scope only temporarily
+    (in addition to :g:`term%scope` for opening a
+    scope applying to all subterms).
+
+  - :tacn:`lazy`, :tacn:`simpl`, :tacn:`cbn` and :tacn:`cbv` and the associated :cmd:`Eval`
+    and :tacn:`eval` reductions learned to do head reduction when given flag `head`.
+
+  - New Ltac2 APIs
+
+  - New performance evaluation facilities: :cmd:`Instructions` to
+    count CPU instructions used by a command (Linux only) and
+    :ref:`profiling` system to produce trace files.
+
+  - New command :cmd:`Attributes` to assign attributes such as
+    :attr:`deprecated` to a library file.
+
+Notable breaking changes:
+
+  - :tacn:`replace` with `by tac` does not automatically attempt to solve
+    the generated equality subgoal using the hypotheses.
+    Use `by first [assumption | symmetry;assumption | tac]`
+    if you need the previous behaviour.
+
+  - Removed old deprecated files from the standard library.
+
+TODO ^ add links to changelog sections
+
+
+See the `Changes in 8.19.0`_ section below for the detailed list of changes,
+including potentially breaking changes marked with **Changed**.
+Coq's `reference manual for 8.19 <https://coq.github.io/doc/v8.19/refman>`_,
+`documentation of the 8.19 standard library <https://coq.github.io/doc/v8.19/stdlib>`_
+and `developer documentation of the 8.19 ML API <https://coq.github.io/doc/v8.19/api>`_
+are also available.
+
+CREDITS TODO
+
+(TODO update, this is copied from 8.17)
+Our current maintainers are Yves Bertot, Frédéric Besson, Ana Borges,
+Ali Caglayan, Tej Chajed, Cyril Cohen, Pierre Corbineau, Pierre Courtieu, Maxime Dénès,
+Andres Erbsen, Jim Fehrle, Julien Forest, Emilio Jesús Gallego Arias, Gaëtan Gilbert,
+Georges Gonthier, Benjamin Grégoire, Jason Gross, Hugo Herbelin,
+Vincent Laporte, Olivier Laurent, Assia Mahboubi, Kenji Maillard,
+Guillaume Melquiond, Pierre-Marie Pédrot, Clément Pit-Claudel, Pierre Roux,
+Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Arnaud Spiwack,
+Matthieu Sozeau, Enrico Tassi, Laurent Théry, Anton Trunov, Li-yao Xia
+and Théo Zimmermann. See the `Coq Team face book <https://coq.inria.fr/coq-team.html>`_
+page for more details.
+
+(TODO resolve usernames)
+The 40 contributors to the 8.19 version are:
+quarkcool, soukouki, yannl35133, Khalid Abdullah, Tanaka Akira,
+Frédéric Besson, Lasse Blaauwbroek, Ana Borges, Ali Caglayan, Nikolaos
+Chatzikonstantinou, Maxime Dénès, Andrej Dudenhefner, Andres Erbsen,
+Jim Fehrle, Gaëtan Gilbert, Jason Gross, Stefan Haan, Hugo Herbelin,
+Emilio Jesús Gallego Arias, Pierre Jouvelot, Ralf Jung, Jan-Oliver
+Kaiser, Robbert Krebbers, Jean-Christophe Léchenet, Rodolphe Lepigre,
+Yann Leray, Yishuai Li, Guillaume Melquiond, Guillaume
+Munch-Maccagnoni, Karl Palmskog, Pierre-Marie Pédrot, Jim Portegies,
+Pierre Rousselin, Pierre Roux, Michael Soegtrop, David Swasey, Enrico
+Tassi, Isaac van Bakel, Shengyi Wang and Théo Zimmermann.
+
+The Coq community at large helped improve this new version via
+the GitHub issue and pull request system, the [email protected] mailing list,
+the `Discourse forum <https://coq.discourse.group/>`_ and the
+`Coq Zulip chat <https://coq.zulipchat.com>`_.
+
+Version 8.19's development spanned 4 months from the release of Coq 8.18.0
+(6 months since the branch for 8.18.0).
+Gaëtan Gilbert and Matthieu Sozeau are the release managers of Coq 8.19.
+This release is the result of 285 merged PRs, closing 70 issues.
+
+| Nantes, January 2024
+| Gaëtan Gilbert for the Coq development team
 
 Changes in 8.19.0
 ~~~~~~~~~~~~~~~~~
@@ -210,6 +294,12 @@ Tactics
   form `0 <= _ < _` for better cleanup in ``zify``
   (`#17984 <https://github.com/coq/coq/pull/17984>`_,
   by Jason Gross).
+- **Changed:**
+  :tacn:`simpl` now refolds applied constants unfolding to reducible
+  fixpoints into the original constant even when this constant
+  would become partially applied
+  (`#17991 <https://github.com/coq/coq/pull/17991>`_,
+  by Hugo Herbelin).
 - **Added:**
   Ltac2 tactic `Std.resolve_tc` to resolve typeclass evars appearing in a given term
   (`#13071 <https://github.com/coq/coq/pull/13071>`_,
@@ -282,12 +372,6 @@ Tactics
 
 Ltac language
 ^^^^^^^^^^^^^
-- **Changed:**
-  :tacn:`simpl` now refolds applied constants unfolding to reducible
-  fixpoints into the original constant even when this constant
-  would become partially applied
-  (`#17991 <https://github.com/coq/coq/pull/17991>`_,
-  by Hugo Herbelin).
 - **Fixed:**
   Fix broken "r <num>" and "r <string>" commands in the coqtop
   Ltac debugger, which also affected the Proof General Ltac debugger