Lean 4 hanging - unsure how to debug

Stream: lean4 dev

[Tobias Grosser]

I am currently debugging some kernel busyloop in lean and am very lost.

[Tobias Grosser]

At a high-level, I want to proof these two statements equal:

def lhs :
    Com InstCombine.LLVM [] .pure (InstCombine.Ty.bitvec 32) := sorry

def aaaaa:
    Com InstCombine.LLVM [] .pure (InstCombine.Ty.bitvec 32) :=
  .var (const 32 (-1)) <|
  .var (add 32 0 0 ) <|
  .var (neg 32 0) <|
  .ret ⟨1, by simp [Ctxt.snoc]⟩

[Tobias Grosser]

In this repo: https://github.com/opencompl/lean-mlir/tree/lean-deadlock

[Tobias Grosser]

I tried the last two days reducing the test case, but was unsuccessful.

[Tobias Grosser]

I call a couple of tactics to simplify the aaaaa rhs of my lhs = aaaaa identity.

[Tobias Grosser]

The tactics succeed, but lean hangs in the kernel.

[Tobias Grosser]

set_option debug.skipKernelTC true stops lean hanging.

[Tobias Grosser]

And replacing the -1 (which seems to be translated to a large unsigned value) to 0, 1, or any small positive number also accelerates things.

[Tobias Grosser]

At 60000 the lean kernel kernel becomes slow again and starts hanging.

[Tobias Grosser]

The entire hanging is very fragile.

[Tobias Grosser]

I found a different sequence of tactics (replacing simp with rw) that leads to the exact same output with set_option pp.all true enabled.

[Tobias Grosser]

Still, when this state is generated with rw lean's kernel check is fast, but when using simp lean hangs.

[Tobias Grosser]

I am a bit out of my depth with respect to how to debug this.

[Tobias Grosser]

With `set_options diagnostics true' I get:

[kernel] unfolded declarations (max: 150035, num: 44): ▼
  [] Nat.rec ↦ 150035
  [] Nat.casesOn ↦ 90048
  [] Nat.add.match_1 ↦ 30004
  [] Nat.beq.match_1 ↦ 30001
  [] InstCombine.Ty ↦ 411

[Tobias Grosser]

The number of Nat.rec increases as I increase the integer value in my input. So it seems there is too much unfolded here.

[Tobias Grosser]

I tried https://github.com/leanprover/lean4/issues/5724 and it seems one of my reduced test cases is solved by it.

[Tobias Grosser]

I am currently looking back to debugging why the full test case. I see similar hanging there.