[isabelle-dev] HOL-Nominal-Examples starving on lxbroy10
makarius at sketis.net
Sat Jul 11 14:58:22 CEST 2020
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
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 833 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev