This is now done, AFP_big has been retired, and afp_build updated accordingly.
I've removed all occurrences of FLYSPEC_SKIP_PROOFS in isatest and afptest, but I'm not sure if it is used in Mira anywhere. It should be fail safe, but should be cleaned up. Cheers, Gerwin On 29/09/2012, at 11:57 AM, Gerwin Klein <kle...@cse.unsw.edu.au> wrote: > 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 > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
