[isabelle-dev] Slow builds due to excessive heap images

[Lars Hupel]

> We are presently testing Poly/ML 5.7.1 by default (see
> Isabelle/aefaaef29c58) and there are already interesting performance
> figures, e.g. see:
> 
> http://isabelle.in.tum.de/devel/build_status
> http://isabelle.in.tum.de/devel/build_status/Linux_A
> http://isabelle.in.tum.de/devel/build_status/AFP
> 
> Overall, performance is mostly the same as in Poly/ML 5.6 from
> Isabelle2017, but there are some dropouts. In particular, loading heap
> images has become relatively slow: this impacts long heap chains like
> HOL-Analysis or big applications in AFP. E.g. see
> http://isabelle.in.tum.de/devel/build_status/AFP/index.html#session_CAVA_LTL_Modelchecker
> (timing vs. ML timing).

Tobias and me have discovered an interesting discrepancy between your
AFP slow setup and our AFP slow setup. They run on identical hardware
with the only difference of 6 vs 8 threads. On 6 threads, it runs
significantly faster. For example, Flyspeck-Tame requires 9:44:16
(elapsed time on 8 threads) vs 8:50:55 (elapsed time on 6 threads).

That difference aside, what I also find alarming is that the total
runtime of Flyspeck-Tame increased by more than 20% after the switch to
Poly/ML 5.7. This now means that the slow sessions rapidly approach 24
hours in build time, which makes it less feasible to run them every day.