Merge PR #11814: Document coq_makefile behavior wrt -native-compiler yes

Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: gares

1 files changed, 34 insertions, 0 deletions

diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 514353e39b..e5ff26520a 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -499,6 +499,40 @@ To build, say, two targets foo.vo and bar.vo in parallel one can use
     (``.PHONY`` or not) please use ``CoqMakefile.local``.
 
 
+Precompiling for ``native_compute``
++++++++++++++++++++++++++++++++++++
+
+To compile files for ``native_compute``, one can use the
+``-native-compiler yes`` option of |Coq|, for instance by putting the
+following in a :ref:`coqmakefilelocal` file:
+
+::
+
+    COQEXTRAFLAGS += -native-compiler yes
+
+The generated ``CoqMakefile`` installation target will then take care
+of installing the extra ``.coq-native`` directories.
+
+.. note::
+
+   As an alternative to modifying any file, one can set the
+   environment variable when calling ``make``:
+
+   ::
+
+      COQEXTRAFLAGS="-native-compiler yes" make
+
+   This can be useful when files cannot be modified, for instance when
+   installing via OPAM a package built with ``coq_makefile``:
+
+   ::
+
+      COQEXTRAFLAGS="-native-compiler yes" opam install coq-package
+
+.. note::
+
+   This requires all dependencies to be themselves compiled with
+   ``-native-compiler yes``.
 
 Building a |Coq| project with Dune
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~