[isabelle-dev] Deadlock while building HOL-Proof

[Makarius]

On 03/03/18 12:09, Clemens Ballarin wrote:
> While building HOL-Proof I observe a deadlock, usually after 13 min CPU
> time.  It can be worked around with ISABELLE_BUILD_OPTIONS="threads=1". 
> The deadlock occurs most of the time.  The earliest changeset I was able
> to reproduce this with is
> 
>   changeset:   67675:738f170f43ee
>   user:        paulson <lp15 at cam.ac.uk>
>   date:        Tue Feb 20 09:34:03 2018 +0000
>   summary:     Merge

> The deadlock happens on a MacBook Pro:
>
>   macOS 10.13.3 (17D102)
>   2,7 GHz Intel Core i5
>   8 GB 1867 MHz DDR3

Thanks for keeping an eye on such details and for exploring the history
already.

Since HOL-Proofs fails occasionally, especially on underpowered
hardware, I did not take recent failures of it seriously. Looking more
closely at the build_log test database, I see that from 5a1b299fe4af to
0cd2fd0c2dcf (pull_date 19/20-Feb-2018) there is a change from normal
failure to timeout. It could be due to lazy locale facts and the new
(parallel) Thm.consolidate_theory operation.

I will investigate this further and try to isolate the actual problem.


	Makarius