From 90d79c5656c394909ffc9343b903dd1231abd7a4 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Mon, 11 Dec 2017 05:21:05 -0500
Subject: Add named timers to LtacProf

I'm not sure if they belong in profile_ltac, or in extratactics, or,
perhaps, in a separate plugin.  But I'd find it very useful to have a
version of `time` that works on constr evaluation, which is what this
commit provides.

I'm not sure that I've picked good naming conventions for the tactics,
either.
---
 plugins/ltac/profile_ltac.ml          | 21 +++++++++++++++++++++
 plugins/ltac/profile_ltac.mli         |  5 ++++-
 plugins/ltac/profile_ltac_tactics.ml4 | 15 +++++++++++++++
 theories/Init/Tactics.v               |  7 +++++++
 4 files changed, 47 insertions(+), 1 deletion(-)

diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 5225420dc..97f43eaa8 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -397,6 +397,27 @@ let reset_profile () =
   reset_profile_tmp ();
   data := SM.empty
 
+(* ****************************** Named timers ****************************** *)
+
+let timer_data = ref M.empty
+
+let timer_name = function
+  | Some v -> v
+  | None -> ""
+
+let restart_timer name =
+  timer_data := M.add (timer_name name) (System.get_time ()) !timer_data
+
+let get_timer name =
+  try M.find (timer_name name) !timer_data
+  with Not_found -> System.get_time ()
+
+let finish_timing ~prefix name =
+  let tend = System.get_time () in
+  let tstart = get_timer name in
+  Feedback.msg_info(str prefix ++ pr_opt str name ++ str " ran for " ++
+                    System.fmt_time_difference tstart tend)
+
 (* ******************** *)
 
 let print_results_filter ~cutoff ~filter =
diff --git a/plugins/ltac/profile_ltac.mli b/plugins/ltac/profile_ltac.mli
index 52827cb36..07990c750 100644
--- a/plugins/ltac/profile_ltac.mli
+++ b/plugins/ltac/profile_ltac.mli
@@ -22,6 +22,10 @@ val print_results_tactic : string -> unit
 
 val reset_profile : unit -> unit
 
+val restart_timer : string option -> unit
+
+val finish_timing : prefix:string -> string option -> unit
+
 val do_print_results_at_close : unit -> unit
 
 (* The collected statistics for a tactic. The timing data is collected over all
@@ -46,4 +50,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/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4
index 58e3a3a57..9864ffeb6 100644
--- a/plugins/ltac/profile_ltac_tactics.ml4
+++ b/plugins/ltac/profile_ltac_tactics.ml4
@@ -27,6 +27,12 @@ let tclSHOW_PROFILE ~cutoff =
 let tclSHOW_PROFILE_TACTIC s =
    Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> print_results_tactic s))
 
+let tclRESTART_TIMER s =
+   Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> restart_timer s))
+
+let tclFINISH_TIMING ?(prefix="Timer") (s : string option) =
+   Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> finish_timing ~prefix s))
+
 TACTIC EXTEND start_ltac_profiling
 | [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ]
 END
@@ -45,6 +51,15 @@ TACTIC EXTEND show_ltac_profile
 | [ "show" "ltac" "profile" string(s) ] -> [ tclSHOW_PROFILE_TACTIC s ]
 END
 
+TACTIC EXTEND restart_timer
+| [ "restart_timer" string_opt(s) ] -> [ tclRESTART_TIMER s ]
+END
+
+TACTIC EXTEND finish_timing
+| [ "finish_timing" string_opt(s) ] -> [ tclFINISH_TIMING ~prefix:"Timer" s ]
+| [ "finish_timing" "(" string(prefix) ")" string_opt(s) ] -> [ tclFINISH_TIMING ~prefix s ]
+END
+
 VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF
   [ "Reset" "Ltac" "Profile" ] -> [ reset_profile () ]
 END
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 5d0e7602a..47a971ef0 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -306,3 +306,10 @@ Ltac inversion_sigma_step :=
     => induction_sigma_in_using H @eq_sigT2_rect
   end.
 Ltac inversion_sigma := repeat inversion_sigma_step.
+
+(** A version of [time] that works for constrs *)
+Ltac time_constr tac :=
+  let eval_early := match goal with _ => restart_timer end in
+  let ret := tac () in
+  let eval_early := match goal with _ => finish_timing ( "Tactic evaluation" ) end in
+  ret.
-- 
cgit v1.2.3