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