From: Makarius <makarius@sketis.net>
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
Last updated: Oct 08 2025 at 20:22 UTC