[isabelle-dev] Regain AFP sanity

[Alexander Krauss]

On 01/11/2012 03:40 PM, Makarius wrote:
> 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)

The AFP setup has the notion of "frequent" entries, which participate in 
more tests. Currently, exactly the two sessions above are excluded (but 
on the spot I can't remember if the nightly run at NICTA currently 
honors this flag... there have been some changes in the configuration).

In Mira, the frequent sessions form the "AFP_fast" configuration, which 
does have frequent and rather painless tests, cf. the second column of
http://isabelle.in.tum.de/reports/Isabelle (many failures recently, though).

So I am not sure if any additional ad-hoc proof skipping is so useful. 
Getting Flyspeck-Tame statistics once every few days should be ok, I 
guess...

The real problem is in fact JinjaThreads. AFAIK, the only machine at TUM 
where it can still build (in principle) is lxbroy10, but as Lukas 
pointed out there are still some failures, cf. 
http://isabelle.in.tum.de/reports/Isabelle/report/628b2a4bd3f94f478b929b72f811c5af. 
I hope that we can get further data on whether this is a repeatable 
problem in the next days.

Alex