[isabelle-dev] HOL-Quickcheck_Benchmark timeouts

Lukas Bulwahn bulwahn at in.tum.de
Sun Dec 16 20:03:35 CET 2012

On 12/11/2012 10:27 PM, Makarius wrote:
> On Mon, 10 Dec 2012, Makarius wrote:
>> On Fri, 30 Nov 2012, Lukas Bulwahn wrote:
>>> It must be considered unmaintained. The benchmarks themself I will 
>>> irregularly have time on weekends and nights to have a look, but I 
>>> cannot keep up with "Isabelle roaring ahead".
>> After several weeks of isatest failing on HOL-Quickcheck_Benchmark 
>> (now at least reliably with Interrupt, not Timeout), the situation is 
>> still unchanged in the repository (presently 0a740d127187).
> In Isabelle/d466ebc27810 isatest is silenced for now, to give Lukas a 
> window of opportunity to make up his mind.  Note that src/HOL/ROOT has 
> other quickcheck tests commented out for a long time already.
> 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 

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.

If other problems occur, I am willing to help whenever I can. However as 
I left Garching, it takes some time to address those issues.
Makarius, thanks for your patience and your work bisecting the cause of 
the failure.


More information about the isabelle-dev mailing list