From 0ce7fbb5550ad7a3acc7e06fe9d9bcc24e14ac70 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 8 Jan 2020 14:21:13 +0100 Subject: Changelog for 8.11.0. --- ...1361-fix-11360-discharge-template-param-var.rst | 4 -- .../10657-minim-toset-flex.rst | 3 - ...ing-variable-pattern-matching-decompilation.rst | 6 -- .../03-notations/11276-master+fix10750.rst | 4 -- .../11311-custom-entries-recursive.rst | 5 -- .../04-tactics/10762-notypeclasses-refine.rst | 4 -- .../04-tactics/11203-fix-time-printing.rst | 4 -- doc/changelog/04-tactics/11263-micromega-fix.rst | 6 -- doc/changelog/04-tactics/11337-omega-with-depr.rst | 6 -- .../11241-master+bug-cofix-with-8.10.rst | 4 -- .../11255-master+fix11254-coqtop-version.rst | 4 -- doc/changelog/08-tools/11357-master.rst | 4 -- .../11227-date.rst | 5 -- doc/sphinx/changes.rst | 83 ++++++++++++++++++++++ 14 files changed, 83 insertions(+), 59 deletions(-) delete mode 100644 doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst delete mode 100644 doc/changelog/02-specification-language/10657-minim-toset-flex.rst delete mode 100644 doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst delete mode 100644 doc/changelog/03-notations/11276-master+fix10750.rst delete mode 100644 doc/changelog/03-notations/11311-custom-entries-recursive.rst delete mode 100644 doc/changelog/04-tactics/10762-notypeclasses-refine.rst delete mode 100644 doc/changelog/04-tactics/11203-fix-time-printing.rst delete mode 100644 doc/changelog/04-tactics/11263-micromega-fix.rst delete mode 100644 doc/changelog/04-tactics/11337-omega-with-depr.rst delete mode 100644 doc/changelog/05-tactic-language/11241-master+bug-cofix-with-8.10.rst delete mode 100644 doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst delete mode 100644 doc/changelog/08-tools/11357-master.rst delete mode 100644 doc/changelog/11-infrastructure-and-dependencies/11227-date.rst 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 `_ - Broken section closing when a template polymorphic inductive type depends on - a section variable through its parameters (`#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 `_, - 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 - `_, by Hugo Herbelin, fixing - `#11231 `_, reported by Barry - Jay). 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 `_, - by Hugo Herbelin, fixing `#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 `_ - by Maxime Dénès, fixes `#9532 `_, - `#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 `_, 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 - `_, fixes `#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 `_. - (`#11263 `_, - fixes `#11063 `_, - and `#11242 `_, - and `#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 `_, - by Emilio Jesus Gallego Arias). 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 `_, - by Hugo Herbelin). 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 `_, by Hugo Herbelin, fixing - `#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 - `_, 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 `_, - by Bernhard M. Wiedemann). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 21000889d3..a1410b0412 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -514,6 +514,89 @@ Changes in 8.11+beta1 (`#10471 `_, by Emilio Jesús Gallego Arias). +Changes in 8.11.0 +~~~~~~~~~~~~~~~~~ + +**Kernel** + +- **Fixed:** `#11360 `_. + Broken section closing when a template polymorphic inductive type depends on + a section variable through its parameters (`#11361 + `_, by Gaëtan Gilbert). + +**Specification language, type inference** + +- **Changed:** Heuristics for universe minimization to :g:`Set`: only + minimize flexible universes (`#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 + `_, by Hugo Herbelin, fixing + `#11231 `_, reported by Barry + Jay). + +**Notations** + +- **Fixed:** + :cmd:`Print Visibility` was failing in the presence of only-printing notations + (`#11276 `_, + by Hugo Herbelin, fixing `#10750 `_). +- **Fixed:** + Recursive notations with custom entries were incorrectly parsing `constr` + instead of custom grammars (`#11311 `_ + by Maxime Dénès, fixes `#9532 `_, + `#9490 `_). + +**Tactics** + +- **Changed:** + The tactics :tacn:`eapply`, :tacn:`refine` and variants no + longer allow shelved goals to be solved by typeclass resolution + (`#10762 `_, by Matthieu Sozeau). +- **Fixed:** The optional string argument to :tacn:`time` is now + properly quoted under :cmd:`Print Ltac` (`#11203 + `_, fixes `#10971 + `_, by Jason Gross) +- **Fixed:** + Efficiency regression introduced by PR `#9725 `_ + (`#11263 `_, + fixes `#11063 `_, + and `#11242 `_, + and `#11270 `_, by Frédéric Besson). +- **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 `_, + by Emilio Jesus Gallego Arias). + +**Tactic language** + +- **Fixed:** + Syntax of tactic `cofix ... with ...` was broken from Coq 8.10. + (`#11241 `_, + by Hugo Herbelin). + +**Tools** + +- **Fixed:** + ``coqtop --version`` was broken when called in the middle of an installation process + (`#11255 `_, by Hugo Herbelin, fixing + `#11254 `_). +- **Fixed:** + ``coq_makefile`` does not break when using the ``CAMLPKGS`` variable + together with an unpacked (``mllib``) plugin. (`#11357 + `_, by Gaëtan Gilbert). + +**Infrastructure and dependencies** + +- **Added:** + Build date can now be overriden by setting the `SOURCE_DATE_EPOCH` + environment variable + (`#11227 `_, + by Bernhard M. Wiedemann). + Version 8.10 ------------ -- cgit v1.2.3 From e976070889c81d833dcdd36b760745dc924698aa Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 14 Jan 2020 14:07:56 +0100 Subject: A few edits to the 8.11 section of the Changes chapter. - Mention Guillaume Claret among maintainers of the OPAM repository (as suggested by Karl Palmskog). - Update links to the documentation to avoid being outdated. - Mention sections beyond the one on 8.11+beta1. --- doc/sphinx/changes.rst | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index a1410b0412..d1ffb4bbdb 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -55,23 +55,23 @@ 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 `). -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**. +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**. 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. -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). 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, 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 -- cgit v1.2.3 From 2b908101ab93303b20a41e9b69a5549109ec4603 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 22 Jan 2020 17:18:20 +0100 Subject: Move new entries in 8.11.0 changelog. --- doc/changelog/01-kernel/11081-native-cleanup.rst | 4 --- doc/changelog/01-kernel/11422-Setplus2.rst | 4 --- .../11428-mltop+depr_lowlevel_dynloads.rst | 6 ---- .../11280-bugfix-11195-vos-vio-interaction.rst | 4 --- .../08-tools/11394-fix-coqdoc-annotations.rst | 5 --- .../09-coqide/11400-gtk-ide-completion.rst | 5 --- .../11396-issue_11396_Rlist.rst | 4 --- doc/sphinx/changes.rst | 40 +++++++++++++++++++++- 8 files changed, 39 insertions(+), 33 deletions(-) delete mode 100644 doc/changelog/01-kernel/11081-native-cleanup.rst delete mode 100644 doc/changelog/01-kernel/11422-Setplus2.rst delete mode 100644 doc/changelog/07-commands-and-options/11428-mltop+depr_lowlevel_dynloads.rst delete mode 100644 doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst delete mode 100644 doc/changelog/08-tools/11394-fix-coqdoc-annotations.rst delete mode 100644 doc/changelog/09-coqide/11400-gtk-ide-completion.rst delete mode 100644 doc/changelog/10-standard-library/11396-issue_11396_Rlist.rst diff --git a/doc/changelog/01-kernel/11081-native-cleanup.rst b/doc/changelog/01-kernel/11081-native-cleanup.rst deleted file mode 100644 index b3e3a78b96..0000000000 --- a/doc/changelog/01-kernel/11081-native-cleanup.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **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 - `_, by Gaëtan Gilbert). diff --git a/doc/changelog/01-kernel/11422-Setplus2.rst b/doc/changelog/01-kernel/11422-Setplus2.rst deleted file mode 100644 index cc174358cc..0000000000 --- a/doc/changelog/01-kernel/11422-Setplus2.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - The type of :g:`Set+1` would be computed to be itself, leading to a proof of False. - (`#11422 `_, - by Gaëtan Gilbert). diff --git a/doc/changelog/07-commands-and-options/11428-mltop+depr_lowlevel_dynloads.rst b/doc/changelog/07-commands-and-options/11428-mltop+depr_lowlevel_dynloads.rst deleted file mode 100644 index a43e950bff..0000000000 --- a/doc/changelog/07-commands-and-options/11428-mltop+depr_lowlevel_dynloads.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **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 adding - additional object files in the linking step or by using a plugin. - (`#11428 `_, - by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst b/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst deleted file mode 100644 index 97f456036d..0000000000 --- a/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Deprecated:** - The ``-quick`` command is renamed to ``-vio``, for consistency with the new ``-vos`` and ``-vok`` flags. Usage of ``-quick`` is now deprecated. - (`#11280 `_, - by charguer). diff --git a/doc/changelog/08-tools/11394-fix-coqdoc-annotations.rst b/doc/changelog/08-tools/11394-fix-coqdoc-annotations.rst deleted file mode 100644 index 10952c6b2c..0000000000 --- a/doc/changelog/08-tools/11394-fix-coqdoc-annotations.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - ``coqdoc`` with option ``-g`` (Gallina only) now correctly prints - commands with attributes (`#11394 `_, - fixes `#11353 `_, - by Karl Palmskog). diff --git a/doc/changelog/09-coqide/11400-gtk-ide-completion.rst b/doc/changelog/09-coqide/11400-gtk-ide-completion.rst deleted file mode 100644 index 2dc3992b9c..0000000000 --- a/doc/changelog/09-coqide/11400-gtk-ide-completion.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - CoqIDE now uses the GtkSourceView native implementation of - the autocomplete mechanism. - (`#11400 `_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/10-standard-library/11396-issue_11396_Rlist.rst b/doc/changelog/10-standard-library/11396-issue_11396_Rlist.rst deleted file mode 100644 index 3e1f1e02a4..0000000000 --- a/doc/changelog/10-standard-library/11396-issue_11396_Rlist.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Removed:** - Export of module ``RList`` in ``Ranalysis.v`` and ``Ranalysis_reg.v``. Module ``RList`` is still there but must be imported explicitly where required. - (`#11396 `_, - by Michael Soegtrop). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index d1ffb4bbdb..473015dea0 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -519,10 +519,17 @@ 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 + `_, by Gaëtan Gilbert). - **Fixed:** `#11360 `_. Broken section closing when a template polymorphic inductive type depends on a section variable through its parameters (`#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 + `_, by Gaëtan Gilbert). **Specification language, type inference** @@ -574,20 +581,51 @@ Changes in 8.11.0 **Tactic language** - **Fixed:** - Syntax of tactic `cofix ... with ...` was broken from Coq 8.10. + Syntax of tactic `cofix ... with ...` was broken from Coq 8.10 (`#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 + `_, by Emilio Jesus Gallego + Arias). + **Tools** - **Fixed:** ``coqtop --version`` was broken when called in the middle of an installation process (`#11255 `_, by Hugo Herbelin, fixing `#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 + `_, by Arthur Charguéraud). - **Fixed:** ``coq_makefile`` does not break when using the ``CAMLPKGS`` variable together with an unpacked (``mllib``) plugin. (`#11357 `_, by Gaëtan Gilbert). +- **Fixed:** + ``coqdoc`` with option ``-g`` (Gallina only) now correctly prints + commands with attributes (`#11394 `_, + fixes `#11353 `_, + by Karl Palmskog). + +**CoqIDE** + +- **Changed:** CoqIDE now uses the GtkSourceView native implementation + of the autocomplete mechanism (`#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 + `_, by Michael Soegtrop). **Infrastructure and dependencies** -- cgit v1.2.3 From 68421494cbd8d9e2bc8ab2482ee6f34a057b157a Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 22 Jan 2020 17:31:19 +0100 Subject: Insert changelog entry for #11430 from v8.11 branch. --- doc/sphinx/changes.rst | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 473015dea0..294f121cf8 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -573,10 +573,15 @@ Changes in 8.11.0 and `#11270 `_, by Frédéric Besson). - **Deprecated:** The undocumented ``omega with`` tactic variant has been deprecated. - Using ``lia`` is the recommended replacement, tho the old semantics + Using :tacn:`lia` is the recommended replacement, tho the old semantics of ``omega with *`` can be recovered with ``zify; omega`` (`#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 loading explicitly the module :g:`ZifyPow`. + (`#11430 `_ by Frédéric Besson + fixes `#11191 `_). **Tactic language** -- cgit v1.2.3