makarius at sketis.net
Tue May 13 18:18:12 CEST 2014
On Tue, 13 May 2014, Tobias Nipkow wrote:
> I added a few lemmas to List and now the HOL-Proofs session no longer
> terminates. This is what I got to see when I interrupted one run:
> ^Cpoly(52110,0xb0185000) malloc: *** mach_vm_map(size=8388608) failed (error code=3)
> *** error: can't allocate region
> *** set a breakpoint in malloc_error_break to debug
> *** Interrupt
> HOL-Proofs FAILED
> When I load the session interactively, I don't have a problem. Any hints what I
> should be doing?
That is a Poly/ML heap allocation problem specifically on Mac OS X. David
Matthews has occasionally explained the technical side-conditions imposed
by Apple, but I did not really understand them.
I usually just tinker with ML_OPTIONS in $ISABELLE_HOME/etc/settings until
it works again. Here is an arbitrary example:
ML_OPTIONS="--minheap 800 --maxheap 3000 --gcthreads 4"
It depends on your hardware what makes sense, and on some luck what works.
More information about the isabelle-dev