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

[Makarius]

On 11/07/2020 07:57, Florian Haftmann wrote:
> 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.

(I don't see a version Isabelle/b8749ed18dd0, but I guess we can approximate
it by your latest Isabelle/a851ce626b78.)

This is probably due to my update to polyml-5.8.1-20200708 in
Isabelle/a7e6ac2dfa58.

David Matthews has resolved a few code generator problems, leading up to
change https://isabelle-dev.sketis.net/rPOLYMLfb10196d998b --- the HOL4 guys
had observed genuine crashes.


So for now, lets continue with the assumption that things work smoothly again.


	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/20200711/b922f8e8/attachment.sig>