[isabelle-dev] HOL-Quickcheck_Benchmark timeouts
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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev