[isabelle-dev] HOL-Proofs

[Makarius]

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