[isabelle-dev] HOL-Quickcheck_Benchmark timeouts

[Lukas Bulwahn]

On 11/29/2012 06:27 PM, Makarius wrote:
> 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?
>
>
It must be considered unmaintained. The benchmarks themself
I will irregularly have time on weekends and nights to have a look, but 
I cannot keep up with "Isabelle roaring ahead".

Lukas

>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>