On 20/02/2016 00:08, Lars Hupel wrote:
Thanks for the suggestion. I've deployed that change on all our build
boxes. We'll see how it works out.
The problem still persists, as can be witnessed from this log:
<https://ci.isabelle.systems/jenkins/job/afp-repo-afp/71/consoleFull>
This time, there are additional messages:
Warning - Unable to increase stack - interrupting thread
Warning - Unable to increase stack - interrupting thread
Warning - Unable to increase stack - interrupting thread
*** Interrupt
Algebraic_Numbers FAILED
Oddly enough this is not reproducible. If I run just the failing sessions
on an identical build box, it works fine.
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.
David
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
