Re: [isabelle] timing individual use_thys?
On Thu, 21 Jun 2012, Christian Sternagel wrote:
your question seems very familiar :o)
I would suggest to have a look at the section "Measuring Time" of the
Isabelle Programming Tutorial:
The timing_wrapper proposed there appears to be a clone of an older
version of the standard timeit/timeap wrappers, which go back to Larry
from the depths of time, but have been continously updated.
So the Cookbook version is a bit outdated, but it is right in using
Timing.message to present the result to the user, not a projection of any
of the record components that "happen to work best on my laptop".
Over time that semi-formal timing output might evolve further, to give
better readings for the parallel evaluation environment that is standard
for quite some years already.
This archive was generated by a fusion of
Pipermail (Mailman edition) and