LtacProf cutoff is for total percent, not time

4 files changed, 49 insertions, 4 deletions

diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
index a91ff98fb..2514ededb 100644
--- a/ltac/profile_ltac.ml
+++ b/ltac/profile_ltac.ml
@@ -128,7 +128,7 @@ let to_ltacprof_results xml =
   | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof XML")
 
 let feedback_results results =
-  Feedback.(feedback 
+  Feedback.(feedback
     (Custom (Loc.dummy_loc, "ltacprof_results", of_ltacprof_results results)))
 
 (* ************** pretty printing ************************************* *)
@@ -218,7 +218,7 @@ let to_string ~filter ?(cutoff=0.0) node =
     !global
   in
   warn_encountered_multi_success_backtracking ();
-  let filter s n = filter s && n >= cutoff in
+  let filter s n = filter s && (all_total <= 0.0 || n /. all_total >= cutoff /. 100.0) in
   let msg =
     h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++
     fnl () ++
diff --git a/test-suite/Makefile b/test-suite/Makefile
index a40ea80ae..e3800ee22 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -304,12 +304,12 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
 	    | grep -v "\[Loading ML file" \
 	    | grep -v "Skipping rcfile loading" \
 	    | grep -v "^<W>" \
-	    | sed -e 's/\s*[0-9]*\.[0-9][0-9]*\s*//g' \
+	    | sed -e 's/\s*[-+0-9]*\.[0-9][0-9]*\s*//g' \
 	          -e 's/\s*0\.\s*//g' \
 		  -e 's/\s*[-+]nan\s*//g' \
 		  -e 's/\s*[-+]inf\s*//g' \
 	    > $$tmpoutput; \
-	  sed -e 's/\s*[0-9]*\.[0-9][0-9]*\s*//g' \
+	  sed -e 's/\s*[-+0-9]*\.[0-9][0-9]*\s*//g' \
 		-e 's/\s*0\.\s*//g' \
 		-e 's/\s*[-+]nan\s*//g' \
 		-e 's/\s*[-+]inf\s*//g' \
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 000000000..13cd87b8c
--- /dev/null
+++ b/test-suite/output-modulo-time/ltacprof_cutoff.out
@@ -0,0 +1,33 @@
+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
+
+ 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
+─constructor ---------------------------   0.0%   0.0%       1    0.000s
+
+ 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
+─constructor ---------------------------   0.0%   0.0%       1    0.000s
+
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 000000000..50131470e
--- /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.