[isabelle-dev] Isabelle build only works in certain directories

[Makarius]

On 28/06/18 16:07, Lawrence Paulson wrote:
> My last email was premature, because the exact same thing happened again: it hung at 2:15 minutes of CPU time. Fortunately I was able to kill it and retry, and thanks to multithreading, you don't have to wait anything like two minutes before reaching the two minute mark.
> 
>> On 28 Jun 2018, at 14:58, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
>>
>> I wonder whether this relates to the problem I have seen from time to time, where the build process "goes to sleep" around two minutes into building HOL. It's reproducible enough that I can feel confident that HOL will build only when the activity monitor shows that the process has consumed at least three minutes of CPU time. But I haven't seen it for a couple of weeks. 

I guess that it is related to the HOL-Proofs multithreading problems,
we've seen in the past few months (especially on threads=2).

I will try to take a deeper look at it again, in the coming weeks before
the Isabelle2018 release.

At the bottom of it, there might be some delicate point in Poly/ML, but
it could be also just in the Isabelle/ML Concurrent modules.


	Makarius