[isabelle-dev] Fwd: status (AFP)

[Makarius]

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.


 	Makarius