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
|
(** TODO: Figure out how to test "sanity" for the ltac profiler output *)
Fixpoint fact (n : nat) := match n with 0 => 1 | S n' => n * fact n' end.
Fixpoint walk (n : nat) := match n with 0 => tt | S n => walk n end.
Ltac slow := idtac + (do 2 (let x := eval lazy in (walk (fact 9)) in idtac)).
Ltac slow2 := idtac + (do 2 (let x := eval lazy in (walk (fact 9)) in idtac)).
Ltac multi := idtac + slow + slow2.
Set Ltac Profiling.
Goal True.
Time try (multi; fail).
(* Warning: Ltac Profiler cannot yet handle backtracking into multi-success
tactics; profiling results may be wildly inaccurate.
[profile-backtracking,ltac] *)
Show Ltac Profile.
(* Used to be:
total time: 0.000s
tactic local total calls max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─multi --------------------------------- 47.1% 47.1% 1 0.000s
─slow ---------------------------------- 35.3% 35.3% 1 0.000s
─slow2 --------------------------------- 17.6% 17.6% 1 0.000s
tactic local total calls max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─multi --------------------------------- 47.1% 47.1% 1 0.000s
─slow ---------------------------------- 35.3% 35.3% 1 0.000s
─slow2 --------------------------------- 17.6% 17.6% 1 0.000s
*)
(* Now:
total time: 2.074s
tactic local total calls max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─multi --------------------------------- 0.0% 100.0% 6 1.119s
─slow ---------------------------------- 54.0% 54.0% 3 1.119s
─slow2 --------------------------------- 46.0% 46.0% 3 0.955s
tactic local total calls max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─multi --------------------------------- 0.0% 100.0% 6 1.119s
├─slow -------------------------------- 54.0% 54.0% 3 1.119s
└─slow2 ------------------------------- 46.0% 46.0% 3 0.955s
*)
Abort.
|
