diff options
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 2 | ||||
| -rw-r--r-- | ltac/profile_ltac_tactics.ml4 | 2 | ||||
| -rw-r--r-- | ltacprof/profile_ltac.ml | 19 |
3 files changed, 19 insertions, 4 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 24f4b2a775..608793d04f 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1204,7 +1204,7 @@ It is possible to measure the time spent in invocations of primitive tactics as \begin{quote} {\tt Start Profiling}. \end{quote} -Enables the profiler and resets the profile +Enables the profiler \begin{quote} {\tt Stop Profiling}. diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4 index 0c4e0b0757..ce00c29202 100644 --- a/ltac/profile_ltac_tactics.ml4 +++ b/ltac/profile_ltac_tactics.ml4 @@ -19,7 +19,7 @@ END;; VERNAC COMMAND EXTEND StartProfiling CLASSIFIED AS SIDEFF - [ "Start" "Profiling" ] -> [ reset_profile(); set_profiling true ] + [ "Start" "Profiling" ] -> [ set_profiling true ] END VERNAC COMMAND EXTEND StopProfiling CLASSIFIED AS SIDEFF diff --git a/ltacprof/profile_ltac.ml b/ltacprof/profile_ltac.ml index 71b96614ce..6ae07689dd 100644 --- a/ltacprof/profile_ltac.ml +++ b/ltacprof/profile_ltac.ml @@ -3,7 +3,8 @@ open Printer open Util -let is_profiling = ref false +(** [is_profiling] and the profiling info ([stack]) should be synchronized with the document; the rest of the ref cells are either local to individual tactic invocations, or global flags, and need not be synchronized, since no document-level backtracking happens within tactics. *) +let is_profiling = Summary.ref false ~name:"is-profiling-ltac" let set_profiling b = is_profiling := b let should_display_profile_at_close = ref false @@ -40,7 +41,21 @@ let add_entry e add_total {total; local; ncalls; max_total} = if add_total then e.max_total <- max e.max_total max_total type treenode = {entry : entry; children : (string, treenode) Hashtbl.t} -let stack = ref [{entry=empty_entry(); children=Hashtbl.create 20}] + +(** Tobias Tebbi wrote some tricky code involving mutation. Rather than rewriting it in a functional style, we simply freeze the state when we need to by issuing a deep copy of the profiling data. *) +let deepcopy_entry {total; local; ncalls; max_total} = + {total; local; ncalls; max_total} + +let rec deepcopy_treenode {entry; children} = + {entry = deepcopy_entry entry; + children = + (let children' = Hashtbl.create (Hashtbl.length children) in + Hashtbl.iter + (fun key subtree -> Hashtbl.add children' key (deepcopy_treenode subtree)) + children; + children')} + +let stack = Summary.ref ~freeze:(fun _ -> List.map deepcopy_treenode) [{entry=empty_entry(); children=Hashtbl.create 20}] ~name:"LtacProf-stack" let on_stack = Hashtbl.create 5 |