It seems that I have the same problem, because the 2 lemmas I added also use metis. Playing around with system parameters does not do anything.
Tobias On 14/05/2014 00:32, Ondřej Kunčar wrote: > 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
