diff options
| author | Pierre Roux | 2020-03-12 22:47:03 +0100 |
|---|---|---|
| committer | Pierre Roux | 2020-03-16 11:43:43 +0100 |
| commit | 57bc1b7921da4ae54ee5d3b999351f297556fd65 (patch) | |
| tree | caab21fedfaf30319d95f999f965b1177e353c0b /test-suite | |
| parent | 0fdc7435d8b3666b17a9270375f5377fa340a773 (diff) | |
Document coq_makefile behavior wrt -native-compiler yes
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/coq-makefile/native2/_CoqProject | 10 | ||||
| -rwxr-xr-x | test-suite/coq-makefile/native2/run.sh | 33 |
2 files changed, 43 insertions, 0 deletions
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 |