Re: [isabelle] timing individual use_thys?
On Thu, 21 Jun 2012, Christoph Sprenger wrote:
I would like to time the processing of individual use_thys commands in
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?
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and