diff options
| author | Enrico Tassi | 2020-03-20 14:26:48 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2020-03-20 14:26:48 +0100 |
| commit | 5b7a6471cf812a708dbbb8943f30d525e46250f6 (patch) | |
| tree | caf236823940843f1609112162801250bf5dfdb6 /test-suite | |
| parent | 06b820259989a59080d0dc68bf0c633994fe221f (diff) | |
| parent | 57bc1b7921da4ae54ee5d3b999351f297556fd65 (diff) | |
Merge PR #11814: Document coq_makefile behavior wrt -native-compiler yes
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: gares
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 3 | ||||
| -rwxr-xr-x | test-suite/coq-makefile/native1/run.sh | 4 | ||||
| -rw-r--r-- | test-suite/coq-makefile/native2/_CoqProject | 10 | ||||
| -rwxr-xr-x | test-suite/coq-makefile/native2/run.sh | 33 |
4 files changed, 47 insertions, 3 deletions
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 |