[isabelle-dev] AFP tests timing out

[Makarius]

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