[isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP

Makarius 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
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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20200619/7c55a6be/attachment.sig>


More information about the isabelle-dev mailing list