Hi Florian,
Thanks for your input.
>> 1. Increase the timeout from 3600 s to, e.g. 4800.
[...]
> So, (1) is my opinion.
Unfortunately, that didn't do the trick (cf. 7f30ec82fe40, e4d540c0dd57).
Judging from the log file, it would appear to me that it's an instance of
multithreading divergence, as we have sometimes witnessed. The last theory
being loaded is also the main one ("Old_Datatype.thy", loaded right after
"Main.thy" now for "HOL-Proofs.thy" -- or "Main.thy" until one week ago.) The
very last timing information is about some lemmas that are quite early in the
dependency graphs (e.g. in "Hilbert_Choice.thy"). The last timings look
reasonable, i.e. milliseconds.
Change be0f5d8d511b still appears to have been the one that triggered the issue
-- unless there has been some hardware or software changes on the server on the
same day. In principle, it should change nothing for "Main" -- it is
generalizing some code so that recursion is possible through phantom type
variables, as necessary for Imperative HOL.
Jasmin
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
