[isabelle-dev] status (AFP)

[Gerwin Klein]

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.

Cheers,
Gerwin