[isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

[David Matthews]

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