[isabelle-dev] HOL-Quickcheck_Benchmark timeouts

[Makarius]

On Sun, 16 Dec 2012, Lukas Bulwahn wrote:

>> If nothing happens, lets say until the last week of the year, I will 
>> start moving find_unused_assms to HOL/ex.
>> 
> Things have changed in 768a3fbe4149 and it solved the issue in 
> find_unused_assms.

Excellent -- it seems to work now.  In 9efc99c990d5 I have made this a bit 
more parallel, so that Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy 
takes approx. 45s on 4 or 8 cores.

Moving this to Quickcheck_Examples for continous testing made it much 
slower, though, probably due to pseudo-random numbers that become really 
random in parallel execution.  For the moment we better leave it like that 
(subject to condition=ISABELLE_FULL_TEST).


> Just for your information, it was due to a non-terminating code equation 
> for the vimage constant.
>
> The Codegenerator_Test session only checks if code is generated but not 
> if the executable equations make much sense, the find_unused_assm theory 
> complements that by actually executing a number of generated programs 
> and should not be dropped in the future if it ever breaks again. A 
> failure in this theory indicates some open issue in the code generation 
> process or setup.

OK.  It is always better to have a tiny repair by someone who understands 
the issue, instead of speculative actions by someone else.

Issue closed.  One less problem for the upcoming release.


 	Makarius