[isabelle-dev] HOL-Quickcheck_Benchmark timeouts
makarius at sketis.net
Thu Nov 29 18:27:04 CET 2012
On Mon, 26 Nov 2012, Makarius wrote:
> In the past few weeks, we've had isatest problems with
> HOL-Quickcheck_Benchmark and ISABELLE_FULL_TEST=true (as used with
> mac-poly64-M4 and mac-poly64-M8).
> After some experimentation and tinkering, it seems that the timeouts in
> Isabelle/978200ae8473 from last Friday work: we've had successful isatest
> runs over the weekend.
> As far as I can see, the tests on macbroy2 terminate around 05:30 CET.
> This might be relavant for later tests of AFP.
That was too optimistic. It seems that find_unused_assms uses a lot of
stack space, and thus fills up memory on x86_64. I've addressed this in
f25bcb8a4591 to get more explicit failure.
I've also started some bisection about where the problem comes from,
without any clear results so far, but I will report more a bit later.
Is Lukas Bulwahn still looking after his stuff, or is this now
More information about the isabelle-dev