On 10/03/18 11:06, Makarius wrote: > On 08/03/18 13:08, Makarius wrote: >> >>> Since David Matthews has make a lot of changes concerning fine-points of >>> heap management in the past few months, I would like to test it with >>> some Poly/ML repository version. But this does not build on macOS at the >>> moment. >> >> I will continue with the investigations here. > > I have now tested it with various experimental versions of Poly/ML: the > problem persists. > > Looking more closely at the ML statistics of the process (after killing > it) reveals that the ML world is fine and active, only my future thread > farm is somehow blocked. > > This indicates that the problem is in my area of responsibility.
In the past couple of weeks I have sporadically tried to work around this resource problem, but failed so far. The latest attempt is Isabelle/f6a22490cca8. As usual, it "works for me on my usual test machines", but there is a remaining chance of problems coming back on other configurations. Overall, my guess is that the Poly/ML parallel GC vs. Isabelle/ML future thread management somehow get into trouble, due to massive resource requirements in parallel HOL-Proofs with a sudden spike of approx. 50000 futures that require a lot of memory. Even x86_64 does not really help. In a sense, it is just the normal situation "invisible concrete wall ahead" -- we've that had occasionally in the past 10-20 years. It is a reminder that scaling is not for free, but explicit efforts are required for it. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev