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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
