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:

http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/isabelle-cookbook/raw-file/tip/progtutorial.pdf

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.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.