[isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

[Lars Hupel]

>> Try adding a --stackspace argument to reserve space for thread stacks
>> and anything else. e.g.
>> ML_OPTIONS="--stackspace 200M"
>> This option keeps this space back whenever Poly tries to grow the heap
>> to avoid the heap using all the available memory.  You may need to
>> experiment a bit with how much to reserve depending on why the memory is
>> required.  It is possible that you could still get the error if there is
>> some sort of loop.
>
> 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.


Cheers
Lars