LtacProf now handles multi-success backtracking

Fixes #12196

1 files changed, 40 insertions, 52 deletions

diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 14fab251d0..c89ecb89bd 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -25,27 +25,20 @@ let is_profiling = Flags.profile_ltac
 let set_profiling b = is_profiling := b
 let get_profiling () = !is_profiling
 
-(** LtacProf cannot yet handle backtracking into multi-success tactics.
-    To properly support this, we'd have to somehow recreate our location in the
-    call-stack, and stop/restart the intervening timers. This is tricky and
-    possibly expensive, so instead we currently just emit a warning that
-    profiling results will be off. *)
-let encountered_multi_success_backtracking = ref false
-
-let warn_profile_backtracking =
-  CWarnings.create ~name:"profile-backtracking" ~category:"ltac"
-    (fun () -> strbrk "Ltac Profiler cannot yet handle backtracking \
-       into multi-success tactics; profiling results may be wildly inaccurate.")
-
-let warn_encountered_multi_success_backtracking () =
-  if !encountered_multi_success_backtracking then
-    warn_profile_backtracking ()
-
-let encounter_multi_success_backtracking () =
-  if not !encountered_multi_success_backtracking
+let encountered_invalid_stack_no_self = ref false
+
+let warn_invalid_stack_no_self =
+  CWarnings.create ~name:"profile-invalid-stack-no-self" ~category:"ltac"
+    (fun () -> strbrk
+        "Ltac Profiler encountered an invalid stack (no self \
+         node). This can happen if you reset the profile during \
+         tactic execution.")
+
+let encounter_invalid_stack_no_self () =
+  if not !encountered_invalid_stack_no_self
   then begin
-    encountered_multi_success_backtracking := true;
-    warn_encountered_multi_success_backtracking ()
+    encountered_invalid_stack_no_self := true;
+    warn_invalid_stack_no_self ()
   end
 
 
@@ -76,8 +69,7 @@ module Local = Summary.Local
 let stack = Local.ref ~name:"LtacProf-stack" [empty_treenode root]
 
 let reset_profile_tmp () =
-  Local.(stack := [empty_treenode root]);
-  encountered_multi_success_backtracking := false
+  Local.(stack := [empty_treenode root])
 
 (* ************** XML Serialization  ********************* *)
 
@@ -218,7 +210,6 @@ let to_string ~filter ?(cutoff=0.0) node =
     cumulate tree;
     !global
   in
-  warn_encountered_multi_success_backtracking ();
   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))) ++
@@ -296,13 +287,15 @@ let exit_tactic ~count_call start_time c =
   match Local.(!stack) with
   | [] | [_] ->
     (* oops, our stack is invalid *)
-    encounter_multi_success_backtracking ();
+    encounter_invalid_stack_no_self ();
     reset_profile_tmp ()
   | node :: (parent :: rest as full_stack) ->
     let name = string_of_call c in
     if not (String.equal name node.name) then
       (* oops, our stack is invalid *)
-      encounter_multi_success_backtracking ();
+      CErrors.anomaly
+        (Pp.strbrk "Ltac Profiler encountered an invalid stack (wrong self node) \
+                    likely due to backtracking into multi-success tactics.");
     let node = { node with
       total = node.total +. diff;
       local = node.local +. diff;
@@ -332,38 +325,32 @@ let exit_tactic ~count_call start_time c =
     (* Calls are over, we reset the stack and send back data *)
     if rest == [] && get_profiling () then begin
       assert(String.equal root parent.name);
+      encountered_invalid_stack_no_self := false;
       reset_profile_tmp ();
       feedback_results parent
     end
 
-let tclFINALLY tac (finally : unit Proofview.tactic) =
-  let open Proofview.Notations in
-  Proofview.tclIFCATCH
-    tac
-    (fun v -> finally <*> Proofview.tclUNIT v)
-    (fun (exn, info) -> finally <*> Proofview.tclZERO ~info exn)
-
 let do_profile s call_trace ?(count_call=true) tac =
-  let open Proofview.Notations in
-  Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
-  if !is_profiling then
-    match call_trace, Local.(!stack) with
-      | (_, c) :: _, parent :: rest ->
-        let name = string_of_call c in
-        let node = get_child name parent in
-        Local.(stack := node :: parent :: rest);
-        Some (time ())
-      | _ :: _, [] -> assert false
-      | _ -> None
-  else None)) >>= function
-  | Some start_time ->
-    tclFINALLY
-      tac
-      (Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
-        (match call_trace with
-        | (_, c) :: _ -> exit_tactic ~count_call start_time c
-        | [] -> ()))))
-  | None -> tac
+  Proofview.tclWRAPFINALLY
+    (Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
+         if !is_profiling then
+           match call_trace, Local.(!stack) with
+           | (_, c) :: _, parent :: rest ->
+             let name = string_of_call c in
+             let node = get_child name parent in
+             Local.(stack := node :: parent :: rest);
+             Some (time ())
+           | _ :: _, [] -> assert false
+           | _ -> None
+         else None)))
+    tac
+    (function
+      | Some start_time ->
+        (Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
+             (match call_trace with
+              | (_, c) :: _ -> exit_tactic ~count_call start_time c
+              | [] -> ()))))
+      | None -> Proofview.tclUNIT ())
 
 (* ************** Accumulation of data from workers ************************* *)
 
@@ -396,6 +383,7 @@ let _ =
     | _ -> ()))
 
 let reset_profile () =
+  encountered_invalid_stack_no_self := false;
   reset_profile_tmp ();
   data := SM.empty