[isabelle-dev] HOL-Proofs

[Ondřej Kunčar]

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