diff options
Diffstat (limited to 'doc')
36 files changed, 273 insertions, 266 deletions
diff --git a/doc/changelog/04-tactics/13741-remove_omega.rst b/doc/changelog/04-tactics/13741-remove_omega.rst new file mode 100644 index 0000000000..0b25c01958 --- /dev/null +++ b/doc/changelog/04-tactics/13741-remove_omega.rst @@ -0,0 +1,7 @@ +- **Removed:** + Removed the `omega` tactic (deprecated in 8.12) and 4 `* Omega *` flags. + Use `lia` instead. + (`#13741 <https://github.com/coq/coq/pull/13741>`_, + by Jim Fehrle, who addressed the final details, building on much work by + Frédéric Besson, who greatly improved :tacn:`lia`, Maxime Dénès, + Vincent Laporte and with the help of many package maintainers, among others). diff --git a/doc/changelog/04-tactics/14033-fix-14009.rst b/doc/changelog/04-tactics/14033-fix-14009.rst new file mode 100644 index 0000000000..3b58e193cb --- /dev/null +++ b/doc/changelog/04-tactics/14033-fix-14009.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Properly expand projection parameters in hint discrimination + nets. (`#14033 <https://github.com/coq/coq/pull/14033>`_, + fixes `#9000 <https://github.com/coq/coq/issues/9000>`_, + `#14009 <https://github.com/coq/coq/issues/14009>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/04-tactics/14089-ltac2_unify.rst b/doc/changelog/04-tactics/14089-ltac2_unify.rst new file mode 100644 index 0000000000..5887781db9 --- /dev/null +++ b/doc/changelog/04-tactics/14089-ltac2_unify.rst @@ -0,0 +1,5 @@ +- **Added:** + Ltac2 now has a `unify` tactic + (`#14089 <https://github.com/coq/coq/pull/14089>`_, + fixes `#14083 <https://github.com/coq/coq/issues/14083>`_, + by Samuel Gruetter). diff --git a/doc/changelog/05-tactic-language/13939-ltac2-open-constr-scope.rst b/doc/changelog/05-tactic-language/13939-ltac2-open-constr-scope.rst new file mode 100644 index 0000000000..9753ce915b --- /dev/null +++ b/doc/changelog/05-tactic-language/13939-ltac2-open-constr-scope.rst @@ -0,0 +1,5 @@ +- **Added:** + Allow scope delimiters in Ltac2 open_constr:(...) quotation + (`#13939 <https://github.com/coq/coq/pull/13939>`_, + fixes `#12806 <https://github.com/coq/coq/issues/12806>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/05-tactic-language/13997-ltac2-ident-ffi.rst b/doc/changelog/05-tactic-language/13997-ltac2-ident-ffi.rst new file mode 100644 index 0000000000..b5b63455c9 --- /dev/null +++ b/doc/changelog/05-tactic-language/13997-ltac2-ident-ffi.rst @@ -0,0 +1,5 @@ +- **Added:** + Added a FFI to convert between Ltac1 and Ltac2 identifiers + (`#13997 <https://github.com/coq/coq/pull/13997>`_, + fixes `#13996 <https://github.com/coq/coq/issues/13996>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/07-vernac-commands-and-options/14093-fix-14092.rst b/doc/changelog/07-vernac-commands-and-options/14093-fix-14092.rst new file mode 100644 index 0000000000..7831d10392 --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/14093-fix-14092.rst @@ -0,0 +1,6 @@ +- **Added:** + The Ltac2 grammar can now be printed using the + Print Grammar ltac2 command + (`#14093 <https://github.com/coq/coq/pull/14093>`_, + fixes `#14092 <https://github.com/coq/coq/issues/14092>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/08-cli-tools/13624-master+fix13581-extraction-letin-in-ind-arity.rst b/doc/changelog/08-cli-tools/13624-master+fix13581-extraction-letin-in-ind-arity.rst new file mode 100644 index 0000000000..6a34f5a70e --- /dev/null +++ b/doc/changelog/08-cli-tools/13624-master+fix13581-extraction-letin-in-ind-arity.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Failure of extraction in the presence of inductive types with local + definitions in parameters + (`#13624 <https://github.com/coq/coq/pull/13624>`_, + fixes `#13581 <https://github.com/coq/coq/issues/13581>`_, + by Hugo Herbelin). diff --git a/doc/changelog/08-cli-tools/14024-coqdep-errors.rst b/doc/changelog/08-cli-tools/14024-coqdep-errors.rst new file mode 100644 index 0000000000..355c0bd7b7 --- /dev/null +++ b/doc/changelog/08-cli-tools/14024-coqdep-errors.rst @@ -0,0 +1,8 @@ +- **Changed:** + ``coqdep`` now reports an error if files specified on the + command line don't exist or if it encounters unreadable files. + Unknown options now generate a warning. Previously these + conditions were ignored. + (`#14024 <https://github.com/coq/coq/pull/14024>`_, + fixes `#14023 <https://github.com/coq/coq/issues/14023>`_, + by Hendrik Tews). diff --git a/doc/changelog/10-standard-library/13955-List_lemmas1.rst b/doc/changelog/10-standard-library/13955-List_lemmas1.rst new file mode 100644 index 0000000000..73eb9a78d9 --- /dev/null +++ b/doc/changelog/10-standard-library/13955-List_lemmas1.rst @@ -0,0 +1,4 @@ +- **Added:** + Lemmas to ``List``: ``Exists_map``, ``Exists_concat``, ``Exists_flat_map``, ``Forall_map``, ``Forall_concat``, ``Forall_flat_map``, ``nth_error_map``, ``nth_repeat``, ``nth_error_repeat`` + (`#13955 <https://github.com/coq/coq/pull/13955>`_, + by Andrej Dudenhefner, with help from Olivier Laurent). diff --git a/doc/changelog/10-standard-library/13986-clean-List-imports.rst b/doc/changelog/10-standard-library/13986-clean-List-imports.rst new file mode 100644 index 0000000000..02e7b9cc97 --- /dev/null +++ b/doc/changelog/10-standard-library/13986-clean-List-imports.rst @@ -0,0 +1,4 @@ +- **Removed:** + from ``List.v`` deprecated/unexpected dependencies ``Setoid``, ``Le``, ``Gt``, ``Minus``, ``Lt`` + (`#13986 <https://github.com/coq/coq/pull/13986>`_, + by Andrej Dudenhefner). diff --git a/doc/changelog/10-standard-library/14008-Cantor-pairing.rst b/doc/changelog/10-standard-library/14008-Cantor-pairing.rst new file mode 100644 index 0000000000..4c217f3fb0 --- /dev/null +++ b/doc/changelog/10-standard-library/14008-Cantor-pairing.rst @@ -0,0 +1,6 @@ +- **Added:** + ``Cantor.v`` containing the Cantor pairing function and its inverse. + ``Cantor.to_nat : nat * nat -> nat`` and ``Cantor.of_nat : nat -> nat * nat`` + are the respective bijections between ``nat * nat`` and ``nat``. + (`#14008 <https://github.com/coq/coq/pull/14008>`_, + by Andrej Dudenhefner). @@ -63,3 +63,6 @@ (files (refman-html as html/refman) (refman-pdf as pdf/refman)) (section doc) (package coq-doc)) + +(documentation + (package coq-doc)) diff --git a/doc/index.mld b/doc/index.mld new file mode 100644 index 0000000000..3a1979bc62 --- /dev/null +++ b/doc/index.mld @@ -0,0 +1,3 @@ +{0 coq-doc } + +The coq-doc package only contains user documentation on the Coq proof assistant and no OCaml library. diff --git a/doc/sphinx/_static/ansi.css b/doc/sphinx/_static/ansi.css index 2a618f68d2..a4850a738b 100644 --- a/doc/sphinx/_static/ansi.css +++ b/doc/sphinx/_static/ansi.css @@ -69,7 +69,7 @@ } .ansi-fg-white { - color: #2e3436; + color: #ffffff; } .ansi-fg-light-black { diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css index abb08d98cc..e262a9305d 100644 --- a/doc/sphinx/_static/notations.css +++ b/doc/sphinx/_static/notations.css @@ -267,6 +267,11 @@ code span.error { color: inherit !important; } + +.coqdoc-comment { + color: #808080 !important +} + /* make the error message index readable */ .indextable code { white-space: inherit; /* break long lines */ diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 5d471c695c..24e35dd85a 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -159,7 +159,6 @@ and checked to be :math:`-1`. This tactic solves linear goals over :g:`Z` by searching for *linear* refutations and cutting planes. :tacn:`lia` provides support for :g:`Z`, :g:`nat`, :g:`positive` and :g:`N` by pre-processing via the :tacn:`zify` tactic. - High level view of `lia` ~~~~~~~~~~~~~~~~~~~~~~~~ @@ -296,7 +295,7 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. The :tacn:`zify` tactic can be extended with new types and operators by declaring and registering new typeclass instances using the following commands. The typeclass declarations can be found in the module ``ZifyClasses`` and the default instances can be found in the module ``ZifyInst``. -.. cmd:: Add Zify @add_zify @one_term +.. cmd:: Add Zify @add_zify @qualid .. insertprodn add_zify add_zify @@ -305,6 +304,9 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. | {| PropOp | PropBinOp | PropUOp | Saturate } Registers an instance of the specified typeclass. + The typeclass type (e.g. :g:`BinOp Z.mul` or :g:`BinRel (@eq Z)`) has the additional constraint that + the non-implicit argument (here, :g:`Z.mul` or :g:`(@eq Z)`) + is either a :n:`@reference` (here, :g:`Z.mul`) or the application of a :n:`@reference` (here, :g:`@eq`) to a sequence of :n:`@one_term`. .. cmd:: Show Zify @show_zify diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst deleted file mode 100644 index 86bb0502c6..0000000000 --- a/doc/sphinx/addendum/omega.rst +++ /dev/null @@ -1,210 +0,0 @@ -.. _omega_chapter: - -Omega: a (deprecated) solver for arithmetic -===================================================================== - -:Author: Pierre Crégut - -.. warning:: - - The :tacn:`omega` tactic is 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). - - It is recommended to switch from :tacn:`omega` to :tacn:`lia` in existing - projects. 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`. If no new issues are - reported, :tacn:`omega` will be removed soon. - - 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`` ------------------------- - -.. tacn:: omega - - .. deprecated:: 8.12 - - Use :tacn:`lia` instead. - - :tacn:`omega` is a tactic for solving goals in Presburger arithmetic, - i.e. for proving formulas made of equations and inequalities over the - type ``nat`` of natural numbers or the type ``Z`` of binary-encoded integers. - Formulas on ``nat`` are automatically injected into ``Z``. The procedure - may use any hypothesis of the current proof session to solve the goal. - - Multiplication is handled by :tacn:`omega` but only goals where at - least one of the two multiplicands of products is a constant are - solvable. This is the restriction meant by "Presburger arithmetic". - - If the tactic cannot solve the goal, it fails with an error message. - In any case, the computation eventually stops. - -Arithmetical goals recognized by ``omega`` ------------------------------------------- - -:tacn:`omega` applies only to quantifier-free formulas built from the connectives:: - - /\ \/ ~ -> - -on atomic formulas. Atomic formulas are built from the predicates:: - - = < <= > >= - -on ``nat`` or ``Z``. In expressions of type ``nat``, :tacn:`omega` recognizes:: - - + - * S O pred - -and in expressions of type ``Z``, :tacn:`omega` recognizes numeral constants and:: - - + - * Z.succ Z.pred - -All expressions of type ``nat`` or ``Z`` not built on these -operators are considered abstractly as if they -were arbitrary variables of type ``nat`` or ``Z``. - -Messages from ``omega`` ------------------------ - -When :tacn:`omega` does not solve the goal, one of the following errors -is generated: - -.. exn:: omega can't solve this system. - - This may happen if your goal is not quantifier-free (if it is - universally quantified, try :tacn:`intros` first; if it contains - existentials quantifiers too, :tacn:`omega` is not strong enough to solve your - goal). This may happen also if your goal contains arithmetical - operators not recognized by :tacn:`omega`. Finally, your goal may be simply - not true! - -.. exn:: omega: Not a quantifier-free goal. - - If your goal is universally quantified, you should first apply - :tacn:`intro` as many times as needed. - -.. exn:: omega: Unrecognized predicate or connective: @ident. - :undocumented: - -.. exn:: omega: Unrecognized atomic proposition: ... - :undocumented: - -.. exn:: omega: Can't solve a goal with proposition variables. - :undocumented: - -.. exn:: omega: Unrecognized proposition. - :undocumented: - -.. exn:: omega: Can't solve a goal with non-linear products. - :undocumented: - -.. exn:: omega: Can't solve a goal with equality on type ... - :undocumented: - - -Using ``omega`` ---------------- - -The ``omega`` tactic does not belong to the core system. It should be -loaded by - -.. coqtop:: in - - Require Import Omega. - -.. example:: - - .. coqtop:: all warn - - Require Import Omega. - - Open Scope Z_scope. - - Goal forall m n:Z, 1 + 2 * m <> 2 * n. - intros; omega. - Abort. - - Goal forall z:Z, z > 0 -> 2 * z + 1 > z. - intro; omega. - Abort. - - -Options -------- - -.. flag:: Stable Omega - - .. deprecated:: 8.5 - - This deprecated flag (on by default) is for compatibility with Coq pre 8.5. It - resets internal name counters to make executions of :tacn:`omega` independent. - -.. flag:: Omega UseLocalDefs - - This flag (on by default) allows :tacn:`omega` to use the :term:`bodies <body>` of local - variables. - -.. flag:: Omega System - - This flag (off by default) activate the printing of debug information - -.. flag:: Omega Action - - This flag (off by default) activate the printing of debug information - -Technical data --------------- - -Overview of the tactic -~~~~~~~~~~~~~~~~~~~~~~ - - * The goal is negated twice and the first negation is introduced as a hypothesis. - * Hypotheses are decomposed in simple equations or inequalities. Multiple - goals may result from this phase. - * Equations and inequalities over ``nat`` are translated over - ``Z``, multiple goals may result from the translation of subtraction. - * Equations and inequalities are normalized. - * Goals are solved by the OMEGA decision procedure. - * The script of the solution is replayed. - -Overview of the OMEGA decision procedure -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -The OMEGA decision procedure involved in the :tacn:`omega` tactic uses -a small subset of the decision procedure presented in :cite:`TheOmegaPaper` -Here is an overview, refer to the original paper for more information. - - * Equations and inequalities are normalized by division by the GCD of their - coefficients. - * Equations are eliminated, using the Banerjee test to get a coefficient - equal to one. - * Note that each inequality cuts the Euclidean space in half. - * Inequalities are solved by projecting on the hyperspace - defined by cancelling one of the variables. They are partitioned - according to the sign of the coefficient of the eliminated - variable. Pairs of inequalities from different classes define a - new edge in the projection. - * Redundant inequalities are eliminated or merged in new - equations that can be eliminated by the Banerjee test. - * The last two steps are iterated until a contradiction is reached - (success) or there is no more variable to eliminate (failure). - -It may happen that there is a real solution and no integer one. The last -steps of the Omega procedure are not implemented, so the -decision procedure is only partial. - -Bugs ----- - - * The simplification procedure is very dumb and this results in - many redundant cases to explore. - - * Much too slow. - - * Certainly other bugs! You can report them to https://coq.inria.fr/bugs/. diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 4f3ee2dcaf..f8d6b35226 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -721,6 +721,33 @@ CoqIDE (`#13870 <https://github.com/coq/coq/pull/13870>`_, by Guillaume Melquiond). +Changes in 8.13.2 +~~~~~~~~~~~~~~~~~ + +Kernel +^^^^^^ + +- **Fixed:** + Crash when using :tacn:`vm_compute` on an irreducible ``PArray.set`` + (`#14005 <https://github.com/coq/coq/pull/14005>`_, + fixes `#13998 <https://github.com/coq/coq/issues/13998>`_, + by Guillaume Melquiond). +- **Fixed:** + Never store persistent arrays as VM / native structured values. + This could be used to make vo marshalling crash, and probably + breaking some other invariants of the kernel + (`#14007 <https://github.com/coq/coq/pull/14007>`_, + fixes `#14006 <https://github.com/coq/coq/issues/14006>`_, + by Pierre-Marie Pédrot). + +Tactic language +^^^^^^^^^^^^^^^^ + +- **Fixed:** + Ltac2 ``Array.init`` no longer incurs exponential overhead when used + recursively (`#14012 <https://github.com/coq/coq/pull/14012>`_, fixes `#14011 + <https://github.com/coq/coq/issues/14011>`_, by Jason Gross). + Version 8.12 ------------ @@ -751,10 +778,8 @@ The main changes include: of chapters along with updated syntax descriptions that match Coq's grammar in most but not all chapters. -Additionally, the :tacn:`omega` tactic is deprecated in this version of Coq, -and we recommend users to switch to :tacn:`lia` in new proof scripts (see -also the warning message in the :ref:`corresponding chapter -<omega_chapter>`). +Additionally, the `omega` tactic is deprecated in this version of Coq, +and we recommend users to switch to :tacn:`lia` in new proof scripts. See the `Changes in 8.12+beta1`_ section and following sections for the detailed list of changes, including potentially breaking changes marked @@ -1019,7 +1044,7 @@ Tactics <https://github.com/coq/coq/pull/10760>`_, by Jason Gross). - **Changed:** The :g:`auto with zarith` tactic and variations (including - :tacn:`intuition`) may now call :tacn:`lia` instead of :tacn:`omega` + :tacn:`intuition`) may now call :tacn:`lia` instead of `omega` (when the `Omega` module is loaded); more goals may be automatically solved, fewer section variables will be captured spuriously (`#11018 <https://github.com/coq/coq/pull/11018>`_, @@ -1115,7 +1140,7 @@ Tactics (`#11883 <https://github.com/coq/coq/pull/11883>`_, by Attila Gáspár). - **Deprecated:** - The :tacn:`omega` tactic is deprecated; + The `omega` tactic is deprecated; use :tacn:`lia` from the :ref:`Micromega <micromega>` plugin instead (`#11976 <https://github.com/coq/coq/pull/11976>`_, by Vincent Laporte). @@ -2102,11 +2127,9 @@ The main changes brought by Coq version 8.11 are: - :ref:`Revision<811Reals>` of the :g:`Coq.Reals` library, its axiomatisation and instances of the constructive and classical real numbers. -Additionally, while the :tacn:`omega` tactic is not yet deprecated in +Additionally, while the `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_chapter>`). +recommend users to switch to :tacn:`lia` in new proof scripts. The ``dev/doc/critical-bugs`` file documents the known critical bugs of Coq and affected releases. See the `Changes in 8.11+beta1`_ diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 9f097b4fe9..abe928fa26 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -5,7 +5,7 @@ The underlying formal language of Coq is a :gdef:`Calculus of Inductive Constructions` (|Cic|) whose inference rules are presented in this chapter. The history of this formalism as well as pointers to related -work are provided in a separate chapter; see *Credits*. +work are provided in a separate chapter; see :ref:`history`. .. _The-terms: diff --git a/doc/sphinx/language/core/conversion.rst b/doc/sphinx/language/core/conversion.rst index 06b6c61ea9..e53e6ea1cb 100644 --- a/doc/sphinx/language/core/conversion.rst +++ b/doc/sphinx/language/core/conversion.rst @@ -4,10 +4,80 @@ Conversion rules ---------------- Coq has conversion rules that can be used to determine if two -terms are equal by definition, or :term:`convertible`. +terms are equal by definition in |CiC|, or :term:`convertible`. Conversion rules consist of reduction rules and expansion rules. -See :ref:`applyingconversionrules`, -which describes tactics that apply these conversion rules. +Equality is determined by +converting both terms to a normal form, then verifying they are syntactically +equal (ignoring differences in the names of bound variables by +:term:`alpha-conversion <alpha-convertible>`). + +.. seealso:: :ref:`applyingconversionrules`, which describes tactics that apply these conversion rules. + +:gdef:`Reductions <reduction>` convert terms to something that is incrementally +closer to its normal form. For example, :term:`zeta-reduction` removes +:n:`let @ident := @term__1 in @term__2` constructs from a term by replacing +:n:`@ident` with :n:`@term__1` wherever :n:`@ident` appears in :n:`@term__2`. +The resulting term may be longer or shorter than the original. + +.. coqtop:: all + + Eval cbv zeta in let i := 1 in i + i. + +:gdef:`Expansions <expansion>` are reductions applied in the opposite direction, +for example expanding `2 + 2` to `let i := 2 in i + i`. While applying +reductions gives a unique result, the associated +expansion may not be unique. For example, `2 + 2` could also be +expanded to `let i := 2 in i + 2`. Reductions that have a unique inverse +expansion are also referred to as :gdef:`contractions <contraction>`. + +The normal form is defined as the result of applying a particular +set of conversion rules (beta-, delta-, iota- and zeta-reduction and eta-expansion) +repeatedly until it's no longer possible to apply any of them. + +Sometimes the result of a reduction tactic will be a simple value, for example reducing +`2*3+4` with `cbv beta delta iota` to `10`, which requires applying several +reduction rules repeatedly. In other cases, it may yield an expression containing +variables, axioms or opaque contants that can't be reduced. + +The useful conversion rules are shown below. All of them except for eta-expansion +can be applied with conversion tactics such as :tacn:`cbv`: + + .. list-table:: + :header-rows: 1 + + * - Conversion name + - Description + + * - beta-reduction + - eliminates `fun` + + * - delta-reduction + - replaces a defined variable or constant with its definition + + * - zeta-reduction + - eliminates `let` + + * - eta-expansion + - replaces a term `f` of type `forall a : A, B` with `fun x : A => f x` + + * - match-reduction + - eliminates `match` + + * - fix-reduction + - replaces a `fix` with a :term:`beta-redex`; + recursive calls to the symbol are replaced with the `fix` term + + * - cofix-reduction + - replaces a `cofix` with a :term:`beta-redex`; + recursive calls to the symbol are replaced with the `cofix` term + + * - iota-reduction + - match-, fix- and cofix-reduction together + +:ref:`applyingconversionrules` +describes tactics that only apply conversion rules. +(Other tactics may use conversion rules in addition +to other changes to the proof state.) α-conversion ~~~~~~~~~~~~ @@ -123,7 +193,7 @@ for :math:`x` an arbitrary variable name fresh in :math:`t`. .. math:: λ x:T.~(t~x)~\not\triangleright_η~t - This is because, in general, the type of :math:`t` need not to be convertible + This is because, in general, the type of :math:`t` need not be convertible to the type of :math:`λ x:T.~(t~x)`. E.g., if we take :math:`f` such that: .. math:: @@ -142,6 +212,30 @@ for :math:`x` an arbitrary variable name fresh in :math:`t`. because the type of the reduced term :math:`∀ x:\Type(2),~\Type(1)` would not be convertible to the type of the original term :math:`∀ x:\Type(1),~\Type(1)`. +Examples +~~~~~~~~ + + .. example:: Simple delta, fix, beta and match reductions + + ``+`` is a :ref:`notation <Notations>` for ``Nat.add``, which is defined + with a :cmd:`Fixpoint`. + + .. coqtop:: all abort + + Print Nat.add. + Goal 1 + 1 = 2. + cbv delta. + cbv fix. + cbv beta. + cbv match. + + The term can be fully reduced with `cbv`: + + .. coqtop:: all abort + + Goal 1 + 1 = 2. + cbv. + .. _proof-irrelevance: Proof Irrelevance diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 5d36ec3cf9..49c2c6b785 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -515,6 +515,11 @@ To build, say, two targets foo.vo and bar.vo in parallel one can use + ``-extra-phony`` and ``-extra`` are deprecated. To provide additional target (``.PHONY`` or not) please use ``CoqMakefile.local``. +.. note:: + + Due to limitations with the compilation chain, makefiles generated + by ``coq_makefile`` won't correctly compile OCaml plugins with OCaml + < 4.07.0 when using more than one job (``-j N`` for ``N > 1``). Precompiling for ``native_compute`` +++++++++++++++++++++++++++++++++++ diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index b1759bf71b..88fca93547 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1666,7 +1666,7 @@ Proving a subgoal as a separate lemma: abstract is chosen to get a fresh name. If the proof is closed with :cmd:`Qed`, the auxiliary lemma is inlined in the final proof term. - This is useful with tactics such as :tacn:`omega` or + This is useful with tactics such as :tacn:`discriminate` that generate huge proof terms with many intermediate goals. It can significantly reduce peak memory use. In most cases it doesn't have a significant impact on run time. One case in which it can reduce run time @@ -2317,11 +2317,10 @@ performance issue. .. coqtop:: reset in - Set Warnings "-omega-is-deprecated". - Require Import Coq.omega.Omega. + Require Import Lia. Ltac mytauto := tauto. - Ltac tac := intros; repeat split; omega || mytauto. + Ltac tac := intros; repeat split; lia || mytauto. Notation max x y := (x + (y - x)) (only parsing). @@ -2340,7 +2339,7 @@ performance issue. Set Ltac Profiling. tac. Show Ltac Profile. - Show Ltac Profile "omega". + Show Ltac Profile "lia". .. coqtop:: in diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 294c56ef06..25ac72069b 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -1375,8 +1375,9 @@ table further down lists the classes that that are handled plainly. the term (as described in :ref:`LocalInterpretationRulesForNotations`). The last :token:`scope_key` is the top of the scope stack that's applied to the :token:`term`. - :n:`open_constr` - Parses an open :token:`term`. + :n:`open_constr {? ( {+, @scope_key } ) }` + Parses an open :token:`term`. Like :n:`constr` above, this class + accepts a list of notation scopes with the same effects. :n:`ident` Parses :token:`ident` or :n:`$@ident`. The first form returns :n:`ident:(@ident)`, diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index bab9d35099..d4749f781a 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -609,7 +609,7 @@ Abbreviations |SSR| extends the :tacn:`set` tactic by supplying: - + an open syntax, similarly to the :tacn:`pose (ssreflect)` tactic; + + an open syntax, similarly to the :tacn:`pose <pose (ssreflect)>` tactic; + a more aggressive matching algorithm; + an improved interpretation of wildcards, taking advantage of the matching algorithm; @@ -899,7 +899,7 @@ context of a goal thanks to the ``in`` tactical. .. tacv:: set @ident := @term in {+ @ident} - This variant of :tacn:`set (ssreflect)` introduces a defined constant + This variant of :tacn:`set <set (ssreflect)>` introduces a defined constant called :token:`ident` in the context, and folds it in the context entries mentioned on the right hand side of ``in``. The body of :token:`ident` is the first subterm matching these context @@ -1202,7 +1202,7 @@ The move tactic. Goal not False. move. - More precisely, the :tacn:`move` tactic inspects the goal and does nothing + More precisely, the :tacn:`move <move (ssreflect)>` tactic inspects the goal and does nothing (:tacn:`idtac`) if an introduction step is possible, i.e. if the goal is a product or a ``let … in``, and performs :tacn:`hnf` otherwise. @@ -1301,7 +1301,7 @@ The apply tactic this use of the :tacn:`refine` tactic implies that the tactic tries to match the goal up to expansion of constants and evaluation of subterms. -:tacn:`apply (ssreflect)` has a special behavior on goals containing +:tacn:`apply <apply (ssreflect)>` has a special behavior on goals containing existential metavariables of sort :g:`Prop`. .. example:: @@ -2461,7 +2461,7 @@ The have tactic. redex, and introduces the lemma under a fresh name, automatically chosen. -Like in the case of the :n:`pose (ssreflect)` tactic (see section :ref:`definitions_ssr`), the types of +Like in the case of the :n:`pose <pose (ssreflect)>` tactic (see section :ref:`definitions_ssr`), the types of the holes are abstracted in term. .. example:: @@ -3775,7 +3775,7 @@ involves the following steps: ``forall n, F1 n = F2 n`` for ``eq_map``). 3. If so :tacn:`under` puts these n goals in head normal form (using - the defective form of the tactic :tacn:`move`), then executes + the defective form of the tactic :tacn:`move <move (ssreflect)>`), then executes the corresponding intro pattern :n:`@i_pattern__i` in each goal. 4. Then :tacn:`under` checks that the first n subgoals @@ -5665,6 +5665,7 @@ Tactics respectively. .. tacn:: move + :name: move (ssreflect) :tacn:`idtac` or :tacn:`hnf` (see :ref:`bookkeeping_ssr`) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index fad02b2645..7bc009fcfe 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1148,7 +1148,7 @@ Managing the local context or at the bottom of the local context. All hypotheses on which the new hypothesis depends are moved too so as to respect the order of dependencies between hypotheses. It is equivalent to :n:`intro {? @ident__1 }` - followed by the appropriate call to :tacn:`move … after …`, + followed by the appropriate call to :tacn:`move`, :tacn:`move … before …`, :tacn:`move … at top`, or :tacn:`move … at bottom`. @@ -1235,7 +1235,6 @@ Managing the local context hypotheses that depend on it. .. tacn:: move @ident__1 after @ident__2 - :name: move … after … This moves the hypothesis named :n:`@ident__1` in the local context after the hypothesis named :n:`@ident__2`, where “after” is in reference to the @@ -1256,7 +1255,7 @@ Managing the local context :name: move … before … This moves :n:`@ident__1` towards and just before the hypothesis - named :n:`@ident__2`. As for :tacn:`move … after …`, dependencies + named :n:`@ident__2`. As for :tacn:`move`, dependencies over :n:`@ident__1` (when :n:`@ident__1` comes before :n:`@ident__2` in the order of dependencies) or in the type of :n:`@ident__1` (when :n:`@ident__1` comes after :n:`@ident__2` in the order of @@ -2502,7 +2501,7 @@ and an explanation of the underlying technique. :name: inversion ... using ... .. todo using … instead of ... in the name above gives a Sphinx error, even though - this works just find for :tacn:`move … after …` + this works just find for :tacn:`move` Let :n:`@ident` have type :g:`(I t)` (:g:`I` an inductive predicate) in the local context, and :n:`@ident` be a (dependent) inversion lemma. Then, this diff --git a/doc/sphinx/proofs/automatic-tactics/index.rst b/doc/sphinx/proofs/automatic-tactics/index.rst index c3712b109d..e458c3a9f5 100644 --- a/doc/sphinx/proofs/automatic-tactics/index.rst +++ b/doc/sphinx/proofs/automatic-tactics/index.rst @@ -14,7 +14,6 @@ complex goals in new domains. :maxdepth: 1 logic - ../../addendum/omega ../../addendum/micromega ../../addendum/ring ../../addendum/nsatz diff --git a/doc/sphinx/refman-preamble.rst b/doc/sphinx/refman-preamble.rst index 32d3e87e68..dd1d6051b5 100644 --- a/doc/sphinx/refman-preamble.rst +++ b/doc/sphinx/refman-preamble.rst @@ -15,7 +15,7 @@ .. |c_i| replace:: `c`\ :math:`_{i}` .. |c_n| replace:: `c`\ :math:`_{n}` .. |Cic| replace:: CIC -.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\beta\delta\iota\zeta}` +.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{βδιζ}` .. |Latex| replace:: :smallcaps:`LaTeX` .. |Ltac| replace:: `L`:sub:`tac` .. |p_1| replace:: `p`\ :math:`_{1}` diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 453e878a5d..d212256765 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -467,6 +467,7 @@ Displaying information about notations - `tactic` - for currently-defined tactic notations, :token:`tactic`\s and tacticals (corresponding to :token:`ltac_expr` in the documentation). - `vernac` - for :token:`command`\s + - `ltac2` - for Ltac2 notations (corresponding to :token:`ltac2_expr`) This command doesn't display all nonterminals of the grammar. For example, productions shown by `Print Grammar tactic` refer to nonterminals `tactic_then_locality` diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index e4f0967794..bca66cc61b 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -58,10 +58,7 @@ theories/micromega/ZifyPow.v theories/micromega/Zify.v theories/nsatz/NsatzTactic.v theories/nsatz/Nsatz.v -theories/omega/Omega.v theories/omega/OmegaLemmas.v -theories/omega/OmegaPlugin.v -theories/omega/OmegaTactic.v theories/omega/PreOmega.v theories/quote/Quote.v theories/romega/ROmega.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index d67906c4a8..6fda3b06ce 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -135,6 +135,7 @@ through the <tt>Require Import</tt> command.</p> theories/Arith/Bool_nat.v theories/Arith/Factorial.v theories/Arith/Wf_nat.v + theories/Arith/Cantor.v </dd> <dt> <b>PArith</b>: diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index 522b9900a5..51e26a9082 100644 --- a/doc/tools/coqrst/coqdoc/main.py +++ b/doc/tools/coqrst/coqdoc/main.py @@ -28,7 +28,7 @@ from bs4 import BeautifulSoup from bs4.element import NavigableString COQDOC_OPTIONS = ['--body-only', '--no-glob', '--no-index', '--no-externals', - '-s', '--html', '--stdout', '--utf8'] + '-s', '--html', '--stdout', '--utf8', '--parse-comments'] COQDOC_SYMBOLS = ["->", "<-", "<->", "=>", "<=", ">=", "<>", "~", "/\\", "\\/", "|-", "*", "forall", "exists"] COQDOC_HEADER = "".join("(** remove printing {} *)".format(s) for s in COQDOC_SYMBOLS) @@ -68,8 +68,19 @@ def lex(source): if isinstance(elem, NavigableString): yield [], elem elif elem.name == "span": - cls = "coqdoc-{}".format(elem['title']) - yield [cls], elem.string + if elem.string: + cls = "coqdoc-{}".format(elem.get("title", "comment")) + yield [cls], elem.string + else: + # handle multi-line comments + children = list(elem.children) + mlc = children[0].startswith("(*") and children[-1].endswith ("*)") + for elem2 in children: + if isinstance(elem2, NavigableString): + cls = ["coqdoc-comment"] if mlc else [] + yield cls, elem2 + elif elem2.name == 'br': + pass elif elem.name == 'br': pass else: diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 1428dae7ef..468b6b648d 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -938,10 +938,11 @@ class CoqtopBlocksTransform(Transform): @staticmethod def split_lines(source): - r"""Split Coq input in chunks + r"""Split Coq input into chunks, which may include single- or + multi-line comments. Nested comments are not supported. A chunk is a minimal sequence of consecutive lines of the input that - ends with a '.' + ends with a '.' or '*)' >>> split_lines('A.\nB.''') ['A.', 'B.'] @@ -962,8 +963,14 @@ class CoqtopBlocksTransform(Transform): >>> split_lines('SearchHead le.\nSearchHead (@eq bool).') ['SearchHead le.', 'SearchHead (@eq bool).'] + + >>> split_lines("(* *) x. (* *)\ny.\n") + ['(* *) x. (* *)', 'y.'] + + >>> split_lines("(* *) x (* \n *)\ny.\n") + ['(* *) x (* \n *)', 'y.'] """ - return re.split(r"(?<=(?<!\.)\.)\n", source.strip()) + return re.split(r"(?:(?<=(?<!\.)\.)|(?<=\*\)))\n", source.strip()) @staticmethod def parse_options(node): @@ -1039,7 +1046,11 @@ class CoqtopBlocksTransform(Transform): if options['warn']: repl.sendone('Set Warnings "default".') for sentence in self.split_lines(node.rawsource): - pairs.append((sentence, repl.sendone(sentence))) + comment = re.compile(r"\s*\(\*.*?\*\)\s*", re.DOTALL) + wo_comments = re.sub(comment, "", sentence) + has_tac = wo_comments != "" and not wo_comments.isspace() + output = repl.sendone(sentence) if has_tac else "" + pairs.append((sentence, output)) if options['abort']: repl.sendone('Abort All.') if options['fail']: @@ -1052,9 +1063,10 @@ class CoqtopBlocksTransform(Transform): # Use Coqdoc to highlight input in_chunks = highlight_using_coqdoc(sentence) dli += nodes.term(sentence, '', *in_chunks, classes=self.block_classes(options['input'])) - # Parse ANSI sequences to highlight output - out_chunks = AnsiColorsParser().colorize_str(output) - dli += nodes.definition(output, *out_chunks, classes=self.block_classes(options['output'], output)) + if output: + # Parse ANSI sequences to highlight output + out_chunks = AnsiColorsParser().colorize_str(output) + dli += nodes.definition(output, *out_chunks, classes=self.block_classes(options['output'], output)) node.clear() node.rawsource = self.make_rawsource(pairs, options['input'], options['output']) node['classes'].extend(self.block_classes(options['input'] or options['output'])) @@ -1180,8 +1192,7 @@ class StdGlossaryIndex(Index): if type == 'term': entries = content[itemname[0].lower()] entries.append([itemname, 0, docname, anchor, '', '', '']) - content = sorted(content.items()) - return content, False + return content.items(), False def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, content=[]): """A grammar production not included in a ``prodn`` directive. diff --git a/doc/tools/coqrst/repl/ansicolors.py b/doc/tools/coqrst/repl/ansicolors.py index 9e23be2409..6700c20b1a 100644 --- a/doc/tools/coqrst/repl/ansicolors.py +++ b/doc/tools/coqrst/repl/ansicolors.py @@ -91,7 +91,10 @@ def parse_ansi(code): leading ‘^[[’ or the final ‘m’ """ classes = [] - parse_style([int(c) for c in code.split(';')], 0, classes) + if code == "37": + pass # ignore white fg + else: + parse_style([int(c) for c in code.split(';')], 0, classes) return ["ansi-" + cls for cls in classes] if __name__ == '__main__': diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune index 4ba60ddd9f..873b2f8dff 100644 --- a/doc/tools/docgram/dune +++ b/doc/tools/docgram/dune @@ -21,7 +21,6 @@ (glob_files %{project_root}/plugins/ltac/*.mlg) (glob_files %{project_root}/plugins/micromega/*.mlg) (glob_files %{project_root}/plugins/nsatz/*.mlg) - (glob_files %{project_root}/plugins/omega/*.mlg) (glob_files %{project_root}/plugins/ring/*.mlg) (glob_files %{project_root}/plugins/rtauto/*.mlg) (glob_files %{project_root}/plugins/ssr/*.mlg) diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 1f5c1ee3e2..fe166524bf 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1777,7 +1777,6 @@ simple_tactic: [ | "zify_iter_let" tactic (* micromega plugin *) | "zify_elim_let" (* micromega plugin *) | "nsatz_compute" constr (* nsatz plugin *) -| "omega" (* omega plugin *) | "protect_fv" string "in" ident (* ring plugin *) | "protect_fv" string (* ring plugin *) | "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr (* ring plugin *) diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 49bcf97850..2b09263cc4 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1855,7 +1855,6 @@ simple_tactic: [ | "zify_iter_let" ltac_expr (* micromega plugin *) | "zify_elim_let" (* micromega plugin *) | "nsatz_compute" one_term (* nsatz plugin *) -| "omega" (* omega plugin *) | "protect_fv" string OPT ( "in" ident ) | "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term (* ring plugin *) | "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term (* ring plugin *) |