inline codegen crash

Stream: lean4

[James Gallicchio]

On leanprover/lean4:nightly-2022-09-26, this code:

@[inline]
def foldr (f : Nat → β → β) (acc : β) : Nat → β
| 0 => acc
| n+1 => foldr f (f n acc) n

def toList (r : Nat) : List Nat :=
  foldr (· :: ·) [] r

causes the server to crash. Unsure if it's already been reported.

[Leonardo de Moura]

I get the error message

/home/leodemoura/projects/lean4/build/release/foldr.lean:6:4: error: maximum recursion depth reached in the code generator
function inline stack:
foldr
...

We will try to improve the error message. The new one will suggest you remove the [inline] annotation from foldr.

[Leonardo de Moura]

See https://github.com/leanprover/lean4/issues/1646

[Henrik Böving]

For me the LSP crashes as well with a stack overflow error, maybe you accidentally already fixed it?

[Mario Carneiro]

lean4#1657 has a variation where there is an actual stack overflow, not the error message

[Henrik Böving]

It is overflowing in the simplifier a few thousand recursive calls to simp deep

[James Gallicchio]

from lean4#1646:

We had similar incorrect annotations in the Init package

Funnily, this is why I placed those annotations on my functions in the first place :joy: thanks for taking a look

[Leonardo de Moura]

@Henrik Böving @Mario Carneiro I will add a new parameter to the compiler Simp that throws an error whenever the inline stack contains more than n occurrences of some function. The defaults will be 1 for [inline] and 32 for [inlineIfReduce].

[Mario Carneiro]

Is that at the declaration or at the use site?

[Mario Carneiro]

"default" meaning it can be changed?

[Leonardo de Moura]

At the use site. I am not working on the declaration site validation right now.
We need checking at the use site anyway for [inlineIfReduce].

[Leonardo de Moura]

Mario Carneiro said:

"default" meaning it can be changed?

Yes, we have to add options to control the optimizer. It is on the TODO list, the issue above is occurring so often that it is time to address it.

[Mario Carneiro]

@Leonardo de Moura in lean4#1657 I found the same thing as Henrik: the stack overflow is in the Simp module:

...
#8473 0x00007ffff531a240 in l_Lean_Compiler_LCNF_Simp_simp () from /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so
#8474 0x00007ffff532fb54 in l_Lean_Compiler_LCNF_Simp_inlineApp_x3f___lambda__4 () from /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so
#8475 0x00007ffff53417dd in l_Lean_Compiler_LCNF_Simp_inlineApp_x3f () from /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so
#8476 0x00007ffff5343482 in l_Lean_Compiler_LCNF_Simp_simp___lambda__1 () from /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so
#8477 0x00007ffff531b872 in l_Lean_Compiler_LCNF_Simp_simp () from /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so
#8478 0x00007ffff7b22109 in lean_apply_7 () from /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so
#8479 0x00007ffff5366e84 in l_ReaderT_bind___at_Lean_Compiler_LCNF_Simp_instMonadFVarSubstSimpMFalse___spec__1___rarg () from /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so
#8480 0x00007ffff7b220b5 in lean_apply_7 () from /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so
#8481 0x00007ffff534964c in l_Lean_Compiler_LCNF_Simp_simp___lambda__8 () from /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so
#8482 0x00007ffff7b23b84 in lean_apply_8 () from /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so
#8483 0x00007ffff53170c3 in l___private_Init_Data_Array_BasicAux_0__mapMonoMImp_go___at_Lean_Compiler_LCNF_Simp_simpFunDecl___spec__4 () from /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so
#8484 0x00007ffff5317cd3 in l___private_Init_Data_Array_BasicAux_0__mapMonoMImp___at_Lean_Compiler_LCNF_Simp_simp___spec__6 () from /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so
#8485 0x00007ffff531a240 in l_Lean_Compiler_LCNF_Simp_simp () from /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so
#8486 0x00007ffff532fb54 in l_Lean_Compiler_LCNF_Simp_inlineApp_x3f___lambda__4 () from /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so
#8487 0x00007ffff53417dd in l_Lean_Compiler_LCNF_Simp_inlineApp_x3f () from /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so
#8488 0x00007ffff5343482 in l_Lean_Compiler_LCNF_Simp_simp___lambda__1 () from /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so
#8489 0x00007ffff531b872 in l_Lean_Compiler_LCNF_Simp_simp () from /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so
...

so probably your fix will fix this; has it already landed on master?

[Leonardo de Moura]

so probably your fix will fix this; has it already landed on master?

Not yet, go distracted with the bug report from Marc in the other thread.

[Leonardo de Moura]

I will push fixes for both of them.