[isabelle-dev] HOL-Quickcheck_Benchmark timeouts

Makarius 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 mailing list