[isabelle-dev] HOL-Quickcheck_Benchmark timeouts

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

I can take care of that, but need an indication of what is the better 
tendency.


 	Makarius