[isabelle-dev] AFP: Session AVL-Trees broken

[Makarius]

On Thu, 8 Nov 2012, Gerwin Klein wrote:

> When I was testing, I was running sessions one at a time, not in 
> parallel, so I wouldn't have seen any issues with too many parallel jobs 
> or similar.
>
> Does anyone know what the timeout measures? Elapsed real time or time 
> spent on that session?

The timeout in Isabelle build is elapsed time and refers to each session 
separately.  In Isabelle/aaf276a28551 the isatest wrapper script sets a 
timeout for the regular Isabelle sessions -- they don't have one that is 
statically wired as in AFP.  Also note that the queue manager of isabelle 
build sorts jobs by the timeout, such that presumably longer ones come 
first.


> The afp test assumes it has the machine to itself and runs at 6:28 in 
> the morning. It should be finished after about 3h.

The situation is getting better, but is not resolved yet.  See the other 
thread about HOL-Quickcheck_Benchmarks: 
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg03443.html


 	Makarius