Document coq_makefile behavior wrt -native-compiler yes

3 files changed, 77 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
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/test-suite/coq-makefile/native2/_CoqProject b/test-suite/coq-makefile/native2/_CoqProject
new file mode 100644
index 0000000000..61136e82f0
--- /dev/null
+++ b/test-suite/coq-makefile/native2/_CoqProject
@@ -0,0 +1,10 @@
+-R src test
+-R theories test
+-I src
+
+src/test_plugin.mlpack
+src/test.mlg
+src/test.mli
+src/test_aux.ml
+src/test_aux.mli
+theories/test.v
diff --git a/test-suite/coq-makefile/native2/run.sh b/test-suite/coq-makefile/native2/run.sh
new file mode 100755
index 0000000000..857f70fdff
--- /dev/null
+++ b/test-suite/coq-makefile/native2/run.sh
@@ -0,0 +1,33 @@
+#!/usr/bin/env bash
+
+NONATIVECOMP=$(grep "let native_compiler = false" ../../../config/coq_config.ml)||true
+if [[ $(which ocamlopt) && ! $NONATIVECOMP ]]; then
+
+. ../template/init.sh
+
+coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
+COQEXTRAFLAGS="-native-compiler yes" make
+make html mlihtml
+make install DSTROOT="$PWD/tmp"
+#make debug
+(cd "$(find tmp -name user-contrib)" && find .) | sort > actual
+sort > desired <<EOT
+.
+./test
+./test/test.glob
+./test/test_plugin.cmi
+./test/test_plugin.cmx
+./test/test_plugin.cmxa
+./test/test_plugin.cmxs
+./test/test.v
+./test/test.vo
+./test/.coq-native
+./test/.coq-native/Ntest_test.cmi
+./test/.coq-native/Ntest_test.cmx
+./test/.coq-native/Ntest_test.cmxs
+EOT
+exec diff -u desired actual
+
+fi
+exit 0 # test skipped