diff options
74 files changed, 454 insertions, 149 deletions
diff --git a/.gitignore b/.gitignore index 6e6f01a43..c55ad24f8 100644 --- a/.gitignore +++ b/.gitignore @@ -64,7 +64,8 @@ test-suite/coq-makefile/*/actual test-suite/coq-makefile/*/desired test-suite/coq-makefile/*/Makefile test-suite/coq-makefile/*/Makefile.conf -test-suite/coq-makefile/*/src/test.ml +test-suite/coq-makefile/*/src +test-suite/coq-makefile/*/theories test-suite/coq-makefile/*/html test-suite/coq-makefile/*/mlihtml test-suite/coq-makefile/*/subdir/done diff --git a/test-suite/Makefile b/test-suite/Makefile index 8a3d383cb..c2d6e540c 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -486,7 +486,7 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v)) coq-makefile: $(patsubst %/run.sh,%.log,$(wildcard coq-makefile/*/run.sh)) coq-makefile/%.log : coq-makefile/%/run.sh - @echo "TEST $*" + @echo "TEST coq-makefile/$*" $(HIDE)(\ cd coq-makefile/$* && \ ./run.sh 2>&1; \ diff --git a/test-suite/coq-makefile/compat-subdirs/_CoqProject b/test-suite/coq-makefile/compat-subdirs/_CoqProject index 700d59d64..4f44bde22 100644 --- a/test-suite/coq-makefile/compat-subdirs/_CoqProject +++ b/test-suite/coq-makefile/compat-subdirs/_CoqProject @@ -1,5 +1,5 @@ --R src/ test --R theories/ test +-R src test +-R theories test -I src src/test_plugin.mlpack diff --git a/test-suite/coq-makefile/compat-subdirs/run.sh b/test-suite/coq-makefile/compat-subdirs/run.sh index 38e54d03e..ccb348c6f 100755 --- a/test-suite/coq-makefile/compat-subdirs/run.sh +++ b/test-suite/coq-makefile/compat-subdirs/run.sh @@ -3,8 +3,7 @@ #set -x set -e -export PATH=../../../bin/:$PATH -git clean -dfx . +. ../template/init.sh coq_makefile -f _CoqProject -o Makefile make exec test -f "subdir/done" diff --git a/test-suite/coq-makefile/compat-subdirs/theories/test.v b/test-suite/coq-makefile/compat-subdirs/theories/test.v deleted file mode 100644 index 7753b56aa..000000000 --- a/test-suite/coq-makefile/compat-subdirs/theories/test.v +++ /dev/null @@ -1,7 +0,0 @@ -Declare ML Module "test_plugin". -Test. -Goal True. -Proof. -test. -exact I. -Qed. diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh index bbe9717ab..e071f1db7 100755 --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -3,8 +3,8 @@ #set -x set -e -export PATH=../../../bin/:$PATH -git clean -dfx . +. ../template/init.sh + coq_makefile -f _CoqProject -o Makefile make make html mlihtml diff --git a/test-suite/coq-makefile/coqdoc1/src/test.ml4 b/test-suite/coq-makefile/coqdoc1/src/test.ml4 deleted file mode 100644 index 8ddc9b095..000000000 --- a/test-suite/coq-makefile/coqdoc1/src/test.ml4 +++ /dev/null @@ -1,13 +0,0 @@ -DECLARE PLUGIN "test_plugin" -let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";; - -VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF - | [ "Test" ] -> [ () ] -END - -TACTIC EXTEND test -| [ "test" ] -> [ Test_aux.tac ] -END - - - diff --git a/test-suite/coq-makefile/coqdoc1/src/test.mli b/test-suite/coq-makefile/coqdoc1/src/test.mli deleted file mode 100644 index e69de29bb..000000000 --- a/test-suite/coq-makefile/coqdoc1/src/test.mli +++ /dev/null diff --git a/test-suite/coq-makefile/coqdoc1/src/test_aux.ml b/test-suite/coq-makefile/coqdoc1/src/test_aux.ml deleted file mode 100644 index a01d0865a..000000000 --- a/test-suite/coq-makefile/coqdoc1/src/test_aux.ml +++ /dev/null @@ -1 +0,0 @@ -let tac = Proofview.tclUNIT () diff --git a/test-suite/coq-makefile/coqdoc1/src/test_aux.mli b/test-suite/coq-makefile/coqdoc1/src/test_aux.mli deleted file mode 100644 index 10020f27d..000000000 --- a/test-suite/coq-makefile/coqdoc1/src/test_aux.mli +++ /dev/null @@ -1 +0,0 @@ -val tac : unit Proofview.tactic diff --git a/test-suite/coq-makefile/coqdoc1/src/test_plugin.mlpack b/test-suite/coq-makefile/coqdoc1/src/test_plugin.mlpack deleted file mode 100644 index cf94d851b..000000000 --- a/test-suite/coq-makefile/coqdoc1/src/test_plugin.mlpack +++ /dev/null @@ -1,2 +0,0 @@ -Test_aux -Test 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..e071f1db7 --- /dev/null +++ b/test-suite/coq-makefile/coqdoc2/run.sh @@ -0,0 +1,53 @@ +#!/bin/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.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..db1160113 --- /dev/null +++ b/test-suite/coq-makefile/extend-subdirs/run.sh @@ -0,0 +1,10 @@ +#!/bin/sh + +#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..45f226911 --- /dev/null +++ b/test-suite/coq-makefile/latex1/run.sh @@ -0,0 +1,15 @@ +#!/bin/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 index cb1ad4a4b..69f47302e 100644 --- a/test-suite/coq-makefile/merlin1/_CoqProject +++ b/test-suite/coq-makefile/merlin1/_CoqProject @@ -1,5 +1,5 @@ --R src/ test --R theories/ test +-R src test +-R theories test -I src src/test_plugin.mlpack diff --git a/test-suite/coq-makefile/merlin1/run.sh b/test-suite/coq-makefile/merlin1/run.sh index 3b5d388c9..9b89e5b6e 100755 --- a/test-suite/coq-makefile/merlin1/run.sh +++ b/test-suite/coq-makefile/merlin1/run.sh @@ -3,11 +3,13 @@ #set -x set -e -export PATH=../../../bin/:$PATH -git clean -dfx . +. ../template/init.sh + coq_makefile -f _CoqProject -o Makefile make .merlin -echo B $PWD/src > desired -echo S $PWD/src >> desired +cat > desired <<EOT +B src +S src +EOT tail -2 .merlin > actual exec diff -u desired actual diff --git a/test-suite/coq-makefile/merlin1/src/test.ml4 b/test-suite/coq-makefile/merlin1/src/test.ml4 deleted file mode 100644 index 8ddc9b095..000000000 --- a/test-suite/coq-makefile/merlin1/src/test.ml4 +++ /dev/null @@ -1,13 +0,0 @@ -DECLARE PLUGIN "test_plugin" -let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";; - -VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF - | [ "Test" ] -> [ () ] -END - -TACTIC EXTEND test -| [ "test" ] -> [ Test_aux.tac ] -END - - - diff --git a/test-suite/coq-makefile/merlin1/src/test.mli b/test-suite/coq-makefile/merlin1/src/test.mli deleted file mode 100644 index e69de29bb..000000000 --- a/test-suite/coq-makefile/merlin1/src/test.mli +++ /dev/null diff --git a/test-suite/coq-makefile/merlin1/src/test_aux.ml b/test-suite/coq-makefile/merlin1/src/test_aux.ml deleted file mode 100644 index a01d0865a..000000000 --- a/test-suite/coq-makefile/merlin1/src/test_aux.ml +++ /dev/null @@ -1 +0,0 @@ -let tac = Proofview.tclUNIT () diff --git a/test-suite/coq-makefile/merlin1/src/test_aux.mli b/test-suite/coq-makefile/merlin1/src/test_aux.mli deleted file mode 100644 index 10020f27d..000000000 --- a/test-suite/coq-makefile/merlin1/src/test_aux.mli +++ /dev/null @@ -1 +0,0 @@ -val tac : unit Proofview.tactic diff --git a/test-suite/coq-makefile/merlin1/src/test_plugin.mlpack b/test-suite/coq-makefile/merlin1/src/test_plugin.mlpack deleted file mode 100644 index cf94d851b..000000000 --- a/test-suite/coq-makefile/merlin1/src/test_plugin.mlpack +++ /dev/null @@ -1,2 +0,0 @@ -Test_aux -Test diff --git a/test-suite/coq-makefile/merlin1/theories/test.v b/test-suite/coq-makefile/merlin1/theories/test.v deleted file mode 100644 index 7753b56aa..000000000 --- a/test-suite/coq-makefile/merlin1/theories/test.v +++ /dev/null @@ -1,7 +0,0 @@ -Declare ML Module "test_plugin". -Test. -Goal True. -Proof. -test. -exact I. -Qed. diff --git a/test-suite/coq-makefile/mllib1/src/test.ml4 b/test-suite/coq-makefile/mllib1/src/test.ml4 deleted file mode 100644 index 8ddc9b095..000000000 --- a/test-suite/coq-makefile/mllib1/src/test.ml4 +++ /dev/null @@ -1,13 +0,0 @@ -DECLARE PLUGIN "test_plugin" -let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";; - -VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF - | [ "Test" ] -> [ () ] -END - -TACTIC EXTEND test -| [ "test" ] -> [ Test_aux.tac ] -END - - - diff --git a/test-suite/coq-makefile/mllib1/src/test.mli b/test-suite/coq-makefile/mllib1/src/test.mli deleted file mode 100644 index e69de29bb..000000000 --- a/test-suite/coq-makefile/mllib1/src/test.mli +++ /dev/null diff --git a/test-suite/coq-makefile/mllib1/src/test_aux.ml b/test-suite/coq-makefile/mllib1/src/test_aux.ml deleted file mode 100644 index a01d0865a..000000000 --- a/test-suite/coq-makefile/mllib1/src/test_aux.ml +++ /dev/null @@ -1 +0,0 @@ -let tac = Proofview.tclUNIT () diff --git a/test-suite/coq-makefile/mllib1/src/test_aux.mli b/test-suite/coq-makefile/mllib1/src/test_aux.mli deleted file mode 100644 index 10020f27d..000000000 --- a/test-suite/coq-makefile/mllib1/src/test_aux.mli +++ /dev/null @@ -1 +0,0 @@ -val tac : unit Proofview.tactic diff --git a/test-suite/coq-makefile/mllib1/src/test_plugin.mllib b/test-suite/coq-makefile/mllib1/src/test_plugin.mllib deleted file mode 100644 index cf94d851b..000000000 --- a/test-suite/coq-makefile/mllib1/src/test_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Test_aux -Test diff --git a/test-suite/coq-makefile/mllib1/theories/test.v b/test-suite/coq-makefile/mllib1/theories/test.v deleted file mode 100644 index 7753b56aa..000000000 --- a/test-suite/coq-makefile/mllib1/theories/test.v +++ /dev/null @@ -1,7 +0,0 @@ -Declare ML Module "test_plugin". -Test. -Goal True. -Proof. -test. -exact I. -Qed. diff --git a/test-suite/coq-makefile/mlpack1/_CoqProject b/test-suite/coq-makefile/mlpack1/_CoqProject index cb1ad4a4b..69f47302e 100644 --- a/test-suite/coq-makefile/mlpack1/_CoqProject +++ b/test-suite/coq-makefile/mlpack1/_CoqProject @@ -1,5 +1,5 @@ --R src/ test --R theories/ test +-R src test +-R theories test -I src src/test_plugin.mlpack diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh index 43d03be4a..418a2fb77 100755 --- a/test-suite/coq-makefile/mlpack1/run.sh +++ b/test-suite/coq-makefile/mlpack1/run.sh @@ -3,8 +3,8 @@ #set -x set -e -export PATH=../../../bin/:$PATH -git clean -dfx . +. ../template/init.sh + coq_makefile -f _CoqProject -o Makefile make make html mlihtml diff --git a/test-suite/coq-makefile/mlpack1/src/test.ml4 b/test-suite/coq-makefile/mlpack1/src/test.ml4 deleted file mode 100644 index 8ddc9b095..000000000 --- a/test-suite/coq-makefile/mlpack1/src/test.ml4 +++ /dev/null @@ -1,13 +0,0 @@ -DECLARE PLUGIN "test_plugin" -let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";; - -VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF - | [ "Test" ] -> [ () ] -END - -TACTIC EXTEND test -| [ "test" ] -> [ Test_aux.tac ] -END - - - diff --git a/test-suite/coq-makefile/mlpack1/src/test.mli b/test-suite/coq-makefile/mlpack1/src/test.mli deleted file mode 100644 index e69de29bb..000000000 --- a/test-suite/coq-makefile/mlpack1/src/test.mli +++ /dev/null diff --git a/test-suite/coq-makefile/mlpack1/src/test_aux.ml b/test-suite/coq-makefile/mlpack1/src/test_aux.ml deleted file mode 100644 index a01d0865a..000000000 --- a/test-suite/coq-makefile/mlpack1/src/test_aux.ml +++ /dev/null @@ -1 +0,0 @@ -let tac = Proofview.tclUNIT () diff --git a/test-suite/coq-makefile/mlpack1/src/test_aux.mli b/test-suite/coq-makefile/mlpack1/src/test_aux.mli deleted file mode 100644 index 10020f27d..000000000 --- a/test-suite/coq-makefile/mlpack1/src/test_aux.mli +++ /dev/null @@ -1 +0,0 @@ -val tac : unit Proofview.tactic diff --git a/test-suite/coq-makefile/mlpack1/src/test_plugin.mlpack b/test-suite/coq-makefile/mlpack1/src/test_plugin.mlpack deleted file mode 100644 index cf94d851b..000000000 --- a/test-suite/coq-makefile/mlpack1/src/test_plugin.mlpack +++ /dev/null @@ -1,2 +0,0 @@ -Test_aux -Test diff --git a/test-suite/coq-makefile/mlpack1/theories/test.v b/test-suite/coq-makefile/mlpack1/theories/test.v deleted file mode 100644 index 7753b56aa..000000000 --- a/test-suite/coq-makefile/mlpack1/theories/test.v +++ /dev/null @@ -1,7 +0,0 @@ -Declare ML Module "test_plugin". -Test. -Goal True. -Proof. -test. -exact I. -Qed. 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..418a2fb77 --- /dev/null +++ b/test-suite/coq-makefile/mlpack2/run.sh @@ -0,0 +1,25 @@ +#!/bin/sh + +#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.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..a24a8a3cf --- /dev/null +++ b/test-suite/coq-makefile/multiroot/run.sh @@ -0,0 +1,61 @@ +#!/bin/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..097bd6398 --- /dev/null +++ b/test-suite/coq-makefile/native1/run.sh @@ -0,0 +1,34 @@ +#!/bin/sh + +#set -x +set -e + +if which ocamlopt; 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.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/mllib1/_CoqProject b/test-suite/coq-makefile/plugin1/_CoqProject index 6b2046d68..4eddc9d70 100644 --- a/test-suite/coq-makefile/mllib1/_CoqProject +++ b/test-suite/coq-makefile/plugin1/_CoqProject @@ -1,4 +1,5 @@ -R theories test +-R src test -I src src/test_plugin.mllib diff --git a/test-suite/coq-makefile/mllib1/run.sh b/test-suite/coq-makefile/plugin1/run.sh index 8f6b8e7ea..684e0ece8 100755 --- a/test-suite/coq-makefile/mllib1/run.sh +++ b/test-suite/coq-makefile/plugin1/run.sh @@ -3,8 +3,9 @@ #set -x set -e -export PATH=../../../bin/:$PATH -git clean -dfx . +. ../template/init.sh + +mv src/test_plugin.mlpack src/test_plugin.mllib coq_makefile -f _CoqProject -o Makefile make make html mlihtml 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..684e0ece8 --- /dev/null +++ b/test-suite/coq-makefile/plugin2/run.sh @@ -0,0 +1,31 @@ +#!/bin/sh + +#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..684e0ece8 --- /dev/null +++ b/test-suite/coq-makefile/plugin3/run.sh @@ -0,0 +1,31 @@ +#!/bin/sh + +#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 100644 index 000000000..bfd2c1b95 --- /dev/null +++ b/test-suite/coq-makefile/template/init.sh @@ -0,0 +1,16 @@ + +export PATH=../../../bin/:$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/compat-subdirs/src/test.ml4 b/test-suite/coq-makefile/template/src/test.ml4 index 8ddc9b095..72765abe0 100644 --- a/test-suite/coq-makefile/compat-subdirs/src/test.ml4 +++ b/test-suite/coq-makefile/template/src/test.ml4 @@ -1,12 +1,13 @@ +open Ltac_plugin DECLARE PLUGIN "test_plugin" let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";; VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF - | [ "Test" ] -> [ () ] + | [ "TestCommand" ] -> [ () ] END TACTIC EXTEND test -| [ "test" ] -> [ Test_aux.tac ] +| [ "test_tactic" ] -> [ Test_aux.tac ] END diff --git a/test-suite/coq-makefile/compat-subdirs/src/test.mli b/test-suite/coq-makefile/template/src/test.mli index e69de29bb..e69de29bb 100644 --- a/test-suite/coq-makefile/compat-subdirs/src/test.mli +++ b/test-suite/coq-makefile/template/src/test.mli diff --git a/test-suite/coq-makefile/compat-subdirs/src/test_aux.ml b/test-suite/coq-makefile/template/src/test_aux.ml index a01d0865a..a01d0865a 100644 --- a/test-suite/coq-makefile/compat-subdirs/src/test_aux.ml +++ b/test-suite/coq-makefile/template/src/test_aux.ml diff --git a/test-suite/coq-makefile/compat-subdirs/src/test_aux.mli b/test-suite/coq-makefile/template/src/test_aux.mli index 10020f27d..10020f27d 100644 --- a/test-suite/coq-makefile/compat-subdirs/src/test_aux.mli +++ b/test-suite/coq-makefile/template/src/test_aux.mli diff --git a/test-suite/coq-makefile/compat-subdirs/src/test_plugin.mlpack b/test-suite/coq-makefile/template/src/test_plugin.mlpack index cf94d851b..cf94d851b 100644 --- a/test-suite/coq-makefile/compat-subdirs/src/test_plugin.mlpack +++ b/test-suite/coq-makefile/template/src/test_plugin.mlpack diff --git a/test-suite/coq-makefile/coqdoc1/theories/sub/testsub.v b/test-suite/coq-makefile/template/theories/sub/testsub.v index 755fc343f..755fc343f 100644 --- a/test-suite/coq-makefile/coqdoc1/theories/sub/testsub.v +++ b/test-suite/coq-makefile/template/theories/sub/testsub.v diff --git a/test-suite/coq-makefile/coqdoc1/theories/test.v b/test-suite/coq-makefile/template/theories/test.v index 7753b56aa..744b5aad7 100644 --- a/test-suite/coq-makefile/coqdoc1/theories/test.v +++ b/test-suite/coq-makefile/template/theories/test.v @@ -1,7 +1,7 @@ Declare ML Module "test_plugin". -Test. +TestCommand. Goal True. Proof. -test. +test_tactic. exact I. Qed. diff --git a/test-suite/coq-makefile/uninstall1/_CoqProject b/test-suite/coq-makefile/uninstall1/_CoqProject index 706cf75cc..35792066b 100644 --- a/test-suite/coq-makefile/uninstall1/_CoqProject +++ b/test-suite/coq-makefile/uninstall1/_CoqProject @@ -1,5 +1,5 @@ --R src/ test --R theories/ test +-R src test +-R theories test -I src src/test_plugin.mlpack diff --git a/test-suite/coq-makefile/uninstall1/run.sh b/test-suite/coq-makefile/uninstall1/run.sh index a3bfe182b..d24176279 100755 --- a/test-suite/coq-makefile/uninstall1/run.sh +++ b/test-suite/coq-makefile/uninstall1/run.sh @@ -3,8 +3,8 @@ #set -x set -e -export PATH=../../../bin/:$PATH -git clean -dfx . +. ../template/init.sh + coq_makefile -f _CoqProject -o Makefile make make html mlihtml diff --git a/test-suite/coq-makefile/uninstall1/src/test.ml4 b/test-suite/coq-makefile/uninstall1/src/test.ml4 deleted file mode 100644 index 8ddc9b095..000000000 --- a/test-suite/coq-makefile/uninstall1/src/test.ml4 +++ /dev/null @@ -1,13 +0,0 @@ -DECLARE PLUGIN "test_plugin" -let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";; - -VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF - | [ "Test" ] -> [ () ] -END - -TACTIC EXTEND test -| [ "test" ] -> [ Test_aux.tac ] -END - - - diff --git a/test-suite/coq-makefile/uninstall1/src/test.mli b/test-suite/coq-makefile/uninstall1/src/test.mli deleted file mode 100644 index e69de29bb..000000000 --- a/test-suite/coq-makefile/uninstall1/src/test.mli +++ /dev/null diff --git a/test-suite/coq-makefile/uninstall1/src/test_aux.ml b/test-suite/coq-makefile/uninstall1/src/test_aux.ml deleted file mode 100644 index a01d0865a..000000000 --- a/test-suite/coq-makefile/uninstall1/src/test_aux.ml +++ /dev/null @@ -1 +0,0 @@ -let tac = Proofview.tclUNIT () diff --git a/test-suite/coq-makefile/uninstall1/src/test_aux.mli b/test-suite/coq-makefile/uninstall1/src/test_aux.mli deleted file mode 100644 index 10020f27d..000000000 --- a/test-suite/coq-makefile/uninstall1/src/test_aux.mli +++ /dev/null @@ -1 +0,0 @@ -val tac : unit Proofview.tactic diff --git a/test-suite/coq-makefile/uninstall1/src/test_plugin.mlpack b/test-suite/coq-makefile/uninstall1/src/test_plugin.mlpack deleted file mode 100644 index cf94d851b..000000000 --- a/test-suite/coq-makefile/uninstall1/src/test_plugin.mlpack +++ /dev/null @@ -1,2 +0,0 @@ -Test_aux -Test diff --git a/test-suite/coq-makefile/uninstall1/theories/sub/testsub.v b/test-suite/coq-makefile/uninstall1/theories/sub/testsub.v deleted file mode 100644 index 755fc343f..000000000 --- a/test-suite/coq-makefile/uninstall1/theories/sub/testsub.v +++ /dev/null @@ -1 +0,0 @@ -Require Import test. diff --git a/test-suite/coq-makefile/uninstall1/theories/test.v b/test-suite/coq-makefile/uninstall1/theories/test.v deleted file mode 100644 index 7753b56aa..000000000 --- a/test-suite/coq-makefile/uninstall1/theories/test.v +++ /dev/null @@ -1,7 +0,0 @@ -Declare ML Module "test_plugin". -Test. -Goal True. -Proof. -test. -exact I. -Qed. 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..d24176279 --- /dev/null +++ b/test-suite/coq-makefile/uninstall2/run.sh @@ -0,0 +1,20 @@ +#!/bin/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..61025021d --- /dev/null +++ b/test-suite/coq-makefile/validate1/run.sh @@ -0,0 +1,10 @@ +#!/bin/sh + +#set -x +set -e + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +make +exec make validate |