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