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.
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.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
