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