[isabelle-dev] HOL-Quickcheck_Benchmark timeouts
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
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".
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev