[isabelle-dev] Datatypes & Isatest failures

[Jasmin Christian Blanchette]

Hi again,

Am 17.09.2014 um 11:40 schrieb Jasmin Christian Blanchette <jasmin.blanchette at gmail.com>:

> 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".

It doesn't seem like "subst_tac" had anything to do with it. I still have no idea about what made "HOL-Proofs" slower on "at-poly-e" beween September 13 and 14. The log reveals nothing special, except a truncation at the end. (while processing "Predicate.thy"). My personal inclination would be to disable this test for this platform -- "HOL-Proofs" isn't exactly used by many people, and I'm not sure there's much value in running CPUs for 1 hour each night to test it on some slow hardware and old version of Poly/ML (5.3).

I see the following options as relatively painless ways of solving this:

1. Increase the timeout from 3600 s to, e.g. 4800.

2. Make "HOL-Proofs" and dependencies "ISABELLE_FULL_TEST".

3. Introduce another condition to control whether "HOL-Proofs" should be built.

Does anybody have an opinion?

Jasmin