[isabelle-dev] Isabelle2013-2 release
nipkow at in.tum.de
Thu Nov 21 11:03:07 CET 2013
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.
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.
> 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
>> 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.
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev