Merge PR #13684: Document the -native-compiler option

Reviewed-by: silene
Ack-by: Zimmi48
Ack-by: jfehrle

2 files changed, 69 insertions, 1 deletions

diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index d20a82e6c0..06a196e951 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -219,6 +219,71 @@ and ``coqtop``, unless stated otherwise:
 :-batch: Exit just after argument parsing. Available for ``coqtop`` only.
 :-verbose: Output the content of the input file as it is compiled.
   This option is available for ``coqc`` only.
+:-native-compiler (yes|no|ondemand): Enable the :tacn:`native_compute`
+  reduction machine and precompilation to ``.cmxs`` files for future use
+  by :tacn:`native_compute`.
+  Setting ``yes`` enables :tacn:`native_compute`; it also causes Coq
+  to precompile the native code for future use; all dependencies need
+  to have been precompiled beforehand. Setting ``no`` disables
+  :tacn:`native_compute` which defaults back to :tacn:`vm_compute`; no files are precompiled.
+  Setting ``ondemand`` enables :tacn:`native_compute`
+  but disables precompilation; all missing dependencies will be recompiled
+  every time :tacn:`native_compute` is called.
+
+  .. _native-compiler-options:
+
+  .. versionchanged:: 8.13
+
+     The default value is set at configure time,
+     ``-config`` can be used to retrieve it.
+     All this can be summarized in the following table:
+
+  .. list-table::
+     :header-rows: 1
+
+     * - ``configure``
+       - ``coqc``
+       - ``native_compute``
+       - outcome
+       - requirements
+     * - yes
+       - yes (default)
+       - native_compute
+       - ``.cmxs``
+       - ``.cmxs`` of deps
+     * - yes
+       - no
+       - vm_compute
+       - none
+       - none
+     * - yes
+       - ondemand
+       - native_compute
+       - none
+       - none
+     * - no
+       - yes, no, ondemand
+       - vm_compute
+       - none
+       - none
+     * - ondemand
+       - yes
+       - native_compute
+       - ``.cmxs``
+       - ``.cmxs`` of deps
+     * - ondemand
+       - no
+       - vm_compute
+       - none
+       - none
+     * - ondemand
+       - ondemand (default)
+       - native_compute
+       - none
+       - none
+
+:-native-output-dir: Set the directory in which to put the aforementioned
+  ``.cmxs`` for :tacn:`native_compute`. Defaults to ``.coq-native``.
 :-vos: Indicate Coq to skip the processing of opaque proofs
   (i.e., proofs ending with :cmd:`Qed` or :cmd:`Admitted`), output a ``.vos`` files
   instead of a ``.vo`` file, and to load ``.vos`` files instead of ``.vo`` files
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index 3649202b45..90404b7321 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -442,7 +442,10 @@ the conversion in hypotheses :n:`{+ @ident}`.
    in :cite:`FullReduction`. If Coq is running in native code, it can be
    typically two to five times faster than :tacn:`vm_compute`. Note however that the
    compilation cost is higher, so it is worth using only for intensive
-   computations.
+   computations. Depending on the configuration, this tactic can either default to
+   :tacn:`vm_compute`, recompile dependencies or fail due to some missing
+   precompiled dependencies,
+   see :ref:`the native-compiler option <native-compiler-options>` for details.
 
    .. flag:: NativeCompute Timing