[isabelle-dev] Regain AFP sanity

[Gerwin Klein]

Yes, the default needs to be the full run. That shouldn't be hard to change, though.

I'm happy to move the AFP test back to Munich, we'll soon reach saturation on the test server here, and a dedicated machine will give less noise on performance data.

Which machine should I run it on?

Cheers,
Gerwin


On 12/01/2012, at 3:42 AM, Tobias Nipkow wrote:

> 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
> behaviour.
> 
> Tobias
> 
> 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.
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>