[isabelle-dev] HOL-Quickcheck_Benchmark timeouts

[Lukas Bulwahn]

On 11/29/2012 10:22 PM, Makarius wrote:
> On Thu, 29 Nov 2012, Makarius wrote:
>
>> I've also started some bisection about where the problem comes from, 
>> without any clear results so far, but I will report more a bit later.
>
> I've spent a few more hours on the problem, repeating the bisection 
> several times, and staring add various changesets that are not at all 
> clear from their text.
>
>
> This is the result:
>
> 50e457bbc5fe bulwahn GOOD
> 6a26fed71755 bulwahn SKIP (BAD)
> 28cd3c9ca278 bulwahn SKIP (BAD)
> fb696ff1f086 bulwahn BAD
>
> Due to skipped revisions, the first bad revision could be any of:
> changeset:   49943:6a26fed71755
> user:        bulwahn
> date:        Sat Oct 20 09:09:32 2012 +0200
> summary:     passing names and types of all bounds around in the simproc
>
> changeset:   49944:28cd3c9ca278
> user:        bulwahn
> date:        Sat Oct 20 09:09:33 2012 +0200
> summary:     tuned tactic in set_comprehension_pointfree simproc to 
> handle composition of negation and vimage
>
> changeset:   49945:fb696ff1f086
> user:        bulwahn
> date:        Sat Oct 20 09:09:34 2012 +0200
> summary:     adjusting proofs
>
>
> And here some explanation reconstructed from the investigations with 
> some guesswork, glossing over the the unexplained things in these 
> changesets.
>
> (1) BAD means the following crash:
>
> theory A imports Main
> begin
>
> find_unused_assms Fun
>
> Warning - Unable to increase stack - interrupting thread
>
> Exception trace for exception - Interrupt
> Generated_Code.value(1)(1)(1)(1)(2)
> Generated_Code.check_all_subsets(4)(1)
> Exhaustive_Generators.compile_generator_expr(2)compile-(1)(1)(1)(1)(1)
> Exhaustive_Generators.compile_generator_expr(2)(1)(1)
> Quickcheck_Common.test_term_with_cardinality(5)test_card_size(4)
> Quickcheck_Common.test_term_with_cardinality(5)test(2)
> Quickcheck_Common.test_term_with_cardinality(5)
> Quickcheck_Common.generator_test_goal_terms(5)
>
>
> (2) SKIP means these changesets were broken: HOL did not compile. 
> Backporting the "adjusting proofs" changeset fb696ff1f086, revealed 
> that they were BAD, too.
>
> Note that it does not make any sense to publish changesets where Pure 
> or HOL do not compile.  There is no obligation to have all session OK 
> all the time before pushing, but the usefulness of changesets is 
> greatly diminished.  Someone else needs to spend much more time in 
> exchange for the 2-3 minutes saved in not running HOL on the spot, 
> before saying "hg commit".  (I usually do a full "isabelle build -a" 
> before *any* commit.) And of course, there is an obligation to run 
> full "isabelle build -a" (or a proven equivalent) before any push.
>
>
> (3) Looking at the critical change 6a26fed71755 "passing names and 
> types of all bounds around in the simproc" several times, I tried to 
> understand why it affects the generated quickcheck code in such a bad 
> way. (The changelog merely repeats the diff in English prose as a 
> "parrot".)
>
> So after backing-out this single-line change from 5a1194acbecd of 
> today, everything worked fine except for 
> src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy crashing as follows:
>
> *** Wellsortedness error
> *** (in code equation Set_Comprehension_Pointfree_Tests.union ?a ?b == 
> {x. x : ?a | x : ?b}):
> *** Type nat not of sort enum
> *** No type arity nat :: enum
> *** At command "export_code" (line 134 of 
> "~~/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy")
>
> Looking in the vicinity of the many other changes related to the 
> critical three above reveals the following:
>
> changeset:   49947:29cd291bfea6
> user:        bulwahn
> date:        Sat Oct 20 09:09:37 2012 +0200
> files:       src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy
> description:
> adding another test case for the set_comprehension_simproc to the 
> theory in HOL/ex
>
> So here one could guess from the greater context that 6a26fed71755 
> with its SKIP (BAD) status was motivated by a problem with passing 
> sort information down to the generated code.  Since this is the 
> "exhaustive" quickcheck tester, having "nat :: enum" or not could make 
> a difference in the amount of enumeration done here.
>
> So "BAD" might actually mean "better" in the sense of more exhaustive, 
> but it breaks down the concrete application of find_unused_assms 
> nonetheless.
>
> Another side remark: Isabelle does not have a tradition for "test 
> cases" and "unit tests".  What we usually made in all these decades 
> were some half-decent applications to explore tools or some stylized 
> examples to show the main points.  These then also serve as a tests 
> somehow. (There is sometimes the odd situation that some manual or 
> "test" theory is the only spot where certain features of certain tools 
> occur, which means there is lack of proof for practical relevance.  
> I've seen this again just today in a different situation that is 
> unrelated to this incident.)
>
>
> Anyway, maybe Lukas himself or codegen export Florian knows how to 
> resolve the situation.
>
I could have time on the weekend to have a closer look again.
The time when these changesets were pushed was rather bad, as at that 
time you were on vacation and not forseeing these bad things (as you 
usually do), mira worked irregularly, the AFP was broken for quite some 
time and various different reasons, and I rushed to change some behavior 
of the simplifier in HOL.


Lukas
> Once the HOL-Quickcheck-Benchmark session is up and running again, I 
> would like to apply some trivial changes to make it properly run in 
> parallel. Then it should become part of the normal build, not under 
> condition ISABELLE_FULL_TEST.  This saves time in manuel re-testing 
> along the history, which mira is better at.
>
>