[isabelle-dev] HOL-Proofs

[Tobias Nipkow]

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