Email Gateway (Aug 18 2022 at 20:09): Email Gateway (Aug 18 2022 at 20:09):From: Christoph Sprenger <sprenger@inf.ethz.ch>
Dear all,
I would like to time the processing of individual use_thys commands in
ROOT.ML files.
If I remember correctly, in earlier versions of Isabelle there was a
variant of the use_thy ML commands that returned timing information
(something like time_use_thy?). Is there a replacement or alternative
to achieve the same effect?
I know that with usedir's option "-t true" I can time the whole
session, but I would like to get a little bit more resolution without
breaking up a session into smaller ones.
Thank you for your time,
Christoph
Email Gateway (Aug 18 2022 at 20:09):From: Christian Sternagel <c-sterna@jaist.ac.jp>
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
cheers
chris
Email Gateway (Aug 18 2022 at 20:13):From: Makarius <makarius@sketis.net>
You get the old behaviour back via "Toplevel.timing := true" in ROOT.ML.
There is a general snag, though, since parallel theory processing makes it
difficult to get sensible timing results. So another (temporary)
"Multithreading.max_threads := 1" might help.
Makarius
Email Gateway (Aug 18 2022 at 20:13):From: Makarius <makarius@sketis.net>
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
Last updated: Nov 21 2024 at 12:39 UTC