diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 21 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 2 |
2 files changed, 16 insertions, 7 deletions
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 09ce002e8c..4eaca8634f 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2292,7 +2292,7 @@ to the others. Iteration ~~~~~~~~~ -.. tacn:: do {? @num } {| @tactic | [ {+| @tactic } ] } +.. tacn:: do {? @mult } {| @tactic | [ {+| @tactic } ] } :name: do (ssreflect) This tactical offers an accurate control on the repetition of tactics. |