[isabelle-dev] Regain AFP sanity

Tobias Nipkow nipkow at in.tum.de
Wed Jan 11 17:42:58 CET 2012

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


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.

More information about the isabelle-dev mailing list