> On 06.10.2015, at 22:37, Makarius <makar...@sketis.net> wrote:
>
>> On Tue, 6 Oct 2015, Dmitriy Traytel wrote:
>>
>> So the main candidates for bad changesets are: ebf296fe88d7, 2ebdd603cd71.
>
> More results on macbroy2:
>
> 5b5656a63bd6
> Finished HOL-Proofs (0:18:14 elapsed time, 0:49:28 cpu time, factor 2.71)
>
> 2ebdd603cd71
> Building HOL-Proofs ...
> Warning - Unable to increase stack - interrupting thread
> Warning - Unable to increase stack - interrupting thread
> *** Interrupt
The problem is most likely caused by ebf296fe88d7. Looking at it more closely,
one sees a proof that is (at least) quadratic in the number of constructors:
fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts
rel_distincts rel_eqs =
HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct1] exhaust)
THEN_ALL_NEW
rtac ctxt (infer_instantiate' ctxt [SOME ct2] exhaust) THEN_ALL_NEW
I would not exclude that this could give rise to some big proof objects in
conjunction with a type like "nibble", for which we previously did not generate
the "case_transfer" rule (nor "rel_cases" upon which it relies).
Let me look into this. It might take a bit of time before I sort this all out,
but hopefully we'll be back to normal tomorrow (Wednesday).
Jasmin
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
