Merge PR coq#18293: Guard profiling with a flag in Ltac2.

Reviewed-by: ppedrot Reviewed-by: JasonGross Ack-by: SkySkimmer Co-authored-by: ppedrot <[email protected]>
SkySkimmer · Dec 4, 2023 · 89a5cee · 89a5cee
2 parents 5ccfab3 + 84d209b
commit 89a5cee
Show file tree

Hide file tree

Showing 4 changed files with 35 additions and 10 deletions.
diff --git a/doc/changelog/06-Ltac2-language/18293-br-ltac2-profiling.rst b/doc/changelog/06-Ltac2-language/18293-br-ltac2-profiling.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  A new flag :flag:`Ltac2 In Ltac1 Profiling` (unset by default) to control
+  whether Ltac2 stack frames are included in Ltac profiles
+  (`#18293 <https://github.com/coq/coq/pull/18293>`_,
+  by Rodolphe Lepigre).
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
@@ -1751,6 +1751,14 @@ Debug
 
    When this :term:`flag` is set, toplevel failures will be printed with a backtrace.
 
+Profiling
+---------
+
+.. flag:: Ltac2 In Ltac1 Profiling
+
+   When this :term:`flag` and :flag:`Ltac Profiling` are set, profiling data is gathered for Ltac2 via the
+   Ltac profiler. It is unset by default.
+
 Compatibility layer with Ltac1
 ------------------------------
 

diff --git a/plugins/ltac2/tac2bt.ml b/plugins/ltac2/tac2bt.ml
@@ -17,6 +17,24 @@ let backtrace : backtrace Exninfo.t = Exninfo.make ()
 
 let print_ltac2_backtrace = ref false
 
+let () = Goptions.declare_bool_option {
+  Goptions.optstage = Summary.Stage.Interp;
+  Goptions.optdepr = None;
+  Goptions.optkey = ["Ltac2"; "Backtrace"];
+  Goptions.optread = (fun () -> !print_ltac2_backtrace);
+  Goptions.optwrite = (fun b -> print_ltac2_backtrace := b);
+}
+
+let ltac2_in_ltac1_profiling = ref false
+
+let () = Goptions.declare_bool_option {
+  Goptions.optstage = Summary.Stage.Interp;
+  Goptions.optdepr = None;
+  Goptions.optkey = ["Ltac2"; "In"; "Ltac1"; "Profiling"];
+  Goptions.optread = (fun () -> !ltac2_in_ltac1_profiling);
+  Goptions.optwrite = (fun b -> ltac2_in_ltac1_profiling := b);
+}
+
 let get_backtrace =
   Proofview.tclEVARMAP >>= fun sigma ->
   match Evd.Store.get (Evd.get_extra_data sigma) backtrace_evd with
@@ -48,5 +66,7 @@ let with_frame frame tac =
       Proofview.tclUNIT ans
     else tac
   in
-  let pr_frame f = Some (Hook.get pr_frame f) in
-  Ltac_plugin.Profile_ltac.do_profile_gen pr_frame frame ~count_call:true tac
+  if !ltac2_in_ltac1_profiling then
+    let pr_frame f = Some (Hook.get pr_frame f) in
+    Ltac_plugin.Profile_ltac.do_profile_gen pr_frame frame ~count_call:true tac
+  else tac
diff --git a/plugins/ltac2/tac2entries.ml b/plugins/ltac2/tac2entries.ml
@@ -965,14 +965,6 @@ let register_struct atts str = match str with
 
 (** Toplevel exception *)
 
-let () = Goptions.declare_bool_option {
-  Goptions.optstage = Summary.Stage.Interp;
-  Goptions.optdepr = None;
-  Goptions.optkey = ["Ltac2"; "Backtrace"];
-  Goptions.optread = (fun () -> !Tac2bt.print_ltac2_backtrace);
-  Goptions.optwrite = (fun b -> Tac2bt.print_ltac2_backtrace := b);
-}
-
 let pr_frame = function
 | FrAnon e -> str "Call {" ++ pr_glbexpr ~avoid:Id.Set.empty e ++ str "}"
 | FrLtac kn ->