Some such effects may indeed play a role, although I originally did not observe it when reloading a theory but while editing an existing theory.
Thanks Tobias Am 21/11/2013 10:48, schrieb Peter Lammich: >>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 > _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
