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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
