[isabelle-dev] AFP: Session AVL-Trees broken
makarius at sketis.net
Mon Dec 3 10:52:31 CET 2012
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
> 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:
More information about the isabelle-dev