[isabelle-dev] testboard stuck?

[Makarius]

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...
> 
> Tobias
> 
> On 01/08/2020 11:15, Lawrence Paulson wrote:
>> Run #347 (with one slightly modified lemma) also aborted, in a different place:
>>
>>> 21:50:01 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Weakening
>>> 21:52:04 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class2
>>> 21:52:06 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class3
>>> 23:42:11 Build timed out (after 180 minutes). Marking the build as aborted.
>>> 23:42:11 Build was aborted
>>
>> What could be going on?
>>
>> Larry

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.


	Makarius