[isabelle-dev] HOL-Quickcheck_Benchmark timeouts
makarius at sketis.net
Mon Dec 17 16:16:58 CET 2012
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
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.
More information about the isabelle-dev