-profile-ltac-cutoff alike Show Ltac Profile Cutoff (#5100)

With this command line flag one can profile ltac in files
/and/ trim the results without actually touching the files.

5 files changed, 6 insertions, 3 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index 13525165ab..d29064c97f 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -226,6 +226,7 @@ let print_mod_uid = ref false
 
 let tactic_context_compat = ref false
 let profile_ltac = ref false
+let profile_ltac_cutoff = ref 0.0
 
 let dump_bytecode = ref false
 let set_dump_bytecode = (:=) dump_bytecode
diff --git a/lib/flags.mli b/lib/flags.mli
index 8fe64d24fa..839c252cbb 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -149,6 +149,7 @@ val tactic_context_compat : bool ref
     context vs. appcontext) is set. *)
 
 val profile_ltac : bool ref
+val profile_ltac_cutoff : float ref
 
 (** Dump the bytecode after compilation (for debugging purposes) *)
 val dump_bytecode : bool ref
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
index 102918e5e5..a91ff98fb9 100644
--- a/ltac/profile_ltac.ml
+++ b/ltac/profile_ltac.ml
@@ -401,11 +401,11 @@ let print_results ~cutoff =
   print_results_filter ~cutoff ~filter:(fun _ -> true)
 
 let print_results_tactic tactic =
-  print_results_filter ~cutoff:0.0 ~filter:(fun s ->
+  print_results_filter ~cutoff:!Flags.profile_ltac_cutoff ~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 ~cutoff:0.0
+  if get_profiling () then print_results ~cutoff:!Flags.profile_ltac_cutoff
 
 let _ = Declaremods.append_end_library_hook do_print_results_at_close
 
diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4
index 9083bda60a..8cb76d81c5 100644
--- a/ltac/profile_ltac_tactics.ml4
+++ b/ltac/profile_ltac_tactics.ml4
@@ -31,7 +31,7 @@ VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF
 END
 
 VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY
-| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:0.0 ]
+| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:!Flags.profile_ltac_cutoff ]
 | [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> [ print_results ~cutoff:(float_of_int n) ]
 END
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index ee331e37c7..47d433d790 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -523,6 +523,7 @@ let parse_args arglist =
     |"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular true (next ())
     |"-outputstate" -> set_outputstate (next ())
     |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0
+    |"-profile-ltac-cutoff" -> Flags.profile_ltac := true; Flags.profile_ltac_cutoff := get_float opt (next ())
     |"-require" -> add_require (next ())
     |"-top" -> set_toplevel_name (dirpath_of_string (next ()))
     |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ())