[isabelle-dev] Regain AFP sanity
makarius at sketis.net
Wed Jan 11 23:15:22 CET 2012
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,
> 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
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
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.
> 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).
More information about the isabelle-dev