Email Gateway (Nov 28 2025 at 12:32): Email Gateway (Nov 28 2025 at 12:32):From: Fabian Huch <huch@in.tum.de>
We are recently seeing OOM errors for builds with 8GB heap memory, e.g.:
https://build.proof.cit.tum.de/build?name=user%2F2212
Since we are using the Z garbage collector, I've now changed the build
manager to use its soft heap max size (8g) with a hard limit of 32g.
This should mean that we won't see any OOM errors unless things really
go wrong. However, it is a bit concerning that we went from <4g to >8g
in the last few months.
If the soft heap limit works well, we could also do this by default in
the distribution.
Fabian
Email Gateway (Nov 28 2025 at 13:27):From: Makarius <makarius@sketis.net>
On 28/11/2025 13:32, Fabian Huch wrote:
Since we are using the Z garbage collector, I've now changed the build manager
to use its soft heap max size (8g) with a hard limit of 32g.
I was not aware of that fine point. Would you say that the Z garbage collector
is where high-end Java applications are going, and that its extra options work
properly?
This should mean that we won't see any OOM errors unless things really go
wrong. However, it is a bit concerning that we went from <4g to >8g in the
last few months.
We have accumulated a lot of extras in Isabelle/Scala, tons of markup, and
recently the online monitoring via Progress.Nodes_Status --- which is
immediately visible in the initial session build panel of Isabelle/jEdit, with
all these percentages and inverse status lines. The actual motivation behind
that was support for "long running commands" in regular progress output, for
batch builds, to see potential non-termination earlier.
I hope this state of affairs is sufficient for the Isabelle2025-1 release, so
that further performance tuning can be postponed.
If the soft heap limit works well, we could also do this by default in the
distribution.
Yes, as long as it means "the Distribution after Isabelle2025-1".
Makarius
Email Gateway (Nov 28 2025 at 14:33):From: Fabian Huch <huch@in.tum.de>
Since we are using the Z garbage collector, I've now changed the
build manager to use its soft heap max size (8g) with a hard limit of
32g.I was not aware of that fine point. Would you say that the Z garbage
collector is where high-end Java applications are going,
I would expect most desktop applications to migrate to generational ZGC.
Latency is better than G1GC, it's more efficient, and allows for desktop
applications with a low memory footprint. That solves all the main
problems with JVM garbage collection.
and that its extra options work properly?
I have never seen JVM options misbehave. The only caveat is that this is
an XX option, i.e. subject to change without notice (but typically even
those remain stable).
Fabian
Last updated: Dec 10 2025 at 12:50 UTC