theory Timingimports "../Appendix"beginsection {* 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 on the Isabelle level. *}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 actual timing is done inside the 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 (writeln (#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 simplifier tactic, amongst others, can be forced to run by just applying the state to it. But ``fully'' lazy tactics, such as @{ML "resolve_tac"}, need even more ``standing-on-ones-head'' to force them to run. The time between start and finish of the simplifier 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) *})donetext {* 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