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 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?

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





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