Merge PR #13352: Configure default value of -native-compiler

Reviewed-by: erikmd
Reviewed-by: silene
Ack-by: mattam82
Ack-by: Blaisorblade
Ack-by: gares
Ack-by: Zimmi48
Ack-by: SkySkimmer
Ack-by: ejgallego

37 files changed, 142 insertions, 21 deletions

diff --git a/config/coq_config.mli b/config/coq_config.mli
index 12856cb6e6..809fa3d758 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -57,4 +57,5 @@ val wwwstdlib : string
 val localwwwrefman : string
 
 val bytecode_compiler : bool
-val native_compiler : bool
+type native_compiler = NativeOff | NativeOn of { ondemand : bool }
+val native_compiler : native_compiler
diff --git a/configure.ml b/configure.ml
index 6a4b1f9a75..e32f780a3d 100644
--- a/configure.ml
+++ b/configure.ml
@@ -225,6 +225,8 @@ let short_date, full_date = get_date ()
 
 type ide = Opt | Byte | No
 
+type nativecompiler = NativeYes | NativeNo | NativeOndemand
+
 type preferences = {
   prefix : string option;
   local : bool;
@@ -252,7 +254,7 @@ type preferences = {
   bin_annot : bool;
   annot : bool;
   bytecodecompiler : bool;
-  nativecompiler : bool;
+  nativecompiler : nativecompiler;
   coqwebsite : string;
   force_caml_version : bool;
   force_findlib_version : bool;
@@ -288,7 +290,8 @@ let default = {
   bin_annot = false;
   annot = false;
   bytecodecompiler = true;
-  nativecompiler = not (os_type_win32 || os_type_cygwin);
+  nativecompiler =
+    if os_type_win32 || os_type_cygwin then NativeNo else NativeOndemand;
   coqwebsite = "http://coq.inria.fr/";
   force_caml_version = false;
   force_findlib_version = false;
@@ -332,6 +335,12 @@ let get_ide = function
   | "no" -> No
   | s -> raise (Arg.Bad ("(opt|byte|no) argument expected instead of "^s))
 
+let get_native = function
+  | "yes" -> NativeYes
+  | "no" -> NativeNo
+  | "ondemand" -> NativeOndemand
+  | s -> raise (Arg.Bad ("(yes|no|ondemand) argument expected instead of "^s))
+
 let arg_bool f = Arg.String (fun s -> prefs := f !prefs (get_bool s))
 
 let arg_string f = Arg.String (fun s -> prefs := f !prefs s)
@@ -346,6 +355,8 @@ let arg_clear_option f = Arg.Unit (fun () -> prefs := f !prefs (Some false))
 
 let arg_ide f = Arg.String (fun s -> prefs := f !prefs (Some (get_ide s)))
 
+let arg_native f = Arg.String (fun s -> prefs := f !prefs (get_native s))
+
 let arg_profile = Arg.String (fun s -> prefs := Profiles.get s !prefs)
 
 (* TODO : earlier any option -foo was also available as --foo *)
@@ -407,8 +418,11 @@ let args_options = Arg.align [
     " Dumps ml binary annotation files while compiling Coq (e.g. for Merlin)";
   "-bytecode-compiler", arg_bool (fun p bytecodecompiler -> { p with bytecodecompiler }),
     "(yes|no) Enable Coq's bytecode reduction machine (VM)";
-  "-native-compiler", arg_bool (fun p nativecompiler -> { p with nativecompiler }),
-    "(yes|no) Compilation to native code for conversion and normalization";
+  "-native-compiler", arg_native (fun p nativecompiler -> { p with nativecompiler }),
+    "(yes|no|ondemand) Compilation to native code for conversion and normalization
+     yes: -native-compiler option of coqc will default to 'yes', stdlib will be precompiled
+     no: no native compilation available at all
+     ondemand (default): -native-compiler option of coqc will default to 'ondemand', stdlib will not be precompiled";
   "-coqwebsite", arg_string (fun p coqwebsite -> { p with coqwebsite }),
     " URL of the coq website";
   "-force-caml-version", arg_set (fun p force_caml_version -> { p with force_caml_version }),
@@ -991,6 +1005,9 @@ let esc s = if String.contains s ' ' then "\"" ^ s ^ "\"" else s
 
 (** * Summary of the configuration *)
 
+let pr_native = function
+  | NativeYes -> "yes" | NativeNo -> "no" | NativeOndemand -> "ondemand"
+
 let print_summary () =
   let pr s = printf s in
   pr "\n";
@@ -1016,7 +1033,7 @@ let print_summary () =
   pr "  Web browser                 : %s\n" browser;
   pr "  Coq web site                : %s\n" !prefs.coqwebsite;
   pr "  Bytecode VM enabled         : %B\n" !prefs.bytecodecompiler;
-  pr "  Native Compiler enabled     : %B\n\n" !prefs.nativecompiler;
+  pr "  Native Compiler enabled     : %s\n\n" (pr_native !prefs.nativecompiler);
   if !prefs.local then
     pr "  Local build, no installation...\n"
   else
@@ -1095,7 +1112,11 @@ let write_configml f =
   pr_s "wwwstdlib" (!prefs.coqwebsite ^ "distrib/V" ^ coq_version ^ "/stdlib/");
   pr_s "localwwwrefman"  ("file:/" ^ docdir ^ "/html/refman");
   pr_b "bytecode_compiler" !prefs.bytecodecompiler;
-  pr_b "native_compiler" !prefs.nativecompiler;
+  pr "type native_compiler = NativeOff | NativeOn of { ondemand : bool }\n";
+  pr "let native_compiler = %s\n"
+    (match !prefs.nativecompiler with
+     | NativeYes -> "NativeOn {ondemand=false}" | NativeNo -> "NativeOff"
+     | NativeOndemand -> "NativeOn {ondemand=true}");
 
   let core_src_dirs = [ "config"; "lib"; "clib"; "kernel"; "library";
                         "engine"; "pretyping"; "interp"; "gramlib"; "gramlib/.pack"; "parsing"; "proofs";
@@ -1217,7 +1238,7 @@ let write_makefile f =
   pr "# Option to control compilation and installation of the documentation\n";
   pr "WITHDOC=%s\n\n" (if !prefs.withdoc then "all" else "no");
   pr "# Option to produce precompiled files for native_compute\n";
-  pr "NATIVECOMPUTE=%s\n" (if !prefs.nativecompiler then "-native-compiler yes" else "");
+  pr "NATIVECOMPUTE=%s\n" (if !prefs.nativecompiler = NativeYes then "-native-compiler yes" else "");
   pr "COQWARNERROR=%s\n" (if !prefs.warn_error then "-w +default" else "");
   close_out o;
   Unix.chmod f 0o444
diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh
index 8570c34194..524555b69c 100755
--- a/dev/ci/ci-bedrock2.sh
+++ b/dev/ci/ci-bedrock2.sh
@@ -6,4 +6,5 @@ ci_dir="$(dirname "$0")"
 FORCE_GIT=1
 git_download bedrock2
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make && make install )
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index a0094b1006..72fc613c43 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")"
 
 git_download color
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/color" && make )
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index 9cb7a65ab5..6b09726606 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -5,6 +5,7 @@ ci_dir="$(dirname "$0")"
 
 git_download compcert
 
+export COQCOPTS='-native-compiler no -w -undeclared-scope -w -omega-is-deprecated'
 ( cd "${CI_BUILD_DIR}/compcert" && \
       ./configure -ignore-coq-version x86_32-linux && \
       make && \
diff --git a/dev/ci/ci-coqprime.sh b/dev/ci/ci-coqprime.sh
index a4fd296896..e12c36e6a7 100755
--- a/dev/ci/ci-coqprime.sh
+++ b/dev/ci/ci-coqprime.sh
@@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")"
 
 git_download coqprime
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/coqprime" && make && make install)
diff --git a/dev/ci/ci-corn.sh b/dev/ci/ci-corn.sh
index ac3978dc8d..785ff4c2ad 100755
--- a/dev/ci/ci-corn.sh
+++ b/dev/ci/ci-corn.sh
@@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")"
 
 git_download corn
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/corn" && ./configure.sh && make && make install )
diff --git a/dev/ci/ci-engine_bench.sh b/dev/ci/ci-engine_bench.sh
index fda7649f88..d976356dd4 100755
--- a/dev/ci/ci-engine_bench.sh
+++ b/dev/ci/ci-engine_bench.sh
@@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")"
 
 git_download engine_bench
 
+export COQEXTRAFLAGS='-native-compiler ondemand'
 ( cd "${CI_BUILD_DIR}/engine_bench" && make coq && make coq-perf-Sanity )
diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh
index 30047e624b..3eda7161c1 100755
--- a/dev/ci/ci-equations.sh
+++ b/dev/ci/ci-equations.sh
@@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")"
 
 git_download equations
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci && make install )
diff --git a/dev/ci/ci-fiat_crypto.sh b/dev/ci/ci-fiat_crypto.sh
index 3ecdb32a51..e8fa8c0be4 100755
--- a/dev/ci/ci-fiat_crypto.sh
+++ b/dev/ci/ci-fiat_crypto.sh
@@ -18,6 +18,7 @@ fiat_crypto_CI_MAKE_ARGS="EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1"
 fiat_crypto_CI_TARGETS1="${fiat_crypto_CI_MAKE_ARGS} pre-standalone-extracted printlite lite"
 fiat_crypto_CI_TARGETS2="${fiat_crypto_CI_MAKE_ARGS} all-except-compiled"
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \
         ulimit -s ${fiat_crypto_CI_STACKSIZE} && \
         make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} )
diff --git a/dev/ci/ci-fiat_crypto_legacy.sh b/dev/ci/ci-fiat_crypto_legacy.sh
index 6d0a803401..57cc121bb4 100755
--- a/dev/ci/ci-fiat_crypto_legacy.sh
+++ b/dev/ci/ci-fiat_crypto_legacy.sh
@@ -9,5 +9,6 @@ git_download fiat_crypto_legacy
 fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite-hardcoded old-pipeline-lite-hardcoded lite-display-hardcoded"
 fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem-hardcoded old-pipeline-nobigmem-hardcoded nonautogenerated-specific nonautogenerated-specific-display selected-specific selected-specific-display"
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && git submodule update --init --recursive && \
   make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} )
