[isabelle-dev] profiling

[Alexander Krauss]

Hi Brian,

> ML {* Toplevel.profiling := 1; *}

> What other profiling tools are available for me to use?

More useful than global profiling is the "profile" combinator, which 
restricts these statistics to specific parts of the code. Using that 
combinator you can also profile an entire session. The data is dumped 
into the logfile in an unreadable form, but the script 
Admin/profiling_report turns it into something that can sometimes be useful.

Also, make sure that you turn off multithreading, otherwise you might 
get spurious data from other threads (though I'm not sure about that. 
@Andy: Did we actually observe this last summer, or was it just a guess?).

> It would be
> nice to have something similar to the profiler in GHC, which outputs a
> tree-like table that shows the time spent in each function, as well as
> the total inherited time from all other functions called by it.

Yes, that would be nice... But polyml currently only traces the 
"innermost" function, not the whole call stack.

Alex