[isabelle-dev] Datatypes & Isatest failures
florian.haftmann at informatik.tu-muenchen.de
Thu Sep 25 10:41:53 CEST 2014
> 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".
Definitely not. HOL-Proofs is am important indicator whether something
got utterly wrong in handling of thm values in Pure. (Or would you like
JinjaThreads depend on ISABELLE_FULL_TEST also ;-)?)
> 3. Introduce another condition to control whether "HOL-Proofs" should be built.
The pain of introducting another condition seems bigger to me than to
raise the timeout.
> Does anybody have an opinion?
So, (1) is my opinion.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 181 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev