build cluster: java.lang.OutOfMemoryError: Java heap space

Makarius makarius at sketis.net
Thu Sep 25 22:59:36 CEST 2025


In current Isabelle/655a15fa86dc we have sporadic breakdowns of our build 
cluster for Isabelle + AFP: java.lang.OutOfMemoryError: Java heap space --- 
but it is hard to tell which subset of sessions actually causes it.

The problem appears to be a consequence of my rearrangements of the underlying 
"isabelle build" process, in various changesets leading to the above version. 
It is unclear to me, if there is really anything wrong, or if current AFP has 
outgrown our system parameters once again.

I wonder if the build cluster actually provides its own Java heap settings. 
The global default has been 4g since 97fc4f657bda (Apr-2020) --- it still 
needs to work with low-end user hardware with only 8GB RAM.

In contrast, I've been using 8g Java heap routinely for AFP tests in a recent 
isabelle_cronjob entry, see 205bad84a1bd from Mar-2024.


So for the moment, my amendment is as follows:

changeset:   83231:06a05e098347
tag:         tip
user:        wenzelm
date:        Thu Sep 25 22:26:31 2025 +0200
files:       etc/settings src/Pure/ROOT.ML
description:
more Java heap space for the sake of Isabelle/AFP cluster build stability, but 
this is better changed elsewhere;
enforce rebuild of Isabelle/ML;


I will be on travel until 04-Oct-2025, and hope to understand the build 
cluster default settings when I return. On 06-Oct-2025, I intend to publish 
Isabelle2025-1-RC0 as an early preview of the start of the release process in 
Nov-2025.


	Makarius


More information about the isabelle-dev mailing list