diff options
54 files changed, 389 insertions, 1 deletions
diff --git a/.gitignore b/.gitignore index 371136fc7..8bbfce5d8 100644 --- a/.gitignore +++ b/.gitignore @@ -60,6 +60,14 @@ test-suite/.nra.cache test-suite/trace test-suite/misc/universes/all_stdlib.v test-suite/misc/universes/universes.txt +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/*/html +test-suite/coq-makefile/*/mlihtml +test-suite/coq-makefile/*/subdir/done # documentation @@ -54,6 +54,7 @@ FIND_VCS_CLAUSE:='(' \ -name "$${GIT_DIR}" -o \ -name '_build' -o \ -name '_build_ci' \ + -name 'coq-makefile' \ ')' -prune -o define find diff --git a/test-suite/Makefile b/test-suite/Makefile index afaa48463..8a3d383cb 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -87,7 +87,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ output-modulo-time interactive micromega $(COMPLEXITY) modules stm # All subsystems -SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk +SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coq-makefile PREREQUISITELOG = prerequisite/admit.v.log \ prerequisite/make_local.v.log prerequisite/make_notation.v.log @@ -151,6 +151,7 @@ summary: $(call summary_dir, "IDE tests", ide); \ $(call summary_dir, "VI tests", vio); \ $(call summary_dir, "Coqchk tests", coqchk); \ + $(call summary_dir, "Coq makefile", coq-makefile); \ nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \ nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \ nb_tests=`expr $$nb_success + $$nb_failure`; \ @@ -481,3 +482,19 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v)) echo " $<...Error!"; \ fi; \ } > "$@" + +coq-makefile: $(patsubst %/run.sh,%.log,$(wildcard coq-makefile/*/run.sh)) + +coq-makefile/%.log : coq-makefile/%/run.sh + @echo "TEST $*" + $(HIDE)(\ + cd coq-makefile/$* && \ + ./run.sh 2>&1; \ + if [ $$? = 0 ]; then \ + echo $(log_success); \ + echo " $<...Ok"; \ + else \ + echo $(log_failure); \ + echo " $<...Error!"; \ + fi; \ + ) > "$@" diff --git a/test-suite/coq-makefile/compat-subdirs/_CoqProject b/test-suite/coq-makefile/compat-subdirs/_CoqProject new file mode 100644 index 000000000..700d59d64 --- /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..38e54d03e --- /dev/null +++ b/test-suite/coq-makefile/compat-subdirs/run.sh @@ -0,0 +1,10 @@ +#!/bin/sh + +#set -x +set -e + +export PATH=../../../bin/:$PATH +git clean -dfx . +coq_makefile -f _CoqProject -o Makefile +make +exec test -f "subdir/done" diff --git a/test-suite/coq-makefile/compat-subdirs/src/test.ml4 b/test-suite/coq-makefile/compat-subdirs/src/test.ml4 new file mode 100644 index 000000000..8ddc9b095 --- /dev/null +++ b/test-suite/coq-makefile/compat-subdirs/src/test.ml4 @@ -0,0 +1,13 @@ +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/compat-subdirs/src/test.mli b/test-suite/coq-makefile/compat-subdirs/src/test.mli new file mode 100644 index 000000000..e69de29bb --- /dev/null +++ b/test-suite/coq-makefile/compat-subdirs/src/test.mli diff --git a/test-suite/coq-makefile/compat-subdirs/src/test_aux.ml b/test-suite/coq-makefile/compat-subdirs/src/test_aux.ml new file mode 100644 index 000000000..a01d0865a --- /dev/null +++ b/test-suite/coq-makefile/compat-subdirs/src/test_aux.ml @@ -0,0 +1 @@ +let tac = Proofview.tclUNIT () diff --git a/test-suite/coq-makefile/compat-subdirs/src/test_aux.mli b/test-suite/coq-makefile/compat-subdirs/src/test_aux.mli new file mode 100644 index 000000000..10020f27d --- /dev/null +++ b/test-suite/coq-makefile/compat-subdirs/src/test_aux.mli @@ -0,0 +1 @@ +val tac : unit Proofview.tactic diff --git a/test-suite/coq-makefile/compat-subdirs/src/test_plugin.mlpack b/test-suite/coq-makefile/compat-subdirs/src/test_plugin.mlpack new file mode 100644 index 000000000..cf94d851b --- /dev/null +++ b/test-suite/coq-makefile/compat-subdirs/src/test_plugin.mlpack @@ -0,0 +1,2 @@ +Test_aux +Test 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/compat-subdirs/theories/test.v b/test-suite/coq-makefile/compat-subdirs/theories/test.v new file mode 100644 index 000000000..7753b56aa --- /dev/null +++ b/test-suite/coq-makefile/compat-subdirs/theories/test.v @@ -0,0 +1,7 @@ +Declare ML Module "test_plugin". +Test. +Goal True. +Proof. +test. +exact I. +Qed. 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..bbe9717ab --- /dev/null +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -0,0 +1,53 @@ +#!/bin/bash + +#set -x +set -e + +export PATH=../../../bin/:$PATH +git clean -dfx . +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/coqdoc1/src/test.ml4 b/test-suite/coq-makefile/coqdoc1/src/test.ml4 new file mode 100644 index 000000000..8ddc9b095 --- /dev/null +++ b/test-suite/coq-makefile/coqdoc1/src/test.ml4 @@ -0,0 +1,13 @@ +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 new file mode 100644 index 000000000..e69de29bb --- /dev/null +++ b/test-suite/coq-makefile/coqdoc1/src/test.mli diff --git a/test-suite/coq-makefile/coqdoc1/src/test_aux.ml b/test-suite/coq-makefile/coqdoc1/src/test_aux.ml new file mode 100644 index 000000000..a01d0865a --- /dev/null +++ b/test-suite/coq-makefile/coqdoc1/src/test_aux.ml @@ -0,0 +1 @@ +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 new file mode 100644 index 000000000..10020f27d --- /dev/null +++ b/test-suite/coq-makefile/coqdoc1/src/test_aux.mli @@ -0,0 +1 @@ +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 new file mode 100644 index 000000000..cf94d851b --- /dev/null +++ b/test-suite/coq-makefile/coqdoc1/src/test_plugin.mlpack @@ -0,0 +1,2 @@ +Test_aux +Test diff --git a/test-suite/coq-makefile/coqdoc1/theories/sub/testsub.v b/test-suite/coq-makefile/coqdoc1/theories/sub/testsub.v new file mode 100644 index 000000000..755fc343f --- /dev/null +++ b/test-suite/coq-makefile/coqdoc1/theories/sub/testsub.v @@ -0,0 +1 @@ +Require Import test. diff --git a/test-suite/coq-makefile/coqdoc1/theories/test.v b/test-suite/coq-makefile/coqdoc1/theories/test.v new file mode 100644 index 000000000..7753b56aa --- /dev/null +++ b/test-suite/coq-makefile/coqdoc1/theories/test.v @@ -0,0 +1,7 @@ +Declare ML Module "test_plugin". +Test. +Goal True. +Proof. +test. +exact I. +Qed. diff --git a/test-suite/coq-makefile/merlin1/_CoqProject b/test-suite/coq-makefile/merlin1/_CoqProject new file mode 100644 index 000000000..cb1ad4a4b --- /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..3b5d388c9 --- /dev/null +++ b/test-suite/coq-makefile/merlin1/run.sh @@ -0,0 +1,13 @@ +#!/bin/sh + +#set -x +set -e + +export PATH=../../../bin/:$PATH +git clean -dfx . +coq_makefile -f _CoqProject -o Makefile +make .merlin +echo B $PWD/src > desired +echo S $PWD/src >> desired +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 new file mode 100644 index 000000000..8ddc9b095 --- /dev/null +++ b/test-suite/coq-makefile/merlin1/src/test.ml4 @@ -0,0 +1,13 @@ +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 new file mode 100644 index 000000000..e69de29bb --- /dev/null +++ b/test-suite/coq-makefile/merlin1/src/test.mli diff --git a/test-suite/coq-makefile/merlin1/src/test_aux.ml b/test-suite/coq-makefile/merlin1/src/test_aux.ml new file mode 100644 index 000000000..a01d0865a --- /dev/null +++ b/test-suite/coq-makefile/merlin1/src/test_aux.ml @@ -0,0 +1 @@ +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 new file mode 100644 index 000000000..10020f27d --- /dev/null +++ b/test-suite/coq-makefile/merlin1/src/test_aux.mli @@ -0,0 +1 @@ +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 new file mode 100644 index 000000000..cf94d851b --- /dev/null +++ b/test-suite/coq-makefile/merlin1/src/test_plugin.mlpack @@ -0,0 +1,2 @@ +Test_aux +Test diff --git a/test-suite/coq-makefile/merlin1/theories/test.v b/test-suite/coq-makefile/merlin1/theories/test.v new file mode 100644 index 000000000..7753b56aa --- /dev/null +++ b/test-suite/coq-makefile/merlin1/theories/test.v @@ -0,0 +1,7 @@ +Declare ML Module "test_plugin". +Test. +Goal True. +Proof. +test. +exact I. +Qed. diff --git a/test-suite/coq-makefile/mllib1/_CoqProject b/test-suite/coq-makefile/mllib1/_CoqProject new file mode 100644 index 000000000..6b2046d68 --- /dev/null +++ b/test-suite/coq-makefile/mllib1/_CoqProject @@ -0,0 +1,9 @@ +-R theories 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/mllib1/run.sh b/test-suite/coq-makefile/mllib1/run.sh new file mode 100755 index 000000000..8f6b8e7ea --- /dev/null +++ b/test-suite/coq-makefile/mllib1/run.sh @@ -0,0 +1,30 @@ +#!/bin/sh + +#set -x +set -e + +export PATH=../../../bin/:$PATH +git clean -dfx . +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/mllib1/src/test.ml4 b/test-suite/coq-makefile/mllib1/src/test.ml4 new file mode 100644 index 000000000..8ddc9b095 --- /dev/null +++ b/test-suite/coq-makefile/mllib1/src/test.ml4 @@ -0,0 +1,13 @@ +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 new file mode 100644 index 000000000..e69de29bb --- /dev/null +++ b/test-suite/coq-makefile/mllib1/src/test.mli diff --git a/test-suite/coq-makefile/mllib1/src/test_aux.ml b/test-suite/coq-makefile/mllib1/src/test_aux.ml new file mode 100644 index 000000000..a01d0865a --- /dev/null +++ b/test-suite/coq-makefile/mllib1/src/test_aux.ml @@ -0,0 +1 @@ +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 new file mode 100644 index 000000000..10020f27d --- /dev/null +++ b/test-suite/coq-makefile/mllib1/src/test_aux.mli @@ -0,0 +1 @@ +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 new file mode 100644 index 000000000..cf94d851b --- /dev/null +++ b/test-suite/coq-makefile/mllib1/src/test_plugin.mllib @@ -0,0 +1,2 @@ +Test_aux +Test diff --git a/test-suite/coq-makefile/mllib1/theories/test.v b/test-suite/coq-makefile/mllib1/theories/test.v new file mode 100644 index 000000000..7753b56aa --- /dev/null +++ b/test-suite/coq-makefile/mllib1/theories/test.v @@ -0,0 +1,7 @@ +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 new file mode 100644 index 000000000..cb1ad4a4b --- /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..43d03be4a --- /dev/null +++ b/test-suite/coq-makefile/mlpack1/run.sh @@ -0,0 +1,25 @@ +#!/bin/sh + +#set -x +set -e + +export PATH=../../../bin/:$PATH +git clean -dfx . +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/mlpack1/src/test.ml4 b/test-suite/coq-makefile/mlpack1/src/test.ml4 new file mode 100644 index 000000000..8ddc9b095 --- /dev/null +++ b/test-suite/coq-makefile/mlpack1/src/test.ml4 @@ -0,0 +1,13 @@ +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 new file mode 100644 index 000000000..e69de29bb --- /dev/null +++ b/test-suite/coq-makefile/mlpack1/src/test.mli diff --git a/test-suite/coq-makefile/mlpack1/src/test_aux.ml b/test-suite/coq-makefile/mlpack1/src/test_aux.ml new file mode 100644 index 000000000..a01d0865a --- /dev/null +++ b/test-suite/coq-makefile/mlpack1/src/test_aux.ml @@ -0,0 +1 @@ +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 new file mode 100644 index 000000000..10020f27d --- /dev/null +++ b/test-suite/coq-makefile/mlpack1/src/test_aux.mli @@ -0,0 +1 @@ +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 new file mode 100644 index 000000000..cf94d851b --- /dev/null +++ b/test-suite/coq-makefile/mlpack1/src/test_plugin.mlpack @@ -0,0 +1,2 @@ +Test_aux +Test diff --git a/test-suite/coq-makefile/mlpack1/theories/test.v b/test-suite/coq-makefile/mlpack1/theories/test.v new file mode 100644 index 000000000..7753b56aa --- /dev/null +++ b/test-suite/coq-makefile/mlpack1/theories/test.v @@ -0,0 +1,7 @@ +Declare ML Module "test_plugin". +Test. +Goal True. +Proof. +test. +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..706cf75cc --- /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..a3bfe182b --- /dev/null +++ b/test-suite/coq-makefile/uninstall1/run.sh @@ -0,0 +1,20 @@ +#!/bin/bash + +#set -x +set -e + +export PATH=../../../bin/:$PATH +git clean -dfx . +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/uninstall1/src/test.ml4 b/test-suite/coq-makefile/uninstall1/src/test.ml4 new file mode 100644 index 000000000..8ddc9b095 --- /dev/null +++ b/test-suite/coq-makefile/uninstall1/src/test.ml4 @@ -0,0 +1,13 @@ +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 new file mode 100644 index 000000000..e69de29bb --- /dev/null +++ b/test-suite/coq-makefile/uninstall1/src/test.mli diff --git a/test-suite/coq-makefile/uninstall1/src/test_aux.ml b/test-suite/coq-makefile/uninstall1/src/test_aux.ml new file mode 100644 index 000000000..a01d0865a --- /dev/null +++ b/test-suite/coq-makefile/uninstall1/src/test_aux.ml @@ -0,0 +1 @@ +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 new file mode 100644 index 000000000..10020f27d --- /dev/null +++ b/test-suite/coq-makefile/uninstall1/src/test_aux.mli @@ -0,0 +1 @@ +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 new file mode 100644 index 000000000..cf94d851b --- /dev/null +++ b/test-suite/coq-makefile/uninstall1/src/test_plugin.mlpack @@ -0,0 +1,2 @@ +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 new file mode 100644 index 000000000..755fc343f --- /dev/null +++ b/test-suite/coq-makefile/uninstall1/theories/sub/testsub.v @@ -0,0 +1 @@ +Require Import test. diff --git a/test-suite/coq-makefile/uninstall1/theories/test.v b/test-suite/coq-makefile/uninstall1/theories/test.v new file mode 100644 index 000000000..7753b56aa --- /dev/null +++ b/test-suite/coq-makefile/uninstall1/theories/test.v @@ -0,0 +1,7 @@ +Declare ML Module "test_plugin". +Test. +Goal True. +Proof. +test. +exact I. +Qed. |