Email Gateway (Apr 19 2024 at 11:16): Email Gateway (Apr 19 2024 at 11:16):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Hi,
We are testing Isabelle2024-RC2 locally on our fairly large proof. We are
noticing extremely slow builds of Pure and HOL heaps after changing the ML
runtime settings. For example, I turned on the debugger exception tracing
and selected ML System 64-bit option in the Isabelle plugin settings and
caused a heap rebuild which has now taken over an hour to reach
HOL.Binomial.
With previous Isabelle versions we have never noticed rebuilds taking this
long after changing ML runtime settings.
This is on an Apple M1 MacBook Pro 32GiB RAM.
Thanks,
Dominic
Email Gateway (Apr 19 2024 at 11:24):From: Manuel Eberl <manuel@pruvisto.org>
Hello,
are you sure this is a regression? In my experience this is perfectly
normal. If you switch on ML debugging and rebuild Pure, Pure takes much
longer to build and HOL takes forever. However, if you switch on
debugging and only rebuild HOL, there is very little overhead.
Manuel
Email Gateway (Apr 25 2024 at 20:52):From: Makarius <makarius@sketis.net>
I have now made some experiments with Mac Studio M1 and the following settings
(according to "isabelle build -?"):
ML_PLATFORM="arm64-darwin"
ML_OPTIONS="--minheap 1500 --maxheap 30000"
Notable options (via etc/preferences):
threads = 8
ML_system_64 = true
ML_debugger = true
Here are some results of "isabelle build -f -b HOL":
Isabelle2023:
Finished HOL (0:21:40 elapsed time, 1:24:30 cpu time, factor 3.90)
Isabelle2024-RC2:
Finished HOL (0:21:44 elapsed time, 1:24:10 cpu time, factor 3.87)
Conclusion from this experiment: There is nothing to be seen here. We can
continue towards the final release. (Unless you have other experiments that
disprove that.)
Makarius
Last updated: May 05 2024 at 01:11 UTC