[isabelle-dev] HOL-Quickcheck_Benchmark timeouts

[Makarius]

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 
unmaintained?


 	Makarius