[isabelle-dev] HOL-Quickcheck_Benchmark timeouts

Tobias Nipkow nipkow at in.tum.de
Mon Dec 10 13:46:49 CET 2012

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 isatest failing on HOL-Quickcheck_Benchmark (now at least
> reliably with Interrupt, not Timeout), the situation is still unchanged in the
> repository (presently 0a740d127187).
> There are basically two possibilities:
>   (1) The critical changesets that were mentioned earlier on this thread
>     are backed out.  Thus find_unused_assms will work as before, but the
>     list_to_set_comprehension suffers again from the unknown problem that
>     was addressed here without saying explicitly what it was.
>   (2) The find_unused_assms command is put in some "experimental" corner,
>     e.g. HOL-ex, together with its documentation that is now in IsarRef.
>     Thus the user does not accidentally bomb his Isabelle session when
>     trying out the command on one of the critical theories that cause
>     problems with the HOL-Quickcheck_Benchmark session.

If (2) solves the problem, you should go for it. In contrast,
list_to_set_comprehension which is an important part of list comprehension


> I can take care of that, but need an indication of what is the better tendency.
>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

More information about the isabelle-dev mailing list