diff options
Diffstat (limited to 'test-suite')
20 files changed, 200 insertions, 18 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index f7447d6cec..758374c5de 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -198,7 +198,6 @@ summary: $(call summary_dir, "Coqdoc tests", coqdoc); \ $(call summary_dir, "tools/ tests", tools); \ $(call summary_dir, "Unit tests", unit-tests); \ - $(call summary_dir, "Machine arithmetic tests", arithmetic); \ $(call summary_dir, "Ltac2 tests", ltac2); \ 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`; \ @@ -223,7 +222,7 @@ report: summary.log # printed for all opened bugs (still active or seems to be closed). # For closed bugs that behave as expected, no message is printed -# All files are assumed to have <# of the bug>.v as a name +# All files are assumed to have bug_<# of the bug>.v as a name # Opened bugs that should not fail $(addsuffix .log,$(wildcard bugs/opened/*.v)): %.v.log: %.v @@ -301,20 +300,20 @@ endif unit-tests/src/utest.cmx: unit-tests/src/utest.ml unit-tests/src/utest.cmi $(SHOW) 'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) -c -I unit-tests/src -package oUnit $< + $(HIDE)$(OCAMLOPT) -c -I unit-tests/src -package ounit2 $< unit-tests/src/utest.cmo: unit-tests/src/utest.ml unit-tests/src/utest.cmi $(SHOW) 'OCAMLC $<' - $(HIDE)$(OCAMLC) -c -I unit-tests/src -package oUnit $< + $(HIDE)$(OCAMLC) -c -I unit-tests/src -package ounit2 $< unit-tests/src/utest.cmi: unit-tests/src/utest.mli $(SHOW) 'OCAMLC $<' - $(HIDE)$(OCAMLC) -package oUnit -c $< + $(HIDE)$(OCAMLC) -package ounit2 -c $< unit-tests: $(UNIT_LOGFILES) # Build executable, run it to generate log file unit-tests/%.ml.log: unit-tests/%.ml unit-tests/src/$(UNIT_LINK) $(SHOW) 'TEST $<' - $(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.toplevel,oUnit \ + $(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.toplevel,ounit2 \ -I unit-tests/src $(UNIT_LINK) $< -o $<.test; $(HIDE)./$<.test @@ -501,8 +500,8 @@ $(addsuffix .log,$(wildcard output-coqchk/*.v)): %.v.log: %.v %.out $(PREREQUISI } > "$(shell dirname $<)/$(shell basename $< .v).chk.log"; fi .PHONY: approve-output -approve-output: output output-coqtop - $(HIDE)for f in output/*.out.real; do \ +approve-output: output output-coqtop output-coqchk + $(HIDE)for f in $(wildcard $(addsuffix /*.out.real,$^)); do \ mv "$$f" "$${f%.real}"; \ echo "Updated $${f%.real}!"; \ done diff --git a/test-suite/bugs/bug_5996.v b/test-suite/bugs/bug_5996.v deleted file mode 100644 index c9e3292b48..0000000000 --- a/test-suite/bugs/bug_5996.v +++ /dev/null @@ -1,8 +0,0 @@ -Goal Type. - let c := constr:(prod nat nat) in - let c' := (eval pattern nat in c) in - let c' := lazymatch c' with ?f _ => f end in - let c'' := lazymatch c' with fun x : Set => ?f => constr:(forall x : Type, f) end in - let _ := type of c'' in - exact c''. -Defined. diff --git a/test-suite/bugs/bug_11140.v b/test-suite/bugs/closed/bug_11140.v index ca806ea324..ca806ea324 100644 --- a/test-suite/bugs/bug_11140.v +++ b/test-suite/bugs/closed/bug_11140.v diff --git a/test-suite/bugs/closed/bug_12676.v b/test-suite/bugs/closed/bug_12676.v new file mode 100644 index 0000000000..5118ddb472 --- /dev/null +++ b/test-suite/bugs/closed/bug_12676.v @@ -0,0 +1,13 @@ + + +Definition nat_eq_dec(i j:nat) : {i=j}+{i<>j}. +Proof. + pose (diseq := false). + decide equality. +Defined. + +Set Mangle Names. +Definition nat_eq_dec_mangle (i j:nat) : {i=j}+{i<>j}. +Proof. + decide equality. (*Error: Anomaly "variable diseq unbound." ...*) +Defined. diff --git a/test-suite/bugs/closed/bug_12763.v b/test-suite/bugs/closed/bug_12763.v new file mode 100644 index 0000000000..6cbcc0d3b0 --- /dev/null +++ b/test-suite/bugs/closed/bug_12763.v @@ -0,0 +1,6 @@ +Inductive bool_list := S (y : bool) (l : bool_list) | O. +Scheme Equality for bool_list. + +Set Mangle Names. +Scheme Equality for nat. +Scheme Equality for list. diff --git a/test-suite/bugs/closed/bug_12787.v b/test-suite/bugs/closed/bug_12787.v new file mode 100644 index 0000000000..2566e1f261 --- /dev/null +++ b/test-suite/bugs/closed/bug_12787.v @@ -0,0 +1,26 @@ +Inductive sigT3 {A: Type} {P: A -> Type} (Q: forall a: A, P a -> Type) := + existT3: forall a: A, forall b: P a, Q a b -> sigT3 Q +. + +Definition projT3_1 {A: Type} {P: A -> Type} {Q: forall a: A, P a -> Type} (a: sigT3 Q) := + let 'existT3 _ x0 _ _ := a in x0. + +Definition projT3_2 {A: Type} {P: A -> Type} {Q: forall a: A, P a -> Type} (a: sigT3 Q) : P (projT3_1 a) := + let 'existT3 _ x0 x1 _ := a in x1. + + + +Lemma projT3_3_eq' (A B: Type) (Q: B -> Type) (a b: sigT3 (fun (_: A) b => Q b)) (H: a = b) : + unit. +Proof. + destruct a as [x0 x1 x2], b as [y0 y1 y2]. + assert (H' := f_equal projT3_1 H). + cbn in H'. + subst x0. + assert (H' := f_equal (projT3_2 (P := fun _ => B)) H). + cbn in H'. + subst x1. + + injection H as H'. + exact tt. +Qed. diff --git a/test-suite/bugs/closed/bug_12860.v b/test-suite/bugs/closed/bug_12860.v new file mode 100644 index 0000000000..243aeceba2 --- /dev/null +++ b/test-suite/bugs/closed/bug_12860.v @@ -0,0 +1,10 @@ +Require Import Coq.nsatz.NsatzTactic. +Require Import Coq.ZArith.ZArith Coq.QArith.QArith. + +Goal forall x y : Z, (x + y = y + x)%Z. + intros; nsatz. +Qed. + +Goal forall x y : Q, Qeq (x + y) (y + x). + intros; nsatz. +Qed. diff --git a/test-suite/bugs/bug_4690.v b/test-suite/bugs/closed/bug_4690.v index f50866a990..f50866a990 100644 --- a/test-suite/bugs/bug_4690.v +++ b/test-suite/bugs/closed/bug_4690.v diff --git a/test-suite/bugs/closed/bug_7015.v b/test-suite/bugs/closed/bug_7015.v new file mode 100644 index 0000000000..a57fa94960 --- /dev/null +++ b/test-suite/bugs/closed/bug_7015.v @@ -0,0 +1,74 @@ +Set Universe Polymorphism. +Set Polymorphic Inductive Cumulativity. +Set Printing Universes. + +Module Simple. + + (* in the real world foo@{i} might be [@paths@{i} nat] I guess *) + Inductive foo : nat -> Type :=. + + (* on [refl (fun x => f x)] this computes to [refl f] *) + Definition eta_out {A B} (f g : forall x : A, B x) (e : (fun x => f x) = (fun x => g x)) : f = g. + Proof. + change (f = g) in e. destruct e;reflexivity. + Defined. + + Section univs. + Universes i j. + Constraint i < j. (* fail instead of forcing equality *) + + Definition one : (fun n => foo@{i} n) = fun n => foo@{j} n := eq_refl. + + Definition two : foo@{i} = foo@{j} := eta_out _ _ one. + + Definition two' : foo@{i} = foo@{j} := Eval compute in two. + + Definition three := @eq_refl (foo@{i} = foo@{j}) two. + Definition four := Eval compute in three. + + Definition five : foo@{i} = foo@{j} := eq_refl. + End univs. + + (* inference tries and succeeds with syntactic equality which doesn't eta expand *) + Fail Definition infer@{i j k|i < k, j < k, k < eq.u0} + : foo@{i} = foo@{j} :> (nat -> Type@{k}) + := eq_refl. + +End Simple. + +Module WithRed. + (** this test needs to reduce the parameter's type to work *) + + + Inductive foo@{i j} (b:bool) (x:if b return Type@{j} then Type@{i} else nat) : Type@{i} := . + + (* on [refl (fun x => f x)] this computes to [refl f] *) + Definition eta_out {A B} (f g : forall x : A, B x) (e : (fun x => f x) = (fun x => g x)) : f = g. + Proof. + change (f = g) in e. destruct e;reflexivity. + Defined. + + Section univs. + Universes i j k. + Constraint i < j. (* fail instead of forcing equality *) + + Definition one : (fun n => foo@{i k} false n) = fun n => foo@{j k} false n := eq_refl. + + Definition two : foo@{i k} false = foo@{j k} false := eta_out _ _ one. + + Definition two' : foo@{i k} false = foo@{j k} false := Eval compute in two. + + (* Failure of SR doesn't just mean that the type changes, sometimes + we lose being well-typed entirely. *) + Definition three := @eq_refl (foo@{i k} false = foo@{j k} false) two. + Definition four := Eval compute in three. + + Definition five : foo@{i k} false = foo@{j k} false := eq_refl. + End univs. + + (* inference tries and succeeds with syntactic equality which doesn't eta expand *) + Fail Definition infer@{i j k|i < k, j < k, k < eq.u0} + : foo@{i k} false = foo@{j k} false :> (nat -> Type@{k}) + := eq_refl. + +End WithRed. diff --git a/test-suite/bugs/bug_9490.v b/test-suite/bugs/closed/bug_9490.v index a5def40c49..a5def40c49 100644 --- a/test-suite/bugs/bug_9490.v +++ b/test-suite/bugs/closed/bug_9490.v diff --git a/test-suite/bugs/bug_9532.v b/test-suite/bugs/closed/bug_9532.v index d198d45f2f..d198d45f2f 100644 --- a/test-suite/bugs/bug_9532.v +++ b/test-suite/bugs/closed/bug_9532.v diff --git a/test-suite/bugs/opened/bug_2904.v b/test-suite/bugs/opened/bug_2904.v new file mode 100644 index 0000000000..da30a509ac --- /dev/null +++ b/test-suite/bugs/opened/bug_2904.v @@ -0,0 +1,18 @@ +Module Type S. +Parameter t : Type. +Module M'. +Parameter t : Type. +Definition u := S.t. +End M'. +End S. + +Module M : S. +Definition t := unit. +Module M'. +Definition t := bool. +Definition u := M.t. +End M'. +End M. + +Require Extraction. +Fail Extraction TestCompile M. diff --git a/test-suite/bugs/opened/bug_5996.v b/test-suite/bugs/opened/bug_5996.v new file mode 100644 index 0000000000..2e81a183cd --- /dev/null +++ b/test-suite/bugs/opened/bug_5996.v @@ -0,0 +1,19 @@ +(* Original example *) +Goal Type. + let c := constr:(prod nat nat) in + let c' := (eval pattern nat in c) in + let c' := lazymatch c' with ?f _ => f end in + let c'' := lazymatch c' with fun x : Set => ?f => constr:(forall x : Type, f) end in + exact c''. +Fail Defined. +Abort. + +(* Workaround *) +Goal Type. + let c := constr:(prod nat nat) in + let c' := (eval pattern nat in c) in + let c' := lazymatch c' with ?f _ => f end in + let c'' := lazymatch c' with fun x : Set => ?f => constr:(forall x : Type, f) end in + let _ := type of c'' in + exact c''. +Defined. diff --git a/test-suite/output/ErrorLocation_12774_3.out b/test-suite/output/ErrorLocation_12774_3.out new file mode 100644 index 0000000000..dbd3dbd1e2 --- /dev/null +++ b/test-suite/output/ErrorLocation_12774_3.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 0-1: +Error: No product even after head-reduction. + diff --git a/test-suite/output/ErrorLocation_12774_3.v b/test-suite/output/ErrorLocation_12774_3.v new file mode 100644 index 0000000000..c624402a81 --- /dev/null +++ b/test-suite/output/ErrorLocation_12774_3.v @@ -0,0 +1,4 @@ +Ltac f := auto; intro. +Goal False. +f. +Abort. diff --git a/test-suite/output/Error_msg_diffs.out b/test-suite/output/Error_msg_diffs.out index 3e337e892d..2645524a70 100644 --- a/test-suite/output/Error_msg_diffs.out +++ b/test-suite/output/Error_msg_diffs.out @@ -1,4 +1,4 @@ -File "stdin", line 32, characters 0-12: +File "stdin", line 32, characters 0-11: [37;41;1mError:[0m In environment T : [33;1mType[0m diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index fa03ec8193..ce51acac95 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -123,3 +123,5 @@ File "stdin", line 297, characters 0-30: Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing] 0 :=: 0 : Prop +fun x : nat => <{ x; (S x) }> + : nat -> nat diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 90d8da2bec..73445bad12 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -298,3 +298,18 @@ Notation "x :=: y" := (x = y). Check (0 :=: 0). End Bug12691. + +Module CoercionEntryTransitivity. + +Declare Custom Entry com. +Declare Custom Entry com_top. +Notation "<{ e }>" := e (at level 0, e custom com_top at level 99). +Notation "x ; y" := + (x + y) + (in custom com_top at level 90, x custom com at level 90, right associativity). +Notation "x" := x (in custom com at level 0, x constr at level 0). +Notation "x" := x (in custom com_top at level 90, x custom com at level 90). + +Check fun x => <{ x ; (S x) }>. + +End CoercionEntryTransitivity. diff --git a/test-suite/output/ssr_error_multiple_intro_after_case.v b/test-suite/output/ssr_error_multiple_intro_after_case.v index 1f87966693..18997b8686 100644 --- a/test-suite/output/ssr_error_multiple_intro_after_case.v +++ b/test-suite/output/ssr_error_multiple_intro_after_case.v @@ -1,3 +1,4 @@ Require Import ssreflect. Goal forall p : nat * nat , True. case => x x. +Abort. diff --git a/test-suite/unit-tests/.merlin.in b/test-suite/unit-tests/.merlin.in index b2279de74e..668b431d52 100644 --- a/test-suite/unit-tests/.merlin.in +++ b/test-suite/unit-tests/.merlin.in @@ -3,4 +3,4 @@ REC S ** B ** -PKG oUnit +PKG ounit2 |