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,
Collections.
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
at least.
@Alex:
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.
@all:
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.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
