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