NEWS: Poly/ML 64_32 heap size 32 GiB instead of 16 GiB
Makarius
makarius at sketis.net
Tue Jul 14 23:43:52 CEST 2026
Here are some measurements from a few days ago:
https://files.sketis.net/build_profiling_11-Jul-2026
This has been produced with a command-line like this:
isabelle build_profiling -A: Automated_Stateful_Protocol_Verification
Bicategory CZH_Universal_Constructions Category3 Frequency_Moments
JinjaThreads MiniSail ResiduatedTransitionSystem2 Two_Hermitian_Results
HOL-Probability
The "isabelle build_profiling" tool is for administrative purposes, which
explains its lack of documentation in the "system" manual. It is so useful,
that I might make it more official for the coming release, with proper
documentation.
The above test sessions are mainly those that hit the former 16 GiB limit,
which explains why the speedup is quite good. Various other sessions, e.g.
requirements of the main tests, need much less ML heap: here we see a small
slowdown and increase of stored heap size.
I do hope that slowdown and increased heap images are not significant in
practice, so that we can proceed with the plan to have just one main Poly/ML
configuration.
Makarius
More information about the isabelle-dev
mailing list