This looks more like a polyml issue than an Isabelle issue, so I'm reposting here.
Since the below I've run a few more experiments, and the theory does run fine with image built after less than 25min with the current svn trunk version of polyml on x86_64-darwin (5.4 Experimental). However, with the polyml-3.1-fixes version, it is still running after 45min with memory usage approaching 7.5GB and still raising. I'm not quite sure how to proceed. I don't think I'll want to run our production proofs on an experimental polyml version. How experimental/far away from release is the current trunk? Cheers, Gerwin Begin forwarded message: > From: Gerwin Klein <[email protected]> > Date: 23 July 2010 4:06:19 PM GMT+02:00 > To: Isabelle Users ML <[email protected]> > Subject: [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 > ML> > > The platform is polyml-5.3.0_x86-linux > with > 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. > > Any ideas? > > I've tried playing around with -H and --mutable/--immutable settings, without > success, but I don't have a good guideline what to try. > > Cheers, > Gerwin > > > _______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
