[isabelle-dev] status (AFP)

[Gerwin Klein]

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 <kleing at cse.unsw.edu.au> wrote:

> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>