makarius at sketis.net
Mon Jul 18 21:51:31 CEST 2016
On 18/07/16 10:39, Lars Hupel wrote:
>> Also the detailed parallel runtime parameters that are emitted every
>> 0.5s during a session running: number of active threads, pending futures
> How can I extract this information from within Isabelle/Scala? How would
> this information be presented?
It is emitted into the session log file. Build.parse_log may serve as an
example how to access it.
Presentation could be done as in the Monitor panel of Isabelle/jEdit.
The Isabelle/Scala modules ML_Statistics and Task_Statistics provide
All this uses JFreeChart, which is a relatively wellknown and decent 2D
chart drawing framework. It is much less than gnuplot, though,
especially concerning interpolation and smoothing of curves.
>>> - What about sessions that grow in size over time?
>> That is indeed important, although we have just ignored it historically.
> Right. But how would we take it into account? What registers as a spike
> in build time for a session could either be a performance regression in
> Isabelle or growing material.
The maximum and final heap size (from the above data) might serve well
as a single value.
Apart from that, the full chart is occasionally useful to understand
resource shortage better.
More information about the isabelle-dev