diff options
Diffstat (limited to 'test-suite')
67 files changed, 856 insertions, 16 deletions
diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache Binary files differindex b99d80e95f..ba85286dd3 100644 --- a/test-suite/.csdp.cache +++ b/test-suite/.csdp.cache diff --git a/test-suite/Makefile b/test-suite/Makefile index afaa48463b..a26f66285f 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -27,10 +27,10 @@ # Default value when called from a freshly compiled Coq, but can be # easily overridden -BIN := ../bin/ LIB := $(shell cd ..; pwd) +BIN := $(LIB)/bin/ -coqtop := $(BIN)coqtop -boot -q -batch -test-mode -R prerequisite TestSuite +coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite coqtopbyte := $(BIN)coqtop.byte @@ -45,7 +45,7 @@ REDIR := $(if $(VERBOSE),,> /dev/null 2>&1) # read out an emacs config and look for coq-prog-args; if such exists, return it get_coq_prog_args_helper = sed -n s'/^.*coq-prog-args:[[:space:]]*(\([^)]*\)).*/\1/p' $(1) -get_coq_prog_args = $(strip $(filter-out "-emacs-U" "-emacs",$(shell $(call get_coq_prog_args_helper,$(1))))) +get_coq_prog_args = $(strip $(shell $(call get_coq_prog_args_helper,$(1)))) SINGLE_QUOTE=" #" # double up on the quotes, in a comment, to appease the emacs syntax highlighter # wrap the arguments in parens, but only if they exist @@ -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`; \ @@ -439,7 +440,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) @echo "TEST $<" $(HIDE){ \ echo $(call log_intro,$<); \ - $(BIN)fake_ide $< "$(BIN)coqtop -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off" 2>&1; \ + $(BIN)fake_ide $< "$(BIN)coqtop -coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off" 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ @@ -481,3 +482,20 @@ 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)(\ + export COQBIN=$(BIN);\ + 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/bugs/closed/5523.v b/test-suite/bugs/closed/5523.v new file mode 100644 index 0000000000..d7582a3797 --- /dev/null +++ b/test-suite/bugs/closed/5523.v @@ -0,0 +1,6 @@ +(* Support for complex constructions in recursive notations, especially "match". *) + +Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y. +Notation "'dlet' x , y := v 'in' ( a , b , .. , c )" + := (Let_In v (fun '(x, y) => pair .. (pair a b) .. c)) + (at level 0). 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..e98da17c78 --- /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 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..28d9878f9b --- /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 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..d6bb52bb4a --- /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 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..d6bb52bb4a --- /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 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..ea5792a937 --- /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 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..214a9d5b28 --- /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 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..752c0c2cea --- /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 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..f6fb3bcb42 --- /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 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..f6fb3bcb42 --- /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 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..863c39f500 --- /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 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..bc9f846dda --- /dev/null +++ b/test-suite/coq-makefile/native1/run.sh @@ -0,0 +1,35 @@ +#!/usr/bin/env bash + +#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.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 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..2ea3deffb7 --- /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 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..24ef8c891b --- /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 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..24ef8c891b --- /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 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..24ef8c891b --- /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 0000000000..c952d41a30 --- /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 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..e525e12086 --- /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 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..e525e12086 --- /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 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..aaa4194b38 --- /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 diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 4d59a92cbf..f4ecfd7362 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -98,5 +98,10 @@ 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 +[fun x : nat => x + 0;; fun x : nat => x + 1;; fun x : nat => x + 2] + : (nat -> nat) * + ((nat -> nat) * + ((nat -> nat) * + ((nat -> nat) * ((nat -> nat) * ((nat -> nat) * (nat -> nat)))))) foo5 x nat x : nat -> nat diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 96d831944f..71536c68fb 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -140,6 +140,12 @@ Notation "'tele' x .. z := b" := Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt. +(* Checking that "fun" in a notation does not mixed up with the + detection of a recursive binder *) + +Notation "[ x ;; .. ;; y ]" := ((x,((fun u => S u), .. (y,(fun u => S u,fun v:nat => v)) ..))). +Check [ fun x => x+0 ;; fun x => x+1 ;; fun x => x+2 ]. + (* Cyprien's part of bug #4765 *) Notation foo5 x T y := (fun x : T => y). diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out new file mode 100644 index 0000000000..8acfed5d00 --- /dev/null +++ b/test-suite/output/Show.out @@ -0,0 +1,12 @@ +3 subgoals (ID 31) + + H : 0 = 0 + ============================ + 1 = 1 + +subgoal 2 (ID 35) is: + 1 = S (S m') +subgoal 3 (ID 22) is: + S (S n') = S m + +(dependent evars: (printing disabled) ) diff --git a/test-suite/output/Show.v b/test-suite/output/Show.v new file mode 100644 index 0000000000..60faac8dd9 --- /dev/null +++ b/test-suite/output/Show.v @@ -0,0 +1,11 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs") -*- *) + +(* tests of Show output with -emacs flag to coqtop; see bug 5535 *) + +Theorem nums : forall (n m : nat), n = m -> (S n) = (S m). +Proof. + intros. + induction n as [| n']. + induction m as [| m']. + Show. +Admitted. diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index c70467912f..d28ee42761 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -6,13 +6,13 @@ fun e : option L => match e with : option L -> option L fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H : forall m n p : nat, S m <= S n + p -> m <= n + p -fun n : nat => let x : T n := A n in ?t ?y : T n +fun n : nat => let y : T n := A n in ?t ?x : T n : forall n : nat, T n where -?t : [n : nat x := A n : T n |- ?T -> T n] -?y : [n : nat x := A n : T n |- ?T] -fun n : nat => ?t ?y : T n +?t : [n : nat y := A n : T n |- ?T -> T n] +?x : [n : nat y := A n : T n |- ?T] +fun n : nat => ?t ?x : T n : forall n : nat, T n where ?t : [n : nat |- ?T -> T n] -?y : [n : nat |- ?T] +?x : [n : nat |- ?T] diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v index 1825db1676..f761a4dc5a 100644 --- a/test-suite/output/inference.v +++ b/test-suite/output/inference.v @@ -27,5 +27,5 @@ Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H). (* Note: exact numbers of evars are not important... *) Inductive T (n:nat) : Type := A : T n. -Check fun n (x:=A n:T n) => _ _ : T n. +Check fun n (y:=A n:T n) => _ _ : T n. Check fun n => _ _ : T n. diff --git a/test-suite/output/names.out b/test-suite/output/names.out index 9471b892dd..48be63a46a 100644 --- a/test-suite/output/names.out +++ b/test-suite/output/names.out @@ -3,3 +3,9 @@ In environment y : nat The term "a y" has type "{y0 : nat | y = y0}" while it is expected to have type "{x : nat | x = y}". +1 focused subgoal +(shelved: 1) + + H : ?n <= 3 -> 3 <= ?n -> ?n = 3 + ============================ + True diff --git a/test-suite/output/names.v b/test-suite/output/names.v index b3b5071a03..f1efd0df2a 100644 --- a/test-suite/output/names.v +++ b/test-suite/output/names.v @@ -3,3 +3,7 @@ Parameter a : forall x, {y:nat|x=y}. Fail Definition b y : {x:nat|x=y} := a y. + +Goal (forall n m, n <= m -> m <= n -> n = m) -> True. +intro H; epose proof (H _ 3) as H. +Show. diff --git a/test-suite/success/Abstract.v b/test-suite/success/Abstract.v index ffd50f6efd..69dc9aca78 100644 --- a/test-suite/success/Abstract.v +++ b/test-suite/success/Abstract.v @@ -1,4 +1,3 @@ - (* Cf coqbugs #546 *) Require Import Omega. 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/forward.v b/test-suite/success/forward.v new file mode 100644 index 0000000000..0ed5b524f3 --- /dev/null +++ b/test-suite/success/forward.v @@ -0,0 +1,18 @@ +(* Testing forward reasoning *) + +Goal 0=0. +Fail assert (_ = _). +eassert (_ = _)by reflexivity. +eassumption. +Qed. + +Goal 0=0. +Fail set (S ?[nl]). +eset (S ?[n]). +remember (S ?n) as x. +instantiate (n:=0). +Fail remember (S (S _)). +eremember (S (S ?[x])). +instantiate (x:=0). +reflexivity. +Qed. 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. |