[isabelle-dev] \nexists

Makarius 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
>> etc.
> 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
further possibilities.

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 mailing list