> 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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev