On 22/02/2016 07:58, Lars Hupel wrote:
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>)
That suggests that you're running the 32-bit version of Poly/ML in which
case the heap is limited to around 3-3.5G by the system and the problem
you're having is the total 4G memory limit. Switch to the 64-bit
version as a starting point. I was assuming that with 32G of memory you
were running the 64-bit version already.
David
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
