diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/_static/ansi.css | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 1 | ||||
| -rw-r--r-- | doc/sphinx/addendum/omega.rst | 210 | ||||
| -rw-r--r-- | doc/sphinx/changes.rst | 43 | ||||
| -rw-r--r-- | doc/sphinx/language/cic.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 9 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 20 | ||||
| -rw-r--r-- | doc/sphinx/proofs/automatic-tactics/index.rst | 1 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/using/libraries/writing.rst | 6 |
11 files changed, 70 insertions, 236 deletions
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/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 5d471c695c..d718454364 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` ~~~~~~~~~~~~~~~~~~~~~~~~ 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/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 9f3f0ef3d5..25ac72069b 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -66,7 +66,6 @@ Current limitations include: - An easy way to get the number of constructors of an inductive type. Currently only way to do this is to destruct a variable of the inductive type and count the number of goals that result. -- The :attr:`deprecated` attribute is not supported for Ltac2 definitions. - Error messages may be cryptic. @@ -229,6 +228,8 @@ One can define new types with the following commands. defined in Coq and give their type information. They can also declare data structures from OCaml. This command has no use for the end user. + This command supports the :attr:`deprecated` attribute. + APIs ~~~~ @@ -263,10 +264,10 @@ There is dedicated syntax for list and array literals. .. prodn:: ltac2_expr ::= @ltac2_expr5 ; @ltac2_expr | @ltac2_expr5 - ltac2_expr5 ::= fun {+ @tac2pat0 } => @ltac2_expr + ltac2_expr5 ::= fun {+ @tac2pat0 } {? : @ltac2_type } => @ltac2_expr | let {? rec } @ltac2_let_clause {* with @ltac2_let_clause } in @ltac2_expr | @ltac2_expr3 - ltac2_let_clause ::= {+ @tac2pat0 } := @ltac2_expr + ltac2_let_clause ::= {+ @tac2pat0 } {? : @ltac2_type } := @ltac2_expr ltac2_expr3 ::= {+, @ltac2_expr2 } ltac2_expr2 ::= @ltac2_expr1 :: @ltac2_expr2 | @ltac2_expr1 @@ -304,7 +305,7 @@ Ltac2 Definitions .. insertprodn tac2def_body tac2def_body .. prodn:: - tac2def_body ::= {| _ | @ident } {* @tac2pat0 } := @ltac2_expr + tac2def_body ::= {| _ | @ident } {* @tac2pat0 } {? : @ltac2_type } := @ltac2_expr This command defines a new global Ltac2 value. If one or more :token:`tac2pat0` are specified, the new value is a function. This is a shortcut for one of the @@ -319,6 +320,8 @@ Ltac2 Definitions If ``mutable`` is set, the definition can be redefined at a later stage (see below). + This command supports the :attr:`deprecated` attribute. + .. cmd:: Ltac2 Set @qualid {? as @ident } := @ltac2_expr This command redefines a previous ``mutable`` definition. @@ -1246,6 +1249,8 @@ Notations so that you may have to resort to thunking to ensure that side-effects are performed at the right time. + This command supports the :attr:`deprecated` attribute. + Abbreviations ~~~~~~~~~~~~~ @@ -1276,6 +1281,8 @@ Abbreviations Note that abbreviations are not type checked at all, and may result in typing errors after expansion. + This command supports the :attr:`deprecated` attribute. + .. _defining_tactics: Defining tactics @@ -1368,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/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/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 557ef10555..d212256765 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -442,6 +442,12 @@ Displaying information about notations Controls whether to use notations for printing terms wherever possible. Default is on. +.. flag:: Printing Raw Literals + + Controls whether to use string and number notations for printing terms + wherever possible (see :ref:`string-notations`). + Default is off. + .. flag:: Printing Parentheses If on, parentheses are printed even if implied by associativity and precedence @@ -461,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/sphinx/using/libraries/writing.rst b/doc/sphinx/using/libraries/writing.rst index 917edf0774..7461bfe443 100644 --- a/doc/sphinx/using/libraries/writing.rst +++ b/doc/sphinx/using/libraries/writing.rst @@ -22,13 +22,17 @@ deprecated compatibility alias using :cmd:`Notation (abbreviation)` by a comma. This attribute is supported by the following commands: :cmd:`Ltac`, - :cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`. + :cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`, :cmd:`Ltac2`, + :cmd:`Ltac2 Notation`, :cmd:`Ltac2 external`. It can trigger the following warnings: .. warn:: Tactic @qualid is deprecated since @string__since. @string__note. Tactic Notation @qualid is deprecated since @string__since. @string__note. Notation @string is deprecated since @string__since. @string__note. + Ltac2 definition @qualid is deprecated since @string__since. @string__note. + Ltac2 alias @qualid is deprecated since @string__since. @string__note. + Ltac2 notation {+ @ltac2_scope } is deprecated since @string__since. @string__note. :n:`@qualid` or :n:`@string` is the notation, :n:`@string__since` is the version number, :n:`@string__note` is |