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