On 12/05/18 00:50, Makarius wrote: > On 10/05/18 00:10, Makarius wrote: >> >> In the past couple of weeks I have sporadically tried to work around >> this resource problem, but failed so far. >> >> The latest attempt is Isabelle/f6a22490cca8. As usual, it "works for me >> on my usual test machines", but there is a remaining chance of problems >> coming back on other configurations. > > So far this change looks good on various test machines with only 2 cores. > > 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 Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
