1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Unicode
open Pp
open Printer
open Util
(** [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. We synchronize
is_profiling via an option. *)
let is_profiling = Flags.profile_ltac
let set_profiling b = is_profiling := b
let get_profiling () = !is_profiling
let new_call = ref false
let entered_call () = new_call := true
let is_new_call () = let b = !new_call in new_call := false; b
(** LtacProf cannot yet handle backtracking into multi-success tactics.
To properly support this, we'd have to somehow recreate our location in the
call-stack, and stop/restart the intervening timers. This is tricky and
possibly expensive, so instead we currently just emit a warning that
profiling results will be off. *)
let encountered_multi_success_backtracking = ref false
let warn_profile_backtracking =
CWarnings.create ~name:"profile-backtracking" ~category:"ltac"
(fun () -> strbrk "Ltac Profiler cannot yet handle backtracking \
into multi-success tactics; profiling results may be wildly inaccurate.")
let warn_encountered_multi_success_backtracking () =
if !encountered_multi_success_backtracking then
warn_profile_backtracking ()
let encounter_multi_success_backtracking () =
if not !encountered_multi_success_backtracking
then begin
encountered_multi_success_backtracking := true;
warn_encountered_multi_success_backtracking ()
end
type entry = {
mutable total : float;
mutable local : float;
mutable ncalls : int;
mutable max_total : float
}
let empty_entry () = { total = 0.; local = 0.; ncalls = 0; max_total = 0. }
let add_entry e add_total { total; local; ncalls; max_total } =
if add_total then e.total <- e.total +. total;
e.local <- e.local +. local;
e.ncalls <- e.ncalls + ncalls;
if add_total then e.max_total <- max e.max_total max_total
type treenode = {
entry : entry;
children : (string, treenode) Hashtbl.t
}
let empty_treenode n = { entry = empty_entry (); children = Hashtbl.create n }
(** 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. *)
(** TODO: rewrite me in purely functional style *)
let deepcopy_entry { total; local; ncalls; max_total } =
{ total; local; ncalls; max_total }
let rec deepcopy_treenode { entry; children } =
let children' = Hashtbl.create (Hashtbl.length children) in
let iter key subtree = Hashtbl.add children' key (deepcopy_treenode subtree) in
let () = Hashtbl.iter iter children in
{ entry = deepcopy_entry entry; children = children' }
let stack =
let freeze _ = List.map deepcopy_treenode in
Summary.ref ~freeze [empty_treenode 20] ~name:"LtacProf-stack"
let on_stack = Hashtbl.create 5
let get_node c table =
try Hashtbl.find table c
with Not_found ->
let new_node = empty_treenode 5 in
Hashtbl.add table c new_node;
new_node
let rec add_node node node' =
add_entry node.entry true node'.entry;
Hashtbl.iter
(fun s node' -> add_node (get_node s node.children) node')
node'.children
let time () =
let times = Unix.times () in
times.Unix.tms_utime +. times.Unix.tms_stime
(*
let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ())
let msgnl strm = msgnl_with !Pp_control.std_ft strm
let rec print_treenode indent (tn : treenode) =
msgnl (str (indent^"{ entry = {"));
Feedback.msg_notice (str (indent^"total = "));
msgnl (str (indent^(string_of_float (tn.entry.total))));
Feedback.msg_notice (str (indent^"local = "));
msgnl (str (indent^(string_of_float tn.entry.local)));
Feedback.msg_notice (str (indent^"ncalls = "));
msgnl (str (indent^(string_of_int tn.entry.ncalls)));
Feedback.msg_notice (str (indent^"max_total = "));
msgnl (str (indent^(string_of_float tn.entry.max_total)));
msgnl (str (indent^"}"));
msgnl (str (indent^"children = {"));
Hashtbl.iter
(fun s node ->
msgnl (str (indent^" "^s^" |-> "));
print_treenode (indent^" ") node
)
tn.children;
msgnl (str (indent^"} }"))
let rec print_stack (st : treenode list) = match st with
| [] -> msgnl (str "[]")
| x :: xs -> print_treenode "" x; msgnl (str ("::")); print_stack xs
*)
let string_of_call ck =
let s =
string_of_ppcmds
(match ck with
| Tacexpr.LtacNotationCall s -> Pptactic.pr_alias_key s
| Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst
| Tacexpr.LtacVarCall (id, t) -> Nameops.pr_id id
| Tacexpr.LtacAtomCall te ->
(Pptactic.pr_glob_tactic (Global.env ())
(Tacexpr.TacAtom (Loc.ghost, te)))
| Tacexpr.LtacConstrInterp (c, _) ->
pr_glob_constr_env (Global.env ()) c
| Tacexpr.LtacMLCall te ->
(Pptactic.pr_glob_tactic (Global.env ())
te)
) in
for i = 0 to String.length s - 1 do if s.[i] = '\n' then s.[i] <- ' ' done;
let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in
CString.strip s
let exit_tactic start_time add_total c = match !stack with
| [] | [_] ->
(* oops, our stack is invalid *)
encounter_multi_success_backtracking ()
| node :: (parent :: _ as stack') ->
stack := stack';
if add_total then Hashtbl.remove on_stack (string_of_call c);
let diff = time () -. start_time in
parent.entry.local <- parent.entry.local -. diff;
let node' = { total = diff; local = diff; ncalls = 1; max_total = diff } in
add_entry node.entry add_total node'
let tclFINALLY tac (finally : unit Proofview.tactic) =
let open Proofview.Notations in
Proofview.tclIFCATCH
tac
(fun v -> finally <*> Proofview.tclUNIT v)
(fun (exn, info) -> finally <*> Proofview.tclZERO ~info exn)
let do_profile s call_trace tac =
let open Proofview.Notations in
Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
if !is_profiling && is_new_call () then
match call_trace with
| (_, c) :: _ ->
let s = string_of_call c in
let parent = List.hd !stack in
let node, add_total = try Hashtbl.find on_stack s, false
with Not_found ->
let node = get_node s parent.children in
Hashtbl.add on_stack s node;
node, true
in
if not add_total && node = List.hd !stack then None else (
stack := node :: !stack;
let start_time = time () in
Some (start_time, add_total)
)
| [] -> None
else None)) >>= function
| Some (start_time, add_total) ->
tclFINALLY
tac
(Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
(match call_trace with
| (_, c) :: _ ->
exit_tactic start_time add_total c
| [] -> ()))))
| None -> tac
let format_sec x = (Printf.sprintf "%.3fs" x)
let format_ratio x = (Printf.sprintf "%.1f%%" (100. *. x))
let padl n s = ws (max 0 (n - utf8_length s)) ++ str s
let padr n s = str s ++ ws (max 0 (n - utf8_length s))
let padr_with c n s =
let ulength = utf8_length s in
str (utf8_sub s 0 n) ++ str (String.make (max 0 (n - ulength)) c)
let rec list_iter_is_last f = function
| [] -> []
| [x] -> [f true x]
| x :: xs -> f false x :: list_iter_is_last f xs
let header =
str " tactic self total calls max" ++
fnl () ++
str "────────────────────────────────────────┴──────┴──────┴───────┴─────────┘" ++
fnl ()
let rec print_node all_total indent prefix (s, n) =
let e = n.entry in
h 0 (
padr_with '-' 40 (prefix ^ s ^ " ")
++ padl 7 (format_ratio (e.local /. all_total))
++ padl 7 (format_ratio (e.total /. all_total))
++ padl 8 (string_of_int e.ncalls)
++ padl 10 (format_sec (e.max_total))
) ++
fnl () ++
print_table all_total indent false n.children
and print_table all_total indent first_level table =
let fold s n l = if n.entry.total /. all_total < 0.02 then l else (s, n) :: l in
let ls = Hashtbl.fold fold table [] in
match ls with
| [s, n] when not first_level ->
print_node all_total indent (indent ^ "└") (s, n)
| _ ->
let ls = List.sort (fun (_, n1) (_, n2) -> compare n2.entry.total n1.entry.total) ls in
let iter is_last =
let sep0 = if first_level then "" else if is_last then " " else " │" in
let sep1 = if first_level then "─" else if is_last then " └─" else " ├─" in
print_node all_total (indent ^ sep0) (indent ^ sep1)
in
prlist_with_sep fnl (fun pr -> pr) (list_iter_is_last iter ls)
let get_results_string () =
let tree = (List.hd !stack).children in
let all_total = -. (List.hd !stack).entry.local in
let global = Hashtbl.create 20 in
let rec cumulate table =
let iter s node =
let node' = get_node s global in
add_entry node'.entry true node.entry;
cumulate node.children
in
Hashtbl.iter iter table
in
cumulate tree;
warn_encountered_multi_success_backtracking ();
let msg =
h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++
fnl () ++
header ++
print_table all_total "" true global ++
fnl () ++
header ++
print_table all_total "" true tree
in
msg
type ltacprof_entry = {total : float; self : float; num_calls : int; max_total : float}
type ltacprof_tactic = {name: string; statistics : ltacprof_entry; tactics : ltacprof_tactic list}
type ltacprof_results = {total_time : float; tactics : ltacprof_tactic list}
let to_ltacprof_entry (e: entry) : ltacprof_entry =
{total=e.total; self=e.local; num_calls=e.ncalls; max_total=e.max_total}
let rec to_ltacprof_tactic (name: string) (t: treenode) : ltacprof_tactic =
{ name = name; statistics = to_ltacprof_entry t.entry; tactics = to_ltacprof_treenode t.children }
and to_ltacprof_treenode (table: (string, treenode) Hashtbl.t) : ltacprof_tactic list =
Hashtbl.fold (fun name' t' c -> to_ltacprof_tactic name' t'::c) table []
let get_profiling_results() : ltacprof_results =
let tree = List.hd !stack in
{ total_time = -. tree.entry.local; tactics = to_ltacprof_treenode tree.children }
let rec of_ltacprof_tactic t =
let open Xml_datatype in
let total = string_of_float t.statistics.total in
let self = string_of_float t.statistics.self in
let num_calls = string_of_int t.statistics.num_calls in
let max_total = string_of_float t.statistics.max_total in
let children = List.map of_ltacprof_tactic t.tactics in
Element ("ltacprof_tactic", [("name", t.name); ("total",total); ("self",self); ("num_calls",num_calls); ("max_total",max_total)], children)
let rec of_ltacprof_results t =
let open Xml_datatype in
let children = List.map of_ltacprof_tactic t.tactics in
Element ("ltacprof", [("total_time", string_of_float t.total_time)], children)
let get_profile_xml() =
of_ltacprof_results (get_profiling_results())
let print_results () =
Feedback.msg_notice (get_results_string());
Feedback.feedback (Feedback.Custom (Loc.dummy_loc, "ltacprof_results", get_profile_xml()))
(* FOR DEBUGGING *)
(* ;
msgnl (str"");
print_stack (!stack)
*)
let print_results_tactic tactic =
let tree = (List.hd !stack).children in
let table_tactic = Hashtbl.create 20 in
let rec cumulate table =
let iter s node =
if String.sub (s ^ ".") 0 (min (1 + String.length s) (String.length tactic)) = tactic
then add_node (get_node s table_tactic) node
else cumulate node.children
in
Hashtbl.iter iter table
in
cumulate tree;
let all_total = -. (List.hd !stack).entry.local in
let tactic_total =
Hashtbl.fold
(fun _ node all_total -> node.entry.total +. all_total)
table_tactic 0. in
warn_encountered_multi_success_backtracking ();
let msg =
h 0 (str"total time: " ++ padl 11 (format_sec (all_total))) ++
h 0 (str"time spent in tactic: " ++ padl 11 (format_sec (tactic_total))) ++
fnl () ++
header ++
print_table tactic_total "" true table_tactic
in
Feedback.msg_notice msg
let reset_profile () =
stack := [empty_treenode 20];
encountered_multi_success_backtracking := false
let do_print_results_at_close () = if get_profiling () then print_results ()
let _ = Declaremods.append_end_library_hook do_print_results_at_close
let _ =
let open Goptions in
declare_bool_option
{ optsync = true;
optdepr = false;
optname = "Ltac Profiling";
optkey = ["Ltac"; "Profiling"];
optread = get_profiling;
optwrite = set_profiling }
|