[isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

[David Matthews]

On 17/02/2016 21:47, Dmitriy Traytel wrote:
>> ML> Exception- SysErr ("Cannot allocate memory", SOME ENOMEM) raised

This looks like an attempt to allocate memory for something other than 
the heap.  There are quite a few situations where this can happen.

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.

David