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 <l...@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.


isabelle-dev mailing list

Reply via email to