[isabelle-dev] HOL-Nominal-Examples starving on lxbroy10

[Florian Haftmann]

As of rev. b8749ed18dd0 with options

ML_OPTIONS=--minheap 500
ISABELLE_TOOL_JAVA_OPTIONS=-Djava.awt.headless=true -Xms512m -Xmx4g
-Xss16m -Xmx8g

and default number of threads, the problem does not occur any longer.

	Florian

Am 02.07.20 um 09:18 schrieb Florian Haftmann:
>> Does "isabelle build pide_session=false" make a difference.
>>
>> Did you use option -N?
>>
>> What is your value for option -j and -o threads?
> 
> * pide_session=false does not make a difference
> 
> * -N is not operating on lxbroy10
> 
> * -j is not relevant since I only build one session
> 
> * threads make a difference: -o threads=2 and -o threads=3 has been
> successful; previously I just used the hardware default.  I did not
> check for -o threads=4 so far.
> 
> Hope this helps,
> 	Florian
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> 

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