1 theory Timing |
1 theory Timing |
2 imports "../Appendix" |
2 imports "../Appendix" |
3 begin |
3 begin |
4 |
4 |
5 section {* Measuring Time\label{rec:timing} *} |
5 section \<open>Measuring Time\label{rec:timing}\<close> |
6 |
6 |
7 text {* |
7 text \<open> |
8 {\bf Problem:} |
8 {\bf Problem:} |
9 You want to measure the running time of a tactic or function.\smallskip |
9 You want to measure the running time of a tactic or function.\smallskip |
10 |
10 |
11 {\bf Solution:} Time can be measured using the function |
11 {\bf Solution:} Time can be measured using the function |
12 @{ML start in Timing} and @{ML result in Timing}.\smallskip |
12 @{ML start in Timing} and @{ML result in Timing}.\smallskip |
13 |
13 |
14 Suppose you defined the Ackermann function on the Isabelle level. |
14 Suppose you defined the Ackermann function on the Isabelle level. |
15 *} |
15 \<close> |
16 |
16 |
17 fun |
17 fun |
18 ackermann:: "(nat \<times> nat) \<Rightarrow> nat" |
18 ackermann:: "(nat \<times> nat) \<Rightarrow> nat" |
19 where |
19 where |
20 "ackermann (0, n) = n + 1" |
20 "ackermann (0, n) = n + 1" |
21 | "ackermann (m, 0) = ackermann (m - 1, 1)" |
21 | "ackermann (m, 0) = ackermann (m - 1, 1)" |
22 | "ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1))" |
22 | "ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1))" |
23 |
23 |
24 text {* |
24 text \<open> |
25 You can measure how long the simplifier takes to verify a datapoint |
25 You can measure how long the simplifier takes to verify a datapoint |
26 of this function. The actual timing is done inside the |
26 of this function. The actual timing is done inside the |
27 wrapper function: |
27 wrapper function: |
28 *} |
28 \<close> |
29 |
29 |
30 ML %linenosgray{*fun timing_wrapper tac st = |
30 ML %linenosgray\<open>fun timing_wrapper tac st = |
31 let |
31 let |
32 val t_start = Timing.start (); |
32 val t_start = Timing.start (); |
33 val res = tac st; |
33 val res = tac st; |
34 val t_end = Timing.result t_start; |
34 val t_end = Timing.result t_start; |
35 in |
35 in |
36 (writeln (Timing.message t_end); res) |
36 (writeln (Timing.message t_end); res) |
37 end*} |
37 end\<close> |
38 |
38 |
39 text {* |
39 text \<open> |
40 Note that this function, in addition to a tactic, also takes a state @{text |
40 Note that this function, in addition to a tactic, also takes a state \<open>st\<close> as argument and applies this state to the tactic (Line 4). The reason is that |
41 "st"} as argument and applies this state to the tactic (Line 4). The reason is that |
|
42 tactics are lazy functions and you need to force them to run, otherwise the |
41 tactics are lazy functions and you need to force them to run, otherwise the |
43 timing will be meaningless. The simplifier tactic, amongst others, can be |
42 timing will be meaningless. The simplifier tactic, amongst others, can be |
44 forced to run by just applying the state to it. But ``fully'' lazy tactics, |
43 forced to run by just applying the state to it. But ``fully'' lazy tactics, |
45 such as @{ML "resolve_tac"}, need even more ``standing-on-ones-head'' to force |
44 such as @{ML "resolve_tac"}, need even more ``standing-on-ones-head'' to force |
46 them to run. |
45 them to run. |
47 |
46 |
48 The time between start and finish of the simplifier will be calculated |
47 The time between start and finish of the simplifier will be calculated |
49 as the end time minus the start time. An example of the |
48 as the end time minus the start time. An example of the |
50 wrapper is the proof |
49 wrapper is the proof |
51 *} |
50 \<close> |
52 |
51 |
53 lemma "ackermann (3, 4) = 125" |
52 lemma "ackermann (3, 4) = 125" |
54 apply(tactic {* |
53 apply(tactic \<open> |
55 timing_wrapper (simp_tac (@{context} addsimps @{thms "eval_nat_numeral"}) 1) *}) |
54 timing_wrapper (simp_tac (@{context} addsimps @{thms "eval_nat_numeral"}) 1)\<close>) |
56 done |
55 done |
57 |
56 |
58 text {* |
57 text \<open> |
59 where it returns something on the scale of 3 seconds. We chose to return |
58 where it returns something on the scale of 3 seconds. We chose to return |
60 this information as a string, but the timing information is also accessible |
59 this information as a string, but the timing information is also accessible |
61 in number format. |
60 in number format. |
62 |
61 |
63 \begin{readmore} |
62 \begin{readmore} |
64 Basic functions regarding timing are defined in @{ML_file |
63 Basic functions regarding timing are defined in @{ML_file |
65 "Pure/General/timing.ML"} (for the PolyML compiler). Some more |
64 "Pure/General/timing.ML"} (for the PolyML compiler). Some more |
66 advanced functions are defined in @{ML_file "Pure/General/output.ML"}. |
65 advanced functions are defined in @{ML_file "Pure/General/output.ML"}. |
67 \end{readmore} |
66 \end{readmore} |
68 *} |
67 \<close> |
69 |
68 |
70 |
69 |
71 |
70 |
72 end |
71 end |