aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/.csdp.cachebin313112 -> 329899 bytes
-rw-r--r--test-suite/Makefile18
-rw-r--r--test-suite/bugs/closed/bug_11342.v19
-rw-r--r--test-suite/ide/debug_ltac.fake1
-rw-r--r--test-suite/ide/undo002.fake1
-rw-r--r--test-suite/output/Inductive.out2
-rw-r--r--test-suite/output/Inductive.v8
-rw-r--r--test-suite/output/bug_11342.out1
-rw-r--r--test-suite/output/bug_11342.v12
-rw-r--r--test-suite/output/bug_11608.out1
-rw-r--r--test-suite/output/bug_11608.v13
-rw-r--r--test-suite/output/bug_8206.out5
-rw-r--r--test-suite/output/bug_8206.v11
-rw-r--r--test-suite/success/pose.v9
14 files changed, 94 insertions, 7 deletions
diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index b3bcb5b056..046cb067c5 100644
--- a/test-suite/.csdp.cache
+++ b/test-suite/.csdp.cache
Binary files differ
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 265c2eafa7..1681150f7b 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -32,11 +32,15 @@ include ../Makefile.common
# Variables
#######################################################################
+# Using quotes to anticipate the possibility of spaces in the directory name
+# Note that this will later need an eval in shell to interpret the quotes
+ROOT='$(shell cd ..; pwd)'
+
ifneq ($(wildcard ../_build),)
-BIN:=$(shell cd ..; pwd)/_build/install/default/bin/
-COQLIB:=$(shell cd ..; pwd)/_build/install/default/lib/coq
+BIN:=$(ROOT)/_build/install/default/bin/
+COQLIB:=$(ROOT)/_build/install/default/lib/coq
else
-BIN := $(shell cd ..; pwd)/bin/
+BIN := $(ROOT)/bin/
COQLIB?=
ifeq ($(COQLIB),)
@@ -602,10 +606,10 @@ $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG)
@echo "TEST $<"
$(HIDE){ \
echo $(call log_intro,$<); \
- export BIN="$(BIN)"; \
- export coqc="$(coqc)"; \
- export coqtop="$(coqc)"; \
- export coqdep="$(coqdep)"; \
+ export BIN=$(BIN); \
+ export coqc="eval $(coqc)"; \
+ export coqtop="eval $(coqc)"; \
+ export coqdep="eval $(coqdep)"; \
"$<" 2>&1; R=$$?; times; \
if [ $$R = 0 ]; then \
echo $(log_success); \
diff --git a/test-suite/bugs/closed/bug_11342.v b/test-suite/bugs/closed/bug_11342.v
new file mode 100644
index 0000000000..3c163fb772
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11342.v
@@ -0,0 +1,19 @@
+(* -*- mode: coq; coq-prog-args: ("-vos") -*- *)
+
+Section foo.
+ Context {H:True}.
+ Set Default Proof Using "Type".
+ Theorem test2 : True.
+ Proof.
+ (* BUG: this gets run when compiling with -vos *)
+ fail "proof with default using".
+ exact I.
+ Qed.
+
+ Theorem test3 : True.
+ Proof using Type.
+ (* this isn't run with -vos *)
+ fail "using".
+ exact I.
+ Qed.
+End foo.
diff --git a/test-suite/ide/debug_ltac.fake b/test-suite/ide/debug_ltac.fake
index aa68fad39e..38c610a5a6 100644
--- a/test-suite/ide/debug_ltac.fake
+++ b/test-suite/ide/debug_ltac.fake
@@ -1,2 +1,3 @@
+ADD { Comments "fakeide doesn't support fail as the first sentence". }
FAILADD { Debug On. }
ADD { Set Debug On. }
diff --git a/test-suite/ide/undo002.fake b/test-suite/ide/undo002.fake
index 5284c5d3a5..eb553f9dfa 100644
--- a/test-suite/ide/undo002.fake
+++ b/test-suite/ide/undo002.fake
@@ -3,6 +3,7 @@
#
# Simple backtrack by 2 before two global definitions
#
+ADD initial { Comments "initial sentence". }
ADD { Definition foo := 0. }
ADD { Definition bar := 1. }
EDIT_AT initial
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index 8ff571ae55..ff2556c5dc 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -5,3 +5,5 @@ Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x
Arguments foo _%type_scope
Arguments Foo _%type_scope
+myprod unit bool
+ : Set
diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v
index 9eec9a7dad..db1276cb6c 100644
--- a/test-suite/output/Inductive.v
+++ b/test-suite/output/Inductive.v
@@ -5,3 +5,11 @@ Fail Inductive list' (A:Set) : Set :=
(* Check printing of let-ins *)
#[universes(template)] Inductive foo (A : Type) (x : A) (y := x) := Foo.
Print foo.
+
+(* Check where clause *)
+Reserved Notation "x ** y" (at level 40, left associativity).
+Inductive myprod A B :=
+ mypair : A -> B -> A ** B
+ where "A ** B" := (myprod A B) (only parsing).
+
+Check unit ** bool.
diff --git a/test-suite/output/bug_11342.out b/test-suite/output/bug_11342.out
new file mode 100644
index 0000000000..9aac16de0d
--- /dev/null
+++ b/test-suite/output/bug_11342.out
@@ -0,0 +1 @@
+without using
diff --git a/test-suite/output/bug_11342.v b/test-suite/output/bug_11342.v
new file mode 100644
index 0000000000..73131a3190
--- /dev/null
+++ b/test-suite/output/bug_11342.v
@@ -0,0 +1,12 @@
+(* -*- mode: coq; coq-prog-args: ("-vos") -*- *)
+
+Section foo.
+ Context {H:True}.
+ Theorem test1 : True.
+ Proof.
+ (* this gets printed with -vos because there's no annotation (either [Set
+ Default Proof Using ...] or an explicit [Proof using ...]) *)
+ idtac "without using".
+ exact I.
+ Qed.
+End foo.
diff --git a/test-suite/output/bug_11608.out b/test-suite/output/bug_11608.out
new file mode 100644
index 0000000000..793ff768d4
--- /dev/null
+++ b/test-suite/output/bug_11608.out
@@ -0,0 +1 @@
+creating x without [Proof.]
diff --git a/test-suite/output/bug_11608.v b/test-suite/output/bug_11608.v
new file mode 100644
index 0000000000..3929082913
--- /dev/null
+++ b/test-suite/output/bug_11608.v
@@ -0,0 +1,13 @@
+(* -*- mode: coq; coq-prog-args: ("-vos") -*- *)
+
+Set Default Proof Using "Type".
+
+Section foo.
+ Context (A:Type).
+ Definition x : option A.
+ (* this can get printed with -vos since without "Proof." there's no Proof
+ using, even with a default annotation. *)
+ idtac "creating x without [Proof.]".
+ exact None.
+ Qed.
+End foo.
diff --git a/test-suite/output/bug_8206.out b/test-suite/output/bug_8206.out
new file mode 100644
index 0000000000..6015fe32f9
--- /dev/null
+++ b/test-suite/output/bug_8206.out
@@ -0,0 +1,5 @@
+File "stdin", line 11, characters 0-23:
+Error: Signature components for label homework do not match: expected type
+"forall a b : nat, bug_8206.M.add a b = bug_8206.M.add b a" but found type
+"nat -> forall b : nat, bug_8206.M.add 0 b = bug_8206.M.add b 0".
+
diff --git a/test-suite/output/bug_8206.v b/test-suite/output/bug_8206.v
new file mode 100644
index 0000000000..8d4e73dfac
--- /dev/null
+++ b/test-suite/output/bug_8206.v
@@ -0,0 +1,11 @@
+Module Type Sig.
+ Parameter add: nat -> nat -> nat.
+ Axiom homework: forall (a b: nat), add a b = add b a.
+End Sig.
+
+Module Impl.
+ Definition add(a b: nat) := plus a b.
+ Axiom homework: forall (a b: nat), add 0 b = add b 0.
+End Impl.
+
+Module M : Sig := Impl.
diff --git a/test-suite/success/pose.v b/test-suite/success/pose.v
new file mode 100644
index 0000000000..17007915fe
--- /dev/null
+++ b/test-suite/success/pose.v
@@ -0,0 +1,9 @@
+(* Test syntax *)
+
+Goal 0=0.
+pose proof (a := I).
+Fail clearbody a.
+epose proof (b := fun _ => eq_refl).
+Fail clearbody b.
+exact (b a).
+Qed.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 19:34:10 +0000