diff options
Diffstat (limited to 'test-suite')
48 files changed, 807 insertions, 160 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 6865dcc76..16a56f440 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -40,6 +40,7 @@ coqtopload := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source coqtopcompile := $(coqtop) -compile coqdep := $(BIN)coqdep -coqlib $(LIB) +VERBOSE?= SHOW := $(if $(VERBOSE),@true,@echo) HIDE := $(if $(VERBOSE),,@) REDIR := $(if $(VERBOSE),,> /dev/null 2>&1) @@ -174,10 +175,20 @@ summary.log: # if not on travis we can get the log files (they're just there for a # local build, and downloadable on GitLab) +PRINT_LOGS?= +TRAVIS?= # special because we want to print travis_fold directives +ifdef APPVEYOR +PRINT_LOGS:=APPVEYOR +else +ifdef CIRCLECI +PRINT_LOGS:=CIRCLECI +endif #CIRCLECI +endif #APPVEYOR + report: summary.log $(HIDE)bash save-logs.sh $(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo "travis_fold:start:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo "travis_fold:end:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';'; fi - $(HIDE)if [ -n "${APPVEYOR}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo {}' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo' ';'; fi + $(HIDE)if [ -n "${PRINT_LOGS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo {}' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo' ';'; fi $(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi ####################################################################### @@ -312,6 +323,13 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) rm $$tmpoutput; \ } > "$@" +# the expected output for the MExtraction test is +# /plugins/micromega/micromega.ml except with additional newline +output/MExtraction.out: ../plugins/micromega/micromega.ml + $(SHOW) GEN $@ + $(HIDE) cp $< $@ + $(HIDE) echo >> $@ + $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ diff --git a/test-suite/README.md b/test-suite/README.md new file mode 100644 index 000000000..1d1195646 --- /dev/null +++ b/test-suite/README.md @@ -0,0 +1,75 @@ +# Coq Test Suite + +The test suite can be run from the Coq root directory by `make test-suite`. +This does a clean step first, so if you've already run it, then change something, +you'll have to do a lot of work again. + +If you run `make` from the `test-suite` directory, there is no clean step. +You can also run `make aaa/bbb/ccc.v.log` to build the log for one test, +or `make ddd` where `ddd` is on of the sub-directories of `test-suite` +to just build the logs for that directory. +In these cases, a summary is not printed, but can be generated by `make summary`. + +`make -B` can be used to rerun tests ( -B meaning always remake). + +From the `test-suite` directory, `make report` (included in `make +all`) prints a summary of which tests failed using the produced log +files (this still works when only some tests are built as described +above). Setting the `PRINT_LOGS` variable will make it print the logs +of the failing tests. + +For instance, running the following in the `test-suite` directory: + +```bash +$ echo Fail. > success/fail.v # make some failing test + +$ make +TEST prerequisite/make_local.v +... +TEST success/fail.v +... +BUILDING SUMMARY FILE +FAILURES + success/fail.v...Error! (should be accepted) +Makefile:189: recipe for target 'all failed +make: *** [report] Error 1 + +$ make report PRINT_LOGS=1 +BUILDING SUMMARY FILE +logs/success/fail.v.log +==========> TESTING success/fail.v <========== +Welcome to Coq (version information) +Skipping rcfile loading. +File "/path/to/success/fail.v", line 1, characters 4-5: +Error: +Syntax error: [vernac:Vernac.vernac_control] expected after 'Fail' (in [vernac:Vernac.vernac_control]). + +0m0.000000s 0m0.000000s +0m0.040000s 0m0.000000s +==========> FAILURE <========== + success/fail.v...Error! (should be accepted) + +FAILURES + success/fail.v...Error! (should be accepted) +Makefile:189: recipe for target 'report' failed +make: *** [report] Error 1 + +$ echo 'Comments "foo".' > success/fail.v + +$ make +TEST success/fail.v +BUILDING SUMMARY FILE +NO FAILURES +``` + +See [`test-suite/Makefile`](/test-suite/Makefile) for more information. + +## Adding a test + +Regression tests for closed bugs should be added to `test-suite/bugs/closed`, as `1234.v` where `1234` is the bug number. +Files in this directory are tested for successful compilation. +When you fix a bug, you should usually add a regression test here as well. + +The error "(bug seems to be opened, please check)" when running `make test-suite` means that a test in `bugs/closed` failed to compile. + +There are also output tests in `test-suite/output` which consist of a `.v` file and a `.out` file with the expected output. diff --git a/test-suite/bugs/closed/4390.v b/test-suite/bugs/closed/4390.v index a96a13700..c069b2d9d 100644 --- a/test-suite/bugs/closed/4390.v +++ b/test-suite/bugs/closed/4390.v @@ -8,16 +8,16 @@ Universe i. End foo. End M. -Check Type@{i}. +Check Type@{M.i}. (* Succeeds *) Fail Check Type@{j}. (* Error: Undeclared universe: j *) -Definition foo@{j} : Type@{i} := Type@{j}. +Definition foo@{j} : Type@{M.i} := Type@{j}. (* ok *) End A. - +Import A. Import M. Set Universe Polymorphism. Fail Universes j. Monomorphic Universe j. diff --git a/test-suite/bugs/closed/5368.v b/test-suite/bugs/closed/5368.v new file mode 100644 index 000000000..410fe1707 --- /dev/null +++ b/test-suite/bugs/closed/5368.v @@ -0,0 +1,6 @@ +Set Universe Polymorphism. + +Record cantype := {T:Type; op:T -> unit}. +Canonical Structure test (P:Type) := {| T := P -> Type; op := fun _ => tt|}. + +Check (op _ ((fun (_:unit) => Set):_)). diff --git a/test-suite/bugs/closed/6323.v b/test-suite/bugs/closed/6323.v new file mode 100644 index 000000000..fdc33befc --- /dev/null +++ b/test-suite/bugs/closed/6323.v @@ -0,0 +1,9 @@ +Goal True. + simple refine (let X : Type := _ in _); + [ abstract exact Set using Set' + | let X' := (eval cbv delta [X] in X) in + clear X; + simple refine (let id' : { x : X' | True } -> X' := _ in _); + [ abstract refine (@proj1_sig _ _) | ] + ]. +Abort. diff --git a/test-suite/bugs/closed/6378.v b/test-suite/bugs/closed/6378.v new file mode 100644 index 000000000..68ae7961d --- /dev/null +++ b/test-suite/bugs/closed/6378.v @@ -0,0 +1,18 @@ +Require Import Coq.ZArith.ZArith. +Ltac profile_constr tac := + let dummy := match goal with _ => reset ltac profile; start ltac profiling end in + let ret := match goal with _ => tac () end in + let dummy := match goal with _ => stop ltac profiling; show ltac profile end in + pose 1. + +Ltac slow _ := eval vm_compute in (Z.div_eucl, Z.div_eucl, Z.div_eucl, Z.div_eucl, Z.div_eucl). + +Goal True. + start ltac profiling. + reset ltac profile. + reset ltac profile. + stop ltac profiling. + time profile_constr slow. + show ltac profile cutoff 0. + show ltac profile "slow". +Abort. diff --git a/test-suite/bugs/closed/gh6384.v b/test-suite/bugs/closed/gh6384.v new file mode 100644 index 000000000..cec84642f --- /dev/null +++ b/test-suite/bugs/closed/gh6384.v @@ -0,0 +1,5 @@ +Theorem test (A:Prop) : A \/ A -> A. + Fail intro H; destruct H as H. + (* Error: Disjunctive/conjunctive introduction pattern expected. *) + Fail intros H; destruct H as H. +Abort. diff --git a/test-suite/bugs/closed/gh6385.v b/test-suite/bugs/closed/gh6385.v new file mode 100644 index 000000000..3bbb664f4 --- /dev/null +++ b/test-suite/bugs/closed/gh6385.v @@ -0,0 +1,5 @@ +Theorem test (A:Prop) : A \/ A -> A. + Fail let H := idtac in intros H; destruct H as H'. + (* Disjunctive/conjunctive introduction pattern expected. *) + Fail let H' := idtac in intros H; destruct H as H'. +Abort. diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh deleted file mode 100755 index e48f704a2..000000000 --- a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh +++ /dev/null @@ -1,36 +0,0 @@ -#!/usr/bin/env bash - -set -e - -cat > _CoqProject <<EOT --I src/ - -./src/test_plugin.mllib -./src/test.ml4 -./src/test.mli -EOT - -mkdir -p src - -cat > src/test_plugin.mllib <<EOT -Test -EOT - -touch src/test.mli - -cat > src/test.ml4 <<EOT -DECLARE PLUGIN "test" - -let _ = Pre_env.empty_env -EOT - -${COQBIN}coq_makefile -f _CoqProject -o Makefile -cat Makefile.conf - -if make VERBOSE=1; then - # make command should have failed (but didn't) - exit 1 -else - # make command should have failed (and it indeed did) - exit 0 -fi diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh deleted file mode 100755 index 4a8f58655..000000000 --- a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh +++ /dev/null @@ -1,31 +0,0 @@ -#!/usr/bin/env bash - -set -e - -cat > _CoqProject <<EOT --bypass-API --I src/ - -./src/test_plugin.mllib -./src/test.ml4 -./src/test.mli -EOT - -mkdir -p src - -cat > src/test_plugin.mllib <<EOT -Test -EOT - -touch src/test.mli - -cat > src/test.ml4 <<EOT -DECLARE PLUGIN "test" - -let _ = Pre_env.empty_env -EOT - -${COQBIN}coq_makefile -f _CoqProject -o Makefile -cat Makefile.conf - -make VERBOSE=1 diff --git a/test-suite/coq-makefile/template/src/test.ml4 b/test-suite/coq-makefile/template/src/test.ml4 index e7d0bfe1f..72765abe0 100644 --- a/test-suite/coq-makefile/template/src/test.ml4 +++ b/test-suite/coq-makefile/template/src/test.ml4 @@ -1,4 +1,3 @@ -open API open Ltac_plugin DECLARE PLUGIN "test_plugin" let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";; diff --git a/test-suite/coq-makefile/template/src/test_aux.ml b/test-suite/coq-makefile/template/src/test_aux.ml index e134abd84..a01d0865a 100644 --- a/test-suite/coq-makefile/template/src/test_aux.ml +++ b/test-suite/coq-makefile/template/src/test_aux.ml @@ -1 +1 @@ -let tac = API.Proofview.tclUNIT () +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 index 2e7ad1529..10020f27d 100644 --- a/test-suite/coq-makefile/template/src/test_aux.mli +++ b/test-suite/coq-makefile/template/src/test_aux.mli @@ -1 +1 @@ -val tac : unit API.Proofview.tactic +val tac : unit Proofview.tactic diff --git a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired index 729de2f36..7900c034d 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired @@ -1,7 +1,6 @@ Makefile:69: warning: undefined variable '*' Makefile:204: warning: undefined variable 'DSTROOT' -COQDEP Fast.v -COQDEP Slow.v +COQDEP VFILES Makefile:69: warning: undefined variable '*' Makefile:204: warning: undefined variable 'DSTROOT' Makefile:69: warning: undefined variable '*' diff --git a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired index b25bc3683..7ab0bc75d 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired @@ -1,7 +1,6 @@ Makefile:69: warning: undefined variable '*' Makefile:204: warning: undefined variable 'DSTROOT' -COQDEP Fast.v -COQDEP Slow.v +COQDEP VFILES Makefile:69: warning: undefined variable '*' Makefile:204: warning: undefined variable 'DSTROOT' Makefile:69: warning: undefined variable '*' diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index 898af5590..2439d3f37 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -31,16 +31,16 @@ coq_makefile -f _CoqProject -o Makefile make cleanall make make-pretty-timed-after TGTS="all" -j1 || exit $? rm -f time-of-build-before.log -make print-pretty-timed-diff TIME_OF_BUILD_BEFORE_FILE=../before/time-of-build-before.log +make print-pretty-timed-diff TIMING_SORT_BY=diff TIME_OF_BUILD_BEFORE_FILE=../before/time-of-build-before.log cp ../before/time-of-build-before.log ./ -make print-pretty-timed-diff || exit $? +make print-pretty-timed-diff TIMING_SORT_BY=diff || exit $? INFINITY="∞" INFINITY_REPLACEMENT="+.%" # assume that if the before time is zero, we expected the time to increase for ext in "" .desired; do for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do - cat ${file}${ext} | grep -v 'warning: undefined variable' | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s'/[0-9]//g' | sed s'/ *$//g' | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/^-*$/------/g' | sed s'/ */ /g' | sed s'/\(Total.*\)-\(.*\)-/\1+\2+/g' > ${file}${ext}.processed + cat ${file}${ext} | grep -v 'warning: undefined variable' | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s'/[0-9]//g' | sed s'/ *$//g' | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/^-*$/------/g' | sed s'/ */ /g' | sed s'/\(Total.*\)-\(.*\)-/\1+\2+/g' > ${file}${ext}.processed done done for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do @@ -74,7 +74,7 @@ echo for ext in "" .desired; do for file in A.v.timing.diff; do - cat ${file}${ext} | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/[0-9]*\.[0-9]*//g' | sed s'/0//g' | sed s'/ */ /g' | sed s'/+/-/g' | sort > ${file}${ext}.processed + cat ${file}${ext} | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/[0-9]*\.[0-9]*//g' | sed s'/0//g' | sed s'/ */ /g' | sed s'/ *$//g' | sed s'/+/-/g' | sort > ${file}${ext}.processed done done for file in A.v.timing.diff; do diff --git a/test-suite/output-modulo-time/ltacprof.out b/test-suite/output-modulo-time/ltacprof.out index cc04c2c9b..5553e1b38 100644 --- a/test-suite/output-modulo-time/ltacprof.out +++ b/test-suite/output-modulo-time/ltacprof.out @@ -1,12 +1,15 @@ -total time: 1.528s +total time: 1.032s - tactic local total calls max + tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─sleep' -------------------------------- 100.0% 100.0% 1 1.528s +─sleep' -------------------------------- 100.0% 100.0% 1 1.032s +─sleep --------------------------------- 0.0% 0.0% 0 0.000s ─constructor --------------------------- 0.0% 0.0% 1 0.000s - tactic local total calls max + tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─sleep' -------------------------------- 100.0% 100.0% 1 1.528s +─sleep' -------------------------------- 100.0% 100.0% 1 1.032s +─sleep --------------------------------- 0.0% 0.0% 0 0.000s +└sleep' -------------------------------- 0.0% 0.0% 0 0.000s ─constructor --------------------------- 0.0% 0.0% 1 0.000s diff --git a/test-suite/output-modulo-time/ltacprof_abstract.out b/test-suite/output-modulo-time/ltacprof_abstract.out new file mode 100644 index 000000000..fef4fa248 --- /dev/null +++ b/test-suite/output-modulo-time/ltacprof_abstract.out @@ -0,0 +1,17 @@ +total time: 0.922s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─abstract (sleep; constructor) --------- 0.0% 100.0% 1 0.922s +─sleep' -------------------------------- 100.0% 100.0% 1 0.922s +─constructor --------------------------- 0.0% 0.0% 1 0.000s +─sleep --------------------------------- 0.0% 0.0% 0 0.000s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─abstract (sleep; constructor) --------- 0.0% 100.0% 1 0.922s + ├─sleep' ------------------------------ 100.0% 100.0% 1 0.922s + ├─constructor ------------------------- 0.0% 0.0% 1 0.000s + └─sleep ------------------------------- 0.0% 0.0% 0 0.000s + └sleep' ------------------------------ 0.0% 0.0% 0 0.000s + diff --git a/test-suite/output-modulo-time/ltacprof_abstract.v b/test-suite/output-modulo-time/ltacprof_abstract.v new file mode 100644 index 000000000..10a76309e --- /dev/null +++ b/test-suite/output-modulo-time/ltacprof_abstract.v @@ -0,0 +1,8 @@ +(* -*- coq-prog-args: ("-profile-ltac-cutoff" "0.0") -*- *) +Ltac sleep' := do 100 (do 100 (do 100 idtac)). +Ltac sleep := sleep'. + +Theorem x : True. +Proof. + idtac. idtac. abstract (sleep; constructor). +Defined. diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.out b/test-suite/output-modulo-time/ltacprof_cutoff.out index 0cd5777cc..d91a38bb5 100644 --- a/test-suite/output-modulo-time/ltacprof_cutoff.out +++ b/test-suite/output-modulo-time/ltacprof_cutoff.out @@ -1,31 +1,37 @@ -total time: 1.584s +total time: 1.632s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s -─sleep --------------------------------- 100.0% 100.0% 3 0.572s -─foo1 ---------------------------------- 0.0% 63.9% 1 1.012s +─sleep --------------------------------- 100.0% 100.0% 3 0.584s +─foo2 ---------------------------------- 0.0% 100.0% 1 1.632s +─foo1 ---------------------------------- 0.0% 64.2% 1 1.048s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s -└foo1 ---------------------------------- 0.0% 63.9% 1 1.012s +─foo2 ---------------------------------- 0.0% 100.0% 1 1.632s +└foo1 ---------------------------------- 0.0% 64.2% 1 1.048s -total time: 1.584s +total time: 0.520s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─foo2 ---------------------------------- 0.0% 100.0% 1 0.520s +─sleep --------------------------------- 99.2% 99.2% 52 0.016s +─foo1 ---------------------------------- 0.0% 97.7% 1 0.508s +─foo0 ---------------------------------- 0.8% 96.2% 1 0.500s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─foo2 ---------------------------------- 0.0% 100.0% 1 0.520s +└foo1 ---------------------------------- 0.0% 97.7% 1 0.508s +└foo0 ---------------------------------- 0.8% 96.2% 1 0.500s +└sleep --------------------------------- 95.4% 95.4% 50 0.016s + +total time: 0.000s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─sleep --------------------------------- 100.0% 100.0% 3 0.572s -─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s -─foo1 ---------------------------------- 0.0% 63.9% 1 1.012s -─foo0 ---------------------------------- 0.0% 31.3% 1 0.496s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s - ├─foo1 -------------------------------- 0.0% 63.9% 1 1.012s - │ ├─sleep ----------------------------- 32.6% 32.6% 1 0.516s - │ └─foo0 ------------------------------ 0.0% 31.3% 1 0.496s - │ └sleep ----------------------------- 31.3% 31.3% 1 0.496s - └─sleep ------------------------------- 36.1% 36.1% 1 0.572s diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v index 3dad6271a..ae5d51bae 100644 --- a/test-suite/output-modulo-time/ltacprof_cutoff.v +++ b/test-suite/output-modulo-time/ltacprof_cutoff.v @@ -1,12 +1,28 @@ (* -*- coq-prog-args: ("-profile-ltac") -*- *) Require Coq.ZArith.BinInt. -Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac). +Module WithIdTac. + Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac). -Ltac foo0 := idtac; sleep. -Ltac foo1 := sleep; foo0. -Ltac foo2 := sleep; foo1. -Goal True. - foo2. - Show Ltac Profile CutOff 47. - constructor. -Qed. + Ltac foo0 := idtac; sleep. + Ltac foo1 := sleep; foo0. + Ltac foo2 := sleep; foo1. + Goal True. + foo2. + Show Ltac Profile CutOff 47. + constructor. + Qed. +End WithIdTac. + +Module TestEval. + Ltac sleep := let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac. + + Ltac foo0 := idtac; do 50 (idtac; sleep). + Ltac foo1 := sleep; foo0. + Ltac foo2 := sleep; foo1. + Goal True. + Reset Ltac Profile. + foo2. + Show Ltac Profile CutOff 47. + constructor. + Qed. +End TestEval. diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 97fa8e254..419dcadb4 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -95,8 +95,7 @@ fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl x : nat n, n0 := match x + 0 with - | 0 => 0 - | S _ => 0 + | 0 | S _ => 0 end : nat e, e0 := match x + 0 as y return (y = y) with @@ -104,8 +103,7 @@ fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl | S n => eq_refl end : x + 0 = x + 0 n1, n2 := match x with - | 0 => 0 - | S _ => 0 + | 0 | S _ => 0 end : nat e1, e2 := match x return (x = x) with | 0 => eq_refl @@ -126,3 +124,48 @@ fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl end : p = p /\ p = p ============================ eq_refl = eq_refl +fun x : comparison => match x with + | Eq => 1 + | _ => 0 + end + : comparison -> nat +fun x : comparison => match x with + | Eq => 1 + | Lt => 0 + | Gt => 0 + end + : comparison -> nat +fun x : comparison => match x with + | Eq => 1 + | Lt | Gt => 0 + end + : comparison -> nat +fun x : comparison => +match x return nat with +| Eq => S O +| Lt => O +| Gt => O +end + : forall _ : comparison, nat +fun x : K => match x with + | a3 | a4 => 3 + | _ => 2 + end + : K -> nat +fun x : K => match x with + | a1 | a2 => 4 + | a3 => 3 + | _ => 2 + end + : K -> nat +fun x : K => match x with + | a1 | a2 => 4 + | a4 => 3 + | _ => 2 + end + : K -> nat +fun x : K => match x with + | a1 | a3 | a4 => 3 + | _ => 2 + end + : K -> nat diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 17fee3303..caf3b2870 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -1,5 +1,7 @@ (* Cases with let-in in constructors types *) +Unset Printing Allow Match Default Clause. + Inductive t : Set := k : let x := t in x -> x. @@ -184,3 +186,33 @@ let p := fresh "p" in |- eq_refl ?p = _ => pose (match eq_refl p in _ = z return p=p /\ z=z with eq_refl => conj eq_refl eq_refl end) end. Show. + +Set Printing Allow Match Default Clause. + +(***************************************************) +(* Testing strategy for factorizing cases branches *) + +(* Factorization + default clause *) +Check fun x => match x with Eq => 1 | _ => 0 end. + +(* No factorization *) +Unset Printing Factorizable Match Patterns. +Check fun x => match x with Eq => 1 | _ => 0 end. +Set Printing Factorizable Match Patterns. + +(* Factorization but no default clause *) +Unset Printing Allow Match Default Clause. +Check fun x => match x with Eq => 1 | _ => 0 end. +Set Printing Allow Match Default Clause. + +(* No factorization in printing all mode *) +Set Printing All. +Check fun x => match x with Eq => 1 | _ => 0 end. +Unset Printing All. + +(* Several clauses *) +Inductive K := a1|a2|a3|a4|a5|a6. +Check fun x => match x with a3 | a4 => 3 | _ => 2 end. +Check fun x => match x with a3 => 3 | a2 | a1 => 4 | _ => 2 end. +Check fun x => match x with a4 => 3 | a2 | a1 => 4 | _ => 2 end. +Check fun x => match x with a3 | a4 | a1 => 3 | _ => 2 end. diff --git a/test-suite/output/Extraction_infix.out b/test-suite/output/Extraction_infix.out new file mode 100644 index 000000000..29d50775a --- /dev/null +++ b/test-suite/output/Extraction_infix.out @@ -0,0 +1,20 @@ +(** val test : foo **) + +let test = + (fun (b, p) -> bar) (True, False) +(** val test : foo **) + +let test = + True@@?False +(** val test : foo **) + +let test = + True#^^False +(** val test : foo **) + +let test = + True@?:::False +(** val test : foo **) + +let test = + True @?::: False diff --git a/test-suite/output/Extraction_infix.v b/test-suite/output/Extraction_infix.v new file mode 100644 index 000000000..fe5926a36 --- /dev/null +++ b/test-suite/output/Extraction_infix.v @@ -0,0 +1,26 @@ +(* @herbelin's example for issue #6212 *) + +Require Import Extraction. +Inductive I := C : bool -> bool -> I. +Definition test := C true false. + +(* the parentheses around the function wrong signalled an infix operator *) + +Extract Inductive I => "foo" [ "(fun (b, p) -> bar)" ]. +Extraction test. + +(* some bonafide infix operators *) + +Extract Inductive I => "foo" [ "(@@?)" ]. +Extraction test. + +Extract Inductive I => "foo" [ "(#^^)" ]. +Extraction test. + +Extract Inductive I => "foo" [ "(@?:::)" ]. +Extraction test. + +(* allow whitespace around infix operator *) + +Extract Inductive I => "foo" [ "( @?::: )" ]. +Extraction test. diff --git a/test-suite/output/InvalidDisjunctiveIntro.out b/test-suite/output/InvalidDisjunctiveIntro.out new file mode 100644 index 000000000..25a306b45 --- /dev/null +++ b/test-suite/output/InvalidDisjunctiveIntro.out @@ -0,0 +1,16 @@ +The command has indeed failed with message: +Cannot coerce to a disjunctive/conjunctive pattern. +The command has indeed failed with message: +Disjunctive/conjunctive introduction pattern expected. +The command has indeed failed with message: +Cannot coerce to a disjunctive/conjunctive pattern. +The command has indeed failed with message: +Cannot coerce to a disjunctive/conjunctive pattern. +The command has indeed failed with message: +Ltac variable H is bound to <tactic closure> which cannot be coerced to +an introduction pattern. +The command has indeed failed with message: +Disjunctive/conjunctive introduction pattern expected. +The command has indeed failed with message: +Ltac variable H' is bound to <tactic closure> which cannot be coerced to +an introduction pattern. diff --git a/test-suite/output/InvalidDisjunctiveIntro.v b/test-suite/output/InvalidDisjunctiveIntro.v new file mode 100644 index 000000000..4febdf034 --- /dev/null +++ b/test-suite/output/InvalidDisjunctiveIntro.v @@ -0,0 +1,18 @@ +Theorem test (A:Prop) : A \/ A -> A. + Fail intros H; destruct H as H. + (* Cannot coerce to a disjunctive/conjunctive pattern. *) + Fail intro H; destruct H as H. + (* Disjunctive/conjunctive introduction pattern expected. *) + Fail let H := fresh in intro H; destruct H as H. + (* Cannot coerce to a disjunctive/conjunctive pattern. *) + Fail let H := fresh in intros H; destruct H as H. + (* Cannot coerce to a disjunctive/conjunctive pattern. *) + Fail let H := idtac in intros H; destruct H as H. + (* Ltac variable H is bound to <tactic closure> which cannot be +coerced to an introduction pattern. *) + Fail let H := idtac in intros H; destruct H as H'. + (* Disjunctive/conjunctive introduction pattern expected. *) + Fail let H' := idtac in intros H; destruct H as H'. +(* Ltac variable H' is bound to <tactic closure> which cannot +be coerced to an introduction pattern. *) +Abort. diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v new file mode 100644 index 000000000..352e422cf --- /dev/null +++ b/test-suite/output/MExtraction.v @@ -0,0 +1,12 @@ +Require Import micromega.MExtraction. +Require Import RingMicromega. +Require Import QArith. +Require Import VarMap. +Require Import ZMicromega. +Require Import QMicromega. +Require Import RMicromega. + +Recursive Extraction + List.map RingMicromega.simpl_cone (*map_cone indexes*) + denorm Qpower vm_add + n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 7bcd7b041..2f0ee765d 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -64,7 +64,7 @@ The command has indeed failed with message: Cannot find where the recursive pattern starts. The command has indeed failed with message: Both ends of the recursive pattern are the same. -SUM (nat * nat) nat +(nat * nat + nat)%type : Set FST (0; 1) : Z @@ -72,7 +72,7 @@ Nil : forall A : Type, list A NIL : list nat : list nat -(false && I 3)%bool /\ I 6 +(false && I 3)%bool /\ (I 6)%bool : Prop [|1, 2, 3; 4, 5, 6|] : Z * Z * Z * (Z * Z * Z) diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index fe6c05c39..413812ee1 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -30,7 +30,7 @@ Check (decomp (true,true) as t, u in (t,u)). Section A. -Notation "! A" := (forall _:nat, A) (at level 60). +Notation "! A" := (forall _:nat, A) (at level 60) : type_scope. Check ! (0=0). Check forall n, n=0. @@ -194,9 +194,9 @@ Open Scope nat_scope. Coercion is_true := fun b => b=true. Coercion of_nat n := match n with 0 => true | _ => false end. -Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10). +Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10) : bool_scope. -Check (false && I 3)%bool /\ I 6. +Check (false && I 3)%bool /\ (I 6)%bool. (**********************************************************************) (* Check notations with several recursive patterns *) diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 1ec701ae8..121a369a9 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -37,11 +37,22 @@ let' f (x y : nat) (a := 0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2 λ (f : nat -> nat) (x : nat), f(x) + S(x) : (nat -> nat) -> nat -> nat Notation plus2 n := (S(S(n))) +λ n : list(nat), match n with + | 1 :: nil => 0 + | _ => 2 + end + : list(nat) -> nat +λ n : list(nat), +match n with +| 1 :: nil => 0 +| nil | 0 :: _ | 1 :: _ :: _ | plus2 _ :: _ => 2 +end + : list(nat) -> nat λ n : list(nat), match n with | nil => 2 | 0 :: _ => 2 -| list1 => 0 +| 1 :: nil => 0 | 1 :: _ :: _ => 2 | plus2 _ :: _ => 2 end @@ -84,3 +95,9 @@ a≡ : Set .α : Set +# a : .α => +# b : .α => +let res := 0 in +for i from 0 to a updating (res) +{{for j from 0 to b updating (res) {{S res}};; res}};; res + : .α -> .α -> .α diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index ceb29d1b9..531398bb0 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -70,6 +70,7 @@ Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2. (* Note: does not work for pattern *) Module A. Notation "f ( x )" := (f x) (at level 10, format "f ( x )"). +Open Scope nat_scope. Check fun f x => f x + S x. Open Scope list_scope. @@ -78,6 +79,13 @@ Notation plus2 n := (S (S n)). (* plus2 was not correctly printed in the two following tests in 8.3pl1 *) Print plus2. Check fun n => match n with list1 => 0 | _ => 2 end. +Unset Printing Allow Match Default Clause. +Check fun n => match n with list1 => 0 | _ => 2 end. +Unset Printing Factorizable Match Patterns. +Check fun n => match n with list1 => 0 | _ => 2 end. +Set Printing Allow Match Default Clause. +Set Printing Factorizable Match Patterns. + End A. (* This one is not fully satisfactory because binders in the same type @@ -145,3 +153,24 @@ Check .a≡. Notation ".α" := nat. Check nat. Check .α. + +(* A test for #6304 *) + +Module M6304. +Notation "'for' m 'from' 0 'to' N 'updating' ( s1 ) {{ b }} ;; rest" := + (let s1 := + (fix rec(n: nat) := match n with + | 0 => s1 + | S m => let s1 := rec m in b + end) N + in rest) + (at level 20). + +Check fun (a b : nat) => + let res := 0 in + for i from 0 to a updating (res) {{ + for j from 0 to b updating (res) {{ S res }};; + res + }};; res. + +End M6304. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 6ef75dd13..1b5725275 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -128,3 +128,13 @@ return (1, 2, 3, 4) : nat *(1.2) : nat +[{0; 0}] + : list (list nat) +[{1; 2; 3}; + {4; 5; 6}; + {7; 8; 9}] + : list (list nat) +amatch = mmatch 0 (with 0 => 1| 1 => 2 end) + : unit +alist = [0; 1; 2] + : list nat diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 8c7bbe591..a8d6c97fb 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -59,7 +59,7 @@ Check fun f => CURRYINVLEFT (x:nat) (y:bool), f. (* Notations with variables bound both as a term and as a binder *) (* This is #4592 *) -Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)). +Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)) : type_scope. Check forall n:nat, {# n | 1 > n}. Parameter foo : forall {T}(x : T)(P : T -> Prop), Prop. @@ -183,9 +183,13 @@ Check letpair x [1] = {0}; return (1,2,3,4). (* Test spacing in #5569 *) +Section S1. +Variable plus : nat -> nat -> nat. +Infix "+" := plus. Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut) (at level 0, xR at level 39, format "{ { xL | xR // xcut } }"). Check 1+1+1. +End S1. (* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *) Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder). @@ -193,7 +197,59 @@ Check !!! (x y:nat), True. (* Allow level for leftmost nonterminal when printing-only, BZ#5739 *) -Notation "* x" := (id x) (only printing, at level 15, format "* x"). -Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y"). +Section S2. +Notation "* x" := (id x) (only printing, at level 15, format "* x") : nat_scope. +Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y") : nat_scope. Check (((id 1) + 2) + 3). Check (id (1 + 2)). +End S2. + +(* Test printing of notations guided by scope *) + +Module A. + +Delimit Scope line_scope with line. +Notation "{ }" := nil (format "{ }") : line_scope. +Notation "{ x }" := (cons x nil) : line_scope. +Notation "{ x ; y ; .. ; z }" := (cons x (cons y .. (cons z nil) ..)) : line_scope. +Notation "[ ]" := nil (format "[ ]") : matx_scope. +Notation "[ l ]" := (cons l%line nil) : matx_scope. +Notation "[ l ; l' ; .. ; l'' ]" := (cons l%line (cons l'%line .. (cons l''%line nil) ..)) + (format "[ '[v' l ; '/' l' ; '/' .. ; '/' l'' ']' ]") : matx_scope. + +Open Scope matx_scope. +Check [[0;0]]. +Check [[1;2;3];[4;5;6];[7;8;9]]. + +End A. + +(* Example by Beta Ziliani *) + +Require Import Lists.List. + +Module B. + +Import ListNotations. + +Delimit Scope pattern_scope with pattern. +Delimit Scope patterns_scope with patterns. + +Notation "a => b" := (a, b) (at level 201) : pattern_scope. +Notation "'with' p1 | .. | pn 'end'" := + ((cons p1%pattern (.. (cons pn%pattern nil) ..))) + (at level 91, p1 at level 210, pn at level 210) : patterns_scope. + +Definition mymatch (n:nat) (l : list (nat * nat)) := tt. +Arguments mymatch _ _%patterns. +Notation "'mmatch' n ls" := (mymatch n ls) (at level 0). + +Close Scope patterns_scope. +Close Scope pattern_scope. + +Definition amatch := mmatch 0 with 0 => 1 | 1 => 2 end. +Print amatch. (* Good: amatch = mmatch 0 (with 0 => 1| 1 => 2 end) *) + +Definition alist := [0;1;2]. +Print alist. + +End B. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index f69379a57..d6d410d1a 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -44,26 +44,45 @@ bar@{u} = nat bar is universe polymorphic foo@{u Top.17 v} = Type@{Top.17} -> Type@{v} -> Type@{u} - : Type@{max(u+1, Top.17+1, v+1)} + : Type@{max(u+1,Top.17+1,v+1)} (* u Top.17 v |= *) foo is universe polymorphic -Monomorphic mono = Type@{u} - : Type@{u+1} -(* {u} |= *) +Monomorphic mono = Type@{mono.u} + : Type@{mono.u+1} +(* {mono.u} |= *) mono is not universe polymorphic +mono + : Type@{mono.u+1} +Type@{mono.u} + : Type@{mono.u+1} +The command has indeed failed with message: +Universe u already exists. +monomono + : Type@{MONOU+1} +mono.monomono + : Type@{mono.MONOU+1} +monomono + : Type@{MONOU+1} +mono + : Type@{mono.u+1} +The command has indeed failed with message: +Universe u already exists. +bobmorane = +let tt := Type@{tt.v} in let ff := Type@{ff.v} in tt -> ff + : Type@{max(tt.u,ff.u)} The command has indeed failed with message: Universe u already bound. foo@{E M N} = Type@{M} -> Type@{N} -> Type@{E} - : Type@{max(E+1, M+1, N+1)} + : Type@{max(E+1,M+1,N+1)} (* E M N |= *) foo is universe polymorphic foo@{Top.16 Top.17 Top.18} = Type@{Top.17} -> Type@{Top.18} -> Type@{Top.16} - : Type@{max(Top.16+1, Top.17+1, Top.18+1)} + : Type@{max(Top.16+1,Top.17+1,Top.18+1)} (* Top.16 Top.17 Top.18 |= *) foo is universe polymorphic @@ -88,9 +107,10 @@ The command has indeed failed with message: This object does not support universe names. The command has indeed failed with message: Cannot enforce v < u because u < gU < gV < v -Monomorphic bind_univs.mono = Type@{u} - : Type@{u+1} -(* {u} |= *) +Monomorphic bind_univs.mono = +Type@{bind_univs.mono.u} + : Type@{bind_univs.mono.u+1} +(* {bind_univs.mono.u} |= *) bind_univs.mono is not universe polymorphic bind_univs.poly@{u} = Type@{u} @@ -99,12 +119,12 @@ bind_univs.poly@{u} = Type@{u} bind_univs.poly is universe polymorphic insec@{v} = Type@{u} -> Type@{v} - : Type@{max(u+1, v+1)} + : Type@{max(u+1,v+1)} (* v |= *) insec is universe polymorphic insec@{u v} = Type@{u} -> Type@{v} - : Type@{max(u+1, v+1)} + : Type@{max(u+1,v+1)} (* u v |= *) insec is universe polymorphic @@ -125,28 +145,28 @@ inmod@{u} = Type@{u} inmod is universe polymorphic Applied.infunct@{u v} = inmod@{u} -> Type@{v} - : Type@{max(u+1, v+1)} + : Type@{max(u+1,v+1)} (* u v |= *) Applied.infunct is universe polymorphic -axfoo@{i Top.33 Top.34} : Type@{Top.33} -> Type@{i} -(* i Top.33 Top.34 |= *) +axfoo@{i Top.41 Top.42} : Type@{Top.41} -> Type@{i} +(* i Top.41 Top.42 |= *) axfoo is universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axfoo -axbar@{i Top.33 Top.34} : Type@{Top.34} -> Type@{i} -(* i Top.33 Top.34 |= *) +axbar@{i Top.41 Top.42} : Type@{Top.42} -> Type@{i} +(* i Top.41 Top.42 |= *) axbar is universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axbar -axfoo' : Type@{Top.36} -> Type@{i} +axfoo' : Type@{Top.44} -> Type@{axbar'.i} axfoo' is not universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axfoo' -axbar' : Type@{Top.36} -> Type@{i} +axbar' : Type@{Top.44} -> Type@{axbar'.i} axbar' is not universe polymorphic Argument scope is [type_scope] diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index 116d5e5e9..266d94ad9 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -1,6 +1,6 @@ Set Universe Polymorphism. Set Printing Universes. -Unset Strict Universe Declaration. +(* Unset Strict Universe Declaration. *) (* universe binders on inductive types and record projections *) Inductive Empty@{u} : Type@{u} := . @@ -25,14 +25,59 @@ Print wrap. Instance bar@{u} : Wrap@{u} Set. Proof. exact nat. Qed. Print bar. +Unset Strict Universe Declaration. (* The universes in the binder come first, then the extra universes in order of appearance. *) Definition foo@{u +} := Type -> Type@{v} -> Type@{u}. Print foo. +Set Strict Universe Declaration. (* Binders even work with monomorphic definitions! *) Monomorphic Definition mono@{u} := Type@{u}. Print mono. +Check mono. +Check Type@{mono.u}. + +Module mono. + Fail Monomorphic Universe u. + Monomorphic Universe MONOU. + + Monomorphic Definition monomono := Type@{MONOU}. + Check monomono. +End mono. +Check mono.monomono. (* qualified MONOU *) +Import mono. +Check monomono. (* unqualified MONOU *) +Check mono. (* still qualified mono.u *) + +Monomorphic Constraint Set < Top.mono.u. + +Module mono2. + Monomorphic Universe u. +End mono2. + +Fail Monomorphic Definition mono2@{u} := Type@{u}. + +Module SecLet. + Unset Universe Polymorphism. + Section foo. + (* Fail Let foo@{} := Type@{u}. (* doesn't parse: Let foo@{...} doesn't exist *) *) + Unset Strict Universe Declaration. + Let tt : Type@{u} := Type@{v}. (* names disappear in the ether *) + Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* if Set Universe Polymorphism: universes are named ff.u and ff.v. Otherwise names disappear into space *) + Definition bobmorane := tt -> ff. + End foo. + Print bobmorane. (* + bobmorane@{Top.15 Top.16 ff.u ff.v} = + let tt := Type@{Top.16} in let ff := Type@{ff.v} in tt -> ff + : Type@{max(Top.15,ff.u)} + (* Top.15 Top.16 ff.u ff.v |= Top.16 < Top.15 + ff.v < ff.u + *) + + bobmorane is universe polymorphic + *) +End SecLet. (* fun x x => foo is nonsense with local binders *) Fail Definition fo@{u u} := Type@{u}. @@ -61,7 +106,7 @@ Monomorphic Universes gU gV. Monomorphic Constraint gU < gV. Fail Lemma foo@{u v|u < gU, gV < v, v < u} : nat. (* Universe binders survive through compilation, sections and modules. *) -Require bind_univs. +Require TestSuite.bind_univs. Print bind_univs.mono. Print bind_univs.poly. diff --git a/test-suite/output/bug5778.out b/test-suite/output/bug5778.out new file mode 100644 index 000000000..91ceb1b58 --- /dev/null +++ b/test-suite/output/bug5778.out @@ -0,0 +1,4 @@ +The command has indeed failed with message: +In nested Ltac calls to "c", "abs" and "abstract b ltac:(())", last call +failed. +The term "I" has type "True" which should be Set, Prop or Type. diff --git a/test-suite/output/bug5778.v b/test-suite/output/bug5778.v new file mode 100644 index 000000000..0dcd76aef --- /dev/null +++ b/test-suite/output/bug5778.v @@ -0,0 +1,7 @@ +Ltac a _ := pose (I : I). +Ltac b _ := a (). +Ltac abs _ := abstract b (). +Ltac c _ := abs (). +Goal True. + Fail c (). +Abort. diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index c5d58ec1e..eb9f57102 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -1,7 +1,7 @@ The command has indeed failed with message: Ltac variable y depends on pattern variable name z which is not bound in current context. Ltac f x y z := - symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize + symmetry in x, y; auto with z; auto; intros; clearbody x; generalize dependent z The command has indeed failed with message: In nested Ltac calls to "g1" and "refine (uconstr)", last call failed. @@ -32,7 +32,7 @@ nat 0 0 Ltac foo := - let x := intros ** in + let x := intros in let y := intros -> in let v := constr:(nil) in let w := () in diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out index 172612405..7326f137c 100644 --- a/test-suite/output/ltac_missing_args.out +++ b/test-suite/output/ltac_missing_args.out @@ -1,20 +1,40 @@ The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable x. +The user-defined tactic "Top.foo" was not fully applied: +There is a missing argument for variable x, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable x. +The user-defined tactic "Top.bar" was not fully applied: +There is a missing argument for variable x, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing arguments for variables y and _. +The user-defined tactic "Top.bar" was not fully applied: +There are missing arguments for variables y and _, +an argument was provided for variable x. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable x. +The user-defined tactic "Top.baz" was not fully applied: +There is a missing argument for variable x, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable x. +The user-defined tactic "Top.qux" was not fully applied: +There is a missing argument for variable x, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable _. +The user-defined tactic "Top.mydo" was not fully applied: +There is a missing argument for variable _, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable _. +An unnamed user-defined tactic was not fully applied: +There is a missing argument for variable _, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable _. +An unnamed user-defined tactic was not fully applied: +There is a missing argument for variable _, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable x. +The user-defined tactic "Top.rec" was not fully applied: +There is a missing argument for variable x, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable x. +An unnamed user-defined tactic was not fully applied: +There is a missing argument for variable x, +an argument was provided for variable tac. diff --git a/test-suite/output/optimize_heap.out b/test-suite/output/optimize_heap.out new file mode 100644 index 000000000..94a0b1911 --- /dev/null +++ b/test-suite/output/optimize_heap.out @@ -0,0 +1,8 @@ +1 subgoal + + ============================ + True +1 subgoal + + ============================ + True diff --git a/test-suite/output/optimize_heap.v b/test-suite/output/optimize_heap.v new file mode 100644 index 000000000..e566bd7ba --- /dev/null +++ b/test-suite/output/optimize_heap.v @@ -0,0 +1,7 @@ +(* optimize_heap should not affect the proof state *) + +Goal True. + idtac. + Show. + optimize_heap. + Show. diff --git a/test-suite/prerequisite/bind_univs.v b/test-suite/prerequisite/bind_univs.v index f17c00e9d..e834fde11 100644 --- a/test-suite/prerequisite/bind_univs.v +++ b/test-suite/prerequisite/bind_univs.v @@ -3,3 +3,5 @@ Monomorphic Definition mono@{u} := Type@{u}. Polymorphic Definition poly@{u} := Type@{u}. + +Monomorphic Universe reqU. diff --git a/test-suite/success/BracketsWithGoalSelector.v b/test-suite/success/BracketsWithGoalSelector.v new file mode 100644 index 000000000..ed035f521 --- /dev/null +++ b/test-suite/success/BracketsWithGoalSelector.v @@ -0,0 +1,16 @@ +Goal forall A B, B \/ A -> A \/ B. +Proof. + intros * [HB | HA]. + 2: { + left. + exact HA. + Fail right. (* No such goal. Try unfocusing with "}". *) + } + Fail 2: { (* Non-existent goal. *) + idtac. (* The idtac is to get a dot, so that IDEs know to stop there. *) + 1:{ (* Syntactic test: no space before bracket. *) + right. + exact HB. +Fail Qed. + } +Qed. diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v index 0f677a849..82b51b1ff 100644 --- a/test-suite/success/Check.v +++ b/test-suite/success/Check.v @@ -12,3 +12,5 @@ Check 0. Check S. Check nat. + +Type Type : Type. diff --git a/test-suite/success/abstract_poly.v b/test-suite/success/abstract_poly.v index b736b734f..aa8da5336 100644 --- a/test-suite/success/abstract_poly.v +++ b/test-suite/success/abstract_poly.v @@ -17,4 +17,4 @@ intros m n P e p. abstract (rewrite e in p; exact p). Defined. -Check bar_subproof@{Set Set Set}. +Check bar_subproof@{Set Set}. diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index 0ee223250..83726bfdc 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -635,6 +635,6 @@ Recursive Extraction Everything. Require Import ZArith. -Extraction Language Ocaml. +Extraction Language OCaml. Recursive Extraction Z_modulo_2 Zdiv_eucl_exist. Extraction TestCompile Z_modulo_2 Zdiv_eucl_exist. diff --git a/test-suite/success/unidecls.v b/test-suite/success/unidecls.v new file mode 100644 index 000000000..c4a1d7c28 --- /dev/null +++ b/test-suite/success/unidecls.v @@ -0,0 +1,121 @@ +Set Printing Universes. + +Module unidecls. + Universes a b. +End unidecls. + +Universe a. + +Constraint a < unidecls.a. + +Print Universes. + +(** These are different universes *) +Check Type@{a}. +Check Type@{unidecls.a}. + +Check Type@{unidecls.b}. + +Fail Check Type@{unidecls.c}. + +Fail Check Type@{i}. +Universe foo. +Module Foo. + (** Already declared globaly: but universe names are scoped at the module level *) + Universe foo. + Universe bar. + + Check Type@{Foo.foo}. + Definition bar := 0. +End Foo. + +(** Already declared in the module *) +Universe bar. + +(** Accessible outside the module: universe declarations are global *) +Check Type@{bar}. +Check Type@{Foo.bar}. + +Check Type@{Foo.foo}. +(** The same *) +Check Type@{foo}. +Check Type@{Top.foo}. + +Universe secfoo. +Section Foo'. + Fail Universe secfoo. + Universe secfoo2. + Check Type@{Foo'.secfoo2}. + Constraint secfoo2 < a. +End Foo'. + +Check Type@{secfoo2}. +Fail Check Type@{Foo'.secfoo2}. +Fail Check eq_refl : Type@{secfoo2} = Type@{a}. + +(** Below, u and v are global, fixed universes *) +Module Type Arg. + Universe u. + Parameter T: Type@{u}. +End Arg. + +Module Fn(A : Arg). + Universes v. + + Check Type@{A.u}. + Constraint A.u < v. + + Definition foo : Type@{v} := nat. + Definition bar : Type@{A.u} := nat. + + Fail Definition foo(A : Type@{v}) : Type@{A.u} := A. +End Fn. + +Module ArgImpl : Arg. + Definition T := nat. +End ArgImpl. + +Module ArgImpl2 : Arg. + Definition T := bool. +End ArgImpl2. + +(** Two applications of the functor result in the exact same universes *) +Module FnApp := Fn(ArgImpl). + +Check Type@{FnApp.v}. +Check FnApp.foo. +Check FnApp.bar. + +Check (eq_refl : Type@{ArgImpl.u} = Type@{ArgImpl2.u}). + +Module FnApp2 := Fn(ArgImpl). +Check Type@{FnApp2.v}. +Check FnApp2.foo. +Check FnApp2.bar. + +Import ArgImpl2. +(** Now u refers to ArgImpl.u and ArgImpl2.u *) +Check FnApp2.bar. + +(** It can be shadowed *) +Universe u. + +(** This refers to the qualified name *) +Check FnApp2.bar. + +Constraint u = ArgImpl.u. +Print Universes. + +Set Universe Polymorphism. + +Section PS. + Universe poly. + + Definition id (A : Type@{poly}) (a : A) : A := a. +End PS. +(** The universe is polymorphic and discharged, does not persist *) +Fail Check Type@{poly}. + +Print Universes. +Check id nat. +Check id@{Set}. |