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

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Jul 2 09:18:10 CEST 2020


> 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

-------------- 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/20200702/9354c0b4/attachment.sig>


More information about the isabelle-dev mailing list