From 3c4d2c9e3b7100a0012ad06b33b46fe7dca6cd29 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 30 Nov 2020 17:12:37 +0100 Subject: Changes for Coq 8.13 --- doc/sphinx/changes.rst | 661 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 661 insertions(+) (limited to 'doc/sphinx/changes.rst') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 249c7794be..e97fba3546 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -8,6 +8,667 @@ Recent changes .. include:: ../unreleased.rst +Version 8.13 +------------ + +Summary of changes +~~~~~~~~~~~~~~~~~~ + +Coq version 8.13 integrates many usability improvements, as well +as extensions of the core language. +The main changes include: + + - Introduction of :ref:`primitive persistent arrays` + in the core language, implemented using imperative persistent arrays. + - Introduction of definitional proof irrelevance 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 results in non-termination in combination with impredicativity. + Use of this flag is also shown by :cmd:`Print Assumptions`. + - Cumulative record and inductives type declarations can now + :ref:`specify<813VarianceDecl>` the variance of their universes. + - Various bugfixes and uniformization of behavior with respect to the use of + implicit arguments and the handling of existential variables in + declarations, unification and tactics. + - New warning for :ref:`unused variables <813UnusedVar>` in catch-all match branches that match + multiple distinct patterns. + - New warning for `Hint` commands outside sections without a locality + attribute, whose goal is to eventually remove the fragile default + behavior of having hints be imported when using `Require` only. + The recommended fix is to declare hints as `export`, instead of + the current default `global`, meaning that they are imported + through `Require Import` only, not `Require`. + See the following `rationale and guidelines `_ + for details. + - General support for :ref:`boolean attributes <813BooleanAttrs>`. + - Many improvements to the handling of :ref:`notations <813Notations>`, + including number notations, recursive notations and notations with bindings. + A new algorithm chooses the most precise notation available to print an expression, + which might introduce changes in printing behavior. + - Tactic improvements in :tacn:`lia` and its :tacn:`zify` preprocessing step, + now supporting reasoning on boolean operators such as `Z.leb` and supporting + primitive integers :g:`Int63`. + - Typing flags can now be specified :ref:`per-constant / inductive <813TypingFlags>`. + +See the `Changes in 8.13`_ section and following sections for the +detailed list of changes, including potentially breaking changes marked +with **Changed**. + +Coq's documentation is available at https://coq.github.io/doc/v8.13/refman (reference +manual), and https://coq.github.io/doc/v8.13/stdlib (documentation of +the standard library). Developer documentation of the ML API is available +at https://coq.github.io/doc/v8.13/api. + +Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael +Soegtrop and Théo Zimmermann worked on maintaining and improving the +continuous integration system and package building infrastructure. + +Erik Martin-Dorel has maintained the `Coq Docker images +`_ that are used in many Coq +projects for continuous integration. + +The OPAM repository for Coq packages has been maintained by +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/. + +TODO updated 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 52 contributors to this version are Reynald Affeldt, Tanaka Akira, Frédéric +Besson, Lasse Blaauwbroek, Clément Blaudeau, Martin Bodin, Ali Caglayan, Tej Chajed, +Cyril Cohen, Julien Coolen, Matthew Dempsky, Maxime Dénès, Andres Erbsen, +Jim Fehrle, Emilio Jesús Gallego Arias, Paolo G. Giarrusso, Attila Gáspár, Gaëtan Gilbert, +Jason Gross, Benjamin Grégoire, Hugo Herbelin, Wolf Honore, Jasper Hugunin, Ignat Insarov, +Ralf Jung, Fabian Kunze, Vincent Laporte, Olivier Laurent, Larry D. Lee Jr, +Thomas Letan, Yishuai Li, Xia Li-yao, James Lottes, Jean-Christophe Léchenet, +Kenji Maillard, Erik Martin-Dorel, Yusuke Matsushita, Guillaume Melquiond, +Carl Patenaude-Poulin, Clément Pit-Claudel, Pierre-Marie Pédrot, Pierre Roux, +Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Matthieu Sozeau, +Enrico Tassi, Anton Trunov, Edward Wang, Li-yao Xia, Beta Ziliani, Théo Zimmermann. + +The Coq community at large helped improve the design of this new version via +the GitHub issue and pull request system, the Coq development mailing list +coqdev@inria.fr, the coq-club@inria.fr mailing list, the `Discourse forum +`_ and the `Coq Zulip chat `_. + +Version 8.13's development spanned 5 months from the release of +Coq 8.12.0. Enrico Tassi and Maxime Dénès are the release managers of Coq 8.13. +This release is the result of 400 PRs merged, closing ~100 issues. + +| Nantes, November 2020, +| Matthieu Sozeau for the Coq development team +| + + +Changes in 8.13 +~~~~~~~~~~~~~~~ + +.. contents:: + :local: + +Kernel +^^^^^^ + +- **Added:** + Definitional UIP, only when :flag:`Definitional UIP` is enabled. See + documentation of the flag for details. + (`#10390 `_, + by Gaëtan Gilbert). +- **Added:** + Built-in support for persistent arrays, which expose a functional + interface but are implemented using an imperative data structure, for + better performance. + (`#11604 `_, + by Maxime Dénès and Benjamin Grégoire, with help from Gaëtan Gilbert). +- **Fixed:** + A loss of definitional equality for declarations obtained through + :cmd:`Include` when entering the scope of a :cmd:`Module` or + :cmd:`Module Type` was causing :cmd:`Search` not to see the included + declarations + (`#12537 `_, fixes `#12525 + `_ and `#12647 + `_, by Hugo Herbelin). +- **Changed:** Primitive arrays are now irrelevant in their single + polymorphic universe (same as a polymorphic cumulative list + inductive would be) (`#13356 + `_, fixes `#13354 + `_, by Gaëtan Gilbert). + +Specification language, type inference +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +- **Changed:** + In :tacn:`refine`, new existential variables unified with existing ones are no + longer considered as fresh. The behavior of :tacn:`simple refine` no longer depends on + the orientation of evar-evar unification problems, and new existential variables + are always turned into (unshelved) goals. This can break compatibility in + some cases (`#7825 `_, by Matthieu + Sozeau, with help from Maxime Dénès, review by Pierre-Marie Pédrot and + Enrico Tassi, fixes `#4095 `_ and + `#4413 `_). +- **Changed:** Heuristics for universe minimization to :g:`Set`: also + use constraints ``Prop <= i`` (`#10331 + `_, by Gaëtan Gilbert with + help from Maxime Dénès and Matthieu Sozeau, fixes `#12414 + `_). + + .. _813VarianceDecl: + +- **Added:** Commands :cmd:`Inductive`, :cmd:`Record` and synonyms now + support syntax `Inductive foo@{=i +j *k l}` to specify variance + information for their universes (in :ref:`Cumulative ` + mode) (`#12653 `_, by Gaëtan + Gilbert). +- **Changed:** + Tweaked the algorithm giving default names to arguments. + Should reduce the frequency that argument names get an + unexpected suffix. + Also makes :flag:`Mangle Names` not mess up argument names. + (`#12756 `_, + fixes `#12001 `_ + and `#6785 `_, + by Jasper Hugunin). + + .. _813UnusedVar: + +- **Added:** + Warning on unused variables in pattern-matching branches of + :n:`match` serving as catch-all branches for at least two distinct + patterns. + (`#12768 `_, + fixes `#12762 `_, + by Hugo Herbelin). +- **Removed:** + Undocumented and experimental forward class hint feature ``:>>``. + Use ``:>`` (see :n:`@of_type`) instead + (`#13106 `_, + by Pierre-Marie Pédrot). +- **Fixed:** + Implicit arguments taken into account in defined fields of a record type declaration + (`#13166 `_, + fixes `#13165 `_, + by Hugo Herbelin). +- **Added:** + Definition and (Co)Fixpoint now support the :attr:`using` attribute. + It has the same effect as :cmd:`Proof using`, which is only available in + interactive mode. + (`#13183 `_, + by Enrico Tassi). +- **Removed:** The type given to :cmd:`Instance` is no longer automatically + generalized over unbound and :ref:`generalizable ` variables. + Use :n:`Instance : \`{@type}` instead of :n:`Instance : @type` to get the old behaviour, or + enable the compatibility flag :flag:`Instance Generalized Output`. + (`#13188 `_, fixes `#6042 + `_, by Gaëtan Gilbert). +- **Fixed:** + Allow use of type classes inference for the return predicate of a :n:`match` + (was deactivated in versions 8.10 to 8.12, `#13217 `_, + fixes `#13216 `_, + by Hugo Herbelin). +- **Added:** + Inference of return predicate of a :g:`match` by inversion takes + sort elimination constraints into account + (`#13290 `_, + grants `#13278 `_, + by Hugo Herbelin). + + .. _813BooleanAttrs: + +- **Changed:** + :term:`Boolean attributes ` are now specified using + key/value pairs, that is to say :n:`@ident__attr{? = {| yes | no } }`. + If the value is missing, the default is :n:`yes`. The old syntax is still + supported, but produces the ``deprecated-attribute-syntax`` warning. + + Deprecated attributes are :attr:`universes(monomorphic)`, + :attr:`universes(notemplate)` and :attr:`universes(noncumulative)`, which are + respectively replaced by :attr:`universes(polymorphic=no) `, + :attr:`universes(template=no) ` + and :attr:`universes(cumulative=no) `. + Attributes :attr:`program` and :attr:`canonical` are also affected, + with the syntax :n:`@ident__attr(false)` being deprecated in favor of + :n:`@ident__attr=no`. + + (`#13312 `_, + by Emilio Jesus Gallego Arias). +- **Fixed:** + A case of unification raising an anomaly IllTypedInstance + (`#13376 `_, + fixes `#13266 `_, + by Hugo Herbelin). +- **Fixed:** + Using :n:`{wf ...}` in local fixpoints is an error, not an anomaly + (`#13383 `_, + fixes `#11816 `_, + by Hugo Herbelin). +- **Fixed:** + issue when two expressions involving different projections and one is + primitive need to be unified + (`#13386 `_, + fixes `#9971 `_, + by Hugo Herbelin). +- **Fixed:** + A bug producing ill-typed instances of existential variables when let-ins + interleaved with assumptions + (`#13387 `_, + fixes `#12348 `_, + by Hugo Herbelin). + + .. _813Notations: + +Notations +^^^^^^^^^ + +- **Changed:** + In notations (except in custom entries), the misleading :n:`@syntax_modifier` + :n:`@ident ident` (which accepted either an identifier or + a :g:`_`) is deprecated and should be replaced by :n:`@ident name`. If + the intent was really to only parse identifiers, this will + eventually become possible, but only as of Coq 8.15. + In custom entries, the meaning of :n:`@ident ident` is silently changed + from parsing identifiers or :g:`_` to parsing only identifiers + without warning, but this presumably affects only rare, recent and + relatively experimental code + (`#11841 `_, + fixes `#9514 `_, + by Hugo Herbelin). +- **Added:** + :flag:`Printing Float` flag to print primitive floats as hexadecimal + instead of decimal values. This is included in the :flag:`Printing All` flag + (`#11986 `_, + by Pierre Roux). +- **Changed:** + Improved support for notations/abbreviations with mixed terms and patterns (such as the forcing modality) + (`#12099 `_, + by Hugo Herbelin). +- **Deprecated** + ``Numeral.v`` is deprecated, please use ``Number.v`` instead. +- **Changed** + Rational and real constants are parsed differently. + The exponent is now encoded separately from the fractional part + using ``Z.pow_pos``. This way, parsing large exponents can no longer + blow up and constants are printed in a form closer to the one they + were parsed (i.e., ``102e-2`` is reprinted as such and not ``1.02``). +- **Removed** + OCaml parser and printer for real constants have been removed. + Real constants are now handled with proven Coq code. +- **Added:** + :ref:`Number Notation ` and :ref:`String Notation + ` commands now + support parameterized inductive and non inductive types + (`#12218 `_, + fixes `#12035 `_, + by Pierre Roux, review by Jason Gross and Jim Fehrle for the + reference manual). +- **Changed:** + Scope information is propagated in indirect applications to a + reference prefixed with :g:`@@`; this covers for instance the case + :g:`r.(@@p) t` where scope information from :g:`p` is now taken into + account for interpreting :g:`t` (`#12685 + `_, by Hugo Herbelin). +- **Added:** + Added support for encoding notations of the form :g:`x ⪯ y ⪯ .. ⪯ z ⪯ t` + (`#12765 `_, + by Hugo Herbelin). +- **Changed:** + New model for ``only parsing`` and ``only printing`` notations with + support for at most one parsing-and-printing or only-parsing + notation per notation and scope, but an arbitrary number of + only-printing notations + (`#12950 `_, + fixes `#4738 `_ + and `#9682 `_ + and part 2 of `#12908 `_, + by Hugo Herbelin). +- **Fixed:** + Issues in the presence of notations recursively referring to another + applicative notations, such as missing scope propagation, or failure + to use a notation for printing + (`#12960 `_, + fixes `#9403 `_ + and `#10803 `_, + by Hugo Herbelin). +- **Fixed:** + Capture of the name of global references by + binders in the presence of notations for binders + (`#12965 `_, + fixes `#9569 `_, + by Hugo Herbelin). +- **Deprecated:** + :n:`Numeral Notation`, please use :ref:`Number Notation ` instead. + (`#12979 `_, + by Pierre Roux). +- **Changed:** + Redeclaring a notation reactivates also its printing rule; in + particular a second :cmd:`Import` of the same module reactivates the + printing rules declared in this module. In theory, this leads to + changes of behavior for printing. However, this is mitigated in + general by the adoption in `#12986 + `_ of a priority given to + notations which match a larger part of the term to print + (`#12984 `_, + fixes `#7443 `_ + and `#10824 `_, + by Hugo Herbelin). +- **Changed:** + Use of notations for printing now gives preference + to notations which match a larger part of the term to abbreviate + (`#12986 `_, + by Hugo Herbelin). +- **Fixed:** + Preventing notations for constructors to involve binders + (`#13092 `_, + fixes `#13078 `_, + by Hugo Herbelin). +- **Added:** + The :n:`@binder` entry of :cmd:`Notation` can now be used in + notations expecting a single (non-recursive) binder + (`#13265 `_, + by Hugo Herbelin, see section :n:`notations-and-binders` of the + reference manual). +- **Fixed:** Notations understand universe names without getting + confused by different imported modules between declaration and use + locations (`#13415 `_, fixes + `#13303 `_, by Gaëtan + Gilbert). + +Tactics +^^^^^^^ + +- **Added:** + :tacn:`lia` is extended to deal with boolean operators e.g. `andb` or `Z.leb`. + (As `lia` gets more powerful, this may break proof scripts relying on `lia` failure.) + (`#11906 `_, by Frédéric Besson). +- **Added:** + `apply in` supports several hypotheses + (`#12246 `_, + by Hugo Herbelin; grants + `#9816 `_). +- **Removed:** + The deprecated and undocumented "prolog" tactic was removed + (`#12399 `_, + by Pierre-Marie Pédrot). +- **Removed:** Removed info tactic that was deprecated in 8.5. + (`#12423 `_, by Jim Fehrle). +- **Added:** + Thhe :tacn:`zify` tactic can now be extended by redefining the `zify_pre_hook` + tactic. (`#12552 `_, + by Kazuhiko Sakaguchi). +- **Added:** + The :tacn:`zify` tactic provides support for primitive integers (module :g:`ZifyInt63`). + (`#12648 `_, by Frédéric Besson). +- **Changed:** + Giving an empty list of occurrences after :n:`in` in tactics is no + longer permitted. Omitting the :n:`in` gives the same behavior + (`#13237 `_, + fixes `#13235 `_, + by Hugo Herbelin). +- **Fixed:** + Avoiding exposing an internal name of the form :n:`_tmp` when applying the + :n:`_` introduction pattern would break a dependency + (`#13337 `_, + fixes `#13336 `_, + by Hugo Herbelin). +- **Fixed:** + The case of tactics, such as :tacn:`eapply`, producing existential variables + under binders with an ill-formed instance + (`#13373 `_, + fixes `#13363 `_, + by Hugo Herbelin). +- **Deprecated:** + Undocumented :n:`eauto @nat_or_var @nat_or_var` syntax in favor of new :tacn:`bfs eauto`. + Also deprecated 2-integer syntax for :tacn:`debug eauto` and :tacn:`info_eauto`. + (Use :tacn:`bfs eauto` with the :flag:`Info Eauto` or :flag:`Debug Eauto` flags instead.) + (`#13381 `_, + by Jim Fehrle). +- **Removed:** + :n:`at @occs_nums` clauses in tactics such as tacn:`unfold` + no longer allow negative values. A "-" before the + list (for set complement) is still supported. Ex: "at -1 -2" + is no longer supported but "at -1 2" is. + (`#13403 `_, + by Jim Fehrle). +- **Removed:** + A number of tactics that formerly accepted negative + numbers as parameters now give syntax errors for negative + values. These include {e}constructor, do, timeout, + 9 {e}auto tactics and psatz*. + (`#13417 `_, + by Jim Fehrle). + +Tactic language +^^^^^^^^^^^^^^^ + +- **Fixed:** + printing of the quotation qualifiers when printing :g:`Ltac` functions + (`#13028 `_, + fixes `#9716 `_ + and `#13004 `_, + by Hugo Herbelin). +- **Added:** + An if-then-else syntax to Ltac2 + (`#13232 `_, + fixes `#10110 `_, + by Pierre-Marie Pédrot). + +SSReflect +^^^^^^^^^ + +- **Added:** + SSReflect intro pattern ltac views ``/[dup]``, ``/[swap]`` and ``/[apply]`` + (`#13317 `_, + by Cyril Cohen). +- **Fixed:** + Working around a bug of interaction between + and /(ltac:(...)) cf #13458 + (`#13459 `_, + by Cyril Cohen). + +Commands and options +^^^^^^^^^^^^^^^^^^^^ + +- **Deprecated:** + :cmd:`Grab Existential Variables` and :cmd:`Existential` commands + (`#12516 `_, + by Maxime Dénès). +- **Removed:** + In the :cmd:`Extraction Language` command, remove `Ocaml` as a valid value. + Use `OCaml` instead. This was deprecated in Coq 8.8, `#6261 `_ + (`#13016 `_, by Jim Fehrle). +- **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 setting so we could optimize more. + (`#13040 `_, + fixes `#11277 `_, + by Emilio Jesus Gallego Arias). +- **Changed:** + Drop prefixes from grammar non-terminal names, + e.g. "constr:global" -> "global", "Prim.name" -> "name". + Visible in the output of :cmd:`Print Grammar` and :cmd:`Print Custom Grammar`. + (`#13096 `_, + by Jim Fehrle). +- **Changed:** + When declaring arbitrary terms as hints, unsolved + evars are not abstracted implicitly anymore and instead + raise an error + (`#13139 `_, + by Pierre-Marie Pédrot). +- **Added:** + Added support for automatic insertion of coercions in :cmd:`Search` + patterns. Additionally, head patterns are now automatically + interpreted as types + (`#13255 `_, + fixes `#13244 `_, + by Hugo Herbelin). +- **Added:** + The :cmd:`Proof using` command can now be used without loading the + Ltac plugin (`-noinit` mode) + (`#13339 `_, + by Théo Zimmermann). +- **Added:** + Clarify in the documentation that :cmd:`Add ML Path` is not exported to compiled files + (`#13345 `_, + fixes `#13344 `_, + by Hugo Herbelin). +- **Changed:** + Option -native-compiler of the configure script now impacts the + default value of the option -native-compiler of coqc. The + -native-compiler option of the configure script is added an 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). +- **Deprecated:** + The default value for hint locality is currently :attr:`local` in a section and + :attr:`global` otherwise, but is scheduled to change in a future release. For the + time being, adding hints outside of sections without specifying an explicit + locality is therefore triggering a deprecation warning. It is recommended to + use :attr:`export` whenever possible + (`#13384 `_, + by Pierre-Marie Pédrot). +- **Changed:** + The :attr:`export` locality can now be used for all Hint commands, + including Hint Cut, Hint Mode, Hint Transparent / Opaque and + Remove Hints + (`#13388 `_, + by Pierre-Marie Pédrot). + +Tools +^^^^^ + +- **Changed:** + Adding the possibility in coq_makefile to directly set the installation folders, + through the :n:`COQLIBINSTALL` and :n:`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). +- **Fixed:** + ``coqchk`` no longer reports names from inner modules of opaque modules as + axioms (`#12862 `_, fixes `#12845 + `_, by Jason Gross). + +CoqIDE +^^^^^^ + +- **Added:** + Support showing diffs for :cmd:`Show Proof` in CoqIDE from the :n:`View` menu. + See :ref:`showing_proof_diffs`. + (`#12874 `_, + by Jim Fehrle and Enrico Tassi) +- **Added:** + Support for flag :flag:`Printing Goal Names` in View menu + (`#13145 `_, + by Hugo Herbelin). + +Standard library +^^^^^^^^^^^^^^^^ + +- **Added:** + Extend some list lemmas to both directions: `app_inj_tail_iff`, `app_inv_head_iff`, `app_inv_tail_iff`. + (`#12094 `_, + fixes `#12093 `_, + by Edward Wang). +- **Changed:** + In the reals theory changed the epsilon in the definition of the modulus of convergence for CReal from 1/n (n in positive) to 2^z (z in Z) + so that a precision coarser than one is possible. Also added an upper bound to CReal to enable more efficient computations. + (`#12186 `_, + by Michael Soegtrop). +- **Added:** + ``Decidable`` instance for negation + (`#12420 `_, + by Yishuai Li). +- **Changed:** + Int63 notations now match up with the rest of the standard library: :g:`a \% + m`, :g:`m == n`, :g:`m < n`, :g:`m <= n`, and :g:`m ≤ n` have been replaced + with :g:`a mod m`, :g:`m =? n`, :g:`m `_, fixes + `#12454 `_, by Jason Gross). +- **Changed:** + PrimFloat notations now match up with the rest of the standard library: :g:`m + == n`, :g:`m < n`, and :g:`m <= n` have been replaced with :g:`m =? n`, :g:`m + `_, fixes `#12454 + `_, by Jason Gross). +- **Deprecated:** + ``prod_curry`` and ``prod_uncurry``, in favor of ``uncurry`` and ``curry`` + (`#12716 `_, + by Yishuai Li). +- **Added:** + New lemmas about ``repeat`` in ``List`` and ``Permutation``: ``repeat_app``, ``repeat_eq_app``, ``repeat_eq_cons``, ``repeat_eq_elt``, ``Forall_eq_repeat``, ``Permutation_repeat`` + (`#12799 `_, + by Olivier Laurent). +- **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. + See for example commit 6f62bda in bignums. + (`#12801 `_, + by Vincent Semeria). +- **Changed:** + ``Require Import Coq.nsatz.NsatzTactic`` now allows using :tacn:`nsatz` + with `Z` and `Q` without having to supply instances or using ``Require Import Coq.nsatz.Nsatz``, which + transitively requires unneeded files declaring axioms used in the reals + (`#12861 `_, + fixes `#12860 `_, + by Jason Gross). +- **Fixed:** + `Coq.Program.Wf.Fix_F_inv` and `Coq.Program.Wf.Fix_eq` are now axiom-free. They no longer assume proof irrelevance. + (`#13365 `_, + by Li-yao Xia). + +Infrastructure and dependencies +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +- **Changed:** + Coq's core system 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 the ``micromega`` still uses + ``num`` + (`#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). + Version 8.12 ------------ -- cgit v1.2.3 From 554a3b171e33a649c65a509046387b86615b4348 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 1 Dec 2020 14:49:18 +0100 Subject: Apply suggestions from @jfehrle code review Co-authored-by: Jim Fehrle --- doc/sphinx/changes.rst | 44 ++++++++++++++++++++++---------------------- 1 file changed, 22 insertions(+), 22 deletions(-) (limited to 'doc/sphinx/changes.rst') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index e97fba3546..0626f240fd 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -237,7 +237,6 @@ Specification language, type inference Attributes :attr:`program` and :attr:`canonical` are also affected, with the syntax :n:`@ident__attr(false)` being deprecated in favor of :n:`@ident__attr=no`. - (`#13312 `_, by Emilio Jesus Gallego Arias). - **Fixed:** @@ -251,7 +250,8 @@ Specification language, type inference fixes `#11816 `_, by Hugo Herbelin). - **Fixed:** - issue when two expressions involving different projections and one is + + Issue when two expressions involving different projections and one is primitive need to be unified (`#13386 `_, fixes `#9971 `_, @@ -296,7 +296,7 @@ Notations Rational and real constants are parsed differently. The exponent is now encoded separately from the fractional part using ``Z.pow_pos``. This way, parsing large exponents can no longer - blow up and constants are printed in a form closer to the one they + blow up and constants are printed in a form closer to the one in which they were parsed (i.e., ``102e-2`` is reprinted as such and not ``1.02``). - **Removed** OCaml parser and printer for real constants have been removed. @@ -338,7 +338,7 @@ Notations and `#10803 `_, by Hugo Herbelin). - **Fixed:** - Capture of the name of global references by + Capture the names of global references by binders in the presence of notations for binders (`#12965 `_, fixes `#9569 `_, @@ -348,10 +348,10 @@ Notations (`#12979 `_, by Pierre Roux). - **Changed:** - Redeclaring a notation reactivates also its printing rule; in + Redeclaring a notation also reactivates its printing rule; in particular a second :cmd:`Import` of the same module reactivates the printing rules declared in this module. In theory, this leads to - changes of behavior for printing. However, this is mitigated in + changes in behavior for printing. However, this is mitigated in general by the adoption in `#12986 `_ of a priority given to notations which match a larger part of the term to print @@ -373,7 +373,7 @@ Notations The :n:`@binder` entry of :cmd:`Notation` can now be used in notations expecting a single (non-recursive) binder (`#13265 `_, - by Hugo Herbelin, see section :n:`notations-and-binders` of the + by Hugo Herbelin, see section :ref:`notations-and-binders` of the reference manual). - **Fixed:** Notations understand universe names without getting confused by different imported modules between declaration and use @@ -389,7 +389,7 @@ Tactics (As `lia` gets more powerful, this may break proof scripts relying on `lia` failure.) (`#11906 `_, by Frédéric Besson). - **Added:** - `apply in` supports several hypotheses + :tacn`apply … in` supports several hypotheses (`#12246 `_, by Hugo Herbelin; grants `#9816 `_). @@ -397,10 +397,10 @@ Tactics The deprecated and undocumented "prolog" tactic was removed (`#12399 `_, by Pierre-Marie Pédrot). -- **Removed:** Removed info tactic that was deprecated in 8.5. +- **Removed:** Removed `info` tactic that was deprecated in 8.5. (`#12423 `_, by Jim Fehrle). - **Added:** - Thhe :tacn:`zify` tactic can now be extended by redefining the `zify_pre_hook` + The :tacn:`zify` tactic can now be extended by redefining the `zify_pre_hook` tactic. (`#12552 `_, by Kazuhiko Sakaguchi). - **Added:** @@ -414,7 +414,7 @@ Tactics by Hugo Herbelin). - **Fixed:** Avoiding exposing an internal name of the form :n:`_tmp` when applying the - :n:`_` introduction pattern would break a dependency + :n:`_` introduction pattern which would break a dependency (`#13337 `_, fixes `#13336 `_, by Hugo Herbelin). @@ -431,7 +431,7 @@ Tactics (`#13381 `_, by Jim Fehrle). - **Removed:** - :n:`at @occs_nums` clauses in tactics such as tacn:`unfold` + :n:`at @occs_nums` clauses in tactics such as :tacn:`unfold` no longer allow negative values. A "-" before the list (for set complement) is still supported. Ex: "at -1 -2" is no longer supported but "at -1 2" is. @@ -449,7 +449,7 @@ Tactic language ^^^^^^^^^^^^^^^ - **Fixed:** - printing of the quotation qualifiers when printing :g:`Ltac` functions + Printing of the quotation qualifiers when printing :g:`Ltac` functions (`#13028 `_, fixes `#9716 `_ and `#13004 `_, @@ -488,7 +488,7 @@ Commands and options 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 setting so we could optimize more. + variable and report back on good settings so we can improve the defaults. (`#13040 `_, fixes `#11277 `_, by Emilio Jesus Gallego Arias). @@ -522,12 +522,12 @@ Commands and options fixes `#13344 `_, by Hugo Herbelin). - **Changed:** - Option -native-compiler of the configure script now impacts the - default value of the option -native-compiler of coqc. The - -native-compiler option of the configure script is added an ondemand + 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 + 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 `_ @@ -543,8 +543,8 @@ Commands and options by Pierre-Marie Pédrot). - **Changed:** The :attr:`export` locality can now be used for all Hint commands, - including Hint Cut, Hint Mode, Hint Transparent / Opaque and - Remove Hints + including :tacn:`Hint Cut`, :tacn:`Hint Mode`, :tacn:`Hint Transparent` / `Opaque` and + :tacn:`Remove Hints` (`#13388 `_, by Pierre-Marie Pédrot). @@ -552,7 +552,7 @@ Tools ^^^^^ - **Changed:** - Adding the possibility in coq_makefile to directly set the installation folders, + Added the ability for coq_makefile to directly set the installation folders, through the :n:`COQLIBINSTALL` and :n:`COQDOCINSTALL` variables. See :ref:`coqmakefilelocal`. (`#12389 `_, by Martin Bodin, review of Enrico Tassi). @@ -648,7 +648,7 @@ Infrastructure and dependencies Coq's core system 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 the ``micromega`` still uses + not longer provided; note that ``micromega`` still uses ``num`` (`#11742 `_, by Emilio Jesus Gallego Arias and Vicent Laporte). -- cgit v1.2.3 From e9b3040326632589d811253e91de4f27c9cf70b4 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 1 Dec 2020 15:05:35 +0100 Subject: Changes without PR references fixes --- doc/sphinx/changes.rst | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) (limited to 'doc/sphinx/changes.rst') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 0626f240fd..c9968a64b2 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -292,15 +292,21 @@ Notations by Hugo Herbelin). - **Deprecated** ``Numeral.v`` is deprecated, please use ``Number.v`` instead. + (`#12218 `_, + by Pierre Roux). - **Changed** Rational and real constants are parsed differently. The exponent is now encoded separately from the fractional part using ``Z.pow_pos``. This way, parsing large exponents can no longer blow up and constants are printed in a form closer to the one in which they were parsed (i.e., ``102e-2`` is reprinted as such and not ``1.02``). + (`#12218 `_, + by Pierre Roux). - **Removed** OCaml parser and printer for real constants have been removed. Real constants are now handled with proven Coq code. + (`#12218 `_, + by Pierre Roux). - **Added:** :ref:`Number Notation ` and :ref:`String Notation ` commands now @@ -543,8 +549,8 @@ Commands and options by Pierre-Marie Pédrot). - **Changed:** The :attr:`export` locality can now be used for all Hint commands, - including :tacn:`Hint Cut`, :tacn:`Hint Mode`, :tacn:`Hint Transparent` / `Opaque` and - :tacn:`Remove Hints` + including :cmd:`Hint Cut`, :cmd:`Hint Mode`, :cmd:`Hint Transparent` / `Opaque` and + :cmd:`Remove Hints` (`#13388 `_, by Pierre-Marie Pédrot). -- cgit v1.2.3 From f23ccddcf3bb72d190cfb05e7b48bee416eb8a42 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 1 Dec 2020 15:08:20 +0100 Subject: Fixes in the summary by Jim Fehrle Co-authored-by: Jim Fehrle --- doc/sphinx/changes.rst | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'doc/sphinx/changes.rst') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index c9968a64b2..674adb2038 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -25,8 +25,8 @@ The main changes include: (deactivated by default). This models definitional uniqueness of identity proofs for this type. It is deactivated by default as it results in non-termination in combination with impredicativity. - Use of this flag is also shown by :cmd:`Print Assumptions`. - - Cumulative record and inductives type declarations can now + Use of this flag is also printed by :cmd:`Print Assumptions`. + - 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 implicit arguments and the handling of existential variables in @@ -50,6 +50,8 @@ The main changes include: now supporting reasoning on boolean operators such as `Z.leb` and supporting primitive integers :g:`Int63`. - Typing flags can now be specified :ref:`per-constant / inductive <813TypingFlags>`. + - Improvements to the reference manual including updated syntax descriptions that + match Coq's grammar in several chapters. See the `Changes in 8.13`_ section and following sections for the detailed list of changes, including potentially breaking changes marked @@ -93,7 +95,7 @@ Thomas Letan, Yishuai Li, Xia Li-yao, James Lottes, Jean-Christophe Léchenet, Kenji Maillard, Erik Martin-Dorel, Yusuke Matsushita, Guillaume Melquiond, Carl Patenaude-Poulin, Clément Pit-Claudel, Pierre-Marie Pédrot, Pierre Roux, Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Matthieu Sozeau, -Enrico Tassi, Anton Trunov, Edward Wang, Li-yao Xia, Beta Ziliani, Théo Zimmermann. +Enrico Tassi, Anton Trunov, Edward Wang, Li-yao Xia, Beta Ziliani and Théo Zimmermann. The Coq community at large helped improve the design of this new version via the GitHub issue and pull request system, the Coq development mailing list @@ -102,7 +104,7 @@ coqdev@inria.fr, the coq-club@inria.fr mailing list, the `Discourse forum Version 8.13's development spanned 5 months from the release of Coq 8.12.0. Enrico Tassi and Maxime Dénès are the release managers of Coq 8.13. -This release is the result of 400 PRs merged, closing ~100 issues. +This release is the result of 400 merged PRs, closing ~100 issues. | Nantes, November 2020, | Matthieu Sozeau for the Coq development team -- cgit v1.2.3 From 002ab0b6bdf38c4dea0ce74e2a0df1e3d2bc238d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 1 Dec 2020 15:15:38 +0100 Subject: Update doc/sphinx/changes.rst Co-authored-by: Jim Fehrle --- doc/sphinx/changes.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/sphinx/changes.rst') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 674adb2038..6facb0e207 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -35,7 +35,7 @@ The main changes include: multiple distinct patterns. - New warning for `Hint` commands outside sections without a locality attribute, whose goal is to eventually remove the fragile default - behavior of having hints be imported when using `Require` only. + behavior of importing hints only when using `Require`. The recommended fix is to declare hints as `export`, instead of the current default `global`, meaning that they are imported through `Require Import` only, not `Require`. -- cgit v1.2.3 From 73eb97c9067caabe5dc93bbb4c5e68b5783f1787 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 1 Dec 2020 17:02:20 +0100 Subject: Apply suggestions from code review Co-authored-by: Jim Fehrle --- doc/sphinx/changes.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'doc/sphinx/changes.rst') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 6facb0e207..9a2e1b686b 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -83,7 +83,7 @@ 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 +Tassi, Laurent Théry, Anton Trunov, Li-yao Xia and Théo Zimmermann The 52 contributors to this version are Reynald Affeldt, Tanaka Akira, Frédéric Besson, Lasse Blaauwbroek, Clément Blaudeau, Martin Bodin, Ali Caglayan, Tej Chajed, @@ -535,8 +535,8 @@ Commands and options `-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. + 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 `_, -- cgit v1.2.3 From dba9b80b25a75b9f210f87d4c1f58bc95ef33fa9 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 2 Dec 2020 16:31:59 +0100 Subject: Apply suggestions from code review Co-authored-by: Théo Zimmermann --- doc/sphinx/changes.rst | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'doc/sphinx/changes.rst') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 9a2e1b686b..0ae80e0685 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -111,8 +111,8 @@ This release is the result of 400 merged PRs, closing ~100 issues. | -Changes in 8.13 -~~~~~~~~~~~~~~~ +Changes in 8.13+beta1 +~~~~~~~~~~~~~~~~~~~~~ .. contents:: :local: @@ -212,7 +212,7 @@ Specification language, type inference (`#13188 `_, fixes `#6042 `_, by Gaëtan Gilbert). - **Fixed:** - Allow use of type classes inference for the return predicate of a :n:`match` + Allow use of typeclass inference for the return predicate of a :n:`match` (was deactivated in versions 8.10 to 8.12, `#13217 `_, fixes `#13216 `_, by Hugo Herbelin). @@ -252,7 +252,6 @@ Specification language, type inference fixes `#11816 `_, by Hugo Herbelin). - **Fixed:** - Issue when two expressions involving different projections and one is primitive need to be unified (`#13386 `_, @@ -319,8 +318,8 @@ Notations reference manual). - **Changed:** Scope information is propagated in indirect applications to a - reference prefixed with :g:`@@`; this covers for instance the case - :g:`r.(@@p) t` where scope information from :g:`p` is now taken into + reference prefixed with :g:`@`; this covers for instance the case + :g:`r.(@p) t` where scope information from :g:`p` is now taken into account for interpreting :g:`t` (`#12685 `_, by Hugo Herbelin). - **Added:** @@ -352,7 +351,7 @@ Notations fixes `#9569 `_, by Hugo Herbelin). - **Deprecated:** - :n:`Numeral Notation`, please use :ref:`Number Notation ` instead. + `Numeral Notation`, please use :cmd:`Number Notation` instead (`#12979 `_, by Pierre Roux). - **Changed:** @@ -397,15 +396,15 @@ Tactics (As `lia` gets more powerful, this may break proof scripts relying on `lia` failure.) (`#11906 `_, by Frédéric Besson). - **Added:** - :tacn`apply … in` supports several hypotheses + :tacn:`apply … in` supports several hypotheses (`#12246 `_, by Hugo Herbelin; grants `#9816 `_). - **Removed:** - The deprecated and undocumented "prolog" tactic was removed + The deprecated and undocumented `prolog` tactic was removed (`#12399 `_, by Pierre-Marie Pédrot). -- **Removed:** Removed `info` tactic that was deprecated in 8.5. +- **Removed:** `info` tactic that was deprecated in 8.5. (`#12423 `_, by Jim Fehrle). - **Added:** The :tacn:`zify` tactic can now be extended by redefining the `zify_pre_hook` @@ -421,7 +420,7 @@ Tactics fixes `#13235 `_, by Hugo Herbelin). - **Fixed:** - Avoiding exposing an internal name of the form :n:`_tmp` when applying the + Avoid exposing an internal name of the form :n:`_tmp` when applying the :n:`_` introduction pattern which would break a dependency (`#13337 `_, fixes `#13336 `_, @@ -476,7 +475,8 @@ SSReflect (`#13317 `_, by Cyril Cohen). - **Fixed:** - Working around a bug of interaction between + and /(ltac:(...)) cf #13458 + Working around a bug of interaction between + and /(ltac:(...)) cf + `#13458 `_ (`#13459 `_, by Cyril Cohen). -- cgit v1.2.3 From d6f42354bc4c0129ee067052c40a5f62a6783c52 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 2 Dec 2020 17:18:15 +0100 Subject: Implement suggestions by Théo Zimmermann --- doc/sphinx/changes.rst | 444 +++++++++++++++++++++++++------------------------ 1 file changed, 228 insertions(+), 216 deletions(-) (limited to 'doc/sphinx/changes.rst') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 0ae80e0685..b5fb2cbcec 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -18,26 +18,26 @@ Coq version 8.13 integrates many usability improvements, as well as extensions of the core language. The main changes include: - - Introduction of :ref:`primitive persistent arrays` + - :ref:`Introduction <813PrimArrays>` of :ref:`primitive persistent arrays` in the core language, implemented using imperative persistent arrays. - - Introduction of definitional proof irrelevance for the equality type + - 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 results in non-termination in combination with impredicativity. + it can lead to non-termination in combination with impredicativity. Use of this flag is also printed by :cmd:`Print Assumptions`. - Cumulative record and inductive type declarations can now - :ref:`specify<813VarianceDecl>` the variance of their universes. + :ref:`specify <813VarianceDecl>` the variance of their universes. - Various bugfixes and uniformization of behavior with respect to the use of implicit arguments and the handling of existential variables in declarations, unification and tactics. - - New warning for :ref:`unused variables <813UnusedVar>` in catch-all match branches that match - multiple distinct patterns. - - New warning for `Hint` commands outside sections without a locality - attribute, whose goal is to eventually remove the fragile default - behavior of importing hints only when using `Require`. - The recommended fix is to declare hints as `export`, instead of - the current default `global`, meaning that they are imported + - New warning for :ref:`unused variables <813UnusedVar>` in catch-all match + branches that match multiple distinct patterns. + - New :ref:`warning <813HintWarning>` for `Hint` commands outside + sections without a locality attribute, whose goal is to eventually + remove the fragile default behavior of importing hints only when + using `Require`. The recommended fix is to declare hints as `export`, + instead of the current default `global`, meaning that they are imported through `Require Import` only, not `Require`. See the following `rationale and guidelines `_ for details. @@ -46,14 +46,15 @@ The main changes include: including number notations, recursive notations and notations with bindings. A new algorithm chooses the most precise notation available to print an expression, which might introduce changes in printing behavior. - - Tactic improvements in :tacn:`lia` and its :tacn:`zify` preprocessing step, - now supporting reasoning on boolean operators such as `Z.leb` and supporting + - Tactic :ref:`improvements <813Tactics>` in :tacn:`lia` and its :tacn:`zify` preprocessing step, + now supporting reasoning on boolean operators such as :g:`Z.leb` and supporting primitive integers :g:`Int63`. - Typing flags can now be specified :ref:`per-constant / inductive <813TypingFlags>`. - - Improvements to the reference manual including updated syntax descriptions that - match Coq's grammar in several chapters. + - Improvements to the reference manual including updated syntax + descriptions that match Coq's grammar in several chapters, and splitting parts of + the tactics chapter to independent sections. -See the `Changes in 8.13`_ section and following sections for the +See the `Changes in 8.13+beta1`_ section and following sections for the detailed list of changes, including potentially breaking changes marked with **Changed**. @@ -75,15 +76,15 @@ 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/. -TODO updated maintainers -Our current 31 maintainers are Yves Bertot, Frédéric Besson, Tej +Our current 32 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 and Théo Zimmermann +Vincent Laporte, Olivier Laurent, 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 +and Théo Zimmermann. The 52 contributors to this version are Reynald Affeldt, Tanaka Akira, Frédéric Besson, Lasse Blaauwbroek, Clément Blaudeau, Martin Bodin, Ali Caglayan, Tej Chajed, @@ -120,17 +121,29 @@ Changes in 8.13+beta1 Kernel ^^^^^^ + .. _813UIP: + - **Added:** Definitional UIP, only when :flag:`Definitional UIP` is enabled. See documentation of the flag for details. (`#10390 `_, by Gaëtan Gilbert). + + .. _813PrimArrays: + - **Added:** Built-in support for persistent arrays, which expose a functional interface but are implemented using an imperative data structure, for better performance. (`#11604 `_, by Maxime Dénès and Benjamin Grégoire, with help from Gaëtan Gilbert). + + Primitive arrays are irrelevant in their single + polymorphic universe (same as a polymorphic cumulative list + inductive would be) (`#13356 + `_, fixes `#13354 + `_, by Gaëtan Gilbert). + - **Fixed:** A loss of definitional equality for declarations obtained through :cmd:`Include` when entering the scope of a :cmd:`Module` or @@ -139,37 +152,39 @@ Kernel (`#12537 `_, fixes `#12525 `_ and `#12647 `_, by Hugo Herbelin). -- **Changed:** Primitive arrays are now irrelevant in their single - polymorphic universe (same as a polymorphic cumulative list - inductive would be) (`#13356 - `_, fixes `#13354 - `_, by Gaëtan Gilbert). Specification language, type inference ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + .. _813BooleanAttrs: + - **Changed:** - In :tacn:`refine`, new existential variables unified with existing ones are no - longer considered as fresh. The behavior of :tacn:`simple refine` no longer depends on - the orientation of evar-evar unification problems, and new existential variables - are always turned into (unshelved) goals. This can break compatibility in - some cases (`#7825 `_, by Matthieu - Sozeau, with help from Maxime Dénès, review by Pierre-Marie Pédrot and - Enrico Tassi, fixes `#4095 `_ and - `#4413 `_). + :term:`Boolean attributes ` are now specified using + key/value pairs, that is to say :n:`@ident__attr{? = {| yes | no } }`. + If the value is missing, the default is :n:`yes`. The old syntax is still + supported, but produces the ``deprecated-attribute-syntax`` warning. + + Deprecated attributes are :attr:`universes(monomorphic)`, + :attr:`universes(notemplate)` and :attr:`universes(noncumulative)`, which are + respectively replaced by :attr:`universes(polymorphic=no) `, + :attr:`universes(template=no) ` + and :attr:`universes(cumulative=no) `. + Attributes :attr:`program` and :attr:`canonical` are also affected, + with the syntax :n:`@ident__attr(false)` being deprecated in favor of + :n:`@ident__attr=no`. + (`#13312 `_, + by Emilio Jesus Gallego Arias). - **Changed:** Heuristics for universe minimization to :g:`Set`: also use constraints ``Prop <= i`` (`#10331 `_, by Gaëtan Gilbert with help from Maxime Dénès and Matthieu Sozeau, fixes `#12414 `_). - - .. _813VarianceDecl: - -- **Added:** Commands :cmd:`Inductive`, :cmd:`Record` and synonyms now - support syntax `Inductive foo@{=i +j *k l}` to specify variance - information for their universes (in :ref:`Cumulative ` - mode) (`#12653 `_, by Gaëtan - Gilbert). +- **Changed:** The type given to :cmd:`Instance` is no longer automatically + generalized over unbound and :ref:`generalizable ` variables. + Use ``Instance : `{type}`` instead of :n:`Instance : @type` to get the old behaviour, or + enable the compatibility flag :flag:`Instance Generalized Output`. + (`#13188 `_, fixes `#6042 + `_, by Gaëtan Gilbert). - **Changed:** Tweaked the algorithm giving default names to arguments. Should reduce the frequency that argument names get an @@ -179,6 +194,19 @@ Specification language, type inference fixes `#12001 `_ and `#6785 `_, by Jasper Hugunin). +- **Removed:** + Undocumented and experimental forward class hint feature ``:>>``. + Use ``:>`` (see :n:`@of_type`) instead + (`#13106 `_, + by Pierre-Marie Pédrot). + + .. _813VarianceDecl: + +- **Added:** Commands :cmd:`Inductive`, :cmd:`Record` and synonyms now + support syntax `Inductive foo@{=i +j *k l}` to specify variance + information for their universes (in :ref:`Cumulative ` + mode) (`#12653 `_, by Gaëtan + Gilbert). .. _813UnusedVar: @@ -189,58 +217,28 @@ Specification language, type inference (`#12768 `_, fixes `#12762 `_, by Hugo Herbelin). -- **Removed:** - Undocumented and experimental forward class hint feature ``:>>``. - Use ``:>`` (see :n:`@of_type`) instead - (`#13106 `_, - by Pierre-Marie Pédrot). -- **Fixed:** - Implicit arguments taken into account in defined fields of a record type declaration - (`#13166 `_, - fixes `#13165 `_, - by Hugo Herbelin). - **Added:** Definition and (Co)Fixpoint now support the :attr:`using` attribute. It has the same effect as :cmd:`Proof using`, which is only available in interactive mode. (`#13183 `_, by Enrico Tassi). -- **Removed:** The type given to :cmd:`Instance` is no longer automatically - generalized over unbound and :ref:`generalizable ` variables. - Use :n:`Instance : \`{@type}` instead of :n:`Instance : @type` to get the old behaviour, or - enable the compatibility flag :flag:`Instance Generalized Output`. - (`#13188 `_, fixes `#6042 - `_, by Gaëtan Gilbert). -- **Fixed:** - Allow use of typeclass inference for the return predicate of a :n:`match` - (was deactivated in versions 8.10 to 8.12, `#13217 `_, - fixes `#13216 `_, - by Hugo Herbelin). - **Added:** Inference of return predicate of a :g:`match` by inversion takes sort elimination constraints into account (`#13290 `_, grants `#13278 `_, by Hugo Herbelin). - - .. _813BooleanAttrs: - -- **Changed:** - :term:`Boolean attributes ` are now specified using - key/value pairs, that is to say :n:`@ident__attr{? = {| yes | no } }`. - If the value is missing, the default is :n:`yes`. The old syntax is still - supported, but produces the ``deprecated-attribute-syntax`` warning. - - Deprecated attributes are :attr:`universes(monomorphic)`, - :attr:`universes(notemplate)` and :attr:`universes(noncumulative)`, which are - respectively replaced by :attr:`universes(polymorphic=no) `, - :attr:`universes(template=no) ` - and :attr:`universes(cumulative=no) `. - Attributes :attr:`program` and :attr:`canonical` are also affected, - with the syntax :n:`@ident__attr(false)` being deprecated in favor of - :n:`@ident__attr=no`. - (`#13312 `_, - by Emilio Jesus Gallego Arias). +- **Fixed:** + Implicit arguments taken into account in defined fields of a record type declaration + (`#13166 `_, + fixes `#13165 `_, + by Hugo Herbelin). +- **Fixed:** + Allow use of typeclass inference for the return predicate of a :n:`match` + (was deactivated in versions 8.10 to 8.12, `#13217 `_, + fixes `#13216 `_, + by Hugo Herbelin). - **Fixed:** A case of unification raising an anomaly IllTypedInstance (`#13376 `_, @@ -282,19 +280,10 @@ Notations (`#11841 `_, fixes `#9514 `_, by Hugo Herbelin). -- **Added:** - :flag:`Printing Float` flag to print primitive floats as hexadecimal - instead of decimal values. This is included in the :flag:`Printing All` flag - (`#11986 `_, - by Pierre Roux). - **Changed:** Improved support for notations/abbreviations with mixed terms and patterns (such as the forcing modality) (`#12099 `_, by Hugo Herbelin). -- **Deprecated** - ``Numeral.v`` is deprecated, please use ``Number.v`` instead. - (`#12218 `_, - by Pierre Roux). - **Changed** Rational and real constants are parsed differently. The exponent is now encoded separately from the fractional part @@ -303,29 +292,12 @@ Notations were parsed (i.e., ``102e-2`` is reprinted as such and not ``1.02``). (`#12218 `_, by Pierre Roux). -- **Removed** - OCaml parser and printer for real constants have been removed. - Real constants are now handled with proven Coq code. - (`#12218 `_, - by Pierre Roux). -- **Added:** - :ref:`Number Notation ` and :ref:`String Notation - ` commands now - support parameterized inductive and non inductive types - (`#12218 `_, - fixes `#12035 `_, - by Pierre Roux, review by Jason Gross and Jim Fehrle for the - reference manual). - **Changed:** Scope information is propagated in indirect applications to a reference prefixed with :g:`@`; this covers for instance the case :g:`r.(@p) t` where scope information from :g:`p` is now taken into account for interpreting :g:`t` (`#12685 `_, by Hugo Herbelin). -- **Added:** - Added support for encoding notations of the form :g:`x ⪯ y ⪯ .. ⪯ z ⪯ t` - (`#12765 `_, - by Hugo Herbelin). - **Changed:** New model for ``only parsing`` and ``only printing`` notations with support for at most one parsing-and-printing or only-parsing @@ -336,24 +308,6 @@ Notations and `#9682 `_ and part 2 of `#12908 `_, by Hugo Herbelin). -- **Fixed:** - Issues in the presence of notations recursively referring to another - applicative notations, such as missing scope propagation, or failure - to use a notation for printing - (`#12960 `_, - fixes `#9403 `_ - and `#10803 `_, - by Hugo Herbelin). -- **Fixed:** - Capture the names of global references by - binders in the presence of notations for binders - (`#12965 `_, - fixes `#9569 `_, - by Hugo Herbelin). -- **Deprecated:** - `Numeral Notation`, please use :cmd:`Number Notation` instead - (`#12979 `_, - by Pierre Roux). - **Changed:** Redeclaring a notation also reactivates its printing rule; in particular a second :cmd:`Import` of the same module reactivates the @@ -371,10 +325,35 @@ Notations to notations which match a larger part of the term to abbreviate (`#12986 `_, by Hugo Herbelin). -- **Fixed:** - Preventing notations for constructors to involve binders - (`#13092 `_, - fixes `#13078 `_, +- **Removed** + OCaml parser and printer for real constants have been removed. + Real constants are now handled with proven Coq code. + (`#12218 `_, + by Pierre Roux). +- **Deprecated** + ``Numeral.v`` is deprecated, please use ``Number.v`` instead. + (`#12218 `_, + by Pierre Roux). +- **Deprecated:** + `Numeral Notation`, please use :cmd:`Number Notation` instead + (`#12979 `_, + by Pierre Roux). +- **Added:** + :flag:`Printing Float` flag to print primitive floats as hexadecimal + instead of decimal values. This is included in the :flag:`Printing All` flag + (`#11986 `_, + by Pierre Roux). +- **Added:** + :ref:`Number Notation ` and :ref:`String Notation + ` commands now + support parameterized inductive and non inductive types + (`#12218 `_, + fixes `#12035 `_, + by Pierre Roux, review by Jason Gross and Jim Fehrle for the + reference manual). +- **Added:** + Added support for encoding notations of the form :g:`x ⪯ y ⪯ .. ⪯ z ⪯ t` + (`#12765 `_, by Hugo Herbelin). - **Added:** The :n:`@binder` entry of :cmd:`Notation` can now be used in @@ -382,15 +361,77 @@ Notations (`#13265 `_, by Hugo Herbelin, see section :ref:`notations-and-binders` of the reference manual). +- **Fixed:** + Issues in the presence of notations recursively referring to another + applicative notations, such as missing scope propagation, or failure + to use a notation for printing + (`#12960 `_, + fixes `#9403 `_ + and `#10803 `_, + by Hugo Herbelin). +- **Fixed:** + Capture the names of global references by + binders in the presence of notations for binders + (`#12965 `_, + fixes `#9569 `_, + by Hugo Herbelin). +- **Fixed:** + Preventing notations for constructors to involve binders + (`#13092 `_, + fixes `#13078 `_, + by Hugo Herbelin). - **Fixed:** Notations understand universe names without getting confused by different imported modules between declaration and use locations (`#13415 `_, fixes `#13303 `_, by Gaëtan Gilbert). + .. _813Tactics: + Tactics ^^^^^^^ +- **Changed:** + In :tacn:`refine`, new existential variables unified with existing ones are no + longer considered as fresh. The behavior of :tacn:`simple refine` no longer depends on + the orientation of evar-evar unification problems, and new existential variables + are always turned into (unshelved) goals. This can break compatibility in + some cases (`#7825 `_, by Matthieu + Sozeau, with help from Maxime Dénès, review by Pierre-Marie Pédrot and + Enrico Tassi, fixes `#4095 `_ and + `#4413 `_). +- **Changed:** + Giving an empty list of occurrences after :n:`in` in tactics is no + longer permitted. Omitting the :n:`in` gives the same behavior + (`#13237 `_, + fixes `#13235 `_, + by Hugo Herbelin). +- **Removed:** + :n:`at @occs_nums` clauses in tactics such as :tacn:`unfold` + no longer allow negative values. A "-" before the + list (for set complement) is still supported. Ex: "at -1 -2" + is no longer supported but "at -1 2" is. + (`#13403 `_, + by Jim Fehrle). +- **Removed:** + A number of tactics that formerly accepted negative + numbers as parameters now give syntax errors for negative + values. These include {e}constructor, do, timeout, + 9 {e}auto tactics and psatz*. + (`#13417 `_, + by Jim Fehrle). +- **Removed:** + The deprecated and undocumented `prolog` tactic was removed + (`#12399 `_, + by Pierre-Marie Pédrot). +- **Removed:** `info` tactic that was deprecated in 8.5. + (`#12423 `_, by Jim Fehrle). +- **Deprecated:** + Undocumented :n:`eauto @nat_or_var @nat_or_var` syntax in favor of new :tacn:`bfs eauto`. + Also deprecated 2-integer syntax for :tacn:`debug eauto` and :tacn:`info_eauto`. + (Use :tacn:`bfs eauto` with the :flag:`Info Eauto` or :flag:`Debug Eauto` flags instead.) + (`#13381 `_, + by Jim Fehrle). - **Added:** :tacn:`lia` is extended to deal with boolean operators e.g. `andb` or `Z.leb`. (As `lia` gets more powerful, this may break proof scripts relying on `lia` failure.) @@ -400,12 +441,6 @@ Tactics (`#12246 `_, by Hugo Herbelin; grants `#9816 `_). -- **Removed:** - The deprecated and undocumented `prolog` tactic was removed - (`#12399 `_, - by Pierre-Marie Pédrot). -- **Removed:** `info` tactic that was deprecated in 8.5. - (`#12423 `_, by Jim Fehrle). - **Added:** The :tacn:`zify` tactic can now be extended by redefining the `zify_pre_hook` tactic. (`#12552 `_, @@ -413,12 +448,6 @@ Tactics - **Added:** The :tacn:`zify` tactic provides support for primitive integers (module :g:`ZifyInt63`). (`#12648 `_, by Frédéric Besson). -- **Changed:** - Giving an empty list of occurrences after :n:`in` in tactics is no - longer permitted. Omitting the :n:`in` gives the same behavior - (`#13237 `_, - fixes `#13235 `_, - by Hugo Herbelin). - **Fixed:** Avoid exposing an internal name of the form :n:`_tmp` when applying the :n:`_` introduction pattern which would break a dependency @@ -431,41 +460,21 @@ Tactics (`#13373 `_, fixes `#13363 `_, by Hugo Herbelin). -- **Deprecated:** - Undocumented :n:`eauto @nat_or_var @nat_or_var` syntax in favor of new :tacn:`bfs eauto`. - Also deprecated 2-integer syntax for :tacn:`debug eauto` and :tacn:`info_eauto`. - (Use :tacn:`bfs eauto` with the :flag:`Info Eauto` or :flag:`Debug Eauto` flags instead.) - (`#13381 `_, - by Jim Fehrle). -- **Removed:** - :n:`at @occs_nums` clauses in tactics such as :tacn:`unfold` - no longer allow negative values. A "-" before the - list (for set complement) is still supported. Ex: "at -1 -2" - is no longer supported but "at -1 2" is. - (`#13403 `_, - by Jim Fehrle). -- **Removed:** - A number of tactics that formerly accepted negative - numbers as parameters now give syntax errors for negative - values. These include {e}constructor, do, timeout, - 9 {e}auto tactics and psatz*. - (`#13417 `_, - by Jim Fehrle). Tactic language ^^^^^^^^^^^^^^^ +- **Added:** + An if-then-else syntax to Ltac2 + (`#13232 `_, + fixes `#10110 `_, + by Pierre-Marie Pédrot). - **Fixed:** Printing of the quotation qualifiers when printing :g:`Ltac` functions (`#13028 `_, fixes `#9716 `_ and `#13004 `_, by Hugo Herbelin). -- **Added:** - An if-then-else syntax to Ltac2 - (`#13232 `_, - fixes `#10110 `_, - by Pierre-Marie Pédrot). SSReflect ^^^^^^^^^ @@ -483,14 +492,6 @@ SSReflect Commands and options ^^^^^^^^^^^^^^^^^^^^ -- **Deprecated:** - :cmd:`Grab Existential Variables` and :cmd:`Existential` commands - (`#12516 `_, - by Maxime Dénès). -- **Removed:** - In the :cmd:`Extraction Language` command, remove `Ocaml` as a valid value. - Use `OCaml` instead. This was deprecated in Coq 8.8, `#6261 `_ - (`#13016 `_, by Jim Fehrle). - **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 @@ -512,23 +513,6 @@ Commands and options raise an error (`#13139 `_, by Pierre-Marie Pédrot). -- **Added:** - Added support for automatic insertion of coercions in :cmd:`Search` - patterns. Additionally, head patterns are now automatically - interpreted as types - (`#13255 `_, - fixes `#13244 `_, - by Hugo Herbelin). -- **Added:** - The :cmd:`Proof using` command can now be used without loading the - Ltac plugin (`-noinit` mode) - (`#13339 `_, - by Théo Zimmermann). -- **Added:** - Clarify in the documentation that :cmd:`Add ML Path` is not exported to compiled files - (`#13345 `_, - fixes `#13344 `_, - by Hugo Herbelin). - **Changed:** Option `-native-compiler` of the configure script now impacts the default value of the `-native-compiler` option of coqc. The @@ -541,6 +525,19 @@ Commands and options `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 `_ + (`#13016 `_, by Jim Fehrle). + + .. _813HintWarning: + - **Deprecated:** The default value for hint locality is currently :attr:`local` in a section and :attr:`global` otherwise, but is scheduled to change in a future release. For the @@ -549,12 +546,27 @@ Commands and options use :attr:`export` whenever possible (`#13384 `_, by Pierre-Marie Pédrot). -- **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). +- **Deprecated:** + :cmd:`Grab Existential Variables` and :cmd:`Existential` commands + (`#12516 `_, + by Maxime Dénès). +- **Added:** + Added support for automatic insertion of coercions in :cmd:`Search` + patterns. Additionally, head patterns are now automatically + interpreted as types + (`#13255 `_, + fixes `#13244 `_, + by Hugo Herbelin). +- **Added:** + The :cmd:`Proof using` command can now be used without loading the + Ltac plugin (`-noinit` mode) + (`#13339 `_, + by Théo Zimmermann). +- **Added:** + Clarify in the documentation that :cmd:`Add ML Path` is not exported to compiled files + (`#13345 `_, + fixes `#13344 `_, + by Hugo Herbelin). Tools ^^^^^ @@ -592,20 +604,11 @@ CoqIDE Standard library ^^^^^^^^^^^^^^^^ -- **Added:** - Extend some list lemmas to both directions: `app_inj_tail_iff`, `app_inv_head_iff`, `app_inv_tail_iff`. - (`#12094 `_, - fixes `#12093 `_, - by Edward Wang). - **Changed:** In the reals theory changed the epsilon in the definition of the modulus of convergence for CReal from 1/n (n in positive) to 2^z (z in Z) so that a precision coarser than one is possible. Also added an upper bound to CReal to enable more efficient computations. (`#12186 `_, by Michael Soegtrop). -- **Added:** - ``Decidable`` instance for negation - (`#12420 `_, - by Yishuai Li). - **Changed:** Int63 notations now match up with the rest of the standard library: :g:`a \% m`, :g:`m == n`, :g:`m < n`, :g:`m <= n`, and :g:`m ≤ n` have been replaced @@ -624,14 +627,6 @@ Standard library get the ``PrimFloat`` notations without unqualifying the various primitives (`#12556 `_, fixes `#12454 `_, by Jason Gross). -- **Deprecated:** - ``prod_curry`` and ``prod_uncurry``, in favor of ``uncurry`` and ``curry`` - (`#12716 `_, - by Yishuai Li). -- **Added:** - New lemmas about ``repeat`` in ``List`` and ``Permutation``: ``repeat_app``, ``repeat_eq_app``, ``repeat_eq_cons``, ``repeat_eq_elt``, ``Forall_eq_repeat``, ``Permutation_repeat`` - (`#12799 `_, - by Olivier Laurent). - **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. See for example commit 6f62bda in bignums. @@ -644,6 +639,23 @@ Standard library (`#12861 `_, fixes `#12860 `_, by Jason Gross). +- **Deprecated:** + ``prod_curry`` and ``prod_uncurry``, in favor of ``uncurry`` and ``curry`` + (`#12716 `_, + by Yishuai Li). +- **Added:** + New lemmas about ``repeat`` in ``List`` and ``Permutation``: ``repeat_app``, ``repeat_eq_app``, ``repeat_eq_cons``, ``repeat_eq_elt``, ``Forall_eq_repeat``, ``Permutation_repeat`` + (`#12799 `_, + by Olivier Laurent). +- **Added:** + Extend some list lemmas to both directions: `app_inj_tail_iff`, `app_inv_head_iff`, `app_inv_tail_iff`. + (`#12094 `_, + fixes `#12093 `_, + by Edward Wang). +- **Added:** + ``Decidable`` instance for negation + (`#12420 `_, + by Yishuai Li). - **Fixed:** `Coq.Program.Wf.Fix_F_inv` and `Coq.Program.Wf.Fix_eq` are now axiom-free. They no longer assume proof irrelevance. (`#13365 `_, -- cgit v1.2.3 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(-) (limited to 'doc/sphinx/changes.rst') 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