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

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

6 files changed, 84 insertions, 5 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 621374da0e..4a053ec03f 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -69,6 +69,7 @@ before_script:
       - _install_ci
       - config/Makefile
       - config/coq_config.py
+      - config/coq_config.ml
       - test-suite/misc/universes/all_stdlib.v
     expire_in: 1 week
   script:
@@ -172,7 +173,7 @@ before_script:
     - BIN=$(readlink -f ../_install_ci/bin)/
     - LIB=$(readlink -f ../_install_ci/lib/coq)/
     - export OCAMLPATH=$(readlink -f ../_install_ci/lib/):"$OCAMLPATH"
-    - make -j "$NJOBS" BIN="$BIN" COQLIB="$LIB" COQFLAGS="${COQFLAGS}" all
+    - COQEXTRAFLAGS="${COQEXTRAFLAGS}" make -j "$NJOBS" BIN="$BIN" COQLIB="$LIB" all
   artifacts:
     name: "$CI_JOB_NAME.logs"
     when: on_failure
@@ -531,7 +532,7 @@ test-suite:base+async:
   needs:
     - build:base
   variables:
-    COQFLAGS: "-async-proofs on -async-proofs-cache force"
+    COQEXTRAFLAGS: "-async-proofs on -async-proofs-cache force"
   timeout: 100m
   allow_failure: true
   only:
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/Makefile b/test-suite/Makefile
index aca7ab0b28..6696f1431e 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -49,7 +49,8 @@ endif
 endif # exists ../_build
 export COQLIB
 
-COQFLAGS?=
+COQEXTRAFLAGS?=
+COQFLAGS?=$(COQEXTRAFLAGS)
 
 coqc := $(BIN)coqc -q -R prerequisite TestSuite $(COQFLAGS)
 coqchk := $(BIN)coqchk -R prerequisite TestSuite
diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh
index 8f9ab9a711..3ffe831b3c 100755
--- a/test-suite/coq-makefile/native1/run.sh
+++ b/test-suite/coq-makefile/native1/run.sh
@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 
-NATIVECOMP=$(grep "let no_native_compiler = false" ../../../config/coq_config.ml)||true
-if [[ $(which ocamlopt) && $NATIVECOMP ]]; then
+NONATIVECOMP=$(grep "let native_compiler = false" ../../../config/coq_config.ml)||true
+if [[ $(which ocamlopt) && ! $NONATIVECOMP ]]; then
 
 . ../template/init.sh
 
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