Re: [isabelle-dev] HOL-Proofs broken?

[Jasmin Blanchette]

Hi Makarius,

> My impression is that ebf296fe88d7 (blanchet) causes HOL-Proofs to run out of 
> resources and fail.  I've made approx. 3 runs in the vicinity -- it always 
> takes very long.
> 
> Is that another failure to do a full "isabelle build -a" before pushing 
> anything?

I did "isabelle build -a" but stopped after some time because "HOL-Proofs" 
diverged. Then I went back to the last repository version and had exactly the 
same divergence behavior. Testboard is down, and if my 2015 MacBook Pro can't 
do it, we have a problem, already before ebf296fe88d7.

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] HOL-Proofs broken?

[Dmitriy Traytel]

As a data point: when testing 8d40ddaa427f I could build “HOL-Proofs” in about 
17 minutes.

Timing = :threads=4elapsed=979.269cpu=2582.077gc=323.518factor=2.64

Dmitriy

> On 06 Oct 2015, at 21:54, Jasmin Blanchette  
> wrote:
> 
> Hi Makarius,
> 
>> My impression is that ebf296fe88d7 (blanchet) causes HOL-Proofs to run out 
>> of resources and fail.  I've made approx. 3 runs in the vicinity -- it 
>> always takes very long.
>> 
>> Is that another failure to do a full "isabelle build -a" before pushing 
>> anything?
> 
> I did "isabelle build -a" but stopped after some time because "HOL-Proofs" 
> diverged. Then I went back to the last repository version and had exactly the 
> same divergence behavior. Testboard is down, and if my 2015 MacBook Pro can't 
> do it, we have a problem, already before ebf296fe88d7.
> 
> Jasmin
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] HOL-Proofs broken?

[Makarius]

On Tue, 6 Oct 2015, Dmitriy Traytel wrote:


As a data point: when testing 8d40ddaa427f I could build “HOL-Proofs” in about 
17 minutes.


This conforms to my expectations: HOL-Proofs is slow, but works.

I am presently on a side-branch starting from 5b5656a63bd6, and that works 
as well: https://bitbucket.org/makarius/isabelle/commits/1727d7d14d76


So the main candidates for bad changesets are: ebf296fe88d7, 2ebdd603cd71.


Makarius___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] HOL-Proofs broken?

[Makarius]

On Tue, 6 Oct 2015, Makarius wrote:


On Tue, 6 Oct 2015, Dmitriy Traytel wrote:


 As a data point: when testing 8d40ddaa427f I could build “HOL-Proofs” in
 about 17 minutes.


This conforms to my expectations: HOL-Proofs is slow, but works.

I am presently on a side-branch starting from 5b5656a63bd6, and that works as 
well: https://bitbucket.org/makarius/isabelle/commits/1727d7d14d76


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


Makarius___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] HOL-Proofs broken?

[Jasmin Blanchette]

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

[isabelle-dev] HOL-Proofs broken?

[Makarius]

My impression is that ebf296fe88d7 (blanchet) causes HOL-Proofs to run out 
of resources and fail.  I've made approx. 3 runs in the vicinity -- it 
always takes very long.


Is that another failure to do a full "isabelle build -a" before pushing 
anything?


I've actually violated this principle myself, and pushed a696414fa3a1 over 
it, which is a change of some Admin/isatest configuration, but that is a 
different story.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev