diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 18:58:21 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 18:58:21 +0100 |
commit | 9266d34a073859f24aa615767a1311d532bba0ac (patch) | |
tree | cda62961092f0162a5ce950a9a6b70ab4a5cd4b2 /plugins/ltac | |
parent | 7e2f9861f3d38829baf246883e4925d48c9e2998 (diff) | |
parent | 4024286d9fdd13e5ec4c474b1dae4ce58ac41683 (diff) |
Merge PR #6381: A version of [time] that works on constr evaluation
Diffstat (limited to 'plugins/ltac')
-rw-r--r-- | plugins/ltac/profile_ltac.ml | 21 | ||||
-rw-r--r-- | plugins/ltac/profile_ltac.mli | 4 | ||||
-rw-r--r-- | plugins/ltac/profile_ltac_tactics.ml4 | 15 |
3 files changed, 40 insertions, 0 deletions
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 5e3b7cf77..161546528 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 feb777352..adedf7ee9 100644 --- a/plugins/ltac/profile_ltac.mli +++ b/plugins/ltac/profile_ltac.mli @@ -52,6 +52,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 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 |