[isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

[Lars Hupel]

> 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:
<https://ci.isabelle.systems/jenkins/job/isabelle-repo-nightly-slow/23/console>)

Cheers
Lars