I also had a similar problem some time ago and I solved it by changing
the proof. You can get by bisecting to the very point that makes
HOL-Proofs choke and change it. I am not sure anymore but I think in my
example I just changed metis for blast or something like this.
Ondrej
On 05/13/2014 06:08 PM, 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?
Tobias
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
