[isabelle-dev] HOL-Quickcheck_Benchmark timeouts

[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 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
infrastructure.

Tobias

> 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