[isabelle-dev] Isabelle2013-2 release

Peter Lammich lammich at in.tum.de
Thu Nov 21 10:48:59 CET 2013


>From your description, this looks like a timeout-problem to me ... while
your machine is loaded by proving the theory, quickcheck times out.
After the edit, there is less load, and quickcheck is faster.

--
  Peter


On Do, 2013-11-21 at 10:40 +0100, Tobias Nipkow wrote:
> Am 20/11/2013 22:49, schrieb Makarius:
> > Are there any other potential problems of Isabelle2013-1 that were not reported
> > yet?
> 
> There is a problem with autoquickcheck in Isabelle/jedit. It sometimes fails to
> find or dislay a counterexample. I have a theory with a wrong lemma in it. When
> I load the theory, no counterexample is displayed. When I edit the theory such
> that that lemma needs to be rechecked, suddenly the counterexample is found.
> Afterwards it is always found reliably. The first time is the difficult time.
> 
> This is not easy to reproduce: if you just use "False" or "x=x", it will find a
> counterexample reliably. I have tried to create a short example but failed. I
> have noticed this some time ago, but was never sure if it was just a fluke. Now
> I have a collection of theories where it reproduces reliably.
> 
> Tobias
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





More information about the isabelle-dev mailing list