[isabelle-dev] Regain AFP sanity

[Tobias Nipkow]

This is the wrong way around. The AFP must contain the real thing that
can be tweaked with some shell variable to skip certain parts. Not the
other way around: the user has to do something special to get the right
behaviour.

Tobias

Am 11/01/2012 15:40, schrieb Makarius:
> Dear all,
> 
> we've already got used to somewhat awkward AFP tests with many variants
> of failures and uninformative statistics like this random noise
> http://isabelle.in.tum.de/devel/stats/afp.html
> 
> 
> The problem seems to boil down to the two really big sessions, because
> they prevent frequent painless testing:
> 
>   Flyspeck-Tame (approx. 6-9h runtime)
>   JinjaThreads (approx. 1-2h runtime, up to 32 GB memory)
> 
> Big applications are not a problem as such, but we should make an effort
> to regain some sanity in everyday testing.  If isatest is moved back to
> a predicable machine like macbroy2 we could get back to useful
> statistics for big applications as well.
> 
> 
> To make a start, the included changeset for Flyspeck-Tame reduces the
> total runtime to a few minutes, while still doing some meaningful tests.
> To refine this, one could easily make a private version of the "eval"
> method in theory ArchComp that depends on an external environment
> variable like "AFP_FULL_TEST" to control this.  That setting would then
> be off by default, but enabled in certain isatest/mira runs.
> 
> For JinjaThreads we will have to spend much further thoughts, though ...
> 
> 
>     Makarius
> 
> 
> This body part will be downloaded on demand.