[isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle (benchmark)

[Makarius]

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