On 21/09/2012, at 9:31 PM, Makarius <makar...@sketis.net> wrote: > On Fri, 21 Sep 2012, Tobias Nipkow wrote: > >> This is just another reminder that people should watch the AFP when they >> check in changes, and fix them. The testboard runs most of the AFP. > > Once the testboard recovers, one could make this a bit more complete. I > usually have FLYSPECK_SKIP_PROOFS=true in my settings and then run *all* of > AFP in 35min on a plain-old 8-core workstation. > > The new Isabelle build configuration has the "condition" option to formalize > the omission of theories, depending on given environment variables. > ISABELLE_FULL_TEST (undefined by default) is already used as a convention to > guard extra tests that take unusually long time. > > If ISABELLE_FULL_TEST would be checked instead of FLYSPECK_SKIP_PROOFS in > afp/thys/Flyspeck-Tame/ArchComp.thy with the inverted meaning, then one could > discontinue the AFP vs. AFP_big distinction. It would work for everyone by > default within the range of 0.5 .. 2h total. > > The full test would then be run infrequently by one of the standard test > frameworks in the background.
I managed to miss this email until Tobias pointed me to it. I think this is a good idea and will have a look at rejigging the AFP build accordingly in the next few days. Cheers, Gerwin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
