[isabelle-dev] Poly/ML 5.7
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:
>> 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.
More information about the isabelle-dev