diff options
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/Makefile | 13 | ||||
-rw-r--r-- | test-suite/README.md | 75 | ||||
-rw-r--r-- | test-suite/bugs/closed/5286.v | 9 | ||||
-rw-r--r-- | test-suite/bugs/closed/6297.v | 8 | ||||
-rw-r--r-- | test-suite/bugs/closed/6490.v | 4 | ||||
-rw-r--r-- | test-suite/bugs/closed/6617.v | 34 | ||||
-rw-r--r-- | test-suite/bugs/opened/6393.v | 11 | ||||
-rwxr-xr-x | test-suite/coq-makefile/timing/run.sh | 8 | ||||
-rw-r--r-- | test-suite/coqchk/primproj2.v | 10 | ||||
-rw-r--r-- | test-suite/output/optimize_heap.out | 8 | ||||
-rw-r--r-- | test-suite/output/optimize_heap.v | 7 | ||||
-rw-r--r-- | test-suite/success/BracketsWithGoalSelector.v | 16 | ||||
-rw-r--r-- | test-suite/success/abstract_poly.v | 2 | ||||
-rw-r--r-- | test-suite/success/dtauto-let-deps.v | 24 |
14 files changed, 223 insertions, 6 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index de669218c..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}" ")" -o "(" -n "${CIRCLECI}" ")" ]; 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 ####################################################################### 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/5286.v b/test-suite/bugs/closed/5286.v new file mode 100644 index 000000000..98d4e5c96 --- /dev/null +++ b/test-suite/bugs/closed/5286.v @@ -0,0 +1,9 @@ +Set Primitive Projections. + +CoInductive R := mkR { p : unit }. + +CoFixpoint foo := mkR tt. + +Check (eq_refl tt : p foo = tt). +Check (eq_refl tt <: p foo = tt). +Check (eq_refl tt <<: p foo = tt). 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/6490.v b/test-suite/bugs/closed/6490.v new file mode 100644 index 000000000..dcf9ff29e --- /dev/null +++ b/test-suite/bugs/closed/6490.v @@ -0,0 +1,4 @@ +Inductive Foo (A' := I) (B : Type) := foo : Foo B. + +Goal Foo True. dtauto. Qed. +Goal Foo True. firstorder. Qed. diff --git a/test-suite/bugs/closed/6617.v b/test-suite/bugs/closed/6617.v new file mode 100644 index 000000000..9cabd62d4 --- /dev/null +++ b/test-suite/bugs/closed/6617.v @@ -0,0 +1,34 @@ +Definition MR {T M : Type} := +fun (R : M -> M -> Prop) (m : T -> M) (x y : T) => R (m x) (m y). + +Set Primitive Projections. + +Record sigma {A : Type} {B : A -> Type} : Type := sigmaI + { pr1 : A; pr2 : B pr1 }. + +Axiom F : forall {A : Type} {R : A -> A -> Prop}, + (forall x, (forall y, R y x -> unit) -> unit) -> forall (x : A), unit. + +Definition foo (A : Type) (l : list A) := + let y := {| pr1 := A; pr2 := l |} in + let bar := MR lt (fun p : sigma => + (fix Ffix (x : list (pr1 p)) : nat := + match x with + | nil => 0 + | cons _ x1 => S (Ffix x1) + end) (pr2 p)) in +fun (_ : bar y y) => +F (fun (r : sigma) + (X : forall q : sigma, bar q r -> unit) => tt). + +Definition fooT (A : Type) (l : list A) : Type := + ltac:(let ty := type of (foo A l) in exact ty). +Parameter P : forall A l, fooT A l -> Prop. + +Goal forall A l, P A l (foo A l). +Proof. + intros; unfold foo. + Fail match goal with + | [ |- context [False]] => idtac + end. +Admitted. diff --git a/test-suite/bugs/opened/6393.v b/test-suite/bugs/opened/6393.v new file mode 100644 index 000000000..8d5d09233 --- /dev/null +++ b/test-suite/bugs/opened/6393.v @@ -0,0 +1,11 @@ +(* These always worked. *) +Goal prod True True. firstorder. Qed. +Goal True -> @sigT True (fun _ => True). firstorder. Qed. +Goal prod True True. dtauto. Qed. +Goal prod True True. tauto. Qed. + +(* These should work. *) +Goal @sigT True (fun _ => True). dtauto. Qed. +(* These should work, but don't *) +(* Goal @sigT True (fun _ => True). firstorder. Qed. *) +(* Goal @sigT True (fun _ => True). tauto. Qed. *) 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/coqchk/primproj2.v b/test-suite/coqchk/primproj2.v new file mode 100644 index 000000000..f73c627ee --- /dev/null +++ b/test-suite/coqchk/primproj2.v @@ -0,0 +1,10 @@ +Set Primitive Projections. + +Record Pack (A : Type) := pack { unpack : A }. + +Definition p : Pack bool. +Proof. +refine (pack _ true). +Qed. + +Definition boom : unpack bool p = let u := unpack _ in u p := eq_refl. 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/dtauto-let-deps.v b/test-suite/success/dtauto-let-deps.v new file mode 100644 index 000000000..094b2f8b3 --- /dev/null +++ b/test-suite/success/dtauto-let-deps.v @@ -0,0 +1,24 @@ +(* +This test is sensitive to changes in which let-ins are expanded when checking +for dependencies in constructors. +If the (x := X) is not reduced, Foo1 won't be recognized as a conjunction, +and if the (y := X) is reduced, Foo2 will be recognized as a conjunction. + +This tests the behavior of engine/termops.ml : prod_applist_assum, +which is currently specified to reduce exactly the parameters. + +If dtauto is changed to reduce lets in constructors before checking dependency, +this test will need to be changed. +*) + +Context (P Q : Type). +Inductive Foo1 (X : Type) (x := X) := foo1 : let y := X in P -> Q -> Foo1 x. +Inductive Foo2 (X : Type) (x := X) := foo2 : let y := X in P -> Q -> Foo2 y. + +Goal P -> Q -> Foo1 nat. +solve [dtauto]. +Qed. + +Goal P -> Q -> Foo2 nat. +Fail solve [dtauto]. +Abort. |