>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 > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
