diff options
Diffstat (limited to 'doc/sphinx')
| -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 |
5 files changed, 54 insertions, 26 deletions
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. |