Re: [isabelle] timing individual use_thys?



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

On 06/21/2012 05:33 PM, Christoph Sprenger wrote:
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








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