Stream: Mirror: Isabelle Development Mailing List

Topic: NEWS: Poly/ML 64_32 heap size 32 GiB instead of 16 GiB

Email Gateway (Jul 14 2026 at 21:35):

From: Makarius <makarius@sketis.net>

On 14/07/2026 23:31, Lawrence Paulson wrote:

Could this be used with Isabelle 2025-2?

Maybe. We have not tried it.

Isabelle development is linear, moving forward on a single branch, or rather
no branches at all.

Makarius

Email Gateway (Jul 14 2026 at 21:38):

From: Makarius <makarius@sketis.net>

* System *

• Poly/ML 5.9.2 has been patched to support larger heap size in the
  special x86_64_32/arm64_32 mode with 32-bit values: the limit is now 32
  GiB, instead of 16 GiB before. The cost is a factor of 1.2 .. 1.5 more
  memory requirement (due to alignment of values), and a slowdown factor
  0.9 .. 0.95 for average sessions. For very large sessions, the gain is a
  speedup factor 1.9 .. 1.2, due to reduced GC time. It also avoids the
  need for bulky x86_64/arm64 mode with 64-bit values and excessive GC
  time.

This refers to Isabelle/e3c3e01d3eb1.

This is the result of significant work by David Matthews in collaboration with
Martin Desharnais-Schäfer.

The plan is to use the enlarged 64_32 memory model as "one size fits for
almost all applications", and omit the old 64_32 mode with 16 GiB that is in
principle still supported by Poly/ML.

The full 64-bit mode is available as before, but discouraged. Its known GC
performance problems will be addressed at a later stage. (Not now and not for
this release.)

Makarius

Email Gateway (Jul 14 2026 at 21:44):

From: Makarius <makarius@sketis.net>

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

Last updated: Aug 05 2026 at 21:11 UTC