[isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory
hupel at in.tum.de
Mon Feb 22 08:58:36 CET 2016
> Another possibility is to set the maximum heap size with --maxheap e.g.
> ML_OPTIONS="--maxheap 28G"
> If the application needs it Poly/ML will try to grow the heap to avoid
> doing a lot of garbage collection. That can result in it crowding out
> other parts of the system that also need memory. The "Unable to
> increase stack" probably results from it being unable to grow an ML
> stack if the application recurses very deeply. I'm guessing that you
> don't have any swap space configured so there's no leeway there. You
> may have to experiment with the setting. You don't need --stackspace if
> you set the maximum heap size.
Thanks for the hint. Indeed, there's no swap space configured, because
all the build boxes have 32 GB of RAM.
I've tried setting the --maxheap to 4 GB, but here's the error I'm getting:
Value of --maxheap option is too large
(Relevant build log:
More information about the isabelle-dev