LtacProf: "Show Ltac Profile CutOff $N" (fix #5080)

It seems we have no grammar rule that parses floats, so I'm
parsing an integer, but the whole machinery supports floats.

3 files changed, 14 insertions, 9 deletions

diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
index fe591c775..102918e5e 100644
--- a/ltac/profile_ltac.ml
+++ b/ltac/profile_ltac.ml
@@ -166,7 +166,7 @@ let rec print_node ~filter all_total indent prefix (s, e) =
 and print_table ~filter all_total indent first_level table =
   let fold _ n l =
     let s, total = n.name, n.total in
-    if filter s then (s, n) :: l else l in
+    if filter s total then (s, n) :: l else l in
   let ls = M.fold fold table [] in
   match ls with
   | [s, n] when not first_level ->
@@ -182,7 +182,7 @@ and print_table ~filter all_total indent first_level table =
     in
     prlist (fun pr -> pr) (list_iter_is_last iter ls)
 
-let to_string ~filter node =
+let to_string ~filter ?(cutoff=0.0) node =
   let tree = node.children in
   let all_total = M.fold (fun _ { total } a -> total +. a) node.children 0.0 in
   let flat_tree =
@@ -218,6 +218,7 @@ let to_string ~filter node =
     !global
   in
   warn_encountered_multi_success_backtracking ();
+  let filter s n = filter s && n >= cutoff in
   let msg =
     h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++
     fnl () ++
@@ -387,22 +388,24 @@ let reset_profile () =
 
 (* ******************** *)
 
-let print_results_filter ~filter =
+let print_results_filter ~cutoff ~filter =
   let valid id _ = Stm.state_of_id id <> `Expired in
   data := SM.filter valid !data;
   let results =
     SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in
   let results = merge_roots results Local.(CList.last !stack) in
-  Feedback.msg_notice (to_string ~filter results)
+  Feedback.msg_notice (to_string ~cutoff ~filter results)
 ;;
 
-let print_results () = print_results_filter ~filter:(fun _ -> true)
+let print_results ~cutoff =
+  print_results_filter ~cutoff ~filter:(fun _ -> true)
 
 let print_results_tactic tactic =
-  print_results_filter ~filter:(fun s ->
+  print_results_filter ~cutoff:0.0 ~filter:(fun s ->
     String.(equal tactic (sub (s ^ ".") 0 (min (1+length s) (length tactic)))))
 
-let do_print_results_at_close () = if get_profiling () then print_results ()
+let do_print_results_at_close () =
+  if get_profiling () then print_results ~cutoff:0.0
 
 let _ = Declaremods.append_end_library_hook do_print_results_at_close
 
diff --git a/ltac/profile_ltac.mli b/ltac/profile_ltac.mli
index 8c4b47b8e..e5e2e4197 100644
--- a/ltac/profile_ltac.mli
+++ b/ltac/profile_ltac.mli
@@ -14,7 +14,8 @@ val do_profile :
 
 val set_profiling : bool -> unit
 
-val print_results : unit -> unit
+(* Cut off results < than specified cutoff *)
+val print_results : cutoff:float -> unit
 
 val print_results_tactic : string -> unit
 
diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4
index c092a0cb6..9083bda60 100644
--- a/ltac/profile_ltac_tactics.ml4
+++ b/ltac/profile_ltac_tactics.ml4
@@ -31,7 +31,8 @@ VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF
 END
 
 VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY
-  [ "Show" "Ltac" "Profile" ] -> [ print_results() ]
+| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:0.0 ]
+| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> [ print_results ~cutoff:(float_of_int n) ]
 END
 
 VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY