deriving DecidableEq timeout 4.22 regresssion?

Stream: lean4

[Malvin Gattinger]

In 4.20 and 4.21 this works, but with 4.22-rc3 and -rc4 it runs out of heartbeats in the deriving DecidableEq line.

abbrev Sequent : Type := List Nat
abbrev History : Type := List Sequent
def rep (H : History) (N : Sequent) : Prop := N ∈ H
def Sequent.basic (N : Sequent) := N = [1]
def LocalTableau (X : Sequent) : Type := sorry
def endNodesOf {X} : LocalTableau X → List Sequent := sorry

inductive Tableau : History → Sequent → Type
  | loc {Hist X} (nrep : ¬ rep Hist X) (nbas : ¬ X.basic) (lt : LocalTableau X)
            (next : ∀ Y ∈ endNodesOf lt, Tableau (X :: Hist) Y) : Tableau Hist X

-- With Lean 4.21.0 already 2000 beats is enough, but in 4.22.0 even 2000000 does not suffice.
set_option maxHeartbeats 2000000 in
inductive PathIn : ∀ {Hist X}, Tableau Hist X → Type
| nil : PathIn _
| loc {nrep nbas lt next Y} (Y_in : Y ∈ endNodesOf lt) (tail : PathIn (next Y Y_in))
    : PathIn (Tableau.loc nrep nbas lt next)
deriving DecidableEq

The difference can be observed on live lean by switching from "latest Mathlib" to "Mathlib stable" in the top-right drop down or here.

The example is a minimization from my pdl project that I am trying to upgrade. Also if instead of deriving the instance I write it by hand the result was a timeout.

With set_option diagnostics true I did not see anything suspicious in what is unfolded :thinking:

How should we further investigate this? Or is any regression like this known already?

Cc @Andrés Goens who helped me debug this (including running lean4checker on the output from 4.21 to exlude an old bug as the root cause.)

[Malvin Gattinger]

Curiously, removing the nbas proof argument in both inductives makes it work again :shock:

abbrev Sequent : Type := List Nat
abbrev History : Type := List Sequent
def rep (H : History) (N : Sequent) : Prop := N ∈ H
def LocalTableau (X : Sequent) : Type := sorry
def endNodesOf {X} : LocalTableau X → List Sequent := sorry

inductive Tableau : History → Sequent → Type
  | loc {Hist X} (nrep : ¬ rep Hist X) (lt : LocalTableau X)
            (next : ∀ Y ∈ endNodesOf lt, Tableau (X :: Hist) Y) : Tableau Hist X

inductive PathIn : ∀ {Hist X}, Tableau Hist X → Type
| nil : PathIn _
| loc {nrep lt next Y} (Y_in : Y ∈ endNodesOf lt) (tail : PathIn (next Y Y_in))
    : PathIn (Tableau.loc nrep lt next)
deriving DecidableEq

[Malvin Gattinger]

Even more strange, also removing nrep (while keeping nbas) in both inductives makes it work. So having one Prop field is fine, but having two triggers the problem. :confusion:

Merging them into one Prop argument that is a conjunction also makes the problem go away :detective:

[Malvin Gattinger]

Maybe this is related? #mathlib4 > deriving DecidableEq gives kernel error for higher universes

[Robin Arnez]

No that other issue is only for enum inductives (no parameters, no fields)

[Malvin Gattinger]

Ah, okay. Then I am curious how to debug the issue about proof fields here.

[Robin Arnez]

Well it's a compiler error

[Robin Arnez]

@Cameron Zwarich it seems like it runs into some kind of infinite loop or at least infinite blowup in toLCNF:

#0  0x00007ffd76bccd30 in mi_free () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libInit_shared.dll
#1  0x00007ffd76b95da5 in lean_dec_ref_cold () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libInit_shared.dll
#2  0x00007ffd6e62709a in l_Lean_Meta_inferTypeImp_infer () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libleanshared_1.dll
#3  0x00007ffd6e6106a4 in lean_infer_type () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libleanshared_1.dll
#4  0x00007ffd6fb0ff0f in l_Lean_Compiler_LCNF_ToLCNF_etaExpandN___redArg () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libleanshared_1.dll
#5  0x00007ffd6fb10fc9 in l_Lean_Compiler_LCNF_ToLCNF_toLCNF_expandNoConfusionMajor___redArg () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libleanshared_1.dll
#6  0x00007ffd6fb291c3 in l_Lean_Compiler_LCNF_ToLCNF_toLCNF_visitNoConfusion___lam__0 () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libleanshared_1.dll
#7  0x00007ffd76ba9910 in lean_apply_6 () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libInit_shared.dll
#8  0x00007ffd6fb2c04b in l_Lean_Compiler_LCNF_ToLCNF_toLCNF_etaIfUnderApplied () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libleanshared_1.dll
#9  0x00007ffd6fb2a9ab in l_Lean_Compiler_LCNF_ToLCNF_toLCNF_visitNoConfusion___lam__1 () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libleanshared_1.dll
#10 0x00007ffd6fb2c94f in l_Lean_Compiler_LCNF_ToLCNF_toLCNF_visitNoConfusion___lam__1___boxed () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libleanshared_1.dll
#11 0x00007ffd76baafa1 in lean_apply_7 () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libInit_shared.dll
#12 0x00007ffd6fb2c657 in l_Lean_Compiler_LCNF_ToLCNF_toLCNF_visitNoConfusion___lam__2 () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libleanshared_1.dll
#13 0x00007ffd76ba9512 in lean_apply_6 () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libInit_shared.dll
#14 0x00007ffd6fb2c04b in l_Lean_Compiler_LCNF_ToLCNF_toLCNF_etaIfUnderApplied () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libleanshared_1.dll
#15 0x00007ffd6fb25cdb in l_Lean_Compiler_LCNF_ToLCNF_toLCNF_visitNoConfusion () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libleanshared_1.dll
#16 0x00007ffd6fb19113 in l_Lean_Compiler_LCNF_ToLCNF_toLCNF_visitApp () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libleanshared_1.dll
#17 0x00007ffd6fb17311 in l_Lean_Compiler_LCNF_ToLCNF_toLCNF_visitCore () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libleanshared_1.dll
#18 0x00007ffd6fb1f27e in l_Lean_Compiler_LCNF_ToLCNF_toLCNF_visit () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libleanshared_1.dll
#19 0x00007ffd6fb1fd7a in l_Lean_Compiler_LCNF_ToLCNF_toLCNF_visitLambda___lam__0 () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libleanshared_1.dll
#20 0x00007ffd76ba9755 in lean_apply_6 () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libInit_shared.dll
#21 0x00007ffd6fb09a8b in l_Lean_Compiler_LCNF_ToLCNF_withNewScope___redArg () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libleanshared_1.dll
#22 0x00007ffd6fb198e3 in l_Lean_Compiler_LCNF_ToLCNF_toLCNF_visitLambda () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libleanshared_1.dll
#23 0x00007ffd6fb177d0 in l_Lean_Compiler_LCNF_ToLCNF_toLCNF_visitCore () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libleanshared_1.dll
#24 0x00007ffd6fb1f27e in l_Lean_Compiler_LCNF_ToLCNF_toLCNF_visit () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libleanshared_1.dll
#25 0x00007ffd6fb39fce in l_Lean_Compiler_LCNF_ToLCNF_toLCNF_visitHEqRec___lam__0 () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libleanshared_1.dll
#26 0x00007ffd6fb3a254 in l_Lean_Compiler_LCNF_ToLCNF_toLCNF_visitHEqRec___lam__0___boxed () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libleanshared_1.dll
#27 0x00007ffd76ba9593 in lean_apply_6 () from /c/Users/robin/lean4dev/lean4/build/release/stage1/bin/libInit_shared.dll
...

[Cameron Zwarich]

Thanks for narrowing it down @Robin Arnez. I honestly haven't gone through the noConfusion lowering here and it's somewhat involved, so it may take a bit of time to figure this out. My hope would be that we just missed some place where we can replace a term with lcProof and avoid recursing.

[Andrés Goens]

yeah it does seem to be a bug in the new compiler! if we add

set_option compiler.enableNew false

it works again, and if we set that to true in 4.21 it breaks there too

[Andrés Goens]

I guess it makes sense to make an issue in the Lean4 repo?

[Malvin Gattinger]

I wanted to try out if the new compiler can be en/disabled locally, but already this gives failed to compile definition when using "Latest Mathlib" :thinking:

set_option compiler.enableNew false

abbrev Sequent : Type := List Nat
abbrev History : Type := List Sequent
def rep (H : History) (N : Sequent) : Prop := N ∈ H
def Sequent.basic (N : Sequent) := N = [1]
def LocalTableau (X : Sequent) : Type := sorry
def endNodesOf {X} : LocalTableau X → List Sequent := sorry -- failed to compile definition

inductive Tableau : History → Sequent → Type
  | loc {Hist X} (nrep : ¬ rep Hist X) (nbas : ¬ X.basic) (lt : LocalTableau X)
            (next : ∀ Y ∈ endNodesOf lt, Tableau (X :: Hist) Y) : Tableau Hist X

inductive PathIn : ∀ {Hist X}, Tableau Hist X → Type
| nil : PathIn _
| loc {nrep nbas lt next Y} (Y_in : Y ∈ endNodesOf lt) (tail : PathIn (next Y Y_in))
    : PathIn (Tableau.loc nrep nbas lt next)
deriving DecidableEq -- failed to compile definition?

[Robin Arnez]

In order for it to work, everything it depends on also needs to have been compiled with the old compiler. If you look at the sorry, you'll see that it actually contains a Name and the old IR and new IR clash in weird ways. The DecidableEq PathIn similarly refers to instDecidableEqNat which the old compiler handles differently to the new compiler - boom crash

[Robin Arnez]

Besides, the old compiler doesn't exist on nightly anymore :-)

[Malvin Gattinger]

For the record, in the new 4.23.0-rc2 and current nightly this still happens, so I made an issue in the lean4 repo now.

[Malvin Gattinger]

It seems @Cameron Zwarich has found the issue and fixed this now https://github.com/leanprover/lean4/commit/dc5766d27a27be935a1efe348ffe7a447edce574 :tada: looking forward to testing it in my project soon!