[isabelle-dev] Pow

[Alexander Krauss]

Makarius wrote:
>> The culprit seems to be f3f0e20923a7, which changed the semantics of 
>> take and drop with negative indices. Errors in find theorems are not 
>> caught by the usual regression tests, unfortunately...
>>
>> changeset:   34059:f3f0e20923a7
>> user:        haftmann
>> date:        Wed Dec 09 21:38:12 2009 +0100
>> summary:     take and drop as projections of chop
> 
> So how did you find out?  Probably via "hg bisect" as usual 

Well, in fact I just guessed, and tested my hypothesis. But if guessing 
does not work, I do use bisect...

>-- but I 
> reckon that more than half of the readers of this list have never used 
> this indispensible tool of Mercurial so far.

For those who are interested, the transcript below shows how "hg
bisect" can be used to find the source of the problem by binary
search.

# Reset bisect state

krauss at lapbroy38:~/wd/isabelle/src/HOL$ hg bisect -r

# update to known-good revision and mark as good (-g)

krauss at lapbroy38:~/wd/isabelle/src/HOL$ hg up a03f3f9874f6
51 files updated, 0 files merged, 2 files removed, 0 files unresolved

krauss at lapbroy38:~/wd/isabelle/src/HOL$ hg bisect -g

# update to known-bad revision and mark as bad (-b)

krauss at lapbroy38:~/wd/isabelle/src/HOL$ hg up ada58d813783
42 files updated, 0 files merged, 1 files removed, 0 files unresolved

krauss at lapbroy38:~/wd/isabelle/src/HOL$ hg bisect -b
Testing changeset 34066:23407a527fe4 (24 changesets remaining, ~4 tests)
26 files updated, 0 files merged, 2 files removed, 0 files unresolved

# hg has picked a changeset to test, so we compile HOL-Plain and try the 
search

krauss at lapbroy38:~/wd/isabelle/src/HOL$ isabelle make HOL-Plain
[...]
Finished HOL-Plain (0:01:46 elapsed time, 0:02:06 cpu time, factor 1.18)
krauss at lapbroy38:~/wd/isabelle/src/HOL$ isabelle tty -l HOL-Plain
 > val it = () : unit
val commit = fn : unit -> bool
Unofficial version of Isabelle/HOL-Plain (unidentified repository version)
 > theory Test imports Plain begin;
theory Test
 > find_theorems Pow;
searched for:
    "Pow"

nothing found in 0.040 secs
 > quit;

# It did not work, so mark as bad:
krauss at lapbroy38:~/wd/isabelle/src/HOL$ hg bisect -b
Testing changeset 34062:050bc943d9ba (13 changesets remaining, ~3 tests)
13 files updated, 0 files merged, 0 files removed, 0 files unresolved

# Same again, with another changeset, again chosen automatically by hg:

krauss at lapbroy38:~/wd/isabelle/src/HOL$ isabelle make HOL-Plain
[...]
Finished HOL-Plain (0:02:24 elapsed time, 0:02:06 cpu time, factor 0.87)
krauss at lapbroy38:~/wd/isabelle/src/HOL$ isabelle tty -l HOL-Plain
 > val it = () : unit
val commit = fn : unit -> bool
Unofficial version of Isabelle/HOL-Plain (unidentified repository version)
 > theory Test imports Plain begin;
theory Test
 > find_theorems Pow;
searched for:
    "Pow"

nothing found in 0.040 secs
 > quit;

# Still bad:

krauss at lapbroy38:~/wd/isabelle/src/HOL$ hg bisect -b
Testing changeset 34059:f3f0e20923a7 (5 changesets remaining, ~2 tests)
16 files updated, 0 files merged, 2 files removed, 0 files unresolved

krauss at lapbroy38:~/wd/isabelle/src/HOL$ isabelle tty -l HOL-Plain
 > val it = () : unit
val commit = fn : unit -> bool
Unofficial version of Isabelle/HOL-Plain (unidentified repository version)
 > Error - Database is not opened for writing.
 > val it = () : unit
