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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
