[isabelle-dev] Datatypes & Isatest failures

[Jasmin Christian Blanchette]

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