Imported Upstream version 8.6upstream/8.6

4 files changed, 63 insertions, 0 deletions

diff --git a/test-suite/output-modulo-time/ltacprof.out b/test-suite/output-modulo-time/ltacprof.out
new file mode 100644
index 00000000..cc04c2c9
--- /dev/null
+++ b/test-suite/output-modulo-time/ltacprof.out
@@ -0,0 +1,12 @@
+total time:      1.528s
+
+ tactic                                   local  total   calls       max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─sleep' -------------------------------- 100.0% 100.0%       1    1.528s
+─constructor ---------------------------   0.0%   0.0%       1    0.000s
+
+ tactic                                   local  total   calls       max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─sleep' -------------------------------- 100.0% 100.0%       1    1.528s
+─constructor ---------------------------   0.0%   0.0%       1    0.000s
+
diff --git a/test-suite/output-modulo-time/ltacprof.v b/test-suite/output-modulo-time/ltacprof.v
new file mode 100644
index 00000000..6611db70
--- /dev/null
+++ b/test-suite/output-modulo-time/ltacprof.v
@@ -0,0 +1,8 @@
+(* -*- coq-prog-args: ("-emacs" "-profile-ltac-cutoff" "0.0") -*- *)
+Ltac sleep' := do 100 (do 100 (do 100 idtac)).
+Ltac sleep := sleep'.
+
+Theorem x : True.
+Proof.
+  idtac. idtac. sleep. constructor.
+Defined.
diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.out b/test-suite/output-modulo-time/ltacprof_cutoff.out
new file mode 100644
index 00000000..0cd5777c
--- /dev/null
+++ b/test-suite/output-modulo-time/ltacprof_cutoff.out
@@ -0,0 +1,31 @@
+total time:      1.584s
+
+ 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
+
+ tactic                                   local  total   calls       max 
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─foo2 ----------------------------------   0.0% 100.0%       1    1.584s
+└foo1 ----------------------------------   0.0%  63.9%       1    1.012s
+
+total time:      1.584s
+
+ 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
new file mode 100644
index 00000000..50131470
--- /dev/null
+++ b/test-suite/output-modulo-time/ltacprof_cutoff.v
@@ -0,0 +1,12 @@
+(* -*- coq-prog-args: ("-emacs" "-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).
+
+Ltac foo0 := idtac; sleep.
+Ltac foo1 := sleep; foo0.
+Ltac foo2 := sleep; foo1.
+Goal True.
+  foo2.
+  Show Ltac Profile CutOff 47.
+  constructor.
+Qed.