From 206e8adedae1b0c479a2cb598510163f909f1a5f Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 29 Apr 2020 12:35:58 -0400
Subject: Decrease LtacProf overhead when not profiling

Note that this slightly changes the semantics of backtracking across
`start ltac profiling`.
---
 plugins/ltac/profile_ltac.ml | 47 +++++++++++++++++++++++++-------------------
 1 file changed, 27 insertions(+), 20 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index c89ecb89bd..44cb531e51 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -331,26 +331,33 @@ let exit_tactic ~count_call start_time c =
     end
 
 let do_profile s call_trace ?(count_call=true) 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 ())
+  let open Proofview.Notations in
+  (* We do an early check to [is_profiling] so that we save the
+     overhead of [Proofview.tclWRAPFINALLY] when profiling is not set
+     *)
+  Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> !is_profiling)) >>= function
+  | false -> tac
+  | true ->
+    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 ************************* *)
 
-- 
cgit v1.2.3