[isabelle-dev] Deadlock while building HOL-Proof

[Makarius]

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