diff options
Diffstat (limited to 'test-suite')
23 files changed, 156 insertions, 65 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 1744138d29..609a61226b 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -543,13 +543,15 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG) res=`echo "$$res"00 | sed -n -e "s/\([0-9]*\)\.\([0-9][0-9]\).*/\1\2/p"`; \ true "find expected time * 100"; \ exp=`sed -n -e "s/(\*.*Expected time < \([0-9]\).\([0-9][0-9]\)s.*\*)/\1\2/p" "$<"`; \ + true "compute corrected effective time, rounded up"; \ + rescorrected=`expr \( $$res \* $(bogomips) \+ 6120 \- 1 \) \/ 6120`; \ ok=`expr \( $$res \* $(bogomips) \) "<" \( $$exp \* 6120 \)`; \ if [ "$$ok" = 1 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ else \ echo $(log_failure); \ - echo " $<...Error! (should run faster)"; \ + echo " $<...Error! (should run faster ($$rescorrected >= $$exp))"; \ $(FAIL); \ fi; \ fi; \ diff --git a/test-suite/bugs/closed/bug_10504.v b/test-suite/bugs/closed/bug_10504.v new file mode 100644 index 0000000000..6e66a6a90a --- /dev/null +++ b/test-suite/bugs/closed/bug_10504.v @@ -0,0 +1,14 @@ +Inductive any_list {A} := +| nil : @any_list A +| cons : forall X, A -> @any_list X -> @any_list A. + +Arguments nil {A}. +Arguments cons {A X}. + +Notation "[]" := (@nil Type). +Notation "hd :: tl" := (cons hd tl). + +Definition xs := true :: 2137 :: false :: 0 :: []. +Fail Definition ys := xs :: xs. + +(* Goal ys = ys. produced an anomaly "Unable to handle arbitrary u+k <= v constraints" *) diff --git a/test-suite/bugs/closed/bug_11039.v b/test-suite/bugs/closed/bug_11039.v new file mode 100644 index 0000000000..f02a3ef177 --- /dev/null +++ b/test-suite/bugs/closed/bug_11039.v @@ -0,0 +1,26 @@ +(* this bug was a proof of False *) + +(* when we require template poly Coq recognizes that it's not allowed *) +Fail #[universes(template)] + Inductive foo@{i} (A:Type@{i}) : Type@{i+1} := bar (X:Type@{i}) : foo A. + +(* variants with letin *) +Fail #[universes(template)] + Inductive foo@{i} (T:=Type@{i}:Type@{i+1}) (A:Type@{i}) : Type@{i+1} := bar (X:T) : foo A. + +Fail #[universes(template)] + Record foo@{i} (T:=Type@{i}:Type@{i+1}) (A:Type@{i}) : Type@{i+1} := bar { X:T }. + + +(* no implicit template poly, no explicit universe annotations *) +Inductive foo (A:Type) := bar X : foo X -> foo A | nonempty. +Arguments nonempty {_}. + +Fail Check foo nat : Type@{foo.u0}. +(* template poly didn't activate *) + +Definition U := Type. +Definition A : U := foo nat. + +Fail Definition down : U -> A := fun u => bar nat u nonempty. +(* this is the one where it's important that it fails *) diff --git a/test-suite/bugs/closed/bug_11161.v b/test-suite/bugs/closed/bug_11161.v new file mode 100644 index 0000000000..22a075e096 --- /dev/null +++ b/test-suite/bugs/closed/bug_11161.v @@ -0,0 +1,10 @@ +(* Ensure that evars are properly normalized in the instance path. + Problems with this can cause eg #11161. *) + +Class Foo (n:nat) := {x : bool}. + +Instance bar n : Foo n. Admitted. + +Instance bar' n : Foo n. split. abstract exact true. Qed. + +Instance bar'' n : Foo n. split. abstract exact true. Defined. diff --git a/test-suite/bugs/closed/bug_2083.v b/test-suite/bugs/closed/bug_2083.v index f33e96cea6..40fda71e66 100644 --- a/test-suite/bugs/closed/bug_2083.v +++ b/test-suite/bugs/closed/bug_2083.v @@ -13,15 +13,15 @@ Program Fixpoint check_n (n : nat) (P : { i | i < n } -> bool) (p : nat) error end. -Require Import Omega. +Require Import Lia. -Solve Obligations with program_simpl ; auto with *; try omega. +Solve Obligations with program_simpl ; auto with *; lia. Next Obligation. - apply H. simpl. omega. + apply H. simpl. lia. Defined. Next Obligation. - case (le_lt_dec p i) ; intros. assert(i = p) by omega. subst. + case (le_lt_dec p i) ; intros. assert(i = p) by lia. subst. revert H0. clear_subset_proofs. auto. apply H. simpl. assumption. Defined. diff --git a/test-suite/bugs/closed/bug_3652.v b/test-suite/bugs/closed/bug_3652.v index 915cfcac27..b21a4d939c 100644 --- a/test-suite/bugs/closed/bug_3652.v +++ b/test-suite/bugs/closed/bug_3652.v @@ -1,6 +1,7 @@ Require Setoid. Require ZArith. Import ZArith. +Require Import Lia. Inductive Erasable(A : Set) : Prop := erasable: A -> Erasable A. @@ -87,12 +88,12 @@ Proof. unfold zotval. unfold mp2a1s. ring_simplify'. - replace 2 with (2*1) at 2 7 by omega. + replace 2 with (2*1) at 2 7 by lia. rewrite <-?Z.mul_assoc. rewrite <-?Z.mul_add_distr_l. rewrite <-Z.mul_sub_distr_l. - rewrite Z.mul_cancel_l by omega. - replace 1 with (2-1) at 1 by omega. + rewrite Z.mul_cancel_l by lia. + replace 1 with (2-1) at 1 by lia. rewrite Z.add_sub_assoc. rewrite Z.sub_cancel_r. Unshelve. diff --git a/test-suite/bugs/closed/bug_4280.v b/test-suite/bugs/closed/bug_4280.v index fd7897509e..31524e5dcf 100644 --- a/test-suite/bugs/closed/bug_4280.v +++ b/test-suite/bugs/closed/bug_4280.v @@ -1,11 +1,11 @@ -Require Import ZArith. +Require Import ZArith Lia. Require Import Eqdep_dec. Local Open Scope Z_scope. Definition t := { n: Z | n > 1 }. Program Definition two : t := 2. -Next Obligation. omega. Qed. +Next Obligation. lia. Qed. Program Definition t_eq (x y: t) : {x=y} + {x<>y} := if Z.eq_dec (proj1_sig x) (proj1_sig y) then left _ else right _. diff --git a/test-suite/bugs/closed/bug_4306.v b/test-suite/bugs/closed/bug_4306.v index f1bce04451..1ad84f9bb5 100644 --- a/test-suite/bugs/closed/bug_4306.v +++ b/test-suite/bugs/closed/bug_4306.v @@ -1,7 +1,7 @@ Require Import List. Require Import Arith. Require Import Recdef. -Require Import Omega. +Require Import Lia. Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat := match xys with @@ -14,9 +14,7 @@ Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) end end. Proof. - intros; simpl; omega. - intros; simpl; omega. - intros; simpl; omega. + all: simpl; lia. Qed. Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat := diff --git a/test-suite/bugs/closed/bug_4456.v b/test-suite/bugs/closed/bug_4456.v index 7685552725..0c26d4de32 100644 --- a/test-suite/bugs/closed/bug_4456.v +++ b/test-suite/bugs/closed/bug_4456.v @@ -10,7 +10,7 @@ Tactic Notation "admit" := case proof_admitted. Require Coq.Program.Program. Require Coq.Strings.String. -Require Coq.omega.Omega. +Require Coq.micromega.Lia. Module Export Fiat_DOT_Common. Module Export Fiat. Module Common. @@ -489,7 +489,8 @@ Defined. End app. Import Coq.Lists.List. -Import Coq.omega.Omega. +Import Coq.Arith.Arith. +Import Coq.micromega.Lia. Import Fiat_DOT_Common.Fiat.Common. Import Fiat.Parsers.ContextFreeGrammar.Valid. Local Open Scope string_like_scope. @@ -585,8 +586,8 @@ Defined. | _ => discriminate | [ H : forall x, (_ * _)%type -> _ |- _ ] => specialize (fun x y z => H x (y, z)) | _ => solve [ eauto with nocore ] - | _ => solve [ apply Min.min_case_strong; omega ] - | _ => omega + | _ => solve [ apply Min.min_case_strong; lia ] + | _ => lia | [ H : production_valid (_::_) |- _ ] => let H' := fresh in pose proof H as H'; diff --git a/test-suite/bugs/closed/bug_4852.v b/test-suite/bugs/closed/bug_4852.v index e2e00f05d3..cdc8cd8b20 100644 --- a/test-suite/bugs/closed/bug_4852.v +++ b/test-suite/bugs/closed/bug_4852.v @@ -2,7 +2,7 @@ Require Import Coq.Lists.List. Import ListNotations. -Require Import Omega. +Require Import Lia. Definition wfi_lt := well_founded_induction_type Wf_nat.lt_wf. @@ -16,7 +16,7 @@ Tactic Notation "wfinduction" constr(term) "on" ne_hyp_list(Hs) "as" ident(H) := Hint Rewrite @app_comm_cons @app_assoc @app_length : app_rws. -Ltac solve_nat := autorewrite with app_rws in *; cbn in *; omega. +Ltac solve_nat := autorewrite with app_rws in *; cbn in *; lia. Notation "| x |" := (length x) (at level 11, no associativity, format "'|' x '|'"). diff --git a/test-suite/bugs/opened/bug_1596.v b/test-suite/bugs/opened/bug_1596.v index 27cb731151..89410047b2 100644 --- a/test-suite/bugs/opened/bug_1596.v +++ b/test-suite/bugs/opened/bug_1596.v @@ -1,7 +1,7 @@ Require Import Relations. Require Import FSets. Require Import Arith. -Require Import Omega. +Require Import Lia. Set Keyed Unification. @@ -147,14 +147,14 @@ Module MessageSpi. Lemma lt_trans : forall (x y z:t),(lt x y)->(lt y z)->(lt x z). unfold lt. induction x;destruct y;simpl;try tauto;destruct z;try tauto;intros. - omega. + lia. Qed. Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y). unfold eq;unfold lt. induction x;destruct y;simpl;try tauto;intro;red;intro;try (discriminate H0);injection H0;intros. - elim (lt_irrefl n);try omega. + elim (lt_irrefl n); lia. Qed. Definition compare : forall (x y:t),(Compare lt eq x y). diff --git a/test-suite/complexity/pattern.v b/test-suite/complexity/pattern.v new file mode 100644 index 0000000000..2101535be7 --- /dev/null +++ b/test-suite/complexity/pattern.v @@ -0,0 +1,38 @@ +(** Testing the performance of [pattern]. For not regressing on COQBUG(https://github.com/coq/coq/issues/11150) and COQBUG(https://github.com/coq/coq/issues/6502) *) +(* Expected time < 1.65s *) +(* reference: 0.673s after adjustment *) +Definition Let_In {A P} (v : A) (f : forall x : A, P x) : P v +:= let x := v in f x. + +Fixpoint big (a : nat) (sz : nat) : nat + := match sz with + | O => a + | S sz' => Let_In (a * a) (fun a' => big a' sz') + end. + +Ltac do_time n := + try ( + once (assert (exists e, e = big 1 n); + [ lazy -[big]; (*match goal with |- ?G => idtac G end;*) lazy [big]; + time pattern Nat.mul, S, O, (@Let_In nat (fun _ => nat)) + | ]); + fail). + +Ltac do_time_to n := + lazymatch (eval vm_compute in n) with + | O => idtac + | ?n' => do_time_to (Nat.div2 n'); idtac n'; do_time n' + end. + +Local Set Warnings "-abstract-large-number". + +(* Don't spend lots of time printing *) +Notation hide := (_ = _). + +Goal True. +Proof. + (* do_time_to 16384. *) (* should be linear, not quadratic *) + assert (exists e, e = big 1 16384). + lazy -[big]; (*match goal with |- ?G => idtac G end;*) lazy [big]. + Timeout 15 Time pattern Nat.mul, S, O, (@Let_In nat (fun _ => nat)). +Abort. diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v index be33104918..4c0ee1b5bd 100644 --- a/test-suite/modules/PO.v +++ b/test-suite/modules/PO.v @@ -35,8 +35,8 @@ Module Pair (X: PO) (Y: PO) <: PO. destruct p2. unfold le. intuition. - cutrewrite (t = t1). - cutrewrite (t0 = t2). + enough (t = t1) as ->. + enough (t0 = t2) as ->. reflexivity. info auto. diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v index 61ae4edbd1..398528de72 100644 --- a/test-suite/output/Fixpoint.v +++ b/test-suite/output/Fixpoint.v @@ -16,7 +16,7 @@ Check end in f 0. -Require Import ZArith_base Omega. +Require Import ZArith_base Lia. Open Scope Z_scope. Inductive even: Z -> Prop := @@ -35,13 +35,13 @@ Proof. fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1). intros. destruct H. - omega. + lia. apply odd_pos_even_pos in H. - omega. + lia. intros. destruct H. apply even_pos_odd_pos in H. - omega. + lia. Qed. CoInductive Inf := S { projS : Inf }. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index ba4ac5a8f9..32120a9674 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -59,3 +59,5 @@ where |- Type] (pat, p0, p cannot be used) fun '{| |} => true : R -> bool +b = a + : Prop diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 4b9d0abd95..d3433949d1 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -140,3 +140,17 @@ Record R := { n : nat }. Check fun '{|n:=x|} => true. End EmptyRecordSyntax. + +Module L. + +(* Testing regression #11053 *) + +Section Test. +Variables (A B : Type) (a : A) (b : B). +Variable c : A -> B. +Coercion c : A >-> B. +Notation COERCION := (c). +Check b = a. +End Test. + +End L. diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v index fd6101bf89..c86548440b 100644 --- a/test-suite/success/CompatCurrentFlag.v +++ b/test-suite/success/CompatCurrentFlag.v @@ -1,3 +1,3 @@ -(* -*- coq-prog-args: ("-compat" "8.11") -*- *) +(* -*- coq-prog-args: ("-compat" "8.12") -*- *) (** Check that the current compatibility flag actually requires the relevant modules. *) -Import Coq.Compat.Coq811. +Import Coq.Compat.Coq812. diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v index f774cef44f..a1c1209db6 100644 --- a/test-suite/success/CompatOldFlag.v +++ b/test-suite/success/CompatOldFlag.v @@ -1,5 +1,5 @@ -(* -*- coq-prog-args: ("-compat" "8.9") -*- *) +(* -*- coq-prog-args: ("-compat" "8.10") -*- *) (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq812. Import Coq.Compat.Coq811. Import Coq.Compat.Coq810. -Import Coq.Compat.Coq89. diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v new file mode 100644 index 0000000000..dd259988ac --- /dev/null +++ b/test-suite/success/CompatOldOldFlag.v @@ -0,0 +1,6 @@ +(* -*- coq-prog-args: ("-compat" "8.9") -*- *) +(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq812. +Import Coq.Compat.Coq811. +Import Coq.Compat.Coq810. +Import Coq.Compat.Coq89. diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v index 1c5ccc1a92..00f4747e3e 100644 --- a/test-suite/success/CompatPreviousFlag.v +++ b/test-suite/success/CompatPreviousFlag.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-compat" "8.10") -*- *) +(* -*- coq-prog-args: ("-compat" "8.11") -*- *) (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq812. Import Coq.Compat.Coq811. -Import Coq.Compat.Coq810. diff --git a/test-suite/success/LocalDefinition.v b/test-suite/success/LocalDefinition.v index 22fb09526d..d944036112 100644 --- a/test-suite/success/LocalDefinition.v +++ b/test-suite/success/LocalDefinition.v @@ -26,28 +26,12 @@ Module TestAdmittedVisibility. Fail Check d2. End TestAdmittedVisibility. -(* Test consistent behavior of Local Definition wrt automatic declaration of instances *) - Module TestVariableAsInstances. - Module Test1. - Set Typeclasses Axioms Are Instances. - Class U. - Local Parameter b : U. - Definition testU := _ : U. (* _ resolved *) - - Class T. - Variable a : T. (* warned to be the same as "Local Parameter" *) - Definition testT := _ : T. (* _ resolved *) - End Test1. - - Module Test2. - Unset Typeclasses Axioms Are Instances. - Class U. - Local Parameter b : U. - Fail Definition testU := _ : U. (* _ unresolved *) + Class U. + Local Parameter b : U. + Fail Definition testU := _ : U. (* _ unresolved *) - Class T. - Variable a : T. (* warned to be the same as "Local Parameter" thus should not be an instance *) - Fail Definition testT := _ : T. (* used to succeed *) - End Test2. + Class T. + Variable a : T. (* warned to be the same as "Local Parameter" thus should not be an instance *) + Fail Definition testT := _ : T. (* used to succeed *) End TestVariableAsInstances. diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 736d05fefc..3f96bf2c35 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -241,13 +241,8 @@ Module IterativeDeepening. End IterativeDeepening. -Module AxiomsAreInstances. - Set Typeclasses Axioms Are Instances. - Class TestClass1 := {}. - Axiom testax1 : TestClass1. - Definition testdef1 : TestClass1 := _. +Module AxiomsAreNotInstances. - Unset Typeclasses Axioms Are Instances. Class TestClass2 := {}. Axiom testax2 : TestClass2. Fail Definition testdef2 : TestClass2 := _. @@ -256,4 +251,4 @@ Module AxiomsAreInstances. Existing Instance testax2. Definition testdef2 : TestClass2 := _. -End AxiomsAreInstances. +End AxiomsAreNotInstances. diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh index 7ff5571ffb..61273c4f37 100755 --- a/test-suite/tools/update-compat/run.sh +++ b/test-suite/tools/update-compat/run.sh @@ -6,4 +6,4 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )" # we assume that the script lives in test-suite/tools/update-compat/, # and that update-compat.py lives in dev/tools/ cd "${SCRIPT_DIR}/../../.." -dev/tools/update-compat.py --assert-unchanged --release || exit $? +dev/tools/update-compat.py --assert-unchanged --master || exit $? |