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.blanche...@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-...@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
