diff options
Diffstat (limited to 'doc/sphinx/changes.rst')
| -rw-r--r-- | doc/sphinx/changes.rst | 181 |
1 files changed, 156 insertions, 25 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 1d0c937792..5ca0d8b81f 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -1,8 +1,10 @@ +.. _changes: + -------------- Recent changes -------------- -.. ifconfig:: not coq_config.is_a_released_version +.. ifconfig:: not is_a_released_version .. include:: ../unreleased.rst @@ -50,23 +52,28 @@ __ 811RefineInstance_ __ 811SSRUnderOver_ __ 811Reals_ -The ``dev/doc/critical-bugs`` file documents the known critical bugs of |Coq| -and affected releases. See the `Changes in 8.11+beta1`_ section for the -detailed list of changes, including potentially breaking changes marked with -**Changed**. +Additionally, while the :tacn:`omega` tactic is not yet deprecated in +this version of Coq, it should soon be the case and we already +recommend users to switch to :tacn:`lia` in new proof scripts (see +also the warning message in the :ref:`corresponding chapter <omega>`). -Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael -Soegtrop, Théo Zimmermann worked on maintaining and improving the -continuous integration system and package building infrastructure. +The ``dev/doc/critical-bugs`` file documents the known critical bugs +of |Coq| and affected releases. See the `Changes in 8.11+beta1`_ +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.11+beta1/api (documentation of -the ML API), https://coq.github.io/doc/V8.11+beta1/refman (reference -manual), and https://coq.github.io/doc/V8.11+beta1/stdlib (documentation of +Coq's documentation is available at https://coq.github.io/doc/v8.11/api (documentation of +the ML API), https://coq.github.io/doc/v8.11/refman (reference +manual), and https://coq.github.io/doc/v8.11/stdlib (documentation of the standard library). +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. + The OPAM repository for |Coq| packages has been maintained by -Karl Palmskog, Matthieu Sozeau, Enrico Tassi with contributions -from many users. A list of packages is available at +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/. The 61 contributors to this version are Michael D. Adams, Guillaume @@ -153,7 +160,7 @@ Changes in 8.11+beta1 Annotation in `Arguments` for bidirectionality hints: it is now possible to tell type inference to use type information from the context once the `n` first arguments of an application are known. The syntax is: - `Arguments foo x y & z`. See :cmd:`Arguments (bidirectionality hints)` + `Arguments foo x y & z`. See :ref:`bidirectionality_hints` (`#10049 <https://github.com/coq/coq/pull/10049>`_, by Maxime Dénès with help from Enrico Tassi). - **Added:** @@ -209,13 +216,13 @@ Changes in 8.11+beta1 - **Changed:** Output of the :cmd:`Print` and :cmd:`About` commands. Arguments meta-data is now displayed as the corresponding - :cmd:`Arguments <Arguments (implicits)>` command instead of the + :cmd:`Arguments` command instead of the human-targeted prose used in previous Coq versions. (`#10985 <https://github.com/coq/coq/pull/10985>`_, by Gaëtan Gilbert). .. _811RefineInstance: -- **Added:** ``#[refine]`` attribute for :cmd:`Instance`, a more +- **Added:** :attr:`refine` attribute for :cmd:`Instance`, a more predictable version of the old ``Refine Instance Mode`` which unconditionally opens a proof (`#10996 <https://github.com/coq/coq/pull/10996>`_, by Gaëtan Gilbert). @@ -350,11 +357,8 @@ Changes in 8.11+beta1 `iff`. Now, it is also performed for any relation `R1` which has a ``RewriteRelation`` instance (a `RelationClasses.Reflexive` instance being also needed so :tacn:`over` can discharge the ``'Under[ _ ]`` - goal by instantiating the hidden evar.) Also, it is now possible to - manipulate `Under_rel _ R1 (f1 i) (?f2 i)` subgoals directly if `R1` - is a `PreOrder` relation or so, thanks to extra instances proving - that `Under_rel` preserves the properties of the `R1` relation. - These two features generalizing support for setoid-like relations is + goal by instantiating the hidden evar.) + This feature generalizing support for setoid-like relations is enabled as soon as we do both ``Require Import ssreflect.`` and ``Require Setoid.`` Finally, a rewrite rule ``UnderE`` has been added if one wants to "unprotect" the evar, and instantiate it @@ -512,6 +516,133 @@ Changes in 8.11+beta1 (`#10471 <https://github.com/coq/coq/pull/10471>`_, by Emilio Jesús Gallego Arias). +Changes in 8.11.0 +~~~~~~~~~~~~~~~~~ + +**Kernel** + +- **Changed:** the native compilation (:tacn:`native_compute`) now + creates a directory to contain temporary files instead of putting + them in the root of the system temporary directory (`#11081 + <https://github.com/coq/coq/pull/11081>`_, by Gaëtan Gilbert). +- **Fixed:** `#11360 <https://github.com/issues/11360>`_. + Broken section closing when a template polymorphic inductive type depends on + a section variable through its parameters (`#11361 + <https://github.com/coq/coq/pull/11361>`_, by Gaëtan Gilbert). +- **Fixed:** The type of :g:`Set+1` would be computed to be itself, + leading to a proof of False (`#11422 + <https://github.com/coq/coq/pull/11422>`_, by Gaëtan Gilbert). + +**Specification language, type inference** + +- **Changed:** Heuristics for universe minimization to :g:`Set`: only + minimize flexible universes (`#10657 <https://github.com/coq/coq/pull/10657>`_, + by Gaëtan Gilbert with help from Maxime Dénès and Matthieu Sozeau). +- **Fixed:** + A dependency was missing when looking for default clauses in the + algorithm for printing pattern matching clauses (`#11233 + <https://github.com/coq/coq/pull/11233>`_, by Hugo Herbelin, fixing + `#11231 <https://github.com/coq/coq/pull/11231>`_, reported by Barry + Jay). + +**Notations** + +- **Fixed:** + :cmd:`Print Visibility` was failing in the presence of only-printing notations + (`#11276 <https://github.com/coq/coq/pull/11276>`_, + by Hugo Herbelin, fixing `#10750 <https://github.com/coq/coq/pull/10750>`_). +- **Fixed:** + Recursive notations with custom entries were incorrectly parsing `constr` + instead of custom grammars (`#11311 <https://github.com/coq/coq/pull/11311>`_ + by Maxime Dénès, fixes `#9532 <https://github.com/coq/coq/pull/9532>`_, + `#9490 <https://github.com/coq/coq/pull/9490>`_). + +**Tactics** + +- **Changed:** + The tactics :tacn:`eapply`, :tacn:`refine` and variants no + longer allow shelved goals to be solved by typeclass resolution + (`#10762 <https://github.com/coq/coq/pull/10762>`_, by Matthieu Sozeau). +- **Fixed:** The optional string argument to :tacn:`time` is now + properly quoted under :cmd:`Print Ltac` (`#11203 + <https://github.com/coq/coq/pull/11203>`_, fixes `#10971 + <https://github.com/coq/coq/issues/10971>`_, by Jason Gross) +- **Fixed:** + Efficiency regression of :tacn:`lia` introduced in 8.10 + by PR `#9725 <https://github.com/coq/coq/pull/9725>`_ + (`#11263 <https://github.com/coq/coq/pull/11263>`_, + fixes `#11063 <https://github.com/coq/coq/issues/11063>`_, + and `#11242 <https://github.com/coq/coq/issues/11242>`_, + and `#11270 <https://github.com/coq/coq/issues/11270>`_, by Frédéric Besson). +- **Deprecated:** + The undocumented ``omega with`` tactic variant has been deprecated. + Using :tacn:`lia` is the recommended replacement, though the old semantics + of ``omega with *`` can be recovered with ``zify; omega`` + (`#11337 <https://github.com/coq/coq/pull/11337>`_, + by Emilio Jesus Gallego Arias). +- **Fixed** + For compatibility reasons, in 8.11, :tacn:`zify` does not support :g:`Z.pow_pos` by default. + It can be enabled by explicitly loading the module :g:`ZifyPow` + (`#11430 <https://github.com/coq/coq/pull/11430>`_ by Frédéric Besson + fixes `#11191 <https://github.com/coq/coq/issues/11191>`_). + +**Tactic language** + +- **Fixed:** + Syntax of tactic `cofix ... with ...` was broken since Coq 8.10 + (`#11241 <https://github.com/coq/coq/pull/11241>`_, + by Hugo Herbelin). + +**Commands and options** + +- **Deprecated:** The `-load-ml-source` and `-load-ml-object` command + line options have been deprecated; their use was very limited, you + can achieve the same by adding object files in the linking step or + by using a plugin (`#11428 + <https://github.com/coq/coq/pull/11428>`_, by Emilio Jesus Gallego + Arias). + +**Tools** + +- **Fixed:** + ``coqtop --version`` was broken when called in the middle of an installation process + (`#11255 <https://github.com/coq/coq/pull/11255>`_, by Hugo Herbelin, fixing + `#11254 <https://github.com/coq/coq/pull/11254>`_). +- **Deprecated:** The ``-quick`` command is renamed to ``-vio``, for + consistency with the new ``-vos`` and ``-vok`` flags. Usage of + ``-quick`` is now deprecated (`#11280 + <https://github.com/coq/coq/pull/11280>`_, by Arthur Charguéraud). +- **Fixed:** + ``coq_makefile`` does not break when using the ``CAMLPKGS`` variable + together with an unpacked (``mllib``) plugin (`#11357 + <https://github.com/coq/coq/pull/11357>`_, by Gaëtan Gilbert). +- **Fixed:** + ``coqdoc`` with option ``-g`` (Gallina only) now correctly prints + commands with attributes (`#11394 <https://github.com/coq/coq/pull/11394>`_, + fixes `#11353 <https://github.com/coq/coq/issues/11353>`_, + by Karl Palmskog). + +**CoqIDE** + +- **Changed:** CoqIDE now uses the GtkSourceView native implementation + of the autocomplete mechanism (`#11400 + <https://github.com/coq/coq/pull/11400>`_, by Pierre-Marie Pédrot). + +**Standard library** + +- **Removed:** Export of module :g:`RList` in :g:`Ranalysis` and + :g:`Ranalysis_reg`. Module :g:`RList` is still there but must be + imported explicitly where required (`#11396 + <https://github.com/coq/coq/pull/11396>`_, by Michael Soegtrop). + +**Infrastructure and dependencies** + +- **Added:** + Build date can now be overridden by setting the `SOURCE_DATE_EPOCH` + environment variable + (`#11227 <https://github.com/coq/coq/pull/11227>`_, + by Bernhard M. Wiedemann). + Version 8.10 ------------ @@ -554,7 +685,7 @@ reference manual. Here are the most important user-visible changes: - Universes: - - Added :cmd:`Print Universes Subgraph` variant of :cmd:`Print Universes`. + - Added Subgraph variant to :cmd:`Print Universes`. Try for instance :g:`Print Universes Subgraph(sigT2.u1 sigT_of_sigT2.u1 projT3_eq.u1).` (`#8451 <https://github.com/coq/coq/pull/8451>`_, by Gaëtan Gilbert). @@ -1185,7 +1316,7 @@ Changes in 8.10+beta3 rules governing template-polymorphic types. To help users incrementally fix this issue, a command line option - `-no-template-check` and a global flag :flag:`Template Check` are + `-no-template-check` and a global flag ``Template Check`` are available to selectively disable the new check. Use at your own risk. (`#9918 <https://github.com/coq/coq/pull/9918>`_, by Matthieu Sozeau @@ -1377,7 +1508,7 @@ changes: - Removed deprecated commands ``Arguments Scope`` and ``Implicit Arguments`` in favor of :cmd:`Arguments (scopes)` and - :cmd:`Arguments (implicits)`, with the help of Jasper Hugunin. + :cmd:`Arguments`, with the help of Jasper Hugunin. - New flag :flag:`Uniform Inductive Parameters` by Jasper Hugunin to avoid repeating uniform parameters in constructor declarations. @@ -4584,7 +4715,7 @@ Specification language Module system -- Include Type is now deprecated since Include now accept both modules and +- Include Type is now deprecated since Include now accepts both modules and module types. - Declare ML Module supports Local option. - The sharing between non-logical object and the management of the |