[isabelle-dev] \nexists

[Makarius]

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.


	Makarius