[isabelle-dev] AFP tests timing out
makarius at sketis.net
Mon Jul 16 11:58:55 CEST 2012
On Mon, 16 Jul 2012, Lukas Bulwahn wrote:
> Hi all,
> for about one month now, we are continuously seeing the AFP tests failing on
> various entries because of timeouts, e.g. AVL-Trees, Regular-Sets,
> To my knowledge, the entries have not changed. So the timeouts seem to be
> caused by recent changes in the Isabelle system itself.
Just one data point in the dark: Isabelle/94a7dc2276e4 and
AFP/4043c38305a3 should work, according to what I see in my local
nohup.out files this morning (based on various manual runs yesterday).
I can't say anything about the last 6 weeks where isatest was mostly not
working, and I was myself on vacation or conferencing. So we have a long
blind spot in the continous performance measurements that we've had since
about 2007. Thanks to Gerwin isatest has recovered in the past few days
> Could you provide graphs of the runtime for the AFP of the last few weeks to
> identify the possibly critical changesets?
I am still hoping for such graphs from mira. When this is working, we can
start to dismantle isatest.
> Are there some educated guesses what could have changed the performance on
> all these theories?
> Should we ignore the performance drop and simply increase the timeouts on
> these sessions?
Once performace is "lost" without knowing the reasons, it is hard to get
it back. Cumulatively it results in bloat and degrading system quality.
So one should make some efforts to find out now.
More information about the isabelle-dev