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.


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

Reply via email to