diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-12-11 05:21:05 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-12-14 12:19:02 -0500 |
| commit | 90d79c5656c394909ffc9343b903dd1231abd7a4 (patch) | |
| tree | 0aec14a5e6547173a47482a3e4d10780828a905d /plugins/ltac/profile_ltac.mli | |
| parent | 6734614d8ace6860e3deb1861611ba4b012cfae1 (diff) | |
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.
Diffstat (limited to 'plugins/ltac/profile_ltac.mli')
| -rw-r--r-- | plugins/ltac/profile_ltac.mli | 5 |
1 files changed, 4 insertions, 1 deletions
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 - |