[isabelle-dev] HOL-Proofs broken?
Jasmin Blanchette
jasmin.blanchette at inria.fr
Tue Oct 6 21:54:15 CEST 2015
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
More information about the isabelle-dev
mailing list