diff options
Diffstat (limited to 'doc')
33 files changed, 314 insertions, 87 deletions
diff --git a/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst b/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst deleted file mode 100644 index 8c84648aa7..0000000000 --- a/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **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). diff --git a/doc/changelog/02-specification-language/10657-minim-toset-flex.rst b/doc/changelog/02-specification-language/10657-minim-toset-flex.rst deleted file mode 100644 index 8983e162fb..0000000000 --- a/doc/changelog/02-specification-language/10657-minim-toset-flex.rst +++ /dev/null @@ -1,3 +0,0 @@ -- 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). diff --git a/doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst b/doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst deleted file mode 100644 index 941469d698..0000000000 --- a/doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **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). diff --git a/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst b/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst new file mode 100644 index 0000000000..a7ffde31fc --- /dev/null +++ b/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst @@ -0,0 +1,6 @@ +- **Changed:** + The warning raised when a trailing implicit is declared to be non maximally + inserted (with the command cmd:`Arguments <Arguments (implicits)>`) has been turned into an error. + This was deprecated since Coq 8.10. + (`#11368 <https://github.com/coq/coq/pull/11368>`_, + by SimonBoulier). diff --git a/doc/changelog/03-notations/11276-master+fix10750.rst b/doc/changelog/03-notations/11276-master+fix10750.rst deleted file mode 100644 index a1b8594f5f..0000000000 --- a/doc/changelog/03-notations/11276-master+fix10750.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **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>`_). diff --git a/doc/changelog/03-notations/11311-custom-entries-recursive.rst b/doc/changelog/03-notations/11311-custom-entries-recursive.rst deleted file mode 100644 index ae9888512d..0000000000 --- a/doc/changelog/03-notations/11311-custom-entries-recursive.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **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>`_). diff --git a/doc/changelog/04-tactics/10762-notypeclasses-refine.rst b/doc/changelog/04-tactics/10762-notypeclasses-refine.rst deleted file mode 100644 index 2fef75dc7f..0000000000 --- a/doc/changelog/04-tactics/10762-notypeclasses-refine.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - The tactics :tacn:`eapply`, :tacn:`refine` and its variants no - longer allows shelved goals to be solved by typeclass resolution. - (`#10762 <https://github.com/coq/coq/pull/10762>`_, by Matthieu Sozeau). diff --git a/doc/changelog/04-tactics/11203-fix-time-printing.rst b/doc/changelog/04-tactics/11203-fix-time-printing.rst deleted file mode 100644 index cdfd2b228e..0000000000 --- a/doc/changelog/04-tactics/11203-fix-time-printing.rst +++ /dev/null @@ -1,4 +0,0 @@ -- 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) diff --git a/doc/changelog/04-tactics/11263-micromega-fix.rst b/doc/changelog/04-tactics/11263-micromega-fix.rst deleted file mode 100644 index ebfb6c19b1..0000000000 --- a/doc/changelog/04-tactics/11263-micromega-fix.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed** - Efficiency regression introduced 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). diff --git a/doc/changelog/04-tactics/11337-omega-with-depr.rst b/doc/changelog/04-tactics/11337-omega-with-depr.rst deleted file mode 100644 index 25e929e030..0000000000 --- a/doc/changelog/04-tactics/11337-omega-with-depr.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Deprecated:** - The undocumented ``omega with`` tactic variant has been deprecated, - using ``lia`` is the recommended replacement, tho 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). diff --git a/doc/changelog/04-tactics/11362-micromega-fix-11191.rst b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst new file mode 100644 index 0000000000..5ecd46bced --- /dev/null +++ b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Regression of ``lia`` due to more powerful ``zify`` + (`#11362 <https://github.com/coq/coq/pull/11362>`_, + fixes `#11191 <https://github.com/coq/coq/issues/11191>`_, + by Frédéric Besson). diff --git a/doc/changelog/04-tactics/11370-zify-elim-let.rst b/doc/changelog/04-tactics/11370-zify-elim-let.rst new file mode 100644 index 0000000000..4eb2732106 --- /dev/null +++ b/doc/changelog/04-tactics/11370-zify-elim-let.rst @@ -0,0 +1,3 @@ +- **Changed** + Improve the efficiency of `PreOmega.elim_let` using an iterator implemented in OCaml. + (`#11370 <https://github.com/coq/coq/pull/11370>`_, by Frédéric Besson). diff --git a/doc/changelog/05-tactic-language/11241-master+bug-cofix-with-8.10.rst b/doc/changelog/05-tactic-language/11241-master+bug-cofix-with-8.10.rst deleted file mode 100644 index 462ba4a7b1..0000000000 --- a/doc/changelog/05-tactic-language/11241-master+bug-cofix-with-8.10.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - Syntax of tactic `cofix ... with ...` was broken from Coq 8.10. - (`#11241 <https://github.com/coq/coq/pull/11241>`_, - by Hugo Herbelin). diff --git a/doc/changelog/07-commands-and-options/11164-let-cs.rst b/doc/changelog/07-commands-and-options/11164-let-cs.rst new file mode 100644 index 0000000000..b9ecd140e7 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11164-let-cs.rst @@ -0,0 +1 @@ +- A section variable introduces with :g:`Let` can be declared as a :g:`Canonical Structure` (`#11164 <https://github.com/coq/coq/pull/11164>`_, by Enrico Tassi). diff --git a/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst b/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst deleted file mode 100644 index ecc134748d..0000000000 --- a/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **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>`_). diff --git a/doc/changelog/08-tools/11357-master.rst b/doc/changelog/08-tools/11357-master.rst deleted file mode 100644 index 599db5b1da..0000000000 --- a/doc/changelog/08-tools/11357-master.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **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). diff --git a/doc/changelog/11-infrastructure-and-dependencies/11227-date.rst b/doc/changelog/11-infrastructure-and-dependencies/11227-date.rst deleted file mode 100644 index 5c08e2b0ea..0000000000 --- a/doc/changelog/11-infrastructure-and-dependencies/11227-date.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Build date can now be overriden by setting the `SOURCE_DATE_EPOCH` - environment variable - (`#11227 <https://github.com/coq/coq/pull/11227>`_, - by Bernhard M. Wiedemann). diff --git a/doc/changelog/12-misc/10486-native-string-extraction.rst b/doc/changelog/12-misc/10486-native-string-extraction.rst new file mode 100644 index 0000000000..c6778403d4 --- /dev/null +++ b/doc/changelog/12-misc/10486-native-string-extraction.rst @@ -0,0 +1,7 @@ +- **Added:** + Support for better extraction of strings in OCaml and Haskell: + `ExtOcamlNativeString` provides bindings from the Coq `String` type to + the OCaml `string` type, and string literals can be extracted to literals, + both in OCaml and Haskell. (`#10486 + <https://github.com/coq/coq/pull/10486>`_, by Xavier Leroy, with help from + Maxime Dénès, review by Hugo Herbelin). diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index 7136cc28d1..d909f98956 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -313,14 +313,21 @@ The system also provides a mechanism to specify ML terms for inductive types and constructors. For instance, the user may want to use the ML native boolean type instead of the |Coq| one. The syntax is the following: -.. cmd:: Extract Inductive @qualid => @string [ {+ @string } ] +.. cmd:: Extract Inductive @qualid => @string__1 [ {+ @string } ] Give an ML extraction for the given inductive type. You must specify - extractions for the type itself (first :token:`string`) and all its - constructors (all the :token:`string` between square brackets). In this form, + extractions for the type itself (:n:`@string__1`) and all its + constructors (all the :n:`@string` between square brackets). In this form, the ML extraction must be an ML inductive datatype, and the native pattern matching of the language will be used. + When :n:`@string__1` matches the name of the type of characters or strings + (``char`` and ``string`` for OCaml, ``Prelude.Char`` and ``Prelude.String`` + for Haskell), extraction of literals is handled in a specialized way, so as + to generate literals in the target language. This feature requires the type + designated by :n:`@qualid` to be registered as the standard char or string type, + using the :cmd:`Register` command. + .. cmdv:: Extract Inductive @qualid => @string [ {+ @string } ] @string Same as before, with a final extra :token:`string` that indicates how to diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 650a444a16..daca43e65e 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -5,6 +5,27 @@ Omega: a solver for quantifier-free problems in Presburger Arithmetic :Author: Pierre Crégut +.. warning:: + + The :tacn:`omega` tactic is about to be deprecated in favor of the + :tacn:`lia` tactic. The goal is to consolidate the arithmetic + solving capabilities of Coq into a single engine; moreover, + :tacn:`lia` is in general more powerful than :tacn:`omega` (it is a + complete Presburger arithmetic solver while :tacn:`omega` was known + to be incomplete). + + Work is in progress to make sure that there are no regressions + (including no performance regression) when switching from + :tacn:`omega` to :tacn:`lia` in existing projects. However, we + already recommend using :tacn:`lia` in new or refactored proof + scripts. We also ask that you report (in our `bug tracker + <https://github.com/coq/coq/issues>`_) any issue you encounter, + especially if the issue was not present in :tacn:`omega`. + + Note that replacing :tacn:`omega` with :tacn:`lia` can break + non-robust proof scripts which rely on incompleteness bugs of + :tacn:`omega` (e.g. using the pattern :g:`; try omega`). + Description of ``omega`` ------------------------ diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index 35729d852d..7a50748c51 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -154,6 +154,18 @@ to a worker process. The threshold can be configured with Batch mode --------------- + .. warning:: + + The ``-vio`` flag is subsumed, for most practical usage, by the + the more recent ``-vos`` flag. See :ref:`compiled-interfaces`. + + .. warning:: + + When working with ``.vio`` files, do not use the ``-vos`` option at + the same time, otherwise stale files might get loaded when executing + a ``Require``. Indeed, the loading of a nonempty ``.vos`` file is + assigned higher priority than the loading of a ``.vio`` file. + When |Coq| is used as a batch compiler by running ``coqc``, it produces a ``.vo`` file for each ``.v`` file. A ``.vo`` file contains, among other things, theorem statements and proofs. Hence to produce a .vo |Coq| @@ -161,10 +173,10 @@ need to process all the proofs of the ``.v`` file. The asynchronous processing of proofs can decouple the generation of a compiled file (like the ``.vo`` one) that can be loaded by ``Require`` from the -generation and checking of the proof objects. The ``-quick`` flag can be +generation and checking of the proof objects. The ``-vio`` flag can be passed to ``coqc`` to produce, quickly, ``.vio`` files. Alternatively, when using a Makefile produced by ``coq_makefile``, -the ``quick`` target can be used to compile all files using the ``-quick`` flag. +the ``vio`` target can be used to compile all files using the ``-vio`` flag. A ``.vio`` file can be loaded using ``Require`` exactly as a ``.vo`` file but proofs will not be available (the Print command produces an error). @@ -173,7 +185,7 @@ inconsistencies might go unnoticed. A ``.vio`` file does not contain proof objects, but proof tasks, i.e. what a worker process can transform into a proof object. -Compiling a set of files with the ``-quick`` flag allows one to work, +Compiling a set of files with the ``-vio`` flag allows one to work, interactively, on any file without waiting for all the proofs to be checked. diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 7adb25cbd6..f9cc25959c 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -529,8 +529,8 @@ sections, except in the following ways: Polymorphic Universe i. Fail Constraint i = i. - This includes constraints implictly declared by commands such as - :cmd:`Variable`, which may as a such need to be used with universe + This includes constraints implicitly declared by commands such as + :cmd:`Variable`, which may need to be used with universe polymorphism activated (locally by attribute or globally by option): .. coqtop:: all diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 33fc211fa5..6d9979a704 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -50,23 +50,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>`). + +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/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, Théo Zimmermann worked on maintaining and improving the +Soegtrop and Théo Zimmermann worked on maintaining and improving the continuous integration system and package building infrastructure. -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 -the standard library). - 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 @@ -509,6 +514,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 ------------ diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index e746096df2..510e271951 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1728,11 +1728,11 @@ Declaring Implicit Arguments To know which are the implicit arguments of an object, use the command :cmd:`Print Implicit` (see :ref:`displaying-implicit-args`). -.. warn:: Argument number @num is a trailing implicit so must be maximal. +.. exn:: Argument @ident is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. For instance in - .. coqtop:: all warn + .. coqtop:: all fail Arguments prod _ [_]. @@ -1983,6 +1983,8 @@ Deactivation of implicit arguments for parsing to be given as if no arguments were implicit. By symmetry, this also affects printing. +.. _canonical-structure-declaration: + Canonical structures ~~~~~~~~~~~~~~~~~~~~ @@ -1993,6 +1995,7 @@ value. The complete documentation of canonical structures can be found in :ref:`canonicalstructures`; here only a simple example is given. .. cmd:: {? Local | #[local] } Canonical {? Structure } @qualid + :name: Canonical Structure This command declares :token:`qualid` as a canonical instance of a structure (a record). When the :g:`#[local]` attribute is given the effect diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 70dadedd35..d591718b17 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1620,6 +1620,17 @@ variety of commands: :n:`@string__1` is the actual notation, :n:`@string__2` is the version number, :n:`@string__3` is the note. +``canonical`` + This attribute can decorate a :cmd:`Definition` or :cmd:`Let` command. + It is equivalent to having a :cmd:`Canonical Structure` declaration just + after the command. + + This attirbute can take the value ``false`` when decorating a record field + declaration with the effect of preventing the field from being involved in + the inference of canonical instances. + + See also :ref:`canonical-structure-declaration`. + .. example:: .. coqtop:: all reset warn diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index d4a61425e1..ba43128bdc 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -253,6 +253,7 @@ and ``coqtop``, unless stated otherwise: :-h, --help: Print a short usage and exit. +.. _compiled-interfaces: Compiled interfaces (produced using ``-vos``) ---------------------------------------------- diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index dd80b29bda..b722b1af74 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -940,6 +940,13 @@ below will fail immediately and won't print anything. In any case, the value returned by the fully applied quotation is an unspecified dummy Ltac1 closure and should not be further used. +Switching between Ltac languages +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +We recommend using the :opt:`Default Proof Mode` option to switch between tactic +languages with a proof-based granularity. This allows to incrementally port +the proof scripts. + Transition from Ltac1 --------------------- diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 6884b6e998..b1734b3f19 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -265,6 +265,35 @@ Name a set of section hypotheses for ``Proof using`` has remaining uninstantiated existential variables. It takes every uninstantiated existential variable and turns it into a goal. +Proof modes +``````````` + +When entering proof mode through commands such as :cmd:`Goal` and :cmd:`Proof`, +|Coq| picks by default the |Ltac| mode. Nonetheless, there exist other proof modes +shipped in the standard |Coq| installation, and furthermore some plugins define +their own proof modes. The default proof mode used when opening a proof can +be changed using the following option. + +.. opt:: Default Proof Mode @string + :name: Default Proof Mode + + Select the proof mode to use when starting a proof. Depending on the proof + mode, various syntactic constructs are allowed when writing an interactive + proof. The possible option values are listed below. + + - "Classic": this is the default. It activates the |Ltac| language to interact + with the proof, and also allows vernacular commands. + + - "Noedit": this proof mode only allows vernacular commands. No tactic + language is activated at all. This is the default when the prelude is not + loaded, e.g. through the `-noinit` option for `coqc`. + + - "Ltac2": this proof mode is made available when requiring the Ltac2 + library, and is set to be the default when it is imported. It allows + to use the Ltac2 language, as well as vernacular commands. + + - Some external plugins also define their own proof mode, which can be + activated via this command. Navigation in the proof tree -------------------------------- @@ -490,6 +519,13 @@ The following example script illustrates all these features: You just finished a goal focused by ``{``, you must unfocus it with ``}``. +Mandatory Bullets +````````````````` + +Using :opt:`Default Goal Selector` with the ``!`` selector forces +tactic scripts to keep focus to exactly one goal (e.g. using bullets) +or use explicit goal selectors. + Set Bullet Behavior ``````````````````` .. opt:: Bullet Behavior {| "None" | "Strict Subproofs" } diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 89b24ea8a3..a38c26c2b3 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1200,7 +1200,7 @@ Controlling the locality of commands + Commands whose default behavior is to extend their effect outside sections but not outside modules when they occur in a section and to extend their effect outside the module or library file they occur in - when no section contains them.For these commands, the Local modifier + when no section contains them. For these commands, the Local modifier limits the effect to the current section or module while the Global modifier extends the effect outside the module even when the command occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this diff --git a/doc/stdlib/dune b/doc/stdlib/dune index 7fe2493fbf..828caecabc 100644 --- a/doc/stdlib/dune +++ b/doc/stdlib/dune @@ -5,7 +5,8 @@ (deps make-library-index index-list.html.template hidden-files (source_tree %{project_root}/theories) - (source_tree %{project_root}/plugins)) + (source_tree %{project_root}/plugins) + (source_tree %{project_root}/user-contrib)) (action (chdir %{project_root} ; On windows run will fail @@ -17,6 +18,7 @@ ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg (source_tree %{project_root}/theories) (source_tree %{project_root}/plugins) + (source_tree %{project_root}/user-contrib) (:header %{project_root}/doc/common/styles/html/coqremote/header.html) (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html) ; For .glob files, should be gone when Coq Dune is smarter. @@ -24,7 +26,7 @@ (action (progn (run mkdir -p html) - (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq $(find %{project_root}/theories %{project_root}/plugins -name *.v)") + (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq -Q %{project_root}/user-contrib/Ltac2 Ltac2 $(find %{project_root}/theories %{project_root}/plugins %{project_root}/user-contrib -name *.v)") (run mv html/index.html html/genindex.html) (with-stdout-to _index.html diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index b816ef6210..dbc3a42ee9 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -12,12 +12,14 @@ plugins/extraction/ExtrHaskellZInteger.v plugins/extraction/ExtrHaskellZNum.v plugins/extraction/ExtrOcamlBasic.v plugins/extraction/ExtrOcamlBigIntConv.v +plugins/extraction/ExtrOcamlChar.v plugins/extraction/ExtrOCamlInt63.v plugins/extraction/ExtrOCamlFloats.v plugins/extraction/ExtrOcamlIntConv.v plugins/extraction/ExtrOcamlNatBigInt.v plugins/extraction/ExtrOcamlNatInt.v plugins/extraction/ExtrOcamlString.v +plugins/extraction/ExtrOcamlNativeString.v plugins/extraction/ExtrOcamlZBigInt.v plugins/extraction/ExtrOcamlZInt.v plugins/extraction/Extraction.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index ac611926b3..5e13214a1a 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -626,6 +626,31 @@ through the <tt>Require Import</tt> command.</p> plugins/ssr/ssrfun.v </dd> + <dt> <b>Ltac2</b>: + The Ltac2 tactic programming language + </dt> + <dd> + user-contrib/Ltac2/Ltac2.v + user-contrib/Ltac2/Array.v + user-contrib/Ltac2/Bool.v + user-contrib/Ltac2/Char.v + user-contrib/Ltac2/Constr.v + user-contrib/Ltac2/Control.v + user-contrib/Ltac2/Env.v + user-contrib/Ltac2/Fresh.v + user-contrib/Ltac2/Ident.v + user-contrib/Ltac2/Init.v + user-contrib/Ltac2/Int.v + user-contrib/Ltac2/List.v + user-contrib/Ltac2/Ltac1.v + user-contrib/Ltac2/Message.v + user-contrib/Ltac2/Notations.v + user-contrib/Ltac2/Option.v + user-contrib/Ltac2/Pattern.v + user-contrib/Ltac2/Std.v + user-contrib/Ltac2/String.v + </dd> + <dt> <b>Unicode</b>: Unicode-based notations </dt> diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index index bea6f24098..732f15b78a 100755 --- a/doc/stdlib/make-library-index +++ b/doc/stdlib/make-library-index @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash # Instantiate links to library files in index template @@ -8,9 +8,14 @@ HIDDEN=$2 cp -f $FILE.template tmp echo -n "Building file index-list.prehtml... " -LIBDIRS=`find theories/* plugins/* -type d ! -name .coq-native` +LIBDIRS=`find theories/* plugins/* user-contrib/* -type d ! -name .coq-native` for k in $LIBDIRS; do + if [[ $k =~ "user-contrib" ]]; then + BASE_PREFIX="" + else + BASE_PREFIX="Coq." + fi d=`basename $k` ls $k | grep -q \.v'$' if [ $? = 0 ]; then @@ -26,7 +31,7 @@ for k in $LIBDIRS; do echo Error: $FILE and $HIDDEN both mention $k/$b.v; exit 1 else p=`echo $k | sed 's:^[^/]*/::' | sed 's:/:.:g'` - sed -e "s:$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2 + sed -e "s:$k/$b.v:<a href=\"$BASE_PREFIX$p.$b.html\">$b</a>:g" tmp > tmp2 mv -f tmp2 tmp fi else |