[isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP
makarius at sketis.net
Fri Jun 19 19:47:45 CEST 2020
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
16 GB is not a big deal for big iron to build AFP, but the test configuration
needs to have specific settings like this:
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
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 833 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev