> 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