[isabelle] insufficient memory exception in polyml
I am currently updating a very large theory from Isabelle2009-1 to Isabelle2009-2. So far this update was less painful than previous one, but I seem to be stuck now:
I am getting various versions of insufficient memory exceptions from polyml-5.3 after the theory has been fully processed at the point (I presume) where polyml is writing the image to disk, possibly while it is doing garbage collection.
A sample output of the log file is (the log file is btw gzipped and the error code is success, but the image is never written):
lemma ... [last lemma of thy]
val it = () : unit
val it = () : unit
ML> Exception- Fail "Insufficient memory" raised
The platform is polyml-5.3.0_x86-linux
ISABELLE_USEDIR_OPTIONS="-M 1 -p 0 -q 0 -v true"
and unchanged standard ML settings.
The machine has 8G of RAM and otherwise works fine for other big developments.
On polyml-5.3.0_x86-darwin, I am getting the same with the same settings. With -M 2, I am getting a C level exception in polyml at the same point with the message to set a breakpoint in a malloc function on stdour/err (but the same exception in the log).
On polyml-5.3.0_x86_64-darwin, I am getting with -M 1 the same log, and this message on std out:
Building CKERNEL ...
poly(5949,0xa0a3e500) malloc: *** mmap(size=134217728) failed (error code=12)
*** error: can't allocate region
*** set a breakpoint in malloc_error_break to debug
Finished CKERNEL (0:32:51 elapsed time, 0:32:47 cpu time, factor 0.99)
(possibly the same as the 32bit version, but I've lost the previous output. Can reproduce if needed)
With -M 3 and -M 2, on 64bit Darwin, I am instead getting exceptions about not being able to start another thread (at the same point). Again, the machine has 8GB of RAM and is otherwise rock solid.
The same image builds easily under 32bit and 64bit polyml 5.3.0 (same version) on machines with less than 4GB of memory in Isabelle2009-1.
I've tried playing around with -H and --mutable/--immutable settings, without success, but I don't have a good guideline what to try.
This archive was generated by a fusion of
Pipermail (Mailman edition) and