Dear David, >> There is definitely some continous bloat factor with every new release, >> although David Matthews was usually ahead of most big applications in >> recent years. In fact he is about to release Poly/ML 5.5.1 pretty soon, >> so a quick test with some repository version of Poly/ML might help (e.g. >> SVN 1843). > > I would suggest trying with the --stackspace option e.g. > ML_OPTIONS='--stackspace 500' > The Fail exception with "Insufficient space" arises in a number of places > such as when trying to fork a thread. This requires memory outside the ML > heap. The stackspace option keeps some space free from the ML heap for these > purposes.
I tried it, but the setting was not high enough: then even earlier sessions crash with a new 'Run out of store - interrupting threads' error message. This also happens if I set stackspace to 1500, but it succeeded with 5000. However, then still afterwards I get the usual poly(6820,0xb09a5000) malloc: *** mmap(size=16777216) failed (error code=12) *** error: can't allocate region error as before, if I use minheap=1000, or drop the minheap parameter. > I would guess that this is when running the X86/32 version rather than X86/64. Yes, I use the 32-bit mode. I will later run some tests when using the 64-bit mode. Here is my current setup: ISABELLE_BUILD_OPTIONS="" ML_PLATFORM="x86-darwin" ML_HOME="/Users/rene/.isabelle/contrib/polyml-5.5.0-3/x86-darwin" ML_SYSTEM="polyml-5.5.0" ML_OPTIONS="--minheap 1000 --stackspace 5000" Best regards, René _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
