Source file profile_ltac.ml
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
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
open Unicode
open Pp
open Printer
open Util
module M = CString.Map
(** [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 encountered_invalid_stack_no_self = ref false
let warn_invalid_stack_no_self =
CWarnings.create ~name:"profile-invalid-stack-no-self" ~category:CWarnings.CoreCategories.ltac
(fun () -> strbrk
"Ltac Profiler encountered an invalid stack (no self \
node). This can happen if you reset the profile during \
tactic execution.")
let encounter_invalid_stack_no_self () =
if not !encountered_invalid_stack_no_self
then begin
encountered_invalid_stack_no_self := true;
warn_invalid_stack_no_self ()
end
type treenode = {
name : string;
total : float;
local : float;
ncalls : int;
max_total : float;
children : treenode M.t
}
let empty_treenode name = {
name;
total = 0.0;
local = 0.0;
ncalls = 0;
max_total = 0.0;
children = M.empty;
}
let root = "root"
let stack = Summary.ref ~name:"LtacProf-stack" ~local:true [empty_treenode root]
let reset_profile_tmp () = stack := [empty_treenode root]
let rec of_ltacprof_tactic (name, t) =
assert (String.equal name t.name);
let open Xml_datatype in
let total = string_of_float t.total in
let local = string_of_float t.local in
let ncalls = string_of_int t.ncalls in
let max_total = string_of_float t.max_total in
let children = List.map of_ltacprof_tactic (M.bindings t.children) in
Element ("ltacprof_tactic",
[ ("name", name); ("total",total); ("local",local);
("ncalls",ncalls); ("max_total",max_total)],
children)
let of_ltacprof_results t =
let open Xml_datatype in
assert(String.equal t.name root);
let children = List.map of_ltacprof_tactic (M.bindings t.children) in
Element ("ltacprof", [("total_time", string_of_float t.total)], children)
let rec to_ltacprof_tactic m xml =
let open Xml_datatype in
match xml with
| Element ("ltacprof_tactic",
[("name", name); ("total",total); ("local",local);
("ncalls",ncalls); ("max_total",max_total)], xs) ->
let node = {
name;
total = float_of_string total;
local = float_of_string local;
ncalls = int_of_string ncalls;
max_total = float_of_string max_total;
children = List.fold_left to_ltacprof_tactic M.empty xs;
} in
M.add name node m
| _ -> CErrors.anomaly Pp.(str "Malformed ltacprof_tactic XML.")
let to_ltacprof_results xml =
let open Xml_datatype in
match xml with
| Element ("ltacprof", [("total_time", t)], xs) ->
{ name = root;
total = float_of_string t;
ncalls = 0;
max_total = 0.0;
local = 0.0;
children = List.fold_left to_ltacprof_tactic M.empty xs }
| _ -> CErrors.anomaly Pp.(str "Malformed ltacprof XML.")
let feedback_results results =
Feedback.(feedback
(Custom (None, "ltacprof_results", of_ltacprof_results results)))
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_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 =
str " tactic local total calls max " ++
fnl () ++
str "────────────────────────────────────────┴──────┴──────┴───────┴─────────┘" ++
fnl ()
let rec print_node ~filter all_total indent prefix (s, e) =
h (
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 ~filter all_total indent false e.children
and print_table ~filter all_total indent first_level table =
let fold _ n l =
let s, total = n.name, n.total in
if filter s total then (s, n) :: l else l in
let ls = M.fold fold table [] in
match ls with
| [s, n] when not first_level ->
v 0 (print_node ~filter all_total indent (indent ^ "└") (s, n))
| _ ->
let ls =
List.sort (fun (_, { total = s1 }) (_, { total = s2}) ->
compare s2 s1) 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 ~filter all_total (indent ^ sep0) (indent ^ sep1)
in
prlist (fun pr -> pr) (list_iter_is_last iter ls)
let to_string ~filter ~cutoff node =
let tree = node.children in
let all_total = M.fold (fun _ { total } a -> total +. a) node.children 0.0 in
let flat_tree =
let global = ref M.empty in
let find_tactic tname l =
try M.find tname !global
with Not_found ->
let e = empty_treenode tname in
global := M.add tname e !global;
e in
let add_tactic tname stats = global := M.add tname stats !global in
let sum_stats add_total
{ name; total = t1; local = l1; ncalls = n1; max_total = m1 }
{ total = t2; local = l2; ncalls = n2; max_total = m2 } = {
name;
total = if add_total then t1 +. t2 else t1;
local = l1 +. l2;
ncalls = n1 + n2;
max_total = if add_total then max m1 m2 else m1;
children = M.empty;
} in
let rec cumulate table =
let iter _ ({ name; children } as statistics) =
if filter name then begin
let stats' = find_tactic name global in
add_tactic name (sum_stats true stats' statistics);
end;
cumulate children
in
M.iter iter table
in
cumulate tree;
!global
in
let filter s n = filter s && (all_total <= 0.0 || n /. all_total >= cutoff /. 100.0) in
let msg =
h (str "total time: " ++ padl 11 (format_sec (all_total))) ++
fnl () ++
fnl () ++
header ++
print_table ~filter all_total "" true flat_tree ++
fnl () ++
header ++
print_table ~filter all_total "" true tree
in
msg
let get_child name node =
try M.find name node.children
with Not_found -> empty_treenode name
let time () =
let times = Unix.times () in
times.Unix.tms_utime +. times.Unix.tms_stime
let pp_ltac_call_kind = function
| Tacexpr.LtacNotationCall s -> Pptactic.pr_alias_key s
| Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst
| Tacexpr.LtacVarCall (_, id, t) -> Names.Id.print id
| Tacexpr.LtacAtomCall te ->
Pptactic.pr_glob_tactic (Global.env ())
(CAst.make (Tacexpr.TacAtom te))
| Tacexpr.LtacConstrInterp (env, sigma, c, _) ->
pr_glob_constr_env env sigma c
| Tacexpr.LtacMLCall te ->
(Pptactic.pr_glob_tactic (Global.env ())
te)
let string_of_call ck =
let s = string_of_ppcmds ck in
let s = String.map (fun c -> if c = '\n' then ' ' else c) s in
let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in
String.trim s
let rec merge_sub_tree name tree acc =
try
let t = M.find name acc in
let t = {
name;
total = t.total +. tree.total;
ncalls = t.ncalls + tree.ncalls;
local = t.local +. tree.local;
max_total = max t.max_total tree.max_total;
children = M.fold merge_sub_tree tree.children t.children;
} in
M.add name t acc
with Not_found -> M.add name tree acc
let merge_roots ?(disjoint=true) t1 t2 =
assert(String.equal t1.name t2.name);
{ name = t1.name;
ncalls = t1.ncalls + t2.ncalls;
local = if disjoint then t1.local +. t2.local else t1.local;
total = if disjoint then t1.total +. t2.total else t1.total;
max_total = if disjoint then max t1.max_total t2.max_total else t1.max_total;
children =
M.fold merge_sub_tree t2.children t1.children }
let rec find_in_stack what acc = function
| [] -> None
| { name } as x :: rest when String.equal name what -> Some(acc, x, rest)
| { name } as x :: rest -> find_in_stack what (x :: acc) rest
let exit_tactic ~count_call start_time name =
let diff = time () -. start_time in
match !stack with
| [] | [_] ->
encounter_invalid_stack_no_self ();
reset_profile_tmp ()
| node :: (parent :: rest as full_stack) ->
if not (String.equal name node.name) then
CErrors.anomaly
(Pp.strbrk "Ltac Profiler encountered an invalid stack (wrong self node) \
likely due to backtracking into multi-success tactics.");
let node = { node with
total = node.total +. diff;
local = node.local +. diff;
ncalls = node.ncalls + (if count_call then 1 else 0);
max_total = max node.max_total diff;
} in
let parent =
match find_in_stack node.name [] full_stack with
| None ->
let parent = { parent with
local = parent.local -. diff;
children = M.add node.name node parent.children } in
stack := parent :: rest;
parent
| Some(to_update, self, rest) ->
let self = merge_roots ~disjoint:false self node in
let updated_stack =
List.fold_left (fun s x ->
(try M.find x.name (List.hd s).children
with Not_found -> x) :: s) (self :: rest) to_update in
stack := updated_stack;
List.hd !stack
in
if rest == [] && get_profiling () then begin
assert(String.equal root parent.name);
encountered_invalid_stack_no_self := false;
reset_profile_tmp ();
feedback_results parent
end
(** [tclWRAPFINALLY before tac finally] runs [before] before each
entry-point of [tac] and passes the result of [before] to
[finally], which is then run at each exit-point of [tac],
regardless of whether it succeeds or fails. Said another way, if
[tac] succeeds, then it behaves as [before >>= fun v -> tac >>= fun
ret -> finally v <*> tclUNIT ret]; otherwise, if [tac] fails with
[e], it behaves as [before >>= fun v -> finally v <*> tclZERO
e]. *)
let rec tclWRAPFINALLY before tac finally =
let open Proofview in
let open Proofview.Notations in
before >>= fun v -> tclCASE tac >>= function
| Fail (e, info) -> finally v >>= fun () -> tclZERO ~info e
| Next (ret, tac') -> tclOR
(finally v >>= fun () -> tclUNIT ret)
(fun e -> tclWRAPFINALLY before (tac' e) finally)
let do_profile_gen pp_call call_trace ?(count_call=true) tac =
let open Proofview.Notations in
Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> !is_profiling)) >>= function
| false -> tac
| true ->
tclWRAPFINALLY
(Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
match pp_call call_trace, !stack with
| Some c, parent :: rest ->
let name = string_of_call c in
let node = get_child name parent in
stack := node :: parent :: rest;
Some (name, time ())
| Some _, [] -> assert false
| _ -> None
)))
tac
(function
| Some (name, start_time) ->
(Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
exit_tactic ~count_call start_time name)))
| None -> Proofview.tclUNIT ())
let do_profile trace ?count_call tac =
do_profile_gen (function
| (_, c) :: _ -> Some (pp_ltac_call_kind c)
| [] -> None)
trace ?count_call tac
let get_local_profiling_results () = List.hd !stack
module DData = struct
type t = Feedback.doc_id * Stateid.t
let compare x y = compare x y
end
module SM = Map.Make(DData)
let data = ref SM.empty
let _ =
Feedback.(add_feeder (function
| { doc_id = d;
span_id = s;
contents = Custom (_, "ltacprof_results", xml) } ->
let results = to_ltacprof_results xml in
let other_results =
try SM.find (d,s) !data
with Not_found -> empty_treenode root in
data := SM.add (d,s) (merge_roots results other_results) !data
| _ -> ()))
let reset_profile () =
encountered_invalid_stack_no_self := false;
reset_profile_tmp ();
data := SM.empty
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_notice(str prefix ++ pr_opt str name ++ str " ran for " ++
System.fmt_time_difference tstart tend)
let print_results_filter ~cutoff ~filter =
data := SM.filter (fun (doc,id) _ -> Stateid.is_valid ~doc id) !data;
let results =
SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in
let results = merge_roots results (CList.last !stack) in
Feedback.msg_notice (to_string ~cutoff ~filter results)
;;
let print_results ~cutoff =
print_results_filter ~cutoff ~filter:(fun _ -> true)
let print_results_tactic tactic =
print_results_filter ~cutoff:!Flags.profile_ltac_cutoff ~filter:(fun s ->
String.(equal tactic (sub (s ^ ".") 0 (min (1+length s) (length tactic)))))
let do_print_results_at_close () =
if get_profiling () then print_results ~cutoff:!Flags.profile_ltac_cutoff
let () = Declaremods.append_end_library_hook do_print_results_at_close
let () =
let open Goptions in
declare_bool_option
{ optstage = Summary.Stage.Interp;
optdepr = None;
optkey = ["Ltac"; "Profiling"];
optread = get_profiling;
optwrite = set_profiling }