Hi again, Am 17.09.2014 um 11:40 schrieb Jasmin Christian Blanchette <jasmin.blanche...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
