Release summary for 8.19

.mailmap

@@ -154,6 +154,7 @@ Jean-Marc Notin <notin@gforge>                     notin,no-port-forwarding,no-a
 Jean-Marc Notin <notin@gforge>                     notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Russell O'Connor <roconnor@blockstream.io>         roconnor <roconnor@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Russell O'Connor <roconnor@blockstream.io>         roconnor-blockstream <roconnor@blockstream.com>
+Sotaro Okada <soukouki0@yahoo.co.jp>               soukouki <soukouki0@yahoo.co.jp>
 Carl Patenaude-Poulin <carlpaten@protonmail.com>   Carl Patenaude Poulin <carl.patenaudepoulin@mail.mcgill.ca>
 Christine Paulin <cpaulin@gforge>                  cpaulin <cpaulin@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Christine Paulin <cpaulin@gforge>                  mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7>

doc/sphinx/changes.rst

@@ -14,7 +14,113 @@ 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`.
+
+  - :ref:`New Ltac2 APIs <819Ltac2>`, improved Ltac2 `exact` and
+    dynamic building of Ltac2 term patterns.
+
+  - 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.
+
+  - :ref:`Removed old deprecated files <819Stdlib>` from the standard library.
+
+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.
+
+Maxime Dénès and Thierry Martinez with support from Erik Martin-Dorel
+and Théo Zimmermann moved the CI away from `gitlab.com <http://gitlab.com>`_
+to use Inria supported runner machines through
+`gitlab.inria.fr <https://gitlab.inria.fr>`_.
+
+Théo Zimmermann with help from Ali Caglayan and Jason Gross maintained
+`coqbot <https://github.com/coq/bot>`_ used to run Coq's CI and other
+pull request management tasks.
+
+Jason Gross maintained the `bug minimizer <https://github.com/JasonGross/coq-tools>`_
+and its `automatic use through coqbot <https://github.com/coq/coq/wiki/Coqbot-minimize-feature>`_.
+
+Jaime Arias and Erik Martin-Dorel maintained the
+`Coq Docker images <https://hub.docker.com/r/coqorg/coq>`_
+and Cyril Cohen, Vincent Laporte, Pierre Roux and Théo Zimmermann
+maintained the `Nix toolbox <https://github.com/coq-community/coq-nix-toolbox>`_
+used by many Coq projects for continuous integration.
+
+Ali Caglayan, Emilio Jesús Gallego Arias, Rudi Grinberg and
+Rodolphe Lepigre maintained the
+`Dune build system for OCaml and Coq <https://github.com/ocaml/dune/>`_
+used to build Coq itself and many Coq projects.
+
+The opam repository for Coq packages has been maintained by
+Guillaume Claret, Guillaume Melquiond, Karl Palmskog and Enrico Tassi with
+contributions from many users. A list of packages is `available on the Coq website <https://coq.inria.fr/coq-package-index>`_.
+
+Our current maintainers are Yves Bertot, Frédéric Besson, Ana Borges,
+Ali Caglayan, Tej Chajed, Cyril Cohen, Pierre Corbineau, Pierre
+Courtieu, 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.
+
+The 40 contributors to the 8.19 version are:
+quarkcool, Khalid Abdullah, Tanaka Akira, Isaac van Bakel,
+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, Sotaro Okada, Karl Palmskog, Pierre-Marie Pédrot, Jim Portegies,
+Pierre Rousselin, Pierre Roux, Michael Soegtrop, David Swasey, Enrico
+Tassi, 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 coq-club@inria.fr 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 +316,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,19 +394,15 @@ 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
   (`#18068 <https://github.com/coq/coq/pull/18068>`_,
   fixes `#18067 <https://github.com/coq/coq/issues/18067>`_,
   by Jim Fehrle).
 
+.. _819Ltac2:
+
 Ltac2 language
 ^^^^^^^^^^^^^^
 - **Changed:**
@@ -443,6 +551,8 @@ Command-line tools
   (`#18165 <https://github.com/coq/coq/pull/18165>`_,
   by Rodolphe Lepigre).
 
+.. _819Stdlib:
+
 Standard library
 ^^^^^^^^^^^^^^^^