krauss at lapbroy38:~/wd/isabelle/src/HOL$ isabelle make HOL-Plain
[...]
Finished HOL-Plain (0:02:28 elapsed time, 0:02:11 cpu time, factor 0.88)
krauss at lapbroy38:~/wd/isabelle/src/HOL$ isabelle tty -l HOL-Plain
 > val it = () : unit
val commit = fn : unit -> bool
Unofficial version of Isabelle/HOL-Plain (unidentified repository version)
 > theory Test imports Plain begin;
theory Test
 > find_theorems Pow;
searched for:
    "Pow"

nothing found in 0.044 secs
 > quit;

# Still bad, so go for next round:

krauss at lapbroy38:~/wd/isabelle/src/HOL$ hg bisect -b
Testing changeset 34058:97fd820dd402 (2 changesets remaining, ~1 tests)
1 files updated, 0 files merged, 0 files removed, 0 files unresolved
krauss at lapbroy38:~/wd/isabelle/src/HOL$ isabelle make HOL-Plain
make[1]: Entering directory `/home/krauss/wd/isabelle/src/Pure'
[...]
Finished HOL-Plain (0:02:25 elapsed time, 0:02:08 cpu time, factor 0.88)
krauss at lapbroy38:~/wd/isabelle/src/HOL$ isabelle tty -l HOL-Plain
 > val it = () : unit
val commit = fn : unit -> bool
Unofficial version of Isabelle/HOL-Plain (unidentified repository version)
 > theory Test imports Plain begin;
theory Test
 > find_theorems Pow;
searched for:
    "Pow"

found 21 theorems in 0.084 secs:

Complete_Lattice.Pow_INT_eq: Pow (INT x:?A. ?B x) = (INT x:?A. Pow (?B x))
Complete_Lattice.UN_Pow_subset: (UN x:?A. Pow (?B x)) <= Pow (UN x:?A. ?B x)
Complete_Lattice.Union_Pow_eq: Union (Pow ?A) = ?A
Complete_Lattice.subset_Pow_Union: ?A <= Pow (Union ?A)
Finite_Set.card_Pow: finite ?A ==> card (Pow ?A) = Suc (Suc 0) ^ card ?A
Finite_Set.finite_Pow_iff: finite (Pow ?A) = finite ?A
Predicate.Powp_Pow_eq: Powp (%x. x : ?A) = (%x. x : Pow ?A)
Set.PowD: ?A : Pow ?B ==> ?A <= ?B
Set.PowI: ?A <= ?B ==> ?A : Pow ?B
Set.Pow_Compl: Pow (- ?A) = {- B |B. ?A : Pow B}
Set.Pow_Int_eq: Pow (?A Int ?B) = Pow ?A Int Pow ?B
Set.Pow_UNIV: Pow UNIV = UNIV
Set.Pow_bottom: {} : Pow ?B
Set.Pow_def: Pow ?A = {B. B <= ?A}
Set.Pow_def_raw: Pow == %A. {B. B <= A}
Set.Pow_empty: Pow {} = {{}}
Set.Pow_iff: (?A : Pow ?B) = (?A <= ?B)
Set.Pow_insert: Pow (insert ?a ?A) = Pow ?A Un insert ?a ` Pow ?A
Set.Pow_mono: ?A <= ?B ==> Pow ?A <= Pow ?B
Set.Pow_top: ?A : Pow ?A
Set.Un_Pow_subset: Pow ?A Un Pow ?B <= Pow (?A Un ?B)
 > quit;

# This time it worked, so mark as good:

krauss at lapbroy38:~/wd/isabelle/src/HOL$ hg bisect -g
The first bad revision is:
changeset:   34059:f3f0e20923a7
user:        haftmann
date:        Wed Dec 09 21:38:12 2009 +0100
summary:     take and drop as projections of chop

# hg shows the first bad revision (which was tested in the round before).