On 28/07/18 22:09, Makarius wrote: > On 12/05/18 00:50, Makarius wrote: >> On 10/05/18 00:10, Makarius wrote: >> >> In Isabelle/a8f40dd73c61 I have made the parallelism a little bit more >> ambitious, and keep watching resulting performance charts at >> https://isabelle.sketis.net/devel/build_status >> >> All this are just workarounds to get back into a situation where all >> sessions work routinely most of the time. > > The spurious problems with HOL-Proofs have remained open over some > months, despite a lot of tinkering. I have now taken another close look > at it: it appears that the situation with a few % CPU usage is due to > worker threads waiting for futures joined by other threads: some kind of > deadlock/livelock. > > The following changes make this more robust, and right now it appears to > work properly: > > https://isabelle.sketis.net/repos/isabelle-release/rev/6ee53660a911 > https://isabelle.sketis.net/repos/isabelle-release/rev/be936cf061ab
It looks like the problem mostly under control now: https://isabelle.sketis.net/devel/build_status/index.html has only one spurious failure of HOL-Proofs left, on a rather underpowered Macbook. So for the purpose of Isabelle2018 I call this thread closed. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
