theory Timing+ −
imports "../Base"+ −
begin+ −
+ −
section {* Measuring Time\label{rec:timing} *} + −
+ −
text {*+ −
{\bf Problem:}+ −
You want to measure the running time of a tactic or function.\smallskip+ −
+ −
{\bf Solution:} Time can be measured using the function + −
@{ML start_timing} and @{ML end_timing}.\smallskip+ −
+ −
Suppose you defined the Ackermann function inside Isabelle. + −
*}+ −
+ −
fun + −
ackermann:: "(nat \<times> nat) \<Rightarrow> nat"+ −
where+ −
"ackermann (0, n) = n + 1"+ −
| "ackermann (m, 0) = ackermann (m - 1, 1)"+ −
| "ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1))"+ −
+ −
text {* + −
You can measure how long the simplifier takes to verify a datapoint+ −
of this function. The timing of a tactic can be done using the following + −
wrapper function:+ −
*}+ −
+ −
ML %linenosgray{*fun timing_wrapper tac st =+ −
let + −
val t_start = start_timing ();+ −
val res = tac st;+ −
val t_end = end_timing t_start;+ −
in+ −
(warning (#message t_end); res)+ −
end*}+ −
+ −
text {*+ −
Note that this function, in addition to a tactic, also takes a state @{text+ −
"st"} as argument and applies this state to the tactic (Line 4). The reason is that+ −
tactics are lazy functions and you need to force them to run, otherwise the+ −
timing will be meaningless. The time between start and finish of the tactic+ −
will be calculated as the end time minus the start time. An example of the+ −
wrapper is the proof+ −
+ −
+ −
*}+ −
+ −
lemma "ackermann (3, 4) = 125"+ −
apply(tactic {* + −
timing_wrapper (simp_tac (@{simpset} addsimps @{thms "nat_number"}) 1) *})+ −
done+ −
+ −
text {*+ −
where it returns something on the scale of 3 seconds. We chose to return+ −
this information as a string, but the timing information is also accessible+ −
in number format.+ −
+ −
\begin{readmore}+ −
Basic functions regarding timing are defined in @{ML_file + −
"Pure/ML-Systems/polyml_common.ML"} (for the PolyML compiler). Some more+ −
advanced functions are defined in @{ML_file "Pure/General/output.ML"}.+ −
\end{readmore}+ −
*}+ −
+ −
+ −
+ −
end+ −