aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/Makefile14
-rw-r--r--test-suite/bugs/closed/8270.v15
-rw-r--r--test-suite/bugs/closed/8288.v7
-rw-r--r--test-suite/bugs/closed/8432.v39
-rw-r--r--test-suite/output/Arguments.v2
-rw-r--r--test-suite/output/Notations.v1
-rw-r--r--test-suite/output/PrintAssumptions.out2
-rw-r--r--test-suite/output/PrintAssumptions.v10
-rw-r--r--test-suite/output/Quote.v36
-rw-r--r--test-suite/output/ltac.out11
-rw-r--r--test-suite/output/ltac.v10
-rw-r--r--test-suite/prerequisite/module_bug7192.v9
-rw-r--r--test-suite/prerequisite/module_bug8416.v2
-rwxr-xr-xtest-suite/report.sh55
-rwxr-xr-xtest-suite/save-logs.sh19
-rw-r--r--test-suite/success/Template.v48
-rw-r--r--test-suite/success/ltac.v29
17 files changed, 246 insertions, 63 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index b8aac8b6f8..93ce519350 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -106,7 +106,8 @@ SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile unit-te
PREREQUISITELOG = prerequisite/admit.v.log \
prerequisite/make_local.v.log prerequisite/make_notation.v.log \
- prerequisite/bind_univs.v.log
+ prerequisite/bind_univs.v.log prerequisite/module_bug8416.v.log \
+ prerequisite/module_bug7192.v.log
#######################################################################
# Phony targets
@@ -126,14 +127,14 @@ clean:
$(SHOW) 'RM <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>'
$(HIDE)find . \( \
-name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' -o -name '*.glob' \
- \) -print0 | xargs -0 rm -f
+ \) -exec rm -f {} +
$(SHOW) 'RM <**/*.cmx> <**/*.cmi> <**/*.o> <**/*.test>'
$(HIDE)find unit-tests \( \
-name '*.cmx' -o -name '*.cmi' -o -name '*.o' -o -name '*.test' \
- \) -print0 | xargs -0 rm -f
+ \) -exec rm -f {} +
distclean: clean
$(SHOW) 'RM <**/*.aux>'
- $(HIDE)find . -name '*.aux' -print0 | xargs -0 rm -f
+ $(HIDE)find . -name '*.aux' -exec rm -f {} +
#######################################################################
# Per-subsystem targets
@@ -195,10 +196,7 @@ PRINT_LOGS:=APPVEYOR
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 "${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
+ $(HIDE)bash report.sh
#######################################################################
# Regression (and progression) tests
diff --git a/test-suite/bugs/closed/8270.v b/test-suite/bugs/closed/8270.v
new file mode 100644
index 0000000000..f36f757f10
--- /dev/null
+++ b/test-suite/bugs/closed/8270.v
@@ -0,0 +1,15 @@
+(* Don't do zeta in cbn when not asked for *)
+
+Goal let x := 0 in
+ let y := x in
+ y = 0.
+ (* We use "cofix" as an example because there are obviously no
+ cofixpoints in sight. This problem arises with any set of
+ reduction flags (not including zeta where the lets are of course reduced away) *)
+ cbn cofix.
+ intro x.
+ unfold x at 1. (* Should succeed *)
+ Undo 2.
+ cbn zeta.
+ Fail unfold x at 1.
+Abort.
diff --git a/test-suite/bugs/closed/8288.v b/test-suite/bugs/closed/8288.v
new file mode 100644
index 0000000000..0350be9c06
--- /dev/null
+++ b/test-suite/bugs/closed/8288.v
@@ -0,0 +1,7 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Set Polymorphic Inductive Cumulativity.
+
+Inductive foo := C : (forall A : Type -> Type, A Type) -> foo.
+(* anomaly invalid subtyping relation *)
diff --git a/test-suite/bugs/closed/8432.v b/test-suite/bugs/closed/8432.v
new file mode 100644
index 0000000000..844ee12668
--- /dev/null
+++ b/test-suite/bugs/closed/8432.v
@@ -0,0 +1,39 @@
+Require Import Program.Tactics.
+
+Obligation Tactic := idtac.
+Set Universe Polymorphism.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+ idpath : paths a a.
+
+Inductive Empty : Type :=.
+Inductive Unit : Type := tt.
+Definition not (A : Type) := A -> Empty.
+
+ Lemma nat_path_O_S (n : nat) (H : paths O (S n)) : Empty.
+ Proof. refine (
+ match H in paths _ i return
+ match i with
+ | O => Unit
+ | S _ => Empty
+ end
+ with
+ | idpath _ => tt
+ end
+ ). Defined.
+ Lemma symmetry {A} (x y : A) (p : paths x y) : paths y x.
+ Proof.
+ destruct p. apply idpath.
+ Defined.
+ Lemma nat_path_S_O (n : nat) (H : paths (S n) O) : Empty.
+ Proof. eapply nat_path_O_S. exact (symmetry _ _ H). Defined.
+Set Printing Universes.
+Program Fixpoint succ_not_zero (n:nat) : not (paths (S n) 0) :=
+match n as n return not (paths (S n) 0) with
+| 0 => nat_path_S_O _
+| S n' => let dummy := succ_not_zero n' in _
+end.
+Next Obligation.
+ intros f _ n dummy H. exact (nat_path_S_O _ H).
+ Show Universes.
+Defined.
diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
index bd9240476f..b67ac4f0df 100644
--- a/test-suite/output/Arguments.v
+++ b/test-suite/output/Arguments.v
@@ -10,6 +10,8 @@ Arguments Nat.sub !n !m.
About Nat.sub.
Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) :=
fun x => (f (fst x), g (snd x)).
+Declare Scope foo_scope.
+Declare Scope bar_scope.
Delimit Scope foo_scope with F.
Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never.
About pf.
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index fe6c05c39e..adab324cf0 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -76,6 +76,7 @@ Open Scope nat_scope.
Inductive znat : Set := Zpos (n : nat) | Zneg (m : nat).
Coercion Zpos: nat >-> znat.
+Declare Scope znat_scope.
Delimit Scope znat_scope with znat.
Open Scope znat_scope.
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
index 34f44cd246..3f4d5ef58c 100644
--- a/test-suite/output/PrintAssumptions.out
+++ b/test-suite/output/PrintAssumptions.out
@@ -20,3 +20,5 @@ Axioms:
M.foo : False
Closed under the global context
Closed under the global context
+Closed under the global context
+Closed under the global context
diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v
index ea1ab63786..3d4dfe603d 100644
--- a/test-suite/output/PrintAssumptions.v
+++ b/test-suite/output/PrintAssumptions.v
@@ -137,3 +137,13 @@ Module F (X : T).
End F.
End SUBMODULES.
+
+(* Testing a variant of #7192 across files *)
+(* This was missing in the original fix to #7192 *)
+Require Import module_bug7192.
+Print Assumptions M7192.D.f.
+
+(* Testing reporting assumptions from modules in files *)
+(* A regression introduced in the original fix to #7192 was missing implementations *)
+Require Import module_bug8416.
+Print Assumptions M8416.f.
diff --git a/test-suite/output/Quote.v b/test-suite/output/Quote.v
deleted file mode 100644
index 2c373d5052..0000000000
--- a/test-suite/output/Quote.v
+++ /dev/null
@@ -1,36 +0,0 @@
-Require Import Quote.
-
-Parameter A B : Prop.
-
-Inductive formula : Type :=
- | f_and : formula -> formula -> formula
- | f_or : formula -> formula -> formula
- | f_not : formula -> formula
- | f_true : formula
- | f_atom : index -> formula
- | f_const : Prop -> formula.
-
-Fixpoint interp_f (vm:
- varmap Prop) (f:formula) {struct f} : Prop :=
- match f with
- | f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2
- | f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2
- | f_not f1 => ~ interp_f vm f1
- | f_true => True
- | f_atom i => varmap_find True i vm
- | f_const c => c
- end.
-
-Goal A \/ B -> A /\ (B \/ A) /\ (A \/ ~ B).
-intro H.
-match goal with
- | H : ?a \/ ?b |- _ => quote interp_f in a using (fun x => idtac x; change (x \/ b) in H)
-end.
-match goal with
- |- ?g => quote interp_f [ A ] in g using (fun x => idtac x)
-end.
-quote interp_f.
-Show.
-simpl; quote interp_f [ A ].
-Show.
-Admitted.
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index eb9f571022..efdc94fb1e 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -38,3 +38,14 @@ Ltac foo :=
let w := () in
let z := 1 in
pose v
+2 subgoals
+
+ n : nat
+ ============================
+ (fix a (n0 : nat) : nat := match n0 with
+ | 0 => 0
+ | S n1 => a n1
+ end) n = n
+
+subgoal 2 is:
+ forall a : nat, a = 0
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 901b1e3aa6..40e743c3f0 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -71,3 +71,13 @@ Ltac foo :=
let z := 1 in
pose v.
Print Ltac foo.
+
+(* Ltac renaming was not applied to "fix" and "cofix" *)
+
+Goal forall a, a = 0.
+match goal with
+|- (forall x, x = _) => assert (forall n, (fix x n := match n with O => O | S n => x n end) n = n)
+end.
+intro.
+Show.
+Abort.
diff --git a/test-suite/prerequisite/module_bug7192.v b/test-suite/prerequisite/module_bug7192.v
new file mode 100644
index 0000000000..82cfe560af
--- /dev/null
+++ b/test-suite/prerequisite/module_bug7192.v
@@ -0,0 +1,9 @@
+(* Variant of #7192 to be tested in a file requiring this file *)
+(* #7192 is about Print Assumptions not entering implementation of submodules *)
+
+Definition a := True.
+Module Type B. Axiom f : Prop. End B.
+Module Type C. Declare Module D : B. End C.
+Module M7192: C.
+ Module D <: B. Definition f := a. End D.
+End M7192.
diff --git a/test-suite/prerequisite/module_bug8416.v b/test-suite/prerequisite/module_bug8416.v
new file mode 100644
index 0000000000..70f43d132a
--- /dev/null
+++ b/test-suite/prerequisite/module_bug8416.v
@@ -0,0 +1,2 @@
+Module Type A. Axiom f : True. End A.
+Module M8416 : A. Definition f := I. End M8416.
diff --git a/test-suite/report.sh b/test-suite/report.sh
new file mode 100755
index 0000000000..05f39b4b02
--- /dev/null
+++ b/test-suite/report.sh
@@ -0,0 +1,55 @@
+#!/usr/bin/env bash
+
+# save failed logs to logs/, then print failure information
+# returns failure code if any failed logs exist
+
+# save step
+
+SAVEDIR="logs"
+
+# reset for local builds
+rm -rf "$SAVEDIR"
+mkdir "$SAVEDIR"
+
+# keep this synced with test-suite/Makefile
+FAILMARK="==========> FAILURE <=========="
+
+FAILED=$(mktemp /tmp/coq-check-XXXXXX)
+find . '(' -path ./bugs/opened -prune ')' -o '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED"
+
+rsync -a --from0 --files-from="$FAILED" . "$SAVEDIR"
+cp summary.log "$SAVEDIR"/
+
+# cleanup
+rm "$FAILED"
+
+# print info
+if [ -n "$TRAVIS" ] || [ -n "$PRINT_LOGS" ]; then
+ find logs/ -name '*.log' -not -name 'summary.log' -print0 | while IFS= read -r -d '' file; do
+ if [ -n "$TRAVIS" ]; then
+ # ${foo////.} replaces every / by . in $foo
+ printf 'travis_fold:start:coq.logs.%s\n' "${file////.}";
+ else printf '%s\n' "$file"
+ fi
+
+ cat "$file"
+
+ if [ -n "$TRAVIS" ]; then
+ # ${foo////.} replaces every / by . in $foo
+ printf 'travis_fold:end:coq.logs.%s\n' "${file////.}";
+ else printf '\n'
+ fi
+ done
+fi
+
+if grep -q -F 'Error!' summary.log ; then
+ echo FAILURES;
+ grep -F 'Error!' summary.log;
+ if [ -z "$TRAVIS" ] && [ -z "$PRINT_LOGS" ]; then
+ echo 'To print details of failed tests, rerun with environment variable PRINT_LOGS=1'
+ echo 'eg "make report PRINT_LOGS=1" from the test suite directory"'
+ echo 'See README.md in the test suite directory for more information.'
+ fi
+ false
+else echo NO FAILURES;
+fi
diff --git a/test-suite/save-logs.sh b/test-suite/save-logs.sh
deleted file mode 100755
index 9b8fff09f8..0000000000
--- a/test-suite/save-logs.sh
+++ /dev/null
@@ -1,19 +0,0 @@
-#!/usr/bin/env bash
-
-SAVEDIR="logs"
-
-# reset for local builds
-rm -rf "$SAVEDIR"
-mkdir "$SAVEDIR"
-
-# keep this synced with test-suite/Makefile
-FAILMARK="==========> FAILURE <=========="
-
-FAILED=$(mktemp /tmp/coq-check-XXXXXX)
-find . '(' -path ./bugs/opened -prune ')' -o '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED"
-
-rsync -a --from0 --files-from="$FAILED" . "$SAVEDIR"
-cp summary.log "$SAVEDIR"/
-
-# cleanup
-rm "$FAILED"
diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v
new file mode 100644
index 0000000000..1c6e2d81d8
--- /dev/null
+++ b/test-suite/success/Template.v
@@ -0,0 +1,48 @@
+Set Printing Universes.
+
+Module AutoYes.
+ Inductive Box (A:Type) : Type := box : A -> Box A.
+
+ About Box.
+
+ (* This checks that Box is template poly, see module No for how it fails *)
+ Universe i j. Constraint i < j.
+ Definition j_lebox (A:Type@{j}) := Box A.
+ Definition box_lti A := Box A : Type@{i}.
+
+End AutoYes.
+
+Module AutoNo.
+ Unset Auto Template Polymorphism.
+ Inductive Box (A:Type) : Type := box : A -> Box A.
+
+ About Box.
+
+ Universe i j. Constraint i < j.
+ Definition j_lebox (A:Type@{j}) := Box A.
+ Fail Definition box_lti A := Box A : Type@{i}.
+
+End AutoNo.
+
+Module Yes.
+ #[template]
+ Inductive Box@{i} (A:Type@{i}) : Type@{i} := box : A -> Box A.
+
+ About Box.
+
+ Universe i j. Constraint i < j.
+ Definition j_lebox (A:Type@{j}) := Box A.
+ Definition box_lti A := Box A : Type@{i}.
+
+End Yes.
+
+Module No.
+ #[notemplate]
+ Inductive Box (A:Type) : Type := box : A -> Box A.
+
+ About Box.
+
+ Universe i j. Constraint i < j.
+ Definition j_lebox (A:Type@{j}) := Box A.
+ Fail Definition box_lti A := Box A : Type@{i}.
+End No.
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 0f22a1f0a0..4404ff3f16 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -348,3 +348,32 @@ symmetry in H.
match goal with h:_ |- _ => assert (h=h) end. (* h should be H0 *)
exact (eq_refl H0).
Abort.
+
+(* Check that internal names used in "match" compilation to push "term
+ to match" on the environment are not interpreted as ltac variables *)
+
+Module ToMatchNames.
+Ltac g c := let r := constr:(match c return _ with a => 1 end) in idtac.
+Goal True.
+g 1.
+Abort.
+End ToMatchNames.
+
+(* An example where internal names used to build the return predicate
+ (here "n" because "a" is bound to "nil" and "n" is the first letter
+ of "nil") by small inversion should be taken distinct from Ltac names. *)
+
+Module LtacNames.
+Inductive t (A : Type) : nat -> Type :=
+ nil : t A 0 | cons : A -> forall n : nat, t A n -> t A (S n).
+
+Ltac f a n :=
+ let x := constr:(match a with nil _ => true | cons _ _ _ _ => I end) in
+ assert (x=x/\n=n).
+
+Goal forall (y:t nat 0), True.
+intros.
+f y true.
+Abort.
+
+End LtacNames.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 09:33:35 +0000