On 19/06/2020 11:36, Makarius wrote: > On 19/06/2020 07:41, Florian Haftmann wrote: >> >> I guess this »java.lang.OutOfMemoryError: Java heap space« is due to > > In recent years, JVM resource limitations have become more and more difficult > to circumvent. The problem is that the heap limit needs to be specified in > advance when starting the java process, but making it too high causes problems > with low-end hardware (e.g. a laptop with only 8GB). > > ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms1g -Xmx8g -Xss16m"
It seems that -Xmx16g is required for a full-scale AFP build with parallel
jobs. The default is -Xmx4g and cannot be increased without affecting regular
users.
16 GB is not a big deal for big iron to build AFP, but the test configuration
needs to have specific settings like this:
ISABELLE_TOOL_JAVA_OPTIONS="$ISABELLE_TOOL_JAVA_OPTIONS -Xmx16g"
Or more ambitiously: -Xmx30g (this is the upper bound for 32bit object
pointers on the JVM).
Since I don't know how to change the jenkins setup, I have merely reverted the
critical changes for now: see also Isabelle/3e7d89d9912e + 23398ed3aecf.
I will come back to this later (although it has been in the pipeline for some
months already).
Makarius
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
