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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
