[isabelle-dev] HOL-Proofs

Tobias Nipkow nipkow at in.tum.de
Tue May 13 18:08:43 CEST 2014


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?

Tobias


More information about the isabelle-dev mailing list