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 can be done using the following wrapper function:+
−
*}+
−
+
−
ML{*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 for which it measures the+
−
  time, also takes a state @{text "st"} as argument and applies this state to+
−
  the tactic. 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 for 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 choose 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+
−