Merge PR #12643: Document "Print Debug GC" command and OCAMLRUNPARAM environment variable

Reviewed-by: Zimmi48
Ack-by: jfehrle

2 files changed, 33 insertions, 9 deletions

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.