[isabelle-dev] Regain AFP sanity
makarius at sketis.net
Wed Jan 18 21:55:32 CET 2012
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
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.
More information about the isabelle-dev