aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/Makefile9
-rw-r--r--test-suite/bugs/closed/5368.v6
-rw-r--r--test-suite/bugs/closed/6378.v14
-rw-r--r--test-suite/coq-makefile/timing/after/time-of-build-after.log.desired3
-rw-r--r--test-suite/coq-makefile/timing/after/time-of-build-before.log.desired3
-rw-r--r--test-suite/output-modulo-time/ltacprof.out13
-rw-r--r--test-suite/output-modulo-time/ltacprof_abstract.out17
-rw-r--r--test-suite/output-modulo-time/ltacprof_abstract.v8
-rw-r--r--test-suite/output-modulo-time/ltacprof_cutoff.out40
-rw-r--r--test-suite/output-modulo-time/ltacprof_cutoff.v34
-rw-r--r--test-suite/output/MExtraction.v12
-rw-r--r--test-suite/output/bug5778.out4
-rw-r--r--test-suite/output/bug5778.v7
-rw-r--r--test-suite/success/extraction.v2
14 files changed, 135 insertions, 37 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 6865dcc768..de669218ce 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -177,7 +177,7 @@ summary.log:
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 "${APPVEYOR}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo {}' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo' ';'; fi
+ $(HIDE)if [ "(" -n "${APPVEYOR}" ")" -o "(" -n "${CIRCLECI}" ")" ]; 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
#######################################################################
@@ -312,6 +312,13 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
rm $$tmpoutput; \
} > "$@"
+# the expected output for the MExtraction test is
+# /plugins/micromega/micromega.ml except with additional newline
+output/MExtraction.out: ../plugins/micromega/micromega.ml
+ $(SHOW) GEN $@
+ $(HIDE) cp $< $@
+ $(HIDE) echo >> $@
+
$(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
diff --git a/test-suite/bugs/closed/5368.v b/test-suite/bugs/closed/5368.v
new file mode 100644
index 0000000000..410fe1707d
--- /dev/null
+++ b/test-suite/bugs/closed/5368.v
@@ -0,0 +1,6 @@
+Set Universe Polymorphism.
+
+Record cantype := {T:Type; op:T -> unit}.
+Canonical Structure test (P:Type) := {| T := P -> Type; op := fun _ => tt|}.
+
+Check (op _ ((fun (_:unit) => Set):_)).
diff --git a/test-suite/bugs/closed/6378.v b/test-suite/bugs/closed/6378.v
index d0ef090d08..68ae7961dd 100644
--- a/test-suite/bugs/closed/6378.v
+++ b/test-suite/bugs/closed/6378.v
@@ -1,4 +1,18 @@
+Require Import Coq.ZArith.ZArith.
+Ltac profile_constr tac :=
+ let dummy := match goal with _ => reset ltac profile; start ltac profiling end in
+ let ret := match goal with _ => tac () end in
+ let dummy := match goal with _ => stop ltac profiling; show ltac profile end in
+ pose 1.
+
+Ltac slow _ := eval vm_compute in (Z.div_eucl, Z.div_eucl, Z.div_eucl, Z.div_eucl, Z.div_eucl).
+
Goal True.
start ltac profiling.
+ reset ltac profile.
+ reset ltac profile.
stop ltac profiling.
+ time profile_constr slow.
+ show ltac profile cutoff 0.
+ show ltac profile "slow".
Abort.
diff --git a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired
index 729de2f366..7900c034da 100644
--- a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired
+++ b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired
@@ -1,7 +1,6 @@
Makefile:69: warning: undefined variable '*'
Makefile:204: warning: undefined variable 'DSTROOT'
-COQDEP Fast.v
-COQDEP Slow.v
+COQDEP VFILES
Makefile:69: warning: undefined variable '*'
Makefile:204: warning: undefined variable 'DSTROOT'
Makefile:69: warning: undefined variable '*'
diff --git a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired
index b25bc3683c..7ab0bc75d9 100644
--- a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired
+++ b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired
@@ -1,7 +1,6 @@
Makefile:69: warning: undefined variable '*'
Makefile:204: warning: undefined variable 'DSTROOT'
-COQDEP Fast.v
-COQDEP Slow.v
+COQDEP VFILES
Makefile:69: warning: undefined variable '*'
Makefile:204: warning: undefined variable 'DSTROOT'
Makefile:69: warning: undefined variable '*'
diff --git a/test-suite/output-modulo-time/ltacprof.out b/test-suite/output-modulo-time/ltacprof.out
index cc04c2c9bd..5553e1b38d 100644
--- a/test-suite/output-modulo-time/ltacprof.out
+++ b/test-suite/output-modulo-time/ltacprof.out
@@ -1,12 +1,15 @@
-total time: 1.528s
+total time: 1.032s
- tactic local total calls max
+ tactic local total calls max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─sleep' -------------------------------- 100.0% 100.0% 1 1.528s
+─sleep' -------------------------------- 100.0% 100.0% 1 1.032s
+─sleep --------------------------------- 0.0% 0.0% 0 0.000s
─constructor --------------------------- 0.0% 0.0% 1 0.000s
- tactic local total calls max
+ tactic local total calls max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─sleep' -------------------------------- 100.0% 100.0% 1 1.528s
+─sleep' -------------------------------- 100.0% 100.0% 1 1.032s
+─sleep --------------------------------- 0.0% 0.0% 0 0.000s
+└sleep' -------------------------------- 0.0% 0.0% 0 0.000s
─constructor --------------------------- 0.0% 0.0% 1 0.000s
diff --git a/test-suite/output-modulo-time/ltacprof_abstract.out b/test-suite/output-modulo-time/ltacprof_abstract.out
new file mode 100644
index 0000000000..fef4fa248d
--- /dev/null
+++ b/test-suite/output-modulo-time/ltacprof_abstract.out
@@ -0,0 +1,17 @@
+total time: 0.922s
+
+ tactic local total calls max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─abstract (sleep; constructor) --------- 0.0% 100.0% 1 0.922s
+─sleep' -------------------------------- 100.0% 100.0% 1 0.922s
+─constructor --------------------------- 0.0% 0.0% 1 0.000s
+─sleep --------------------------------- 0.0% 0.0% 0 0.000s
+
+ tactic local total calls max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─abstract (sleep; constructor) --------- 0.0% 100.0% 1 0.922s
+ ├─sleep' ------------------------------ 100.0% 100.0% 1 0.922s
+ ├─constructor ------------------------- 0.0% 0.0% 1 0.000s
+ └─sleep ------------------------------- 0.0% 0.0% 0 0.000s
+ └sleep' ------------------------------ 0.0% 0.0% 0 0.000s
+
diff --git a/test-suite/output-modulo-time/ltacprof_abstract.v b/test-suite/output-modulo-time/ltacprof_abstract.v
new file mode 100644
index 0000000000..10a76309e3
--- /dev/null
+++ b/test-suite/output-modulo-time/ltacprof_abstract.v
@@ -0,0 +1,8 @@
+(* -*- coq-prog-args: ("-profile-ltac-cutoff" "0.0") -*- *)
+Ltac sleep' := do 100 (do 100 (do 100 idtac)).
+Ltac sleep := sleep'.
+
+Theorem x : True.
+Proof.
+ idtac. idtac. abstract (sleep; constructor).
+Defined.
diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.out b/test-suite/output-modulo-time/ltacprof_cutoff.out
index 0cd5777ccf..d91a38bb54 100644
--- a/test-suite/output-modulo-time/ltacprof_cutoff.out
+++ b/test-suite/output-modulo-time/ltacprof_cutoff.out
@@ -1,31 +1,37 @@
-total time: 1.584s
+total time: 1.632s
tactic local total calls max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s
-─sleep --------------------------------- 100.0% 100.0% 3 0.572s
-─foo1 ---------------------------------- 0.0% 63.9% 1 1.012s
+─sleep --------------------------------- 100.0% 100.0% 3 0.584s
+─foo2 ---------------------------------- 0.0% 100.0% 1 1.632s
+─foo1 ---------------------------------- 0.0% 64.2% 1 1.048s
tactic local total calls max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s
-└foo1 ---------------------------------- 0.0% 63.9% 1 1.012s
+─foo2 ---------------------------------- 0.0% 100.0% 1 1.632s
+└foo1 ---------------------------------- 0.0% 64.2% 1 1.048s
-total time: 1.584s
+total time: 0.520s
+
+ tactic local total calls max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─foo2 ---------------------------------- 0.0% 100.0% 1 0.520s
+─sleep --------------------------------- 99.2% 99.2% 52 0.016s
+─foo1 ---------------------------------- 0.0% 97.7% 1 0.508s
+─foo0 ---------------------------------- 0.8% 96.2% 1 0.500s
+
+ tactic local total calls max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─foo2 ---------------------------------- 0.0% 100.0% 1 0.520s
+└foo1 ---------------------------------- 0.0% 97.7% 1 0.508s
+└foo0 ---------------------------------- 0.8% 96.2% 1 0.500s
+└sleep --------------------------------- 95.4% 95.4% 50 0.016s
+
+total time: 0.000s
tactic local total calls max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─sleep --------------------------------- 100.0% 100.0% 3 0.572s
-─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s
-─foo1 ---------------------------------- 0.0% 63.9% 1 1.012s
-─foo0 ---------------------------------- 0.0% 31.3% 1 0.496s
tactic local total calls max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s
- ├─foo1 -------------------------------- 0.0% 63.9% 1 1.012s
- │ ├─sleep ----------------------------- 32.6% 32.6% 1 0.516s
- │ └─foo0 ------------------------------ 0.0% 31.3% 1 0.496s
- │ └sleep ----------------------------- 31.3% 31.3% 1 0.496s
- └─sleep ------------------------------- 36.1% 36.1% 1 0.572s
diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v
index 3dad6271af..ae5d51bae8 100644
--- a/test-suite/output-modulo-time/ltacprof_cutoff.v
+++ b/test-suite/output-modulo-time/ltacprof_cutoff.v
@@ -1,12 +1,28 @@
(* -*- coq-prog-args: ("-profile-ltac") -*- *)
Require Coq.ZArith.BinInt.
-Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac).
+Module WithIdTac.
+ Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac).
-Ltac foo0 := idtac; sleep.
-Ltac foo1 := sleep; foo0.
-Ltac foo2 := sleep; foo1.
-Goal True.
- foo2.
- Show Ltac Profile CutOff 47.
- constructor.
-Qed.
+ Ltac foo0 := idtac; sleep.
+ Ltac foo1 := sleep; foo0.
+ Ltac foo2 := sleep; foo1.
+ Goal True.
+ foo2.
+ Show Ltac Profile CutOff 47.
+ constructor.
+ Qed.
+End WithIdTac.
+
+Module TestEval.
+ Ltac sleep := let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac.
+
+ Ltac foo0 := idtac; do 50 (idtac; sleep).
+ Ltac foo1 := sleep; foo0.
+ Ltac foo2 := sleep; foo1.
+ Goal True.
+ Reset Ltac Profile.
+ foo2.
+ Show Ltac Profile CutOff 47.
+ constructor.
+ Qed.
+End TestEval.
diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v
new file mode 100644
index 0000000000..352e422cf7
--- /dev/null
+++ b/test-suite/output/MExtraction.v
@@ -0,0 +1,12 @@
+Require Import micromega.MExtraction.
+Require Import RingMicromega.
+Require Import QArith.
+Require Import VarMap.
+Require Import ZMicromega.
+Require Import QMicromega.
+Require Import RMicromega.
+
+Recursive Extraction
+ List.map RingMicromega.simpl_cone (*map_cone indexes*)
+ denorm Qpower vm_add
+ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
diff --git a/test-suite/output/bug5778.out b/test-suite/output/bug5778.out
new file mode 100644
index 0000000000..91ceb1b583
--- /dev/null
+++ b/test-suite/output/bug5778.out
@@ -0,0 +1,4 @@
+The command has indeed failed with message:
+In nested Ltac calls to "c", "abs" and "abstract b ltac:(())", last call
+failed.
+The term "I" has type "True" which should be Set, Prop or Type.
diff --git a/test-suite/output/bug5778.v b/test-suite/output/bug5778.v
new file mode 100644
index 0000000000..0dcd76aeff
--- /dev/null
+++ b/test-suite/output/bug5778.v
@@ -0,0 +1,7 @@
+Ltac a _ := pose (I : I).
+Ltac b _ := a ().
+Ltac abs _ := abstract b ().
+Ltac c _ := abs ().
+Goal True.
+ Fail c ().
+Abort.
diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index 0ee2232502..83726bfdc5 100644
--- a/test-suite/success/extraction.v
+++ b/test-suite/success/extraction.v
@@ -635,6 +635,6 @@ Recursive Extraction Everything.
Require Import ZArith.
-Extraction Language Ocaml.
+Extraction Language OCaml.
Recursive Extraction Z_modulo_2 Zdiv_eucl_exist.
Extraction TestCompile Z_modulo_2 Zdiv_eucl_exist.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 21:17:47 +0000