[isabelle-dev] HOL-Proofs broken?

[Jasmin Blanchette]

> On 06.10.2015, at 22:55, Jasmin Blanchette <jasmin.blanchette at inria.fr> wrote:
> 
> 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).

My suspicion appears to have been correct. I am now able to build "HOL-Proofs" in 13 min on my MacBook Pro. (I have no idea why my test of 5b5656a63bd6 "diverged" yesterday.) I'm now testing everything and will push once this is done.

Sorry for the trouble.

Jasmin