[isabelle-dev] status (AFP)
kleing at cse.unsw.edu.au
Sat Sep 29 03:57:59 CEST 2012
On 21/09/2012, at 9:31 PM, Makarius <makarius at 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.
More information about the isabelle-dev