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.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
