[isabelle-dev] Regain AFP sanity
krauss at in.tum.de
Wed Jan 11 21:29:14 CET 2012
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
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.
I hope that we can get further data on whether this is a repeatable
problem in the next days.
More information about the isabelle-dev