[isabelle-dev] HOL-Proofs broken?

Tue Oct 6 22:03:41 CEST 2015

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 <jasmin.blanchette at inria.fr> 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev