[isabelle-dev] HOL-Quickcheck_Benchmark timeouts

Lukas Bulwahn bulwahn at in.tum.de
Fri Nov 30 00:12:46 CET 2012

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".


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

More information about the isabelle-dev mailing list