From 2d7a257b7822192b7ff8e145e9e043fa2c2449a4 Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Sat, 4 Jul 2020 14:04:19 -0700 Subject: Document "Print Debug GC" command and OCAMLRUNPARAM env variable --- doc/sphinx/proof-engine/proof-handling.rst | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) (limited to 'doc/sphinx/proof-engine') 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 `_ + 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 `_ + Perform a heap compaction. This is generally an expensive operation. + See: `OCaml Gc.compact `_ There is also an analogous tactic :tacn:`optimize_heap`. + +Memory usage parameters can be set through the :ref:`OCAMLRUNPARAM ` +environment variable. -- cgit v1.2.3