On 13/03/2019 21:06, Lars Hupel wrote:
>> "Unable to increase stack" is one of the various messages that tells
>> you that PolyML has run out of resources. It doesn't really tell you
>> what the problem is though. It might be an actual problem or a
>> temporary problem caused by a machine being overloaded.
>
> This is likely connected to the recent change of platform. I will
> investigate this; maybe bumping the memory limit will resolve it.
BTW, with Poly/ML 5.8 being official, you can avoid full x86_64 for most
applications and always use the default x86_64_32.
This saves a lot of resources: I usually have ML_OPTIONS="--minheap
1500" with an open upper end -- the implicit limit is approx. 16G.
Even some entries of the slow/large groups of AFP work well with
x86_64_32, but I usually throw them into on big x86_64 pot as a special
case.
Another remaining application of full x86_64 is the huge PIDE session
forked by "isabelle dump" and related tools: it can require 64GB
(excluding slow), and I have not explored the upper end yet.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
