Re: [isabelle-dev] HOL-Quickcheck_Benchmark timeouts

2012-12-17 Thread Makarius
On Sun, 16 Dec 2012, Lukas Bulwahn wrote: If nothing happens, lets say until the last week of the year, I will start moving find_unused_assms to HOL/ex. Things have changed in 768a3fbe4149 and it solved the issue in find_unused_assms. Excellent -- it seems to work now. In 9efc99c990d5 I

Re: [isabelle-dev] HOL-Quickcheck_Benchmark timeouts

2012-12-16 Thread Lukas Bulwahn
On 12/11/2012 10:27 PM, Makarius wrote: On Mon, 10 Dec 2012, Makarius wrote: On Fri, 30 Nov 2012, Lukas Bulwahn wrote: 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

Re: [isabelle-dev] HOL-Quickcheck_Benchmark timeouts

2012-12-11 Thread Makarius
On Mon, 10 Dec 2012, Makarius wrote: On Fri, 30 Nov 2012, Lukas Bulwahn wrote: 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. After several weeks of isatest

Re: [isabelle-dev] HOL-Quickcheck_Benchmark timeouts

2012-12-10 Thread Makarius
On Fri, 30 Nov 2012, Lukas Bulwahn wrote: 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. After several weeks of isatest failing on HOL-Quickcheck_Benchmark (now

Re: [isabelle-dev] HOL-Quickcheck_Benchmark timeouts

2012-12-10 Thread Tobias Nipkow
Am 10/12/2012 13:38, schrieb Makarius: On Fri, 30 Nov 2012, Lukas Bulwahn wrote: 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. After several weeks of

Re: [isabelle-dev] HOL-Quickcheck_Benchmark timeouts

2012-11-29 Thread 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

Re: [isabelle-dev] HOL-Quickcheck_Benchmark timeouts

2012-11-29 Thread Makarius
On Thu, 29 Nov 2012, Makarius wrote: 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. I've spent a few more hours on the problem, repeating the bisection several times, and staring add various

Re: [isabelle-dev] HOL-Quickcheck_Benchmark timeouts

2012-11-29 Thread Lukas Bulwahn
On 11/29/2012 10:22 PM, Makarius wrote: On Thu, 29 Nov 2012, Makarius wrote: 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. I've spent a few more hours on the problem, repeating the bisection several

Re: [isabelle-dev] HOL-Quickcheck_Benchmark timeouts

2012-11-29 Thread 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

[isabelle-dev] HOL-Quickcheck_Benchmark timeouts

2012-11-26 Thread Makarius
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