diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/08-tools/12772-fix-details.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/evars.rst | 32 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/implicit-arguments.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/match.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 21 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 21 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 6 |
8 files changed, 74 insertions, 31 deletions
diff --git a/doc/changelog/08-tools/12772-fix-details.rst b/doc/changelog/08-tools/12772-fix-details.rst new file mode 100644 index 0000000000..67ee061285 --- /dev/null +++ b/doc/changelog/08-tools/12772-fix-details.rst @@ -0,0 +1,5 @@ +- **Fixed:** + The `details` environment added in the 8.12 release can now be used + as advertised in the reference manual + (`#12772 <https://github.com/coq/coq/pull/12772>`_, + by Thomas Letan). diff --git a/doc/sphinx/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst index 40e0898871..20f4310d13 100644 --- a/doc/sphinx/language/extensions/evars.rst +++ b/doc/sphinx/language/extensions/evars.rst @@ -13,13 +13,13 @@ Existential variables | ?[ ?@ident ] | ?@ident {? @%{ {+; @ident := @term } %} } -|Coq| terms can include existential variables which represents unknown -subterms to eventually be replaced by actual subterms. +|Coq| terms can include existential variables that represent unknown +subterms that are eventually replaced with actual subterms. -Existential variables are generated in place of unsolvable implicit +Existential variables are generated in place of unsolved implicit arguments or “_” placeholders when using commands such as ``Check`` (see Section :ref:`requests-to-the-environment`) or when using tactics such as -:tacn:`refine`, as well as in place of unsolvable instances when using +:tacn:`refine`, as well as in place of unsolved instances when using tactics such that :tacn:`eapply`. An existential variable is defined in a context, which is the context of variables of the placeholder which generated the existential variable, and a type, @@ -43,22 +43,18 @@ existential variable is represented by “?” followed by an identifier. Check identity _ (fun x => _). In the general case, when an existential variable :n:`?@ident` appears -outside of its context of definition, its instance, written under the -form :n:`{ {*; @ident := @term} }` is appending to its name, indicating +outside its context of definition, its instance, written in the +form :n:`{ {*; @ident := @term} }`, is appended to its name, indicating how the variables of its defining context are instantiated. -The variables of the context of the existential variables which are -instantiated by themselves are not written, unless the :flag:`Printing Existential Instances` flag -is on (see Section :ref:`explicit-display-existentials`), and this is why an -existential variable used in the same context as its context of definition is written with no instance. +Only the variables that are defined in another context are displayed: +this is why an existential variable used in the same context as its +context of definition is written with no instance. +This behaviour may be changed: see :ref:`explicit-display-existentials`. .. coqtop:: all Check (fun x y => _) 0 1. - Set Printing Existential Instances. - - Check (fun x y => _) 0 1. - Existential variables can be named by the user upon creation using the syntax :n:`?[@ident]`. This is useful when the existential variable needs to be explicitly handled later in the script (e.g. @@ -88,6 +84,14 @@ Explicit displaying of existential instances for pretty-printing context of an existential variable is instantiated at each of the occurrences of the existential variable. +.. coqtop:: all + + Check (fun x y => _) 0 1. + + Set Printing Existential Instances. + + Check (fun x y => _) 0 1. + .. _tactics-in-terms: Solving existential variables using tactics diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst index bbd486e3ba..ca69072cb9 100644 --- a/doc/sphinx/language/extensions/implicit-arguments.rst +++ b/doc/sphinx/language/extensions/implicit-arguments.rst @@ -70,7 +70,7 @@ is said *contextual* if it can be inferred only from the knowledge of the type of the context of the current expression. For instance, the only argument of:: - nil : forall A:Set, list A` + nil : forall A:Set, list A is contextual. Similarly, both arguments of a term of type:: @@ -539,7 +539,7 @@ with free variables into a closed statement where these variables are quantified explicitly. Use the :cmd:`Generalizable` command to designate which variables should be generalized. -It is activated for a binder by prefixing a \`, and for terms by +It is activated within a binder by prefixing it with \`, and for terms by surrounding it with \`{ }, or \`[ ] or \`( ). Terms surrounded by \`{ } introduce their free variables as maximally diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index b4558ef07f..d6a828521f 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -94,7 +94,7 @@ The expression :n:`let ( {*, @ident__i } ) := @term__0 in @term__1` performs case analysis on :n:`@term__0` whose type must be an inductive type with exactly one constructor. The number of variables :n:`@ident__i` must correspond to the number of arguments of this -contrustor. Then, in :n:`@term__1`, these variables are bound to the +constructor. Then, in :n:`@term__1`, these variables are bound to the arguments of the constructor in :n:`@term__0`. For instance, the definition diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 058b8ccd5c..ec182ce08f 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -81,8 +81,7 @@ loading of the resource file with the option ``-q``. By environment variables ~~~~~~~~~~~~~~~~~~~~~~~~~ -Load path can be specified to the |Coq| system by setting up ``$COQPATH`` -environment variable. It is a list of directories separated by +``$COQPATH`` can be used to specify the load path. It is a list of directories separated by ``:`` (``;`` on Windows). |Coq| will also honor ``$XDG_DATA_HOME`` and ``$XDG_DATA_DIRS`` (see Section :ref:`libraries-and-filesystem`). @@ -92,7 +91,7 @@ not set, they look for the commands in the executable path. .. _COQ_COLORS: -The ``$COQ_COLORS`` environment variable can be used to specify the set +``$COQ_COLORS`` can be used to specify the set of colors used by ``coqtop`` to highlight its output. It uses the same syntax as the ``$LS_COLORS`` variable from GNU’s ls, that is, a colon-separated list of assignments of the form :n:`name={*; attr}` where @@ -108,6 +107,22 @@ sets the highlights for added text in diffs to underlined (the 4) with a backgro color (0, 0, 240) and for removed text in diffs to a red background. Note that if you specify ``COQ_COLORS``, the predefined attributes are ignored. +.. _OCAMLRUNPARAM: + +``$OCAMLRUNPARAM``, described +`here <https://caml.inria.fr/pub/docs/manual-ocaml/runtime.html#s:ocamlrun-options>`_, +can be used to specify certain runtime and memory usage parameters. In most cases, +experimenting with these settings will likely not cause a significant performance difference +and should be harmless. + +If the variable is not set, |Coq| uses the +`default values <https://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#TYPEcontrol>`_, +except that ``space_overhead`` is set to 120 and ``minor_heap_size`` is set to 32Mwords +(256MB with 64-bit executables or 128MB with 32-bit executables). + +.. todo: Using the same text "here" for both of the links in the last 2 paragraphs generates + an incorrect warning: coq-commands.rst:4: WARNING: Duplicate explicit target name: "here". + The warning doesn't even have the right line number. :-( .. _command-line-options: diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 00aafe1266..4480b10319 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -858,19 +858,28 @@ Controlling the effect of proof editing commands Controlling memory usage ------------------------ +.. cmd:: Print Debug GC + + Prints heap usage statistics, which are values from the `stat` type of the `Gc` module + described + `here <https://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#TYPEstat>`_ + in the OCaml documentation. + The `live_words`, `heap_words` and `top_heap_words` values give the basic information. + Words are 8 bytes or 4 bytes, respectively, for 64- and 32-bit executables. + When experiencing high memory usage the following commands can be used to force |Coq| to optimize some of its internal data structures. - .. cmd:: Optimize Proof - This command forces |Coq| to shrink the data structure used to represent - the ongoing proof. + Shrink the data structure used to represent the current proof. .. cmd:: Optimize Heap - This command forces the |OCaml| runtime to perform a heap compaction. - This is in general an expensive operation. - See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ + Perform a heap compaction. This is generally an expensive operation. + See: `OCaml Gc.compact <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ There is also an analogous tactic :tacn:`optimize_heap`. + +Memory usage parameters can be set through the :ref:`OCAMLRUNPARAM <OCAMLRUNPARAM>` +environment variable. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 3b4b80ca21..4eaca8634f 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1211,6 +1211,8 @@ The move tactic. :tacn:`revert`, :tacn:`rename`, :tacn:`clear` and :tacn:`pattern` tactics. +.. _the_case_tactic_ssr: + The case tactic ``````````````` @@ -1235,7 +1237,17 @@ The case tactic x = 1 -> y = 2 -> G. - Note also that the case of |SSR| performs :g:`False` elimination, even + The :tacn:`case` can generate the following warning: + + .. warn:: SSReflect: cannot obtain new equations out of ... + + The tactic was run on an equation that cannot generate simpler equations, + for example `x = 1`. + + The warning can be silenced or made fatal by using the :opt:`Warnings` option + and the `spurious-ssr-injection` key. + + Finally the :tacn:`case` tactic of |SSR| performs :g:`False` elimination, even if no branch is generated by this case operation. Hence the tactic :tacn:`case` on a goal of the form :g:`False -> G` will succeed and prove the goal. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 25c4de7389..c5fab0983f 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2227,9 +2227,6 @@ and an explanation of the underlying technique. then :n:`injection @ident` first introduces the hypothesis in the local context using :n:`intros until @ident`. - .. exn:: Not a projectable equality but a discriminable one. - :undocumented: - .. exn:: Nothing to do, it is an equality between convertible terms. :undocumented: @@ -2237,7 +2234,8 @@ and an explanation of the underlying technique. :undocumented: .. exn:: Nothing to inject. - :undocumented: + + This error is given when one side of the equality is not a constructor. .. tacv:: injection @num |