> 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.
Could be.
> 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.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
