[isabelle-dev] Regain AFP sanity

[Makarius]

On Thu, 19 Jan 2012, Gerwin Klein wrote:

> The AFP test should now be running on macbroy2, starting each day at 
> 6:28am. We will see the next few days if it works..
>
> It is currently doing the full run each day which takes about 10:30h. 
> Please let me know if this interferes with anything, I'm not sure who 
> else is using the machine when.

Since you mean 10:30 hours, not until 10:30 a.m. it is wasting a lot of 
cycles of the fastest machine at TUM. Even though macbroy2 is not heavely 
used recently, I can imagine that some people might want to run some quick 
tests occasionally during daytime, especially since lxbroy10 is broken 
again.

Moreover, an isatest that competes with other sessions during daytime will 
produce ininformative statistics, like the NICTA one.

This is exactly why I've added the FLYSPECK_SKIP_PROOFS=true mode in 
AFP/3dcc6b9eae2b in the first place, to re-enable AFP isatest on macbroy2 
without adverse effects.

BTW, this versions merely skips the really slow proofs of same4, same5, 
same6, but runs the fast one of same3 unconditionally.  Superficially this 
looks like a reasonable test.  Or is their significant information gained 
from attempting the slow proofs as well (say once a week or once a month)? 
Tobias should be able to say more about it.


 	Makarius