[isabelle-dev] status (AFP)
kleing at cse.unsw.edu.au
Thu Oct 4 01:16:28 CEST 2012
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.
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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev