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