diff options
Diffstat (limited to 'test-suite')
26 files changed, 267 insertions, 112 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/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/6297.v b/test-suite/bugs/closed/6297.v new file mode 100644 index 000000000..a28607058 --- /dev/null +++ b/test-suite/bugs/closed/6297.v @@ -0,0 +1,8 @@ +Set Printing Universes. + +(* Error: Anomaly "Uncaught exception "Anomaly: Incorrect universe Set + declared for inductive type, inferred level is max(Prop, Set+1)."." + Please report at http://coq.inria.fr/bugs/. *) +Fail Record LTS: Set := + lts { St: Set; + init: St }. diff --git a/test-suite/bugs/closed/6378.v b/test-suite/bugs/closed/6378.v index d0ef090d0..68ae7961d 100644 --- a/test-suite/bugs/closed/6378.v +++ b/test-suite/bugs/closed/6378.v @@ -1,4 +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/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/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/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/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/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/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. |