[isabelle-dev] HOL-Proofs

[David Matthews]

On 13/05/2014 17:18, Makarius wrote:
> 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.

On its own this is at most a warning.  If the ML application requires a 
large heap Poly/ML tries to allocate as much memory as it can.  There is 
no way to find out how much free space is left so this sometimes 
involves making allocation requests and testing the result to see if 
they have succeeded.  If a call fails Poly/ML recovers from it.  That is 
perfectly normal.  Other operating systems simply return a failure 
result in these circumstances but for some reason Apple have decided to 
print this message as well.  It typically appears in 32-bit mode when 
the maximum address space has been reached.

That, though is a separate issue from why the session does not 
terminate.  The most likely explanation is that it requires more memory 
than is available and the garbage-collector can't keep up.  I don't know 
why it should be different when you run it interactively.

I would assume that you are running in 32-bit mode.  Have you tried in 
64-bit mode with a larger heap?

David