Re: [isabelle] timing individual use_thys?

On Thu, 21 Jun 2012, Christian Sternagel wrote:

Dear Christoph,

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 MHonArc.