diff options
Diffstat (limited to 'test-suite')
59 files changed, 800 insertions, 5 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index afaa48463b..c2d6e540c6 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 coq-makefile/$*" + $(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/bugs/closed/348.v b/test-suite/bugs/closed/348.v index 28cc5cb1e6..48f0b55129 100644 --- a/test-suite/bugs/closed/348.v +++ b/test-suite/bugs/closed/348.v @@ -9,5 +9,5 @@ End D. Module D' (M:S). Import M. - Definition empty:Set. exact nat. Save. + Definition empty:Set. exact nat. Qed. End D'. diff --git a/test-suite/bugs/closed/38.v b/test-suite/bugs/closed/38.v index 4fc8d7c97d..6b6e83779f 100644 --- a/test-suite/bugs/closed/38.v +++ b/test-suite/bugs/closed/38.v @@ -14,7 +14,7 @@ Definition same := fun (l m : liste) => forall (x : A), e x l <-> e x m. Definition same_refl (x:liste) : (same x x). unfold same; split; intros; trivial. -Save. +Qed. Goal forall (x:liste), (same x x). intro. diff --git a/test-suite/bugs/closed/5153.v b/test-suite/bugs/closed/5153.v new file mode 100644 index 0000000000..be6407b5fa --- /dev/null +++ b/test-suite/bugs/closed/5153.v @@ -0,0 +1,8 @@ +(* An example where it does not hurt having more type-classes resolution *) +Class some_type := { Ty : Type }. +Instance: some_type := { Ty := nat }. +Arguments Ty : clear implicits. +Goal forall (H : forall t : some_type, @Ty t -> False) (H' : False -> 1 = 2), 1 = 2. +Proof. +intros H H'. +specialize (H' (@H _ O)). (* was failing *) diff --git a/test-suite/coq-makefile/arg/_CoqProject b/test-suite/coq-makefile/arg/_CoqProject new file mode 100644 index 0000000000..afdb32e7cf --- /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 0000000000..28b9bcb969 --- /dev/null +++ b/test-suite/coq-makefile/arg/run.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +#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 0000000000..4f44bde22a --- /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 0000000000..ccb348c6fa --- /dev/null +++ b/test-suite/coq-makefile/compat-subdirs/run.sh @@ -0,0 +1,9 @@ +#!/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/compat-subdirs/subdir/Makefile b/test-suite/coq-makefile/compat-subdirs/subdir/Makefile new file mode 100644 index 0000000000..846c9b791b --- /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 0000000000..35792066bb --- /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 0000000000..e071f1db7a --- /dev/null +++ b/test-suite/coq-makefile/coqdoc1/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/coqdoc2/_CoqProject b/test-suite/coq-makefile/coqdoc2/_CoqProject new file mode 100644 index 0000000000..d2a547d47b --- /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 0000000000..e071f1db7a --- /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 0000000000..b031d30dbd --- /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 0000000000..69f47302e1 --- /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 0000000000..db11601132 --- /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 0000000000..23f52b154a --- /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 0000000000..35792066bb --- /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 0000000000..45f2269113 --- /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 new file mode 100644 index 0000000000..69f47302e1 --- /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 0000000000..9b89e5b6e9 --- /dev/null +++ b/test-suite/coq-makefile/merlin1/run.sh @@ -0,0 +1,15 @@ +#!/bin/sh + +#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 0000000000..69f47302e1 --- /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 0000000000..418a2fb775 --- /dev/null +++ b/test-suite/coq-makefile/mlpack1/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/mlpack2/_CoqProject b/test-suite/coq-makefile/mlpack2/_CoqProject new file mode 100644 index 0000000000..51864a87ae --- /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 0000000000..418a2fb775 --- /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 0000000000..b384bb6d97 --- /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 0000000000..a24a8a3cf7 --- /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 0000000000..a6fa17348c --- /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 0000000000..097bd6398a --- /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/only/_CoqProject b/test-suite/coq-makefile/only/_CoqProject new file mode 100644 index 0000000000..357384fddf --- /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 0000000000..4b471bcb80 --- /dev/null +++ b/test-suite/coq-makefile/only/run.sh @@ -0,0 +1,12 @@ +#!/bin/sh + +#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 0000000000..4eddc9d708 --- /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 0000000000..684e0ece82 --- /dev/null +++ b/test-suite/coq-makefile/plugin1/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/plugin2/_CoqProject b/test-suite/coq-makefile/plugin2/_CoqProject new file mode 100644 index 0000000000..0bf1e07f25 --- /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 0000000000..684e0ece82 --- /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 0000000000..2028d49a8b --- /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 0000000000..684e0ece82 --- /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 0000000000..bfd2c1b959 --- /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/template/src/test.ml4 b/test-suite/coq-makefile/template/src/test.ml4 new file mode 100644 index 0000000000..72765abe04 --- /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 0000000000..e69de29bb2 --- /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 0000000000..a01d0865a8 --- /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 0000000000..10020f27de --- /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 0000000000..cf94d851bb --- /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 0000000000..755fc343f2 --- /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 0000000000..744b5aad78 --- /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 0000000000..35792066bb --- /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 0000000000..d241762791 --- /dev/null +++ b/test-suite/coq-makefile/uninstall1/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/uninstall2/_CoqProject b/test-suite/coq-makefile/uninstall2/_CoqProject new file mode 100644 index 0000000000..d2a547d47b --- /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 0000000000..d241762791 --- /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 0000000000..69f47302e1 --- /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 0000000000..61025021d0 --- /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 diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 360f379676..4d59a92cbf 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -98,3 +98,5 @@ fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0)) : nat -> Prop tele (t : Type) '(y, z) (x : t0) := tt : forall t : Type, nat * nat -> t -> fpack +foo5 x nat x + : nat -> nat diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 4b8bfe3124..96d831944f 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -139,3 +139,8 @@ Notation "'tele' x .. z := b" := (at level 85, x binder, z binder). Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt. + +(* Cyprien's part of bug #4765 *) + +Notation foo5 x T y := (fun x : T => y). +Check foo5 x nat x. diff --git a/test-suite/output/goal_output.out b/test-suite/output/goal_output.out new file mode 100644 index 0000000000..773533a8d3 --- /dev/null +++ b/test-suite/output/goal_output.out @@ -0,0 +1,8 @@ +Nat.t = nat + : Set +Nat.t = nat + : Set +1 subgoal + + ============================ + False diff --git a/test-suite/output/goal_output.v b/test-suite/output/goal_output.v new file mode 100644 index 0000000000..327b80b0aa --- /dev/null +++ b/test-suite/output/goal_output.v @@ -0,0 +1,13 @@ +(* From + - https://coq.inria.fr/bugs/show_bug.cgi?id=5529 + - https://coq.inria.fr/bugs/show_bug.cgi?id=5537 + *) + +Print Nat.t. +Timeout 1 Print Nat.t. + +Lemma toto: False. +Set Printing All. +Show. +Abort. + diff --git a/test-suite/success/ROmega0.v b/test-suite/success/ROmega0.v index 1348bb6238..42730f2e16 100644 --- a/test-suite/success/ROmega0.v +++ b/test-suite/success/ROmega0.v @@ -135,11 +135,13 @@ Qed. (* Magaud #240 *) Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x. +Proof. intros. romega. Qed. Lemma test_romega_8b : forall x y:Z, x*x<y*y-> ~ y*y <= x*x. +Proof. intros x y. romega. Qed. @@ -147,6 +149,20 @@ Qed. (* Besson #1298 *) Lemma test_romega9 : forall z z':Z, z<>z' -> z'=z -> False. +Proof. intros. romega. Qed. + +(* Letouzey, May 2017 *) + +Lemma test_romega10 : forall x a a' b b', + a' <= b -> + a <= b' -> + b < b' -> + a < a' -> + a <= x < b' <-> a <= x < b \/ a' <= x < b'. +Proof. + intros. + romega. +Qed. diff --git a/test-suite/success/change.v b/test-suite/success/change.v index 1f0b7d38a9..a9821b027f 100644 --- a/test-suite/success/change.v +++ b/test-suite/success/change.v @@ -59,3 +59,12 @@ unfold x. (* check that n in 0+n is not interpreted as the n from "fun n" *) change n with (0+n). Abort. + +(* Check non-collision of non-normalized defined evars with pattern variables *) + +Goal exists x, 1=1 -> x=1/\x=1. +eexists ?[n]; intros; split. +eassumption. +match goal with |- ?x=1 => change (x=1) with (0+x=1) end. +match goal with |- 0+1=1 => trivial end. +Qed. diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index 12ddbda84e..f5bb884d27 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -15,7 +15,7 @@ Proof. intros n H. dependent destruction H. assumption. -Save. +Qed. Require Import ProofIrrelevance. @@ -25,7 +25,7 @@ Proof. dependent destruction v. exists v ; exists a. reflexivity. -Save. +Qed. (* Extraction Unnamed_thm. *) diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v index fba05cd902..4b41a509e5 100644 --- a/test-suite/success/specialize.v +++ b/test-suite/success/specialize.v @@ -72,3 +72,11 @@ intros. specialize (H 1) as ->. reflexivity. Qed. + +(* A test from corn *) + +Goal (forall x y, x=0 -> y=0 -> True) -> True. +intros. +specialize (fun z => H 0 z eq_refl). +exact (H 0 eq_refl). +Qed. |