[isabelle-dev] Datatypes & Isatest failures

[Jasmin Christian Blanchette]

Hi all,

The good news is that the port to the new datatypes have been overall a success. There are only a handful of "old_datatype"s left in the AFP, and they will go away as soon as Dmitriy gets a chance to fix a bug in his code (presumably once he's back from vacation). Also good news: Timing information as I could see it show no big impact on the AFP, e.g. JinjaThread. Although the new package is much more efficient in its handling of nested recursion, it is generally heavier due to its reliance on local theories and on the BNF composition pipeline -- thankfully not too much heavier, as far as I could tell so far.

The bad news is that we've been experiencing Isatest failures since then. Let me classify them:

1. "HOL-Proofs" times out since September 14 on "at-poly-e". On September 13, we had

    Timing HOL-Proofs (2 threads, 3161.882s elapsed time, 2889.329s cpu time, 840.167s GC time, factor 0.91)
    Finished HOL-Proofs (0:54:37 elapsed time, 0:48:53 cpu time, factor 0.89)

which is close to the timeout (1 hour, I believe) but not *that* close. Still, the failures on September 14, 15, 16, and 17 have been consistent enough to suggest that change be0f5d8d511b (the only relevant one between Sept. 13 and 14) is the cause, in which case I have a strong suspicion about "subst_tac". I will investigate. Yesterday I tried something, but it had no effect. Due to the "liveness" flavor of the bug, it may still take some rounds to nail it down. (Building "HOL-Proofs" takes 4.5 minutes on my laptop, so it's not as if I could easily reproduce the problem locally.)

2. "HOL-Datatype_Examples" causes random problems on random platforms. Today there was a timeout on "at-poly-e", which I cannot really explain.

3. Freak errors, e.g. crash in "HOL-Decision_Procs". These appear unrelated to my changes, and we had those before already.

Bottom line: I'm working on it. If you have ideas/suggestions on how to help this converge faster, please let me know.

Jasmin