Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] timing individual use_thys?


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 08:18 UTC