[isabelle-dev] Quickcheck Examples

[Makarius]

On Fri, 20 Apr 2012, Lukas Bulwahn wrote:

> On 02/27/2012 02:31 PM, Makarius wrote:
>> 
>> The process is running with approx. 100-200% most of the time, which is 
>> neither sequential nor fully parallel.  Probably you merely benefit from 
>> theory parallelism, not from more fine-grained Par_List things that could 
>> be used in your own code.
>> 
>> One potential source of problems is the pseudo-random generator, with 
>> its global state.  There have been funny effects in the past that might 
>> have come back in one form or the other, even though random generators 
>> have been changed several times.
>> 
>> Anyway, how long does the session run on "your laptop"?
>> 
> I have not noticed that non-termination on my laptop when checking my 
> changesets.
> Also with the setting mentioned above, I could not reproduce the 
> non-terminating behaviour on macbroy2 with changesets baf90cb2a606.
>
> I will continue testing Quickcheck-Examples to see if it only occurs 
> infrequently.

My observation on 27-Feb-2012 was still very crude, I've updated that in a 
private mail on 16-Mar-2012.

In particular, "nontermination" means "termination after 1-2 hours", and 
it is independent of parallelism:

http://isabelle.in.tum.de/devel/stats/at-poly/HOL-Quickcheck_Examples.png
http://isabelle.in.tum.de/devel/stats/mac-poly-M4/HOL-Quickcheck_Examples.png

The isatest settings are in Admin/isatest/settings/.


 	Makarius