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

14 files changed, 69 insertions, 3 deletions

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