Merge PR #6411: Fix #5081 by more fine-grained LtacProf recording

3 files changed, 39 insertions, 8 deletions

diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 5225420dc..5e3b7cf77 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -289,7 +289,7 @@ let rec find_in_stack what acc = function
   | { name } as x :: rest when String.equal name what -> Some(acc, x, rest)
   | { name } as x :: rest -> find_in_stack what (x :: acc) rest
 
-let exit_tactic start_time c =
+let exit_tactic ~count_call start_time c =
   let diff = time () -. start_time in
   match Local.(!stack) with
   | [] | [_] ->
@@ -304,7 +304,7 @@ let exit_tactic start_time c =
     let node = { node with
       total = node.total +. diff;
       local = node.local +. diff;
-      ncalls = node.ncalls + 1;
+      ncalls = node.ncalls + (if count_call then 1 else 0);
       max_total = max node.max_total diff;
     } in
     (* updating the stack *)
@@ -341,7 +341,7 @@ let tclFINALLY tac (finally : unit Proofview.tactic) =
     (fun v -> finally <*> Proofview.tclUNIT v)
     (fun (exn, info) -> finally <*> Proofview.tclZERO ~info exn)
 
-let do_profile s call_trace tac =
+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
@@ -359,7 +359,7 @@ let do_profile s call_trace tac =
       tac
       (Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
         (match call_trace with
-        | (_, c) :: _ -> exit_tactic start_time c
+        | (_, c) :: _ -> exit_tactic ~count_call start_time c
         | [] -> ()))))
   | None -> tac
 
diff --git a/plugins/ltac/profile_ltac.mli b/plugins/ltac/profile_ltac.mli
index 52827cb36..feb777352 100644
--- a/plugins/ltac/profile_ltac.mli
+++ b/plugins/ltac/profile_ltac.mli
@@ -9,9 +9,39 @@
 
 (** Ltac profiling primitives *)
 
+(* Note(JasonGross): Ltac semantics are a bit insane.  There isn't
+   really a good notion of how many times a tactic has been "called",
+   because tactics can be partially evaluated, and it's unclear
+   whether the number of "calls" should be the number of times the
+   body is fetched and unfolded, or the number of times the code is
+   executed to a value, etc.  The logic in [Tacinterp.eval_tactic]
+   gives a decent approximation, which I believe roughly corresponds
+   to the number of times that the engine runs the tactic value which
+   results from evaluating the tactic expression bound to the name
+   we're considering.  However, this is a poor approximation of the
+   time spent in the tactic; we want to consider time spent evaluating
+   a tactic expression to a tactic value to be time spent in the
+   expression, not just time spent in the caller of the expression.
+   So we need to wrap some nodes in additional profiling calls which
+   don't count towards to total call count.  Whether or not a call
+   "counts" is indicated by the [count_call] boolean argument.
+
+   Unfortunately, at present, we can get very strange call graphs when
+   a named tactic expression never runs as a tactic value: if we have
+   [Ltac t0 := t.] and [Ltac t1 := t0.], then [t1] is considered to
+   run 0(!) times.  It evaluates to [t] during tactic expression
+   evaluation, and although the call trace records the fact that it
+   was called by [t0] which was called by [t1], the tactic running
+   phase never sees this.  Thus we get one call tree (from expression
+   evaluation) that has [t1] calls [t0] calls [t], and another call
+   tree which says that the caller of [t1] calls [t] directly; the
+   expression evaluation time goes in the first tree, and the call
+   count and tactic running time goes in the second tree.  Alas, I
+   suspect that fixing this requires a redesign of how the profiler
+   hooks into the tactic engine. *)
 val do_profile :
   string -> ('a * Tacexpr.ltac_call_kind) list ->
-    'b Proofview.tactic -> 'b Proofview.tactic
+    ?count_call:bool -> 'b Proofview.tactic -> 'b Proofview.tactic
 
 val set_profiling : bool -> unit
 
@@ -46,4 +76,3 @@ type treenode = {
 (* Returns the profiling results known by the current process *)
 val get_local_profiling_results : unit -> treenode
 val feedback_results : treenode -> unit
-
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index ded902a8f..179952f28 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1272,7 +1272,8 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
       let extra = TacStore.set extra f_trace trace in
       let ist = { lfun = Id.Map.empty; extra = extra; } in
       let appl = GlbAppl[r,[]] in
-      val_interp ~appl ist (Tacenv.interp_ltac r)
+      Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false
+        (val_interp ~appl ist (Tacenv.interp_ltac r))
 
 and interp_tacarg ist arg : Val.t Ftactic.t =
   match arg with
@@ -1338,7 +1339,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
               let ist = {
                 lfun = newlfun;
                 extra = TacStore.set ist.extra f_trace []; } in
-              catch_error_tac trace (val_interp ist body) >>= fun v ->
+              Profile_ltac.do_profile "interp_app" trace ~count_call:false
+                (catch_error_tac trace (val_interp ist body)) >>= fun v ->
               Ftactic.return (name_vfun (push_appl appl largs) v)
             end
 	    begin fun (e, info) ->