diff options
Diffstat (limited to 'test-suite')
31 files changed, 237 insertions, 24 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 8ef59a3b6e..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 @@ -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_12001.v b/test-suite/bugs/closed/bug_12001.v new file mode 100644 index 0000000000..19533e49f1 --- /dev/null +++ b/test-suite/bugs/closed/bug_12001.v @@ -0,0 +1,24 @@ +(* Argument names don't get mangled *) +Set Mangle Names. +Lemma leibniz_equiv_iff {A : Type} (x y : A) : True. +Proof. tauto. Qed. +Check leibniz_equiv_iff (A := nat) 2 3 : True. +Unset Mangle Names. + +(* Coq doesn't make up names for arguments *) +Definition bar (a a : nat) : nat := 3. +Arguments bar _ _ : assert. +Fail Arguments bar a a0 : assert. + +(* This definition caused an anomaly in a version of this PR +without the change to prepare_implicits *) +Set Implicit Arguments. +Definition foo (_ : nat) (_ : @eq nat ltac:(assumption) 2) : True := I. +Fail Check foo (H := 2). + +Definition baz (a b : nat) := b. +Arguments baz a {b}. +Set Mangle Names. +Definition baz2 (a b : nat) := b. +Arguments baz2 a {b}. +Unset Mangle Names. 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/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/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index e0aa758812..c28bb14eb3 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -84,8 +84,6 @@ Argument lists should agree on the names they provide. The command has indeed failed with message: Sequences of implicit arguments must be of different lengths. The command has indeed failed with message: -Some argument names are duplicated: F -The command has indeed failed with message: Argument number 3 is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ]. The command has indeed failed with message: diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v index 6ac09cf771..6001850046 100644 --- a/test-suite/output/Arguments_renaming.v +++ b/test-suite/output/Arguments_renaming.v @@ -48,7 +48,6 @@ Check @myplus. Fail Arguments eq_refl {F g}, [H] k. Fail Arguments eq_refl {F}, [F] : rename. -Fail Arguments eq_refl {F F}, [F] F : rename. Fail Arguments eq {A} x [z] : rename. Fail Arguments eq {F} x z y. Fail Arguments eq {R} s t. diff --git a/test-suite/output/ErrorLocation_12774_1.out b/test-suite/output/ErrorLocation_12774_1.out new file mode 100644 index 0000000000..e27992ed59 --- /dev/null +++ b/test-suite/output/ErrorLocation_12774_1.out @@ -0,0 +1,3 @@ +File "stdin", line 2, characters 13-14: +Error: The term "0" has type "nat" while it is expected to have type "Type". + diff --git a/test-suite/output/ErrorLocation_12774_1.v b/test-suite/output/ErrorLocation_12774_1.v new file mode 100644 index 0000000000..8516d402d1 --- /dev/null +++ b/test-suite/output/ErrorLocation_12774_1.v @@ -0,0 +1,3 @@ +Goal Type. +simpl; exact 0. +Abort. diff --git a/test-suite/output/ErrorLocation_12774_2.out b/test-suite/output/ErrorLocation_12774_2.out new file mode 100644 index 0000000000..434275eca5 --- /dev/null +++ b/test-suite/output/ErrorLocation_12774_2.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 9-10: +Error: The term "0" has type "nat" while it is expected to have type "Type". + diff --git a/test-suite/output/ErrorLocation_12774_2.v b/test-suite/output/ErrorLocation_12774_2.v new file mode 100644 index 0000000000..e50e1caa0f --- /dev/null +++ b/test-suite/output/ErrorLocation_12774_2.v @@ -0,0 +1,4 @@ +Ltac f := simpl. +Goal Type. +f; exact 0. +Abort. 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/ErrorLocation_tac_in_term_1.out b/test-suite/output/ErrorLocation_tac_in_term_1.out new file mode 100644 index 0000000000..55ad5a36da --- /dev/null +++ b/test-suite/output/ErrorLocation_tac_in_term_1.out @@ -0,0 +1,4 @@ +File "stdin", line 2, characters 21-25: +Error: +The term "true" has type "bool" while it is expected to have type "nat". + diff --git a/test-suite/output/ErrorLocation_tac_in_term_1.v b/test-suite/output/ErrorLocation_tac_in_term_1.v new file mode 100644 index 0000000000..ef0b5aa757 --- /dev/null +++ b/test-suite/output/ErrorLocation_tac_in_term_1.v @@ -0,0 +1,3 @@ +Goal True. +apply ltac:(apply (S true)). +Abort. diff --git a/test-suite/output/ErrorLocation_tac_in_term_2.out b/test-suite/output/ErrorLocation_tac_in_term_2.out new file mode 100644 index 0000000000..5bff5ede43 --- /dev/null +++ b/test-suite/output/ErrorLocation_tac_in_term_2.out @@ -0,0 +1,4 @@ +File "stdin", line 4, characters 12-20: +Error: +The term "true" has type "bool" while it is expected to have type "nat". + diff --git a/test-suite/output/ErrorLocation_tac_in_term_2.v b/test-suite/output/ErrorLocation_tac_in_term_2.v new file mode 100644 index 0000000000..e0fc2a9f4f --- /dev/null +++ b/test-suite/output/ErrorLocation_tac_in_term_2.v @@ -0,0 +1,5 @@ +Ltac f x y := apply (x y). + +Goal True. +apply ltac:(f S true). +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/Implicit.out b/test-suite/output/Implicit.out index ef7667936c..2265028d3e 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -5,7 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I d2 = fun x : nat => d1 (y:=x) : forall x x0 : nat, x0 = x -> x0 = x -Arguments d2 [x x0]%nat_scope +Arguments d2 [x x]%nat_scope map id (1 :: nil) : list nat map id' (1 :: nil) diff --git a/test-suite/output/RecordMissingField.out b/test-suite/output/RecordMissingField.out index 7c80a6065f..28beee90b2 100644 --- a/test-suite/output/RecordMissingField.out +++ b/test-suite/output/RecordMissingField.out @@ -1,4 +1,16 @@ -File "stdin", line 8, characters 5-22: -Error: Cannot infer field y2p of record point2d in environment: -p : point2d - +The command has indeed failed with message: +The following term contains unresolved implicit arguments: + (fun p : point2d => {| x2p := x2p p + 1; y2p := ?y2p |}) +More precisely: +- ?y2p: Cannot infer field y2p of record point2d in environment: + p : point2d +The command has indeed failed with message: +The following term contains unresolved implicit arguments: + (fun p : point2d => {| x2p := x2p p + (fun n : nat => ?n) 1; y2p := ?y2p |}) +More precisely: +- ?n: Cannot infer this placeholder of type "nat" in + environment: + p : point2d + n : nat +- ?y2p: Cannot infer field y2p of record point2d in environment: + p : point2d diff --git a/test-suite/output/RecordMissingField.v b/test-suite/output/RecordMissingField.v index 84f1748fa0..8ca721564b 100644 --- a/test-suite/output/RecordMissingField.v +++ b/test-suite/output/RecordMissingField.v @@ -3,6 +3,10 @@ should contain missing field, and the inferred type of the record **) Record point2d := mkPoint { x2p: nat; y2p: nat }. - -Definition increment_x (p: point2d) : point2d := +Fail Definition increment_x (p: point2d) : point2d := {| x2p := x2p p + 1; |}. + +(* Here there is also an unresolved implicit, which should give an + understadable error as well *) +Fail Definition increment_x (p: point2d) : point2d := + {| x2p := x2p p + (fun n => _) 1; |}. diff --git a/test-suite/output/ssr_error_multiple_intro_after_case.out b/test-suite/output/ssr_error_multiple_intro_after_case.out new file mode 100644 index 0000000000..51fb208ae9 --- /dev/null +++ b/test-suite/output/ssr_error_multiple_intro_after_case.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 0-11: +Error: x already used + diff --git a/test-suite/output/ssr_error_multiple_intro_after_case.v b/test-suite/output/ssr_error_multiple_intro_after_case.v new file mode 100644 index 0000000000..1f87966693 --- /dev/null +++ b/test-suite/output/ssr_error_multiple_intro_after_case.v @@ -0,0 +1,3 @@ +Require Import ssreflect. +Goal forall p : nat * nat , True. +case => x x. diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 563651cfa5..7acaa92b89 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -190,7 +190,7 @@ Record Monad {m : Type -> Type} := { Print Visibility. Print unit. -Arguments unit {m m0 α}. +Arguments unit {m _ α}. Arguments Monad : clear implicits. Notation "'return' t" := (unit t). |