diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 11 | ||||
| -rw-r--r-- | doc/sphinx/changes.rst | 23 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 133 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 6 |
7 files changed, 140 insertions, 41 deletions
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index cc19c8b6a9..f706633da9 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -35,6 +35,17 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`, use the Simplex method for solving linear goals. If it is not set, the decision procedures are using Fourier elimination. +.. opt:: Dump Arith + + This option (unset by default) may be set to a file path where + debug info will be written. + +.. cmd:: Show Lia Profile + + This command prints some statistics about the amount of pivoting + operations needed by :tacn:`lia` and may be useful to detect + inefficiencies (only meaningful if flag :flag:`Simplex` is set). + .. flag:: Lia Cache This flag (set by default) instructs :tacn:`lia` to cache its results in the file `.lia.cache` diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 294f121cf8..6d9979a704 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -60,17 +60,17 @@ 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/api (documentation of the ML API), https://coq.github.io/doc/v8.11/refman (reference manual), and https://coq.github.io/doc/v8.11/stdlib (documentation of the standard library). +Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael +Soegtrop and Théo Zimmermann worked on maintaining and improving the +continuous integration system and package building infrastructure. + The OPAM repository for |Coq| packages has been maintained by -Guillaume Claret, Karl Palmskog, Matthieu Sozeau, Enrico Tassi with +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/. @@ -566,27 +566,28 @@ Changes in 8.11.0 <https://github.com/coq/coq/pull/11203>`_, fixes `#10971 <https://github.com/coq/coq/issues/10971>`_, by Jason Gross) - **Fixed:** - Efficiency regression introduced by PR `#9725 <https://github.com/coq/coq/pull/9725>`_ + 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, tho the old semantics + 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 loading explicitly the module :g:`ZifyPow`. + 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 from Coq 8.10 + Syntax of tactic `cofix ... with ...` was broken since Coq 8.10 (`#11241 <https://github.com/coq/coq/pull/11241>`_, by Hugo Herbelin). @@ -611,7 +612,7 @@ Changes in 8.11.0 <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 + 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 @@ -635,7 +636,7 @@ Changes in 8.11.0 **Infrastructure and dependencies** - **Added:** - Build date can now be overriden by setting the `SOURCE_DATE_EPOCH` + 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). diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 510e271951..f0bbaed8f3 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1570,11 +1570,26 @@ inserted. In the second case, the function is considered to be implicitly applied to the implicit arguments it is waiting for: one says that the implicit argument is maximally inserted. -Each implicit argument can be declared to have to be inserted maximally or non -maximally. This can be governed argument per argument by the command -:cmd:`Arguments (implicits)` or globally by the :flag:`Maximal Implicit Insertion` flag. +Each implicit argument can be declared to be inserted maximally or non +maximally. In Coq, maximally-inserted implicit arguments are written between curly braces +"{ }" and non-maximally-inserted implicit arguments are written in square brackets "[ ]". -.. seealso:: :ref:`displaying-implicit-args`. +.. seealso:: :flag:`Maximal Implicit Insertion` + +Trailing Implicit Arguments ++++++++++++++++++++++++++++ + +An implicit argument is considered trailing when all following arguments are declared +implicit. Trailing implicit arguments cannot be declared non maximally inserted, +otherwise they would never be inserted. + +.. exn:: Argument @name is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. + + For instance: + + .. coqtop:: all fail + + Fail Definition double [n] := n + n. Casual use of implicit arguments @@ -1608,7 +1623,7 @@ Implicit Argument Binders In the first setting, one wants to explicitly give the implicit arguments of a declared object as part of its definition. To do this, one has to surround the bindings of implicit arguments by curly -braces: +braces or square braces: .. coqtop:: all @@ -1624,6 +1639,17 @@ absent in every situation but still be able to specify it if needed: Goal forall A, compose id id = id (A:=A). +For non maximally inserted implicit arguments, use square brackets: + +.. coqtop:: all + + Fixpoint map [A B : Type] (f : A -> B) (l : list A) : list B := + match l with + | nil => nil + | cons a t => cons (f a) (map f t) + end. + + Print Implicit map. The syntax is supported in all top-level definitions: :cmd:`Definition`, :cmd:`Fixpoint`, :cmd:`Lemma` and so on. For (co-)inductive datatype @@ -1643,17 +1669,55 @@ For example: One can always specify the parameter if it is not uniform using the usual implicit arguments disambiguation syntax. +The syntax is also supported in internal binders. For instance, in the +following kinds of expressions, the type of each declaration present +in :token:`binders` can be bracketed to mark the declaration as +implicit: +:n:`fun (@ident:forall @binders, @type) => @term`, +:n:`forall (@ident:forall @binders, @type), @type`, +:n:`let @ident @binders := @term in @term`, +:n:`fix @ident @binders := @term in @term` and +:n:`cofix @ident @binders := @term in @term`. +Here is an example: + +.. coqtop:: all + + Axiom Ax : + forall (f:forall {A} (a:A), A * A), + let g {A} (x y:A) := (x,y) in + f 0 = g 0 0. + +.. warn:: Ignoring implicit binder declaration in unexpected position + + This is triggered when setting an argument implicit in an + expression which does not correspond to the type of an assumption + or to the body of a definition. Here is an example: + + .. coqtop:: all warn + + Definition f := forall {y}, y = 0. + +.. warn:: Making shadowed name of implicit argument accessible by position + + This is triggered when two variables of same name are set implicit + in the same block of binders, in which case the first occurrence is + considered to be unnamed. Here is an example: + + .. coqtop:: all warn + + Check let g {x:nat} (H:x=x) {x} (H:x=x) := x in 0. + Declaring Implicit Arguments ++++++++++++++++++++++++++++ -.. cmd:: Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } +.. cmd:: Arguments @qualid {* {| [ @name ] | { @name } | @name } } :name: Arguments (implicits) This command is used to set implicit arguments *a posteriori*, - where the list of possibly bracketed :token:`ident` is a prefix of the list of + where the list of possibly bracketed :token:`name` is a prefix of the list of arguments of :token:`qualid` where the ones to be declared implicit are surrounded by square brackets and the ones to be declared as maximally inserted implicits are surrounded by curly braces. @@ -1667,20 +1731,20 @@ Declaring Implicit Arguments This command clears implicit arguments. -.. cmdv:: Global Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } +.. cmdv:: Global Arguments @qualid {* {| [ @name ] | { @name } | @name } } This command is used to recompute the implicit arguments of :token:`qualid` after ending of the current section if any, enforcing the implicit arguments known from inside the section to be the ones declared by the command. -.. cmdv:: Local Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } +.. cmdv:: Local Arguments @qualid {* {| [ @name ] | { @name } | @name } } When in a module, tell not to activate the implicit arguments of :token:`qualid` declared by this command to contexts that require the module. -.. cmdv:: {? {| Global | Local } } Arguments @qualid {*, {+ {| [ @ident ] | { @ident } | @ident } } } +.. cmdv:: {? {| Global | Local } } Arguments @qualid {*, {+ {| [ @name ] | { @name } | @name } } } For names of constants, inductive types, constructors, lemmas which can only be applied to a fixed number of @@ -1728,14 +1792,6 @@ Declaring Implicit Arguments To know which are the implicit arguments of an object, use the command :cmd:`Print Implicit` (see :ref:`displaying-implicit-args`). -.. exn:: Argument @ident is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. - - For instance in - - .. coqtop:: all fail - - Arguments prod _ [_]. - Automatic declaration of implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1811,7 +1867,7 @@ appear strictly in the body of the type, they are implicit. Mode for automatic declaration of implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +++++++++++++++++++++++++++++++++++++++++++++++++++++ .. flag:: Implicit Arguments @@ -1823,7 +1879,7 @@ Mode for automatic declaration of implicit arguments .. _controlling-strict-implicit-args: Controlling strict implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ++++++++++++++++++++++++++++++++++++++ .. flag:: Strict Implicit @@ -1842,7 +1898,7 @@ Controlling strict implicit arguments .. _controlling-contextual-implicit-args: Controlling contextual implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ++++++++++++++++++++++++++++++++++++++++++ .. flag:: Contextual Implicit @@ -1853,7 +1909,7 @@ Controlling contextual implicit arguments .. _controlling-rev-pattern-implicit-args: Controlling reversible-pattern implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ++++++++++++++++++++++++++++++++++++++++++++++++++ .. flag:: Reversible Pattern Implicit @@ -1864,7 +1920,7 @@ Controlling reversible-pattern implicit arguments .. _controlling-insertion-implicit-args: Controlling the insertion of implicit arguments not followed by explicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ .. flag:: Maximal Implicit Insertion @@ -1873,6 +1929,28 @@ Controlling the insertion of implicit arguments not followed by explicit argumen function is partially applied and the next argument of the function is an implicit one. +Combining manual declaration and automatic declaration +++++++++++++++++++++++++++++++++++++++++++++++++++++++ + +When some arguments are manually specified implicit with binders in a definition +and the automatic declaration mode in on, the manual implicit arguments are added to the +automatically declared ones. + +In that case, and when the flag :flag:`Maximal Implicit Insertion` is set to off, +some trailing implicit arguments can be inferred to be non maximally inserted. In +this case, they are converted to maximally inserted ones. + +.. example:: + + .. coqtop:: all + + Set Implicit Arguments. + Axiom eq0_le0 : forall (n : nat) (x : n = 0), n <= 0. + Print Implicit eq0_le0. + Axiom eq0_le0' : forall (n : nat) {x : n = 0}, n <= 0. + Print Implicit eq0_le0'. + + .. _explicit-applications: Explicit applications @@ -2136,8 +2214,10 @@ Implicit generalization ~~~~~~~~~~~~~~~~~~~~~~~ .. index:: `{ } +.. index:: `[ ] .. index:: `( ) .. index:: `{! } +.. index:: `[! ] .. index:: `(! ) Implicit generalization is an automatic elaboration of a statement @@ -2145,11 +2225,12 @@ with free variables into a closed statement where these variables are quantified explicitly. It is activated for a binder by prefixing a \`, and for terms by -surrounding it with \`{ } or \`( ). +surrounding it with \`{ }, or \`[ ] or \`( ). Terms surrounded by \`{ } introduce their free variables as maximally -inserted implicit arguments, and terms surrounded by \`( ) introduce -them as explicit arguments. +inserted implicit arguments, terms surrounded by \`[ ] introduce them as +non maximally inserted implicit arguments and terms surrounded by \`( ) +introduce them as explicit arguments. Generalizing binders always introduce their free variables as maximally inserted implicit arguments. The binder itself introduces diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index d591718b17..09090ce89a 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -283,8 +283,10 @@ Binders | ( {+ @name } : @term ) | ( @name {? : @term } := @term ) | %{ {+ @name } {? : @term } %} + | [ {+ @name } {? : @term } ] | `( {+, @typeclass_constraint } ) | `%{ {+, @typeclass_constraint } %} + | `[ {+, @typeclass_constraint } ] | ' @pattern0 | ( @name : @term %| @term ) typeclass_constraint ::= {? ! } @term diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index ba43128bdc..98d222e317 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -157,8 +157,6 @@ and ``coqtop``, unless stated otherwise: loading the default resource file from the standard configuration directories. :-q: Do not to load the default resource file. -:-load-ml-source *file*: Load the OCaml source file *file*. -:-load-ml-object *file*: Load the OCaml object file *file*. :-l *file*, -load-vernac-source *file*: Load and execute the |Coq| script from *file.v*. :-lv *file*, -load-vernac-source-verbose *file*: Load and execute the diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 853ddfd6dc..46215f16a6 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2222,14 +2222,14 @@ tactics to *permute* the subgoals generated by a tactic. If :token:`num`\'s value is :math:`k`, this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n` - in focus. The first subgoal becomes :math:`G_{n + 1 − k}` and the + in focus. Subgoal :math:`G_{n + 1 − k}` becomes the first, and the circular order of subgoals remains unchanged. .. tacn:: first @num last If :token:`num`\'s value is :math:`k`, this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n` - in focus. The first subgoal becomes :math:`G_k` and the circular order + in focus. Subgoal :math:`G_{k + 1 \bmod n}` becomes the first, and the circular order of subgoals remains unchanged. Finally, the tactics ``last`` and ``first`` combine with the branching syntax diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 53cfb973d4..36a5916868 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3113,6 +3113,12 @@ the conversion in hypotheses :n:`{+ @ident}`. compilation cost is higher, so it is worth using only for intensive computations. + .. flag:: NativeCompute Timing + + This flag causes all calls to the native compiler to print + timing information for the compilation, execution, and + reification phases of native compilation. + .. flag:: NativeCompute Profiling On Linux, if you have the ``perf`` profiler installed, this flag makes |