From 0fdc7435d8b3666b17a9270375f5377fa340a773 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sat, 14 Mar 2020 18:42:54 +0100
Subject: Fix coq-makefile/native1 test

This was accidentaly disabled by #6264 when no_native_compiler was
renamed to native_compiler.

Moreover, the (then unactivated test) was broken by commit 48ae6ce
(part of #9088).
---
 test-suite/Makefile                    | 3 ++-
 test-suite/coq-makefile/native1/run.sh | 4 ++--
 2 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 1681150f7b..3703d97c88 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
 
-- 
cgit v1.2.3


From 57bc1b7921da4ae54ee5d3b999351f297556fd65 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 12 Mar 2020 22:47:03 +0100
Subject: Document coq_makefile behavior wrt -native-compiler yes

---
 test-suite/coq-makefile/native2/_CoqProject | 10 +++++++++
 test-suite/coq-makefile/native2/run.sh      | 33 +++++++++++++++++++++++++++++
 2 files changed, 43 insertions(+)
 create mode 100644 test-suite/coq-makefile/native2/_CoqProject
 create mode 100755 test-suite/coq-makefile/native2/run.sh

(limited to 'test-suite')

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
-- 
cgit v1.2.3