[isabelle-dev] Deadlock while building HOL-Proof

Makarius makarius at sketis.net
Sat Jul 28 22:09:03 CEST 2018

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

The following changes make this more robust, and right now it appears to
work properly:



More information about the isabelle-dev mailing list