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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
