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