diff options
Diffstat (limited to 'test-suite/coq-makefile')
47 files changed, 715 insertions, 0 deletions
diff --git a/test-suite/coq-makefile/arg/_CoqProject b/test-suite/coq-makefile/arg/_CoqProject new file mode 100644 index 000000000..afdb32e7c --- /dev/null +++ b/test-suite/coq-makefile/arg/_CoqProject @@ -0,0 +1,11 @@ +-R theories test +-R src test +-I src +-arg "-compat 8.4" + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/arg/run.sh b/test-suite/coq-makefile/arg/run.sh new file mode 100755 index 000000000..e98da17c7 --- /dev/null +++ b/test-suite/coq-makefile/arg/run.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +#set -x +set -e + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +make diff --git a/test-suite/coq-makefile/compat-subdirs/_CoqProject b/test-suite/coq-makefile/compat-subdirs/_CoqProject new file mode 100644 index 000000000..4f44bde22 --- /dev/null +++ b/test-suite/coq-makefile/compat-subdirs/_CoqProject @@ -0,0 +1,11 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v +subdir/ diff --git a/test-suite/coq-makefile/compat-subdirs/run.sh b/test-suite/coq-makefile/compat-subdirs/run.sh new file mode 100755 index 000000000..28d9878f9 --- /dev/null +++ b/test-suite/coq-makefile/compat-subdirs/run.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +#set -x +set -e + +. ../template/init.sh +coq_makefile -f _CoqProject -o Makefile +make +exec test -f "subdir/done" diff --git a/test-suite/coq-makefile/compat-subdirs/subdir/Makefile b/test-suite/coq-makefile/compat-subdirs/subdir/Makefile new file mode 100644 index 000000000..846c9b791 --- /dev/null +++ b/test-suite/coq-makefile/compat-subdirs/subdir/Makefile @@ -0,0 +1,3 @@ +all: + test -f ../theories/test.vo + touch done diff --git a/test-suite/coq-makefile/coqdoc1/_CoqProject b/test-suite/coq-makefile/coqdoc1/_CoqProject new file mode 100644 index 000000000..35792066b --- /dev/null +++ b/test-suite/coq-makefile/coqdoc1/_CoqProject @@ -0,0 +1,11 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v +theories/sub/testsub.v diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh new file mode 100755 index 000000000..d6bb52bb4 --- /dev/null +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -0,0 +1,54 @@ +#!/usr/bin/env bash + +#set -x +set -e + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +make +make html mlihtml +make install DSTROOT="$PWD/tmp" +make install-doc DSTROOT="$PWD/tmp" +#make debug +(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual +sort -u > desired <<EOT +. +./test +./test/test_plugin.cma +./test/test_plugin.cmi +./test/test_plugin.cmo +./test/test_plugin.cmx +./test/test_plugin.cmxs +./test/test.glob +./test/test.v +./test/test.vo +./test/sub +./test/sub/testsub.glob +./test/sub/testsub.v +./test/sub/testsub.vo +./test/mlihtml +./test/mlihtml/index_exceptions.html +./test/mlihtml/index.html +./test/mlihtml/index_class_types.html +./test/mlihtml/type_Test_aux.html +./test/mlihtml/index_module_types.html +./test/mlihtml/index_classes.html +./test/mlihtml/type_Test.html +./test/mlihtml/style.css +./test/mlihtml/index_attributes.html +./test/mlihtml/index_types.html +./test/mlihtml/Test_aux.html +./test/mlihtml/index_values.html +./test/mlihtml/Test.html +./test/mlihtml/index_extensions.html +./test/mlihtml/index_methods.html +./test/mlihtml/index_modules.html +./test/html +./test/html/index.html +./test/html/test.sub.testsub.html +./test/html/toc.html +./test/html/coqdoc.css +./test/html/test.test.html +EOT +exec diff -u desired actual diff --git a/test-suite/coq-makefile/coqdoc2/_CoqProject b/test-suite/coq-makefile/coqdoc2/_CoqProject new file mode 100644 index 000000000..d2a547d47 --- /dev/null +++ b/test-suite/coq-makefile/coqdoc2/_CoqProject @@ -0,0 +1,11 @@ +-R src/ test +-R theories/ test +-I src/ + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v +theories/sub/testsub.v diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh new file mode 100755 index 000000000..d6bb52bb4 --- /dev/null +++ b/test-suite/coq-makefile/coqdoc2/run.sh @@ -0,0 +1,54 @@ +#!/usr/bin/env bash + +#set -x +set -e + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +make +make html mlihtml +make install DSTROOT="$PWD/tmp" +make install-doc DSTROOT="$PWD/tmp" +#make debug +(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual +sort -u > desired <<EOT +. +./test +./test/test_plugin.cma +./test/test_plugin.cmi +./test/test_plugin.cmo +./test/test_plugin.cmx +./test/test_plugin.cmxs +./test/test.glob +./test/test.v +./test/test.vo +./test/sub +./test/sub/testsub.glob +./test/sub/testsub.v +./test/sub/testsub.vo +./test/mlihtml +./test/mlihtml/index_exceptions.html +./test/mlihtml/index.html +./test/mlihtml/index_class_types.html +./test/mlihtml/type_Test_aux.html +./test/mlihtml/index_module_types.html +./test/mlihtml/index_classes.html +./test/mlihtml/type_Test.html +./test/mlihtml/style.css +./test/mlihtml/index_attributes.html +./test/mlihtml/index_types.html +./test/mlihtml/Test_aux.html +./test/mlihtml/index_values.html +./test/mlihtml/Test.html +./test/mlihtml/index_extensions.html +./test/mlihtml/index_methods.html +./test/mlihtml/index_modules.html +./test/html +./test/html/index.html +./test/html/test.sub.testsub.html +./test/html/toc.html +./test/html/coqdoc.css +./test/html/test.test.html +EOT +exec diff -u desired actual diff --git a/test-suite/coq-makefile/extend-subdirs/Makefile.local b/test-suite/coq-makefile/extend-subdirs/Makefile.local new file mode 100644 index 000000000..b031d30db --- /dev/null +++ b/test-suite/coq-makefile/extend-subdirs/Makefile.local @@ -0,0 +1,4 @@ +pre-all:: + $(MAKE) -C subdir pre +post-all:: + $(MAKE) -C subdir post diff --git a/test-suite/coq-makefile/extend-subdirs/_CoqProject b/test-suite/coq-makefile/extend-subdirs/_CoqProject new file mode 100644 index 000000000..69f47302e --- /dev/null +++ b/test-suite/coq-makefile/extend-subdirs/_CoqProject @@ -0,0 +1,10 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/extend-subdirs/run.sh b/test-suite/coq-makefile/extend-subdirs/run.sh new file mode 100755 index 000000000..ea5792a93 --- /dev/null +++ b/test-suite/coq-makefile/extend-subdirs/run.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +#set -x +set -e + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +make +exec test -f "subdir/done" diff --git a/test-suite/coq-makefile/extend-subdirs/subdir/Makefile b/test-suite/coq-makefile/extend-subdirs/subdir/Makefile new file mode 100644 index 000000000..23f52b154 --- /dev/null +++ b/test-suite/coq-makefile/extend-subdirs/subdir/Makefile @@ -0,0 +1,5 @@ +pre: + test ! -f ../theories/test.vo +post: + test -f ../theories/test.vo + touch done diff --git a/test-suite/coq-makefile/latex1/_CoqProject b/test-suite/coq-makefile/latex1/_CoqProject new file mode 100644 index 000000000..35792066b --- /dev/null +++ b/test-suite/coq-makefile/latex1/_CoqProject @@ -0,0 +1,11 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v +theories/sub/testsub.v diff --git a/test-suite/coq-makefile/latex1/run.sh b/test-suite/coq-makefile/latex1/run.sh new file mode 100755 index 000000000..214a9d5b2 --- /dev/null +++ b/test-suite/coq-makefile/latex1/run.sh @@ -0,0 +1,15 @@ +#!/usr/bin/env bash + +#set -x +set -e + +if which pdflatex; then + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +make +exec make all.pdf + +fi +exit 0 # test skipped diff --git a/test-suite/coq-makefile/merlin1/_CoqProject b/test-suite/coq-makefile/merlin1/_CoqProject new file mode 100644 index 000000000..69f47302e --- /dev/null +++ b/test-suite/coq-makefile/merlin1/_CoqProject @@ -0,0 +1,10 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/merlin1/run.sh b/test-suite/coq-makefile/merlin1/run.sh new file mode 100755 index 000000000..752c0c2ce --- /dev/null +++ b/test-suite/coq-makefile/merlin1/run.sh @@ -0,0 +1,15 @@ +#!/usr/bin/env bash + +#set -x +set -e + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +make .merlin +cat > desired <<EOT +B src +S src +EOT +tail -2 .merlin > actual +exec diff -u desired actual diff --git a/test-suite/coq-makefile/mlpack1/_CoqProject b/test-suite/coq-makefile/mlpack1/_CoqProject new file mode 100644 index 000000000..69f47302e --- /dev/null +++ b/test-suite/coq-makefile/mlpack1/_CoqProject @@ -0,0 +1,10 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh new file mode 100755 index 000000000..f6fb3bcb4 --- /dev/null +++ b/test-suite/coq-makefile/mlpack1/run.sh @@ -0,0 +1,26 @@ +#!/usr/bin/env bash + +#set -x +set -e + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +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.cma +./test/test_plugin.cmi +./test/test_plugin.cmo +./test/test_plugin.cmx +./test/test_plugin.cmxs +./test/test.v +./test/test.vo +EOT +exec diff -u desired actual diff --git a/test-suite/coq-makefile/mlpack2/_CoqProject b/test-suite/coq-makefile/mlpack2/_CoqProject new file mode 100644 index 000000000..51864a87a --- /dev/null +++ b/test-suite/coq-makefile/mlpack2/_CoqProject @@ -0,0 +1,10 @@ +-R src/ test +-R theories/ test +-I src/ + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh new file mode 100755 index 000000000..f6fb3bcb4 --- /dev/null +++ b/test-suite/coq-makefile/mlpack2/run.sh @@ -0,0 +1,26 @@ +#!/usr/bin/env bash + +#set -x +set -e + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +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.cma +./test/test_plugin.cmi +./test/test_plugin.cmo +./test/test_plugin.cmx +./test/test_plugin.cmxs +./test/test.v +./test/test.vo +EOT +exec diff -u desired actual diff --git a/test-suite/coq-makefile/multiroot/_CoqProject b/test-suite/coq-makefile/multiroot/_CoqProject new file mode 100644 index 000000000..b384bb6d9 --- /dev/null +++ b/test-suite/coq-makefile/multiroot/_CoqProject @@ -0,0 +1,12 @@ +-R theories/ test +-R theories2 test2 +-R src/ test +-I src/ + +./src/test_plugin.mllib +./src/test.ml4 +./src/test.mli +./src/test_aux.ml +./src/test_aux.mli +./theories/test.v +./theories2/test.v diff --git a/test-suite/coq-makefile/multiroot/run.sh b/test-suite/coq-makefile/multiroot/run.sh new file mode 100755 index 000000000..863c39f50 --- /dev/null +++ b/test-suite/coq-makefile/multiroot/run.sh @@ -0,0 +1,61 @@ +#!/usr/bin/env bash + +#set -x +set -e + +. ../template/init.sh + +cp -r theories theories2 +mv src/test_plugin.mlpack src/test_plugin.mllib +coq_makefile -f _CoqProject -o Makefile +make +make html mlihtml +make install DSTROOT="$PWD/tmp" +make install-doc DSTROOT="$PWD/tmp" +#make debug +(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual +sort > desired <<EOT +. +./test +./test/test.glob +./test/test.cmi +./test/test.cmo +./test/test.cmx +./test/test_aux.cmi +./test/test_aux.cmo +./test/test_aux.cmx +./test/test_plugin.cma +./test/test_plugin.cmxa +./test/test_plugin.cmxs +./test/test.v +./test/test.vo +./test2 +./test2/test.glob +./test2/test.v +./test2/test.vo +./orphan_test_test2_test +./orphan_test_test2_test/html +./orphan_test_test2_test/html/coqdoc.css +./orphan_test_test2_test/html/index.html +./orphan_test_test2_test/html/test2.test.html +./orphan_test_test2_test/html/test.test.html +./orphan_test_test2_test/html/toc.html +./orphan_test_test2_test/mlihtml +./orphan_test_test2_test/mlihtml/index_attributes.html +./orphan_test_test2_test/mlihtml/index_classes.html +./orphan_test_test2_test/mlihtml/index_class_types.html +./orphan_test_test2_test/mlihtml/index_exceptions.html +./orphan_test_test2_test/mlihtml/index_extensions.html +./orphan_test_test2_test/mlihtml/index.html +./orphan_test_test2_test/mlihtml/index_methods.html +./orphan_test_test2_test/mlihtml/index_modules.html +./orphan_test_test2_test/mlihtml/index_module_types.html +./orphan_test_test2_test/mlihtml/index_types.html +./orphan_test_test2_test/mlihtml/index_values.html +./orphan_test_test2_test/mlihtml/style.css +./orphan_test_test2_test/mlihtml/Test_aux.html +./orphan_test_test2_test/mlihtml/Test.html +./orphan_test_test2_test/mlihtml/type_Test_aux.html +./orphan_test_test2_test/mlihtml/type_Test.html +EOT +exec diff -u desired actual diff --git a/test-suite/coq-makefile/native1/_CoqProject b/test-suite/coq-makefile/native1/_CoqProject new file mode 100644 index 000000000..a6fa17348 --- /dev/null +++ b/test-suite/coq-makefile/native1/_CoqProject @@ -0,0 +1,11 @@ +-R src test +-R theories test +-I src +-arg -native-compiler + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh new file mode 100755 index 000000000..f07966263 --- /dev/null +++ b/test-suite/coq-makefile/native1/run.sh @@ -0,0 +1,36 @@ +#!/usr/bin/env bash + +#set -x +set -e + +NATIVECOMP=`grep "let no_native_compiler = false" ../../../config/coq_config.ml`||true +if [[ `which ocamlopt` && $NATIVECOMP ]]; then + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +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.cma +./test/test_plugin.cmi +./test/test_plugin.cmo +./test/test_plugin.cmx +./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 diff --git a/test-suite/coq-makefile/only/_CoqProject b/test-suite/coq-makefile/only/_CoqProject new file mode 100644 index 000000000..357384fdd --- /dev/null +++ b/test-suite/coq-makefile/only/_CoqProject @@ -0,0 +1,11 @@ +-R theories/ test +-R src/ test +-I src/ + +./src/test_plugin.mlpack +./src/test.ml4 +./src/test.mli +./src/test_aux.ml +./src/test_aux.mli +./theories/test.v +./theories/sub/testsub.v diff --git a/test-suite/coq-makefile/only/run.sh b/test-suite/coq-makefile/only/run.sh new file mode 100755 index 000000000..2ea3deffb --- /dev/null +++ b/test-suite/coq-makefile/only/run.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash + +#set -x +set -e + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +make only TGTS="src/test.cmi src/test_aux.cmi" -j2 +test -f src/test.cmi +test -f src/test_aux.cmi +! test -f src/test.cmo diff --git a/test-suite/coq-makefile/plugin1/_CoqProject b/test-suite/coq-makefile/plugin1/_CoqProject new file mode 100644 index 000000000..4eddc9d70 --- /dev/null +++ b/test-suite/coq-makefile/plugin1/_CoqProject @@ -0,0 +1,10 @@ +-R theories test +-R src test +-I src + +src/test_plugin.mllib +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/plugin1/run.sh b/test-suite/coq-makefile/plugin1/run.sh new file mode 100755 index 000000000..24ef8c891 --- /dev/null +++ b/test-suite/coq-makefile/plugin1/run.sh @@ -0,0 +1,31 @@ +#!/usr/bin/env bash + +#set -x +set -e + +. ../template/init.sh + +mv src/test_plugin.mlpack src/test_plugin.mllib +coq_makefile -f _CoqProject -o Makefile +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.cmi +./test/test.cmo +./test/test.cmx +./test/test_aux.cmi +./test/test_aux.cmo +./test/test_aux.cmx +./test/test_plugin.cma +./test/test_plugin.cmxa +./test/test_plugin.cmxs +./test/test.v +./test/test.vo +EOT +exec diff -u desired actual diff --git a/test-suite/coq-makefile/plugin2/_CoqProject b/test-suite/coq-makefile/plugin2/_CoqProject new file mode 100644 index 000000000..0bf1e07f2 --- /dev/null +++ b/test-suite/coq-makefile/plugin2/_CoqProject @@ -0,0 +1,10 @@ +-R theories/ test +-R src/ test +-I src/ + +src/test_plugin.mllib +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh new file mode 100755 index 000000000..24ef8c891 --- /dev/null +++ b/test-suite/coq-makefile/plugin2/run.sh @@ -0,0 +1,31 @@ +#!/usr/bin/env bash + +#set -x +set -e + +. ../template/init.sh + +mv src/test_plugin.mlpack src/test_plugin.mllib +coq_makefile -f _CoqProject -o Makefile +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.cmi +./test/test.cmo +./test/test.cmx +./test/test_aux.cmi +./test/test_aux.cmo +./test/test_aux.cmx +./test/test_plugin.cma +./test/test_plugin.cmxa +./test/test_plugin.cmxs +./test/test.v +./test/test.vo +EOT +exec diff -u desired actual diff --git a/test-suite/coq-makefile/plugin3/_CoqProject b/test-suite/coq-makefile/plugin3/_CoqProject new file mode 100644 index 000000000..2028d49a8 --- /dev/null +++ b/test-suite/coq-makefile/plugin3/_CoqProject @@ -0,0 +1,10 @@ +-R theories/ test +-R src/ test +-I src/ + +./src/test_plugin.mllib +./src/test.ml4 +./src/test.mli +./src/test_aux.ml +./src/test_aux.mli +./theories/test.v diff --git a/test-suite/coq-makefile/plugin3/run.sh b/test-suite/coq-makefile/plugin3/run.sh new file mode 100755 index 000000000..24ef8c891 --- /dev/null +++ b/test-suite/coq-makefile/plugin3/run.sh @@ -0,0 +1,31 @@ +#!/usr/bin/env bash + +#set -x +set -e + +. ../template/init.sh + +mv src/test_plugin.mlpack src/test_plugin.mllib +coq_makefile -f _CoqProject -o Makefile +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.cmi +./test/test.cmo +./test/test.cmx +./test/test_aux.cmi +./test/test_aux.cmo +./test/test_aux.cmx +./test/test_plugin.cma +./test/test_plugin.cmxa +./test/test_plugin.cmxs +./test/test.v +./test/test.vo +EOT +exec diff -u desired actual diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh new file mode 100755 index 000000000..c952d41a3 --- /dev/null +++ b/test-suite/coq-makefile/template/init.sh @@ -0,0 +1,16 @@ + +export PATH=$COQBIN:$PATH + +rm -rf theories src Makefile Makefile.conf tmp +git clean -dfx || true + +mkdir -p src +mkdir -p theories/sub + +cp ../template/theories/sub/testsub.v theories/sub +cp ../template/theories/test.v theories +cp ../template/src/test.ml4 src +cp ../template/src/test_aux.mli src +cp ../template/src/test.mli src +cp ../template/src/test_plugin.mlpack src +cp ../template/src/test_aux.ml src diff --git a/test-suite/coq-makefile/template/src/test.ml4 b/test-suite/coq-makefile/template/src/test.ml4 new file mode 100644 index 000000000..72765abe0 --- /dev/null +++ b/test-suite/coq-makefile/template/src/test.ml4 @@ -0,0 +1,14 @@ +open Ltac_plugin +DECLARE PLUGIN "test_plugin" +let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";; + +VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF + | [ "TestCommand" ] -> [ () ] +END + +TACTIC EXTEND test +| [ "test_tactic" ] -> [ Test_aux.tac ] +END + + + diff --git a/test-suite/coq-makefile/template/src/test.mli b/test-suite/coq-makefile/template/src/test.mli new file mode 100644 index 000000000..e69de29bb --- /dev/null +++ b/test-suite/coq-makefile/template/src/test.mli diff --git a/test-suite/coq-makefile/template/src/test_aux.ml b/test-suite/coq-makefile/template/src/test_aux.ml new file mode 100644 index 000000000..a01d0865a --- /dev/null +++ b/test-suite/coq-makefile/template/src/test_aux.ml @@ -0,0 +1 @@ +let tac = Proofview.tclUNIT () diff --git a/test-suite/coq-makefile/template/src/test_aux.mli b/test-suite/coq-makefile/template/src/test_aux.mli new file mode 100644 index 000000000..10020f27d --- /dev/null +++ b/test-suite/coq-makefile/template/src/test_aux.mli @@ -0,0 +1 @@ +val tac : unit Proofview.tactic diff --git a/test-suite/coq-makefile/template/src/test_plugin.mlpack b/test-suite/coq-makefile/template/src/test_plugin.mlpack new file mode 100644 index 000000000..cf94d851b --- /dev/null +++ b/test-suite/coq-makefile/template/src/test_plugin.mlpack @@ -0,0 +1,2 @@ +Test_aux +Test diff --git a/test-suite/coq-makefile/template/theories/sub/testsub.v b/test-suite/coq-makefile/template/theories/sub/testsub.v new file mode 100644 index 000000000..755fc343f --- /dev/null +++ b/test-suite/coq-makefile/template/theories/sub/testsub.v @@ -0,0 +1 @@ +Require Import test. diff --git a/test-suite/coq-makefile/template/theories/test.v b/test-suite/coq-makefile/template/theories/test.v new file mode 100644 index 000000000..744b5aad7 --- /dev/null +++ b/test-suite/coq-makefile/template/theories/test.v @@ -0,0 +1,7 @@ +Declare ML Module "test_plugin". +TestCommand. +Goal True. +Proof. +test_tactic. +exact I. +Qed. diff --git a/test-suite/coq-makefile/uninstall1/_CoqProject b/test-suite/coq-makefile/uninstall1/_CoqProject new file mode 100644 index 000000000..35792066b --- /dev/null +++ b/test-suite/coq-makefile/uninstall1/_CoqProject @@ -0,0 +1,11 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v +theories/sub/testsub.v diff --git a/test-suite/coq-makefile/uninstall1/run.sh b/test-suite/coq-makefile/uninstall1/run.sh new file mode 100755 index 000000000..e525e1208 --- /dev/null +++ b/test-suite/coq-makefile/uninstall1/run.sh @@ -0,0 +1,20 @@ +#!/usr/bin/env bash + +#set -x +set -e + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +make +make html mlihtml +make install DSTROOT="$PWD/tmp" +make install-doc DSTROOT="$PWD/tmp" +make uninstall DSTROOT="$PWD/tmp" +make uninstall-doc DSTROOT="$PWD/tmp" +#make debug +(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual +sort -u > desired <<EOT +. +EOT +exec diff -u desired actual diff --git a/test-suite/coq-makefile/uninstall2/_CoqProject b/test-suite/coq-makefile/uninstall2/_CoqProject new file mode 100644 index 000000000..d2a547d47 --- /dev/null +++ b/test-suite/coq-makefile/uninstall2/_CoqProject @@ -0,0 +1,11 @@ +-R src/ test +-R theories/ test +-I src/ + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v +theories/sub/testsub.v diff --git a/test-suite/coq-makefile/uninstall2/run.sh b/test-suite/coq-makefile/uninstall2/run.sh new file mode 100755 index 000000000..e525e1208 --- /dev/null +++ b/test-suite/coq-makefile/uninstall2/run.sh @@ -0,0 +1,20 @@ +#!/usr/bin/env bash + +#set -x +set -e + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +make +make html mlihtml +make install DSTROOT="$PWD/tmp" +make install-doc DSTROOT="$PWD/tmp" +make uninstall DSTROOT="$PWD/tmp" +make uninstall-doc DSTROOT="$PWD/tmp" +#make debug +(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual +sort -u > desired <<EOT +. +EOT +exec diff -u desired actual diff --git a/test-suite/coq-makefile/validate1/_CoqProject b/test-suite/coq-makefile/validate1/_CoqProject new file mode 100644 index 000000000..69f47302e --- /dev/null +++ b/test-suite/coq-makefile/validate1/_CoqProject @@ -0,0 +1,10 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/validate1/run.sh b/test-suite/coq-makefile/validate1/run.sh new file mode 100755 index 000000000..aaa4194b3 --- /dev/null +++ b/test-suite/coq-makefile/validate1/run.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +#set -x +set -e + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +make +exec make validate |