[isabelle-dev] testboard stuck?

[Makarius]

On 03/08/2020 13:33, Makarius wrote:
> On 01/08/2020 13:24, Tobias Nipkow wrote:
>> I suspect that is not of your making. Poly/ML, OS and even the hardware come
>> to mind...
>>
>> On 01/08/2020 11:15, Lawrence Paulson wrote:
>>> Run #347 (with one slightly modified lemma) also aborted, in a different place:
> 
> There might be even changes in timing due to hot temperatures outside.
> 
> But I've seen such spurious "hangs" occasionally, approx. in the past 12
> months. It might be due to subtle changes in how parallel proofs and proof
> terms are managed. I am in the process to investigate it further: luckily
> there is a mostly reproducible situation on a Mac Mini provided by EPFL.

In the meantime I have made a few changes towards a more robust situation,
notably:


changeset:   72078:b8d0b8659e0a
user:        wenzelm
date:        Wed Jul 29 14:23:19 2020 +0200
files:       src/Pure/Concurrent/future.ML
description:
more robust scheduler shutdown, notably for spurious crashes;

This could lead to problems with $HOME/.polyml filled up with odd
poly-stats-xyz files. It it advisable to clean up home directories to get rid
of such garbage. (I will see how to avoid it in the future.)


changeset:   72085:41e1e2395a67
user:        wenzelm
date:        Wed Aug 05 16:16:37 2020 +0200
files:       src/Pure/Concurrent/future.ML
description:
avoid exhaustion of worker threads, notably due to complex interaction of
future/promise/lazy in Proofterm.make_thm_node;

This was seen on laramac01 (EPFL) with isabelle build -o threads=4
HOL-Complex_Analysis


	Makarius