OOM Errors in 8GB JVM builds, -XX:SoftMaxHeapSize

[Makarius]

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