From d20e4edab5912eb41b8408c3c8ab7541f4fc7834 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 3 Dec 2020 12:30:27 +0100 Subject: Implement review corrections by Théo Zimmermann --- doc/sphinx/changes.rst | 114 +++++++++++++++++++++++-------------------------- 1 file changed, 53 insertions(+), 61 deletions(-) diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index b5fb2cbcec..c2b32afea2 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -21,11 +21,7 @@ The main changes include: - :ref:`Introduction <813PrimArrays>` of :ref:`primitive persistent arrays` in the core language, implemented using imperative persistent arrays. - Introduction of :ref:`definitional proof irrelevance <813UIP>` for the equality type - defined in the SProp sort, using the :flag:`Definitional UIP` flag, - (deactivated by default). This models definitional uniqueness of - identity proofs for this type. It is deactivated by default as - it can lead to non-termination in combination with impredicativity. - Use of this flag is also printed by :cmd:`Print Assumptions`. + defined in the SProp sort. - Cumulative record and inductive type declarations can now :ref:`specify <813VarianceDecl>` the variance of their universes. - Various bugfixes and uniformization of behavior with respect to the use of @@ -124,7 +120,11 @@ Kernel .. _813UIP: - **Added:** - Definitional UIP, only when :flag:`Definitional UIP` is enabled. See + Definitional UIP, only when :flag:`Definitional UIP` is enabled. + This models definitional uniqueness of identity proofs for the equality + type in SProp. It is deactivated by default as it can lead to + non-termination in combination with impredicativity. + Use of this flag is also printed by :cmd:`Print Assumptions`. See documentation of the flag for details. (`#10390 `_, by Gaëtan Gilbert). @@ -223,6 +223,16 @@ Specification language, type inference interactive mode. (`#13183 `_, by Enrico Tassi). + + .. _813TypingFlags: + +- **Added:** + Typing flags can now be specified per-constant / inductive, this + allows to fine-grain specify them from plugins or attributes. See + :ref:`controlling-typing-flags` for details on attribute syntax. + (`#12586 `_, + by Emilio Jesus Gallego Arias). + - **Added:** Inference of return predicate of a :g:`match` by inversion takes sort elimination constraints into account @@ -492,15 +502,6 @@ SSReflect Commands and options ^^^^^^^^^^^^^^^^^^^^ -- **Changed:** - When compiled with OCaml >= 4.10.0, Coq will use the new best-fit GC - policy, which should provide some performance benefits. Coq's policy - is optimized for speed, but could increase memory consumption in - some cases. You are welcome to tune it using the ``OCAMLRUNPARAM`` - variable and report back on good settings so we can improve the defaults. - (`#13040 `_, - fixes `#11277 `_, - by Emilio Jesus Gallego Arias). - **Changed:** Drop prefixes from grammar non-terminal names, e.g. "constr:global" -> "global", "Prim.name" -> "name". @@ -513,24 +514,6 @@ Commands and options raise an error (`#13139 `_, by Pierre-Marie Pédrot). -- **Changed:** - Option `-native-compiler` of the configure script now impacts the - default value of the `-native-compiler` option of coqc. The - `-native-compiler` option of the configure script is added as an on demand - value, which becomes the default, thus preserving the previous default - behavior. - The stdlib is still precompiled when configuring with `-native-compiler - yes`. It is not precompiled otherwise. - This an implementation of point 2 of - `CEP #48 `_ - (`#13352 `_, - by Pierre Roux). -- **Changed:** - The :attr:`export` locality can now be used for all Hint commands, - including :cmd:`Hint Cut`, :cmd:`Hint Mode`, :cmd:`Hint Transparent` / `Opaque` and - :cmd:`Remove Hints` - (`#13388 `_, - by Pierre-Marie Pédrot). - **Removed:** In the :cmd:`Extraction Language` command, remove `Ocaml` as a valid value. Use `OCaml` instead. This was deprecated in Coq 8.8, `#6261 `_ @@ -551,7 +534,14 @@ Commands and options (`#12516 `_, by Maxime Dénès). - **Added:** - Added support for automatic insertion of coercions in :cmd:`Search` + The :attr:`export` locality can now be used for all Hint commands, + including :cmd:`Hint Cut`, :cmd:`Hint Mode`, :cmd:`Hint Transparent` / + :cmd:`Opaque ` and + :cmd:`Remove Hints` + (`#13388 `_, + by Pierre-Marie Pédrot). +- **Added:** + Support for automatic insertion of coercions in :cmd:`Search` patterns. Additionally, head patterns are now automatically interpreted as types (`#13255 `_, @@ -571,15 +561,23 @@ Commands and options Tools ^^^^^ +- **Changed:** + Option `-native-compiler` of the configure script now impacts the + default value of the `-native-compiler` option of coqc. The + `-native-compiler` option of the configure script supports a new `ondemand` + value, which becomes the default, thus preserving the previous default + behavior. + The stdlib is still precompiled when configuring with `-native-compiler + yes`. It is not precompiled otherwise. + This an implementation of point 2 of + `CEP #48 `_ + (`#13352 `_, + by Pierre Roux). - **Changed:** Added the ability for coq_makefile to directly set the installation folders, - through the :n:`COQLIBINSTALL` and :n:`COQDOCINSTALL` variables. + through the `COQLIBINSTALL` and `COQDOCINSTALL` variables. See :ref:`coqmakefilelocal`. (`#12389 `_, by Martin Bodin, review of Enrico Tassi). -- **Changed:** - ``dev/tools/make-changelog.sh`` now asks for a list of bugs fixed by the PR - (`#12410 `_, fixes `#12386 - `_, by Jason Gross). - **Removed:** The option ``-I`` of coqchk was removed (it was deprecated in Coq 8.8) (`#12613 `_, by Gaëtan Gilbert). @@ -627,8 +625,8 @@ Standard library get the ``PrimFloat`` notations without unqualifying the various primitives (`#12556 `_, fixes `#12454 `_, by Jason Gross). -- **Changed:** - Change the sort of cyclic numbers from Type to Set. For backward compatibility, a dynamic sort was defined in the 3 packages bignums, coqprime and color. +- **Changed:** the sort of cyclic numbers from Type to Set. + For backward compatibility, a dynamic sort was defined in the 3 packages bignums, coqprime and color. See for example commit 6f62bda in bignums. (`#12801 `_, by Vincent Semeria). @@ -665,29 +663,23 @@ Infrastructure and dependencies ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - **Changed:** - Coq's core system now uses the `zarith `_ + When compiled with OCaml >= 4.10.0, Coq will use the new best-fit GC + policy, which should provide some performance benefits. Coq's policy + is optimized for speed, but could increase memory consumption in + some cases. You are welcome to tune it using the ``OCAMLRUNPARAM`` + variable and report back on good settings so we can improve the defaults. + (`#13040 `_, + fixes `#11277 `_, + by Emilio Jesus Gallego Arias). +- **Changed:** + Coq now uses the `zarith `_ library, based on GNU's gmp instead of ``num`` which is deprecated upstream. The custom ``bigint`` module is - not longer provided; note that ``micromega`` still uses - ``num`` + no longer provided. (`#11742 `_, - by Emilio Jesus Gallego Arias and Vicent Laporte). -- **Removed:** - The `num` library is not linked to Coq anymore - (`#13007 `_, - by Emilio Jesus Gallego Arias). - -Miscellaneous -^^^^^^^^^^^^^ - - .. _813TypingFlags: - -- **Added:** - Typing flags can now be specified per-constant / inductive, this - allows to fine-grain specify them from plugins or attributes. See - :ref:`controlling-typing-flags` for details on attribute syntax. - (`#12586 `_, - by Emilio Jesus Gallego Arias). + `#13007 `_, + by Emilio Jesus Gallego Arias and Vicent Laporte, with help from + Frédéric Besson). Version 8.12 ------------ -- cgit v1.2.3