[isabelle-dev] HOL-Quickcheck_Benchmark timeouts
makarius at sketis.net
Tue Dec 11 22:27:38 CET 2012
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 failing on HOL-Quickcheck_Benchmark (now at
> least reliably with Interrupt, not Timeout), the situation is still unchanged
> in the repository (presently 0a740d127187).
In Isabelle/d466ebc27810 isatest is silenced for now, to give Lukas a
window of opportunity to make up his mind. Note that src/HOL/ROOT has
other quickcheck tests commented out for a long time already.
If nothing happens, lets say until the last week of the year, I will start
moving find_unused_assms to HOL/ex.
More information about the isabelle-dev