diff --git a/dev/ci/ci-fiat_crypto_ocaml.sh b/dev/ci/ci-fiat_crypto_ocaml.sh
index 20d3deb14f..c63690d5c9 100755
--- a/dev/ci/ci-fiat_crypto_ocaml.sh
+++ b/dev/ci/ci-fiat_crypto_ocaml.sh
@@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")"
 
 fiat_crypto_CI_MAKE_ARGS="EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1"
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/fiat_crypto" && make ${fiat_crypto_CI_MAKE_ARGS} standalone-ocaml lite-generated-files )
diff --git a/dev/ci/ci-fiat_parsers.sh b/dev/ci/ci-fiat_parsers.sh
index ac74ebf667..8409e25bdc 100755
--- a/dev/ci/ci-fiat_parsers.sh
+++ b/dev/ci/ci-fiat_parsers.sh
@@ -6,4 +6,5 @@ ci_dir="$(dirname "$0")"
 FORCE_GIT=1
 git_download fiat_parsers
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/fiat_parsers" && make parsers parsers-examples && make fiat-core )
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 4b92c8cb4d..679bef3b5e 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -5,4 +5,6 @@ ci_dir="$(dirname "$0")"
 
 git_download hott
 
-( cd "${CI_BUILD_DIR}/hott" && ./autogen.sh -skip-submodules && ./configure && make && make validate )
+( cd "${CI_BUILD_DIR}/hott" && ./autogen.sh -skip-submodules && ./configure \
+      && sed -i.bak 's/\(HOQC =.*\)/\1 -native-compiler no/' Makefile \
+      && make && make validate )
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
index 27876d68de..813ea9b07a 100755
--- a/dev/ci/ci-metacoq.sh
+++ b/dev/ci/ci-metacoq.sh
@@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")"
 
 git_download metacoq
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/metacoq" && ./configure.sh local && make .merlin && make ci-local && make install )
diff --git a/dev/ci/ci-perennial.sh b/dev/ci/ci-perennial.sh
index 306cbdf63c..43add8254a 100755
--- a/dev/ci/ci-perennial.sh
+++ b/dev/ci/ci-perennial.sh
@@ -6,4 +6,5 @@ ci_dir="$(dirname "$0")"
 FORCE_GIT=1
 git_download perennial
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/perennial" && git submodule update --init --recursive && make TIMED=false lite )
diff --git a/dev/ci/ci-rewriter.sh b/dev/ci/ci-rewriter.sh
index 235482ffeb..ec7ac5bddc 100755
--- a/dev/ci/ci-rewriter.sh
+++ b/dev/ci/ci-rewriter.sh
@@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")"
 
 git_download rewriter
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/rewriter" && make && make install)
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
index 704e278a4b..3d320617f2 100755
--- a/dev/ci/ci-unimath.sh
+++ b/dev/ci/ci-unimath.sh
@@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")"
 
 git_download unimath
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/unimath" && make BUILD_COQ=no )
diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh
index 4a332406a2..a151cf0ba6 100755
--- a/dev/ci/ci-vst.sh
+++ b/dev/ci/ci-vst.sh
@@ -7,4 +7,5 @@ git_download vst
 
 export COMPCERT=bundled
 
+sed -i.bak 's/\(COQC=.*\)/\1 -native-compiler no/' ${CI_BUILD_DIR}/vst/Makefile
 ( cd "${CI_BUILD_DIR}/vst" && make IGNORECOQVERSION=true )
diff --git a/doc/changelog/07-commands-and-options/13352-cep-48.rst b/doc/changelog/07-commands-and-options/13352-cep-48.rst
new file mode 100644
index 0000000000..cb2eeea74b
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/13352-cep-48.rst
@@ -0,0 +1,12 @@
+- **Changed:**
+  Option -native-compiler of the configure script now impacts the
+  default value of the option -native-compiler of coqc. The
+  -native-compiler option of the configure script is added an ondemand
+  value, which becomes the default, thus preserving the previous default
+  behavior.
+  The stdlib is still precompiled when configuring with -native-compiler
+  yes. It is not precompiled otherwise.
+  This an implementation of point 2 of
+  `CEP #48 <https://github.com/coq/ceps/pull/48>`_
+  (`#13352 <https://github.com/coq/coq/pull/13352>`_,
+  by Pierre Roux).
diff --git a/lib/envars.ml b/lib/envars.ml
index c9c97eaa97..585d5185b4 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -181,5 +181,9 @@ let print_config ?(prefix_var_name="") f coq_src_subdirs =
   fprintf f "%sWARN=%s\n" prefix_var_name "-warn-error +a-3";
   fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name
     (if Coq_config.has_natdynlink then "true" else "false");
-  fprintf f "%sCOQ_SRC_SUBDIRS=%s\n" prefix_var_name (String.concat " " coq_src_subdirs)
-
+  fprintf f "%sCOQ_SRC_SUBDIRS=%s\n" prefix_var_name (String.concat " " coq_src_subdirs);
+  fprintf f "%sCOQ_NATIVE_COMPILER_DEFAULT=%s\n" prefix_var_name
+    (match Coq_config.native_compiler with
+     | Coq_config.NativeOn {ondemand=false} -> "yes"
+     | Coq_config.NativeOff -> "no"
+     | Coq_config.NativeOn {ondemand=true} -> "ondemand")
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 279f32c903..6a7cc0428c 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -252,7 +252,12 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+	  (echo "\
+	     bugs/closed/bug_3783.v \
+	     bugs/closed/bug_4157.v \
+	     bugs/closed/bug_5127.v \
+	   " | grep -q "$<") && no_native="-native-compiler no"; \
+	  $(coqc) $$no_native "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh
index 88237815b1..d878b13ce6 100755
--- a/test-suite/coq-makefile/coqdoc1/run.sh
+++ b/test-suite/coq-makefile/coqdoc1/run.sh
@@ -21,6 +21,10 @@ make install-doc DSTROOT="$PWD/tmp"
 sort -u > desired <<EOT
 .
 ./test
+./test/.coq-native
+./test/.coq-native/Ntest_test.cmi
+./test/.coq-native/Ntest_test.cmx
+./test/.coq-native/Ntest_test.cmxs
 ./test/test_plugin.cmi
 ./test/test_plugin.cmx
 ./test/test_plugin.cmxa
@@ -29,6 +33,10 @@ sort -u > desired <<EOT
 ./test/test.v
 ./test/test.vo
 ./test/sub
+./test/sub/.coq-native
+./test/sub/.coq-native/Ntest_sub_testsub.cmi
+./test/sub/.coq-native/Ntest_sub_testsub.cmx
+./test/sub/.coq-native/Ntest_sub_testsub.cmxs
 ./test/sub/testsub.glob
 ./test/sub/testsub.v
 ./test/sub/testsub.vo
@@ -56,4 +64,5 @@ sort -u > desired <<EOT
 ./test/html/coqdoc.css
 ./test/html/test.test.html
 EOT
+(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired
 exec diff -u desired actual
diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh
index 5811dd17e4..757667e8bd 100755
--- a/test-suite/coq-makefile/coqdoc2/run.sh
+++ b/test-suite/coq-makefile/coqdoc2/run.sh
@@ -19,6 +19,10 @@ make install-doc DSTROOT="$PWD/tmp"
 sort -u > desired <<EOT
 .
 ./test
+./test/.coq-native
+./test/.coq-native/Ntest_test.cmi
+./test/.coq-native/Ntest_test.cmx
+./test/.coq-native/Ntest_test.cmxs
 ./test/test_plugin.cmi
 ./test/test_plugin.cmx
 ./test/test_plugin.cmxa
@@ -27,6 +31,10 @@ sort -u > desired <<EOT
 ./test/test.v
 ./test/test.vo
 ./test/sub
+./test/sub/.coq-native
+./test/sub/.coq-native/Ntest_sub_testsub.cmi
+./test/sub/.coq-native/Ntest_sub_testsub.cmx
+./test/sub/.coq-native/Ntest_sub_testsub.cmxs
 ./test/sub/testsub.glob
 ./test/sub/testsub.v
 ./test/sub/testsub.vo
@@ -54,4 +62,5 @@ sort -u > desired <<EOT
 ./test/html/coqdoc.css
 ./test/html/test.test.html
 EOT
+(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired
 exec diff -u desired actual
diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh
index bbd2fc460c..113a862d97 100755
--- a/test-suite/coq-makefile/mlpack1/run.sh
+++ b/test-suite/coq-makefile/mlpack1/run.sh
@@ -12,6 +12,10 @@ make install DSTROOT="$PWD/tmp"
 sort > desired <<EOT
 .
 ./test
+./test/.coq-native
+./test/.coq-native/Ntest_test.cmi
+./test/.coq-native/Ntest_test.cmx
+./test/.coq-native/Ntest_test.cmxs
 ./test/test.glob
 ./test/test_plugin.cmi
 ./test/test_plugin.cmx
@@ -20,4 +24,5 @@ sort > desired <<EOT
 ./test/test.v
 ./test/test.vo
 EOT
+(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired
 exec diff -u desired actual
diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh
index bbd2fc460c..113a862d97 100755
--- a/test-suite/coq-makefile/mlpack2/run.sh
+++ b/test-suite/coq-makefile/mlpack2/run.sh
@@ -12,6 +12,10 @@ make install DSTROOT="$PWD/tmp"
 sort > desired <<EOT
 .
 ./test
+./test/.coq-native
+./test/.coq-native/Ntest_test.cmi
+./test/.coq-native/Ntest_test.cmx
+./test/.coq-native/Ntest_test.cmxs
 ./test/test.glob
 ./test/test_plugin.cmi
 ./test/test_plugin.cmx
@@ -20,4 +24,5 @@ sort > desired <<EOT
 ./test/test.v
 ./test/test.vo
 EOT
+(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired
 exec diff -u desired actual
diff --git a/test-suite/coq-makefile/multiroot/run.sh b/test-suite/coq-makefile/multiroot/run.sh
index 45bf1481df..be0d04f93d 100755
--- a/test-suite/coq-makefile/multiroot/run.sh
+++ b/test-suite/coq-makefile/multiroot/run.sh
@@ -20,6 +20,10 @@ make install-doc DSTROOT="$PWD/tmp"
 sort > desired <<EOT
 .
 ./test
+./test/.coq-native
+./test/.coq-native/Ntest_test.cmi
+./test/.coq-native/Ntest_test.cmx
+./test/.coq-native/Ntest_test.cmxs
 ./test/test.glob
 ./test/test.cmi
 ./test/test.cmx
@@ -30,6 +34,10 @@ sort > desired <<EOT
 ./test/test.v
 ./test/test.vo
 ./test2
+./test2/.coq-native
+./test2/.coq-native/Ntest2_test.cmi
+./test2/.coq-native/Ntest2_test.cmx
+./test2/.coq-native/Ntest2_test.cmxs
 ./test2/test.glob
 ./test2/test.v
 ./test2/test.vo
@@ -58,4 +66,5 @@ sort > desired <<EOT
 ./orphan_test_test2_test/mlihtml/type_Test_aux.html
 ./orphan_test_test2_test/mlihtml/type_Test.html
 EOT
+(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired
 exec diff -u desired actual
diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh
index 3ffe831b3c..5dd36757be 100755
--- a/test-suite/coq-makefile/native1/run.sh
+++ b/test-suite/coq-makefile/native1/run.sh
@@ -1,6 +1,6 @@
 #!/usr/bin/env bash
 
-NONATIVECOMP=$(grep "let native_compiler = false" ../../../config/coq_config.ml)||true
+NONATIVECOMP=$(grep "let native_compiler = NativeOff" ../../../config/coq_config.ml)||true
 if [[ $(which ocamlopt) && ! $NONATIVECOMP ]]; then
 
 . ../template/init.sh
diff --git a/test-suite/coq-makefile/native2/run.sh b/test-suite/coq-makefile/native2/run.sh
index aaae81630f..47befc50c3 100755
--- a/test-suite/coq-makefile/native2/run.sh
+++ b/test-suite/coq-makefile/native2/run.sh
@@ -1,6 +1,6 @@
 #!/usr/bin/env bash
 
-NONATIVECOMP=$(grep "let native_compiler = false" ../../../config/coq_config.ml)||true
+NONATIVECOMP=$(grep "let native_compiler = NativeOff" ../../../config/coq_config.ml)||true
 if [[ $(which ocamlopt) && ! $NONATIVECOMP ]]; then
 
 . ../template/init.sh
diff --git a/test-suite/coq-makefile/plugin1/run.sh b/test-suite/coq-makefile/plugin1/run.sh
index 1e2bd979b3..f69e8c1b8c 100755
--- a/test-suite/coq-makefile/plugin1/run.sh
+++ b/test-suite/coq-makefile/plugin1/run.sh
@@ -13,6 +13,10 @@ make install DSTROOT="$PWD/tmp"
 sort > desired <<EOT
 .
 ./test
+./test/.coq-native
+./test/.coq-native/Ntest_test.cmi
+./test/.coq-native/Ntest_test.cmx
+./test/.coq-native/Ntest_test.cmxs
 ./test/test.glob
 ./test/test.cmi
 ./test/test.cmx
@@ -23,4 +27,5 @@ sort > desired <<EOT
 ./test/test.v
 ./test/test.vo
 EOT
+(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired
 exec diff -u desired actual
diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh
index 1e2bd979b3..f69e8c1b8c 100755
--- a/test-suite/coq-makefile/plugin2/run.sh
+++ b/test-suite/coq-makefile/plugin2/run.sh
@@ -13,6 +13,10 @@ make install DSTROOT="$PWD/tmp"
 sort > desired <<EOT
 .
 ./test
+./test/.coq-native
+./test/.coq-native/Ntest_test.cmi
+./test/.coq-native/Ntest_test.cmx
+./test/.coq-native/Ntest_test.cmxs
 ./test/test.glob
 ./test/test.cmi
 ./test/test.cmx
@@ -23,4 +27,5 @@ sort > desired <<EOT
 ./test/test.v
 ./test/test.vo
 EOT
+(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired
 exec diff -u desired actual
diff --git a/test-suite/coq-makefile/plugin3/run.sh b/test-suite/coq-makefile/plugin3/run.sh
index 1e2bd979b3..f69e8c1b8c 100755
--- a/test-suite/coq-makefile/plugin3/run.sh
+++ b/test-suite/coq-makefile/plugin3/run.sh
@@ -13,6 +13,10 @@ make install DSTROOT="$PWD/tmp"
 sort > desired <<EOT
 .
 ./test
+./test/.coq-native
+./test/.coq-native/Ntest_test.cmi
+./test/.coq-native/Ntest_test.cmx
+./test/.coq-native/Ntest_test.cmxs
 ./test/test.glob
 ./test/test.cmi
 ./test/test.cmx
@@ -23,4 +27,5 @@ sort > desired <<EOT
 ./test/test.v
 ./test/test.vo
 EOT
+(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired
 exec diff -u desired actual
diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh
index ed5a4f93f5..426c9ea53f 100755
--- a/test-suite/coq-makefile/timing/run.sh
+++ b/test-suite/coq-makefile/timing/run.sh
@@ -3,6 +3,9 @@
 #set -x
 set -e
 
+NONATIVECOMP=$(grep "let native_compiler = NativeOff" ../../../config/coq_config.ml)||true
+if [[ ! $NONATIVECOMP ]]; then exit 0 ; fi
+
 . ../template/path-init.sh
 
 # reset MAKEFLAGS so that, e.g., `make -C test-suite -B coq-makefile` doesn't give us issues
diff --git a/test-suite/coq-makefile/uninstall1/run.sh b/test-suite/coq-makefile/uninstall1/run.sh
index fc95d84b9a..0f05acd072 100755
--- a/test-suite/coq-makefile/uninstall1/run.sh
+++ b/test-suite/coq-makefile/uninstall1/run.sh
@@ -19,5 +19,8 @@ make uninstall-doc DSTROOT="$PWD/tmp"
 ) | sort -u > actual
 sort -u > desired <<EOT
 .
+./test
+./test/sub
 EOT
+(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/test/d' desired
 exec diff -u desired actual
diff --git a/test-suite/coq-makefile/uninstall2/run.sh b/test-suite/coq-makefile/uninstall2/run.sh
index fc95d84b9a..0f05acd072 100755
--- a/test-suite/coq-makefile/uninstall2/run.sh
+++ b/test-suite/coq-makefile/uninstall2/run.sh
@@ -19,5 +19,8 @@ make uninstall-doc DSTROOT="$PWD/tmp"
 ) | sort -u > actual
 sort -u > desired <<EOT
 .
+./test
+./test/sub
 EOT
+(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/test/d' desired
 exec diff -u desired actual
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index c6ccf2a427..ec339c69c6 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -36,7 +36,8 @@ let set_type_in_type () =
 
 type color = [`ON | `AUTO | `EMACS | `OFF]
 
-type native_compiler = NativeOff | NativeOn of { ondemand : bool }
+type native_compiler = Coq_config.native_compiler =
+  NativeOff | NativeOn of { ondemand : bool }
 
 type coqargs_logic_config = {
   impredicative_set : Declarations.set_predicativity;
@@ -96,10 +97,7 @@ type t = {
 
 let default_toplevel = Names.(DirPath.make [Id.of_string "Top"])
 
-let default_native =
-  if Coq_config.native_compiler
-  then NativeOn {ondemand=true}
-  else NativeOff
+let default_native = Coq_config.native_compiler
 
 let default_logic_config = {
   impredicative_set = Declarations.PredicativeSet;
@@ -301,7 +299,7 @@ let get_native_compiler s =
     | ("no" | "off") -> NativeOff
     | _ ->
        error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler") in
-  if not Coq_config.native_compiler && n <> NativeOff then
+  if Coq_config.native_compiler = NativeOff && n <> NativeOff then
     let () = warn_no_native_compiler s in
     NativeOff
   else
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index c8634b7847..f6222e4ec4 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -12,7 +12,8 @@ type color = [`ON | `AUTO | `EMACS | `OFF]
 
 val default_toplevel : Names.DirPath.t
 
-type native_compiler = NativeOff | NativeOn of { ondemand : bool }
+type native_compiler = Coq_config.native_compiler =
+  NativeOff | NativeOn of { ondemand : bool }
 
 type coqargs_logic_config = {
   impredicative_set : Declarations.set_predicativity;