[isabelle-dev] HOL-Proofs broken?

[Jasmin Blanchette]

> On 06.10.2015, at 22:37, Makarius <makarius at 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