[isabelle-dev] Isabelle2013-2 release

[Tobias Nipkow]

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
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>