aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/Makefile23
-rw-r--r--test-suite/bugs/closed/5692.v38
-rw-r--r--test-suite/bugs/closed/5741.v4
-rw-r--r--test-suite/bugs/closed/5757.v76
-rwxr-xr-xtest-suite/coq-makefile/template/init.sh1
-rw-r--r--test-suite/coqwc/BZ5637.out2
-rw-r--r--test-suite/coqwc/BZ5637.v5
-rw-r--r--test-suite/coqwc/BZ5756.out2
-rw-r--r--test-suite/coqwc/BZ5756.v3
-rw-r--r--test-suite/coqwc/false.out2
-rw-r--r--test-suite/coqwc/false.v8
-rw-r--r--test-suite/coqwc/next-obligation.out2
-rw-r--r--test-suite/coqwc/next-obligation.v10
-rw-r--r--test-suite/coqwc/theorem.out2
-rw-r--r--test-suite/coqwc/theorem.v10
-rw-r--r--test-suite/output/UnivBinders.out6
-rw-r--r--test-suite/output/UnivBinders.v6
-rw-r--r--test-suite/output/auto.out2
-rw-r--r--test-suite/output/auto.v4
-rw-r--r--test-suite/output/ltac_extra_args.out8
-rw-r--r--test-suite/output/ltac_extra_args.v10
-rw-r--r--test-suite/success/polymorphism.v46
-rw-r--r--test-suite/success/qed_export.v18
-rw-r--r--test-suite/success/unshelve.v8
24 files changed, 277 insertions, 19 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index ae426f0daf..61e75fa5d3 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -92,7 +92,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
coqdoc
# All subsystems
-SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coq-makefile
+SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile
PREREQUISITELOG = prerequisite/admit.v.log \
prerequisite/make_local.v.log prerequisite/make_notation.v.log
@@ -156,6 +156,7 @@ summary:
$(call summary_dir, "IDE tests", ide); \
$(call summary_dir, "VI tests", vio); \
$(call summary_dir, "Coqchk tests", coqchk); \
+ $(call summary_dir, "Coqwc tests", coqwc); \
$(call summary_dir, "Coq makefile", coq-makefile); \
$(call summary_dir, "Coqdoc tests", coqdoc); \
nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \
@@ -498,6 +499,26 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v))
fi; \
} > "$@"
+# coqwc : test output
+
+coqwc : $(patsubst %.v,%.v.log,$(wildcard coqwc/*.v))
+
+coqwc/%.v.log : coqwc/%.v
+ $(HIDE){ \
+ echo $(call log_intro,$<); \
+ tmpoutput=`mktemp /tmp/coqwc.XXXXXX`; \
+ $(BIN)coqwc $< 2>&1 > $$tmpoutput; \
+ diff -u --strip-trailing-cr coqwc/$*.out $$tmpoutput 2>&1; R=$$?; times; \
+ if [ $$R = 0 ]; then \
+ echo $(log_success); \
+ echo " $<...Ok"; \
+ else \
+ echo $(log_failure); \
+ echo " $<...Error! (unexpected output)"; \
+ fi; \
+ rm $$tmpoutput; \
+ } > "$@"
+
# coq_makefile
coq-makefile: $(patsubst %/run.sh,%.log,$(wildcard coq-makefile/*/run.sh))
diff --git a/test-suite/bugs/closed/5692.v b/test-suite/bugs/closed/5692.v
new file mode 100644
index 0000000000..55ef7abe40
--- /dev/null
+++ b/test-suite/bugs/closed/5692.v
@@ -0,0 +1,38 @@
+Set Primitive Projections.
+Require Import ZArith ssreflect.
+
+Module Test3.
+
+Set Primitive Projections.
+
+Structure semigroup := SemiGroup {
+ sg_car :> Type;
+ sg_op : sg_car -> sg_car -> sg_car;
+}.
+
+Structure group := Something {
+ group_car :> Type;
+ group_op : group_car -> group_car -> group_car;
+ group_neg : group_car -> group_car;
+ group_neg_op' x y : group_neg (group_op x y) = group_op (group_neg x) (group_neg y)
+}.
+
+Coercion group_sg (X : group) : semigroup :=
+ SemiGroup (group_car X) (group_op X).
+Canonical Structure group_sg.
+
+Axiom group_neg_op : forall (X : group) (x y : X),
+ group_neg X (sg_op (group_sg X) x y) = sg_op (group_sg X) (group_neg X x) (group_neg X y).
+
+Canonical Structure Z_sg := SemiGroup Z Z.add .
+Canonical Structure Z_group := Something Z Z.add Z.opp Z.opp_add_distr.
+
+Lemma foo (x y : Z) :
+ sg_op Z_sg (group_neg Z_group x) (group_neg Z_group y) =
+ group_neg Z_group (sg_op Z_sg x y).
+Proof.
+ rewrite -group_neg_op.
+ reflexivity.
+Qed.
+
+End Test3.
diff --git a/test-suite/bugs/closed/5741.v b/test-suite/bugs/closed/5741.v
new file mode 100644
index 0000000000..f6598f192d
--- /dev/null
+++ b/test-suite/bugs/closed/5741.v
@@ -0,0 +1,4 @@
+(* Check no anomaly in info_trivial *)
+
+Goal True.
+info_trivial.
diff --git a/test-suite/bugs/closed/5757.v b/test-suite/bugs/closed/5757.v
new file mode 100644
index 0000000000..0d0f2eed44
--- /dev/null
+++ b/test-suite/bugs/closed/5757.v
@@ -0,0 +1,76 @@
+(* Check that resolved status of evars follows "restrict" *)
+
+Axiom H : forall (v : nat), Some 0 = Some v -> True.
+Lemma L : True.
+eapply H with _;
+match goal with
+ | |- Some 0 = Some ?v => change (Some (0+0) = Some v)
+end.
+Abort.
+
+(* The original example *)
+
+Set Default Proof Using "Type".
+
+Module heap_lang.
+
+Inductive expr :=
+ | InjR (e : expr).
+
+Inductive val :=
+ | InjRV (v : val).
+
+Bind Scope val_scope with val.
+
+Fixpoint of_val (v : val) : expr :=
+ match v with
+ | InjRV v => InjR (of_val v)
+ end.
+
+Fixpoint to_val (e : expr) : option val := None.
+
+End heap_lang.
+Export heap_lang.
+
+Module W.
+Inductive expr :=
+ | Val (v : val)
+ (* Sums *)
+ | InjR (e : expr).
+
+Fixpoint to_expr (e : expr) : heap_lang.expr :=
+ match e with
+ | Val v => of_val v
+ | InjR e => heap_lang.InjR (to_expr e)
+ end.
+
+End W.
+
+
+
+Section Tests.
+
+ Context (iProp: Type).
+ Context (WPre: expr -> Prop).
+
+ Context (tac_wp_alloc :
+ forall (e : expr) (v : val),
+ to_val e = Some v -> WPre e).
+
+ Lemma push_atomic_spec (x: val) :
+ WPre (InjR (of_val x)).
+ Proof.
+(* This works. *)
+eapply tac_wp_alloc with _.
+match goal with
+ | |- to_val ?e = Some ?v =>
+ change (to_val (W.to_expr (W.InjR (W.Val x))) = Some v)
+end.
+Undo. Undo.
+(* This is fixed *)
+eapply tac_wp_alloc with _;
+match goal with
+ | |- to_val ?e = Some ?v =>
+ change (to_val (W.to_expr (W.InjR (W.Val x))) = Some v)
+end.
+Abort.
diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh
index 803fe8029a..c4bd11c57d 100755
--- a/test-suite/coq-makefile/template/init.sh
+++ b/test-suite/coq-makefile/template/init.sh
@@ -2,6 +2,7 @@ set -e
set -o pipefail
export PATH=$COQBIN:$PATH
+export LC_ALL=C
rm -rf theories src Makefile Makefile.conf tmp
git clean -dfx || true
diff --git a/test-suite/coqwc/BZ5637.out b/test-suite/coqwc/BZ5637.out
new file mode 100644
index 0000000000..f0b5e4f7eb
--- /dev/null
+++ b/test-suite/coqwc/BZ5637.out
@@ -0,0 +1,2 @@
+ spec proof comments
+ 5 0 0 coqwc/BZ5637.v
diff --git a/test-suite/coqwc/BZ5637.v b/test-suite/coqwc/BZ5637.v
new file mode 100644
index 0000000000..6428b10ff8
--- /dev/null
+++ b/test-suite/coqwc/BZ5637.v
@@ -0,0 +1,5 @@
+Local Obligation Tactic := idtac.
+Definition a := 1.
+Definition b := 1.
+Definition c := 1.
+Definition d := 1.
diff --git a/test-suite/coqwc/BZ5756.out b/test-suite/coqwc/BZ5756.out
new file mode 100644
index 0000000000..039d1e5008
--- /dev/null
+++ b/test-suite/coqwc/BZ5756.out
@@ -0,0 +1,2 @@
+ spec proof comments
+ 3 0 2 coqwc/BZ5756.v
diff --git a/test-suite/coqwc/BZ5756.v b/test-suite/coqwc/BZ5756.v
new file mode 100644
index 0000000000..ccb12076a3
--- /dev/null
+++ b/test-suite/coqwc/BZ5756.v
@@ -0,0 +1,3 @@
+Definition myNextValue := 0. (* OK *)
+Definition x := myNextValue. (* not OK *)
+Definition y := 0.
diff --git a/test-suite/coqwc/false.out b/test-suite/coqwc/false.out
new file mode 100644
index 0000000000..14c5713f6d
--- /dev/null
+++ b/test-suite/coqwc/false.out
@@ -0,0 +1,2 @@
+ spec proof comments
+ 3 3 1 coqwc/false.v
diff --git a/test-suite/coqwc/false.v b/test-suite/coqwc/false.v
new file mode 100644
index 0000000000..640f9ea7f0
--- /dev/null
+++ b/test-suite/coqwc/false.v
@@ -0,0 +1,8 @@
+Axiom x : nat.
+
+Definition foo (x : nat) := x + 1.
+
+Lemma bar : False.
+ idtac.
+ idtac. (* truth is overrated *)
+Admitted.
diff --git a/test-suite/coqwc/next-obligation.out b/test-suite/coqwc/next-obligation.out
new file mode 100644
index 0000000000..7a0fd777c1
--- /dev/null
+++ b/test-suite/coqwc/next-obligation.out
@@ -0,0 +1,2 @@
+ spec proof comments
+ 1 7 0 coqwc/next-obligation.v
diff --git a/test-suite/coqwc/next-obligation.v b/test-suite/coqwc/next-obligation.v
new file mode 100644
index 0000000000..786df98913
--- /dev/null
+++ b/test-suite/coqwc/next-obligation.v
@@ -0,0 +1,10 @@
+(* make sure all proof lines are counted *)
+
+Goal True.
+ Next Obligation.
+ idtac.
+ Next Obligation.
+ idtac.
+ Next Obligation.
+ idtac.
+Qed.
diff --git a/test-suite/coqwc/theorem.out b/test-suite/coqwc/theorem.out
new file mode 100644
index 0000000000..d01507bf78
--- /dev/null
+++ b/test-suite/coqwc/theorem.out
@@ -0,0 +1,2 @@
+ spec proof comments
+ 1 9 2 coqwc/theorem.v
diff --git a/test-suite/coqwc/theorem.v b/test-suite/coqwc/theorem.v
new file mode 100644
index 0000000000..901c9074fd
--- /dev/null
+++ b/test-suite/coqwc/theorem.v
@@ -0,0 +1,10 @@
+Theorem foo : True.
+Proof.
+ idtac. (* comment *)
+ idtac.
+ idtac.
+ idtac. (* comment *)
+ idtac.
+ idtac.
+ auto.
+Qed.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 128bc77673..904ff68aa7 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -4,3 +4,9 @@ bar@{u} = nat
*)
bar is universe polymorphic
+foo@{u Top.8 v} =
+Type@{Top.8} -> Type@{v} -> Type@{u}
+ : Type@{max(u+1, Top.8+1, v+1)}
+(* u Top.8 v |= *)
+
+foo is universe polymorphic
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index d9e89e43c6..8656ff1a39 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -1,7 +1,13 @@
Set Universe Polymorphism.
Set Printing Universes.
+Unset Strict Universe Declaration.
Class Wrap A := wrap : A.
Instance bar@{u} : Wrap@{u} Set. Proof nat.
Print bar.
+
+(* The universes in the binder come first, then the extra universes in
+ order of appearance. *)
+Definition foo@{u +} := Type -> Type@{v} -> Type@{u}.
+Print foo.
diff --git a/test-suite/output/auto.out b/test-suite/output/auto.out
index a5b55a9993..2761b87b02 100644
--- a/test-suite/output/auto.out
+++ b/test-suite/output/auto.out
@@ -18,3 +18,5 @@ Debug: 1 depth=5
Debug: 1.1 depth=4 simple apply or_intror
Debug: 1.1.1 depth=4 intro
Debug: 1.1.1.1 depth=4 exact H
+(* info trivial: *)
+exact I (in core).
diff --git a/test-suite/output/auto.v b/test-suite/output/auto.v
index a77b7b82e6..92917cdfc7 100644
--- a/test-suite/output/auto.v
+++ b/test-suite/output/auto.v
@@ -9,3 +9,7 @@ info_eauto.
Undo.
debug eauto.
Qed.
+
+Goal True.
+info_trivial.
+Qed.
diff --git a/test-suite/output/ltac_extra_args.out b/test-suite/output/ltac_extra_args.out
new file mode 100644
index 0000000000..77e799d359
--- /dev/null
+++ b/test-suite/output/ltac_extra_args.out
@@ -0,0 +1,8 @@
+The command has indeed failed with message:
+Illegal tactic application: got 1 extra argument.
+The command has indeed failed with message:
+Illegal tactic application: got 2 extra arguments.
+The command has indeed failed with message:
+Illegal tactic application: got 1 extra argument.
+The command has indeed failed with message:
+Illegal tactic application: got 2 extra arguments.
diff --git a/test-suite/output/ltac_extra_args.v b/test-suite/output/ltac_extra_args.v
new file mode 100644
index 0000000000..4caf619fee
--- /dev/null
+++ b/test-suite/output/ltac_extra_args.v
@@ -0,0 +1,10 @@
+Ltac foo := idtac.
+Ltac bar H := idtac.
+
+Goal True.
+Proof.
+ Fail foo H.
+ Fail foo H H'.
+ Fail bar H H'.
+ Fail bar H H' H''.
+Abort.
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index ecc988507c..7eaafc3545 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -156,6 +156,52 @@ Polymorphic Definition twoprojs (d : dyn) := dyn_proof d = dyn_proof d.
End structures.
+
+Module binders.
+
+ Definition mynat@{|} := nat.
+
+ Definition foo@{i j | i < j, i < j} (A : Type@{i}) : Type@{j}.
+ exact A.
+ Defined.
+
+ Definition nomoreu@{i j | i < j +} (A : Type@{i}) : Type@{j}.
+ pose(foo:=Type).
+ exact A.
+ Fail Defined.
+ Abort.
+
+ Polymorphic Definition moreu@{i j +} (A : Type@{i}) : Type@{j}.
+ pose(foo:=Type).
+ exact A.
+ Defined.
+
+ Check moreu@{_ _ _ _}.
+
+ Fail Definition morec@{i j|} (A : Type@{i}) : Type@{j} := A.
+
+ (* By default constraints are extensible *)
+ Polymorphic Definition morec@{i j} (A : Type@{i}) : Type@{j} := A.
+ Check morec@{_ _}.
+
+ (* Handled in proofs as well *)
+ Lemma bar@{i j | } : Type@{i}.
+ exact Type@{j}.
+ Fail Defined.
+ Abort.
+
+ Lemma bar@{i j| i < j} : Type@{j}.
+ Proof.
+ exact Type@{i}.
+ Qed.
+
+ Lemma barext@{i j|+} : Type@{j}.
+ Proof.
+ exact Type@{i}.
+ Qed.
+
+End binders.
+
Section cats.
Local Set Universe Polymorphism.
Require Import Utf8.
diff --git a/test-suite/success/qed_export.v b/test-suite/success/qed_export.v
deleted file mode 100644
index b3e41ab1fb..0000000000
--- a/test-suite/success/qed_export.v
+++ /dev/null
@@ -1,18 +0,0 @@
-Lemma a : True.
-Proof.
-assert True as H.
- abstract (trivial) using exported_seff.
-exact H.
-Fail Qed exporting a_subproof.
-Qed exporting exported_seff.
-Check ( exported_seff : True ).
-
-Lemma b : True.
-Proof.
-assert True as H.
- abstract (trivial) using exported_seff2.
-exact H.
-Qed.
-
-Fail Check ( exported_seff2 : True ).
-
diff --git a/test-suite/success/unshelve.v b/test-suite/success/unshelve.v
index 672222bdd6..a4fa544cd9 100644
--- a/test-suite/success/unshelve.v
+++ b/test-suite/success/unshelve.v
@@ -9,3 +9,11 @@ unshelve (refine (F _ _ _ _)).
+ exact (@eq_refl bool true).
+ exact (@eq_refl unit tt).
Qed.
+
+(* This was failing in 8.6, because of ?a:nat being wrongly duplicated *)
+
+Goal (forall a : nat, a = 0 -> True) -> True.
+intros F.
+unshelve (eapply (F _);clear F).
+2:reflexivity.
+Qed.
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 01:08:50 +0000