[isabelle-dev] Regain AFP sanity

[Makarius]

On Wed, 11 Jan 2012, Alexander Krauss wrote:

> 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...

We have here a mixture of several old and new attempts to approximate some 
testing and performance mesasurement.  I don't mind to see more of Mira, 
say some nice statistics and graph plotting of its more fine-grained 
results, but right now I am still stuck with the plain old 
http://isabelle.in.tum.de/devel/stats/ view (which I am checking every 
day).

What we really need is useful AFP statistics again, like 
http://isabelle.in.tum.de/devel/stats/afp.html was until a year ago or so.

Gerwin should be able to do some very basic tinkering with 
FLYSPECK_SKIP_PROOFS=true for a classic AFP isatest on macbroy2, for 
example.  (He said it was discontinued when the whole bunch of tests on 
macbroy2 had exceeded a whole day.)


> 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.

I am running JinjaThreads routinely on a regular workstation (8 cores, 32 
GB), say during lunch-time.

I've recently entertained myself to see how Isabelle/Scala/jEdit fares 
with JinjaThreads, but not everything is settled yet. With a few more 
rounds of timing and profiling we should eventually see where the 
resources go (like was done so many times over the years to re-adjust to 
the natural inflation of applications).


 	Makarius