[isabelle-dev] Poly/ML 5.7

Makarius makarius at sketis.net
Fri May 19 10:36:34 CEST 2017


On 15/05/17 14:33, Makarius wrote:
> On 15/05/17 12:14, Makarius wrote:
>> Some results can be seen here:
>>
>> http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux/index.html
>> http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux_2_threads/index.html
>>
>> The test hardware is similar or actually the same as "Linux A", but this
>> needs to be investigated further. It is also important to compare
>> timings for the *same* Isabelle versions, but the Poly_ML_5.7_Linux task
>> is still busy digging into older history.
> 
> Maybe I also manage to get ml_statistics into the charts soon. Then we
> can look at heap, task, thread details etc.

I have now done that in various changes leading to Isabelle/65e132abab1e.

Moreover, I have made a fresh start for "Poly/ML 5.7" measurements, with
precisely the same parameters as "Linux A" (Isabelle/d547173212d2). This
explains why there are only a few data points for Poly/ML 5.7, but the
situation will improve every day.


This means we can now compare the measurements and analyze the (slight)
performance losses of Poly/ML 5.7.


	Makarius



More information about the isabelle-dev mailing list