VS Code Extension LSP stack overflow

Stream: lean4

[Matthew Ballard]

I am getting

Stack overflow detected. Aborting.
[Error - 11:22:34 AM] Request textDocument/completion failed.
  Message: Server process for file:///home/matt/foo/Foo.lean crashed, likely due to a stack overflow in user code.
  Code: -32603
[Error - 11:22:34 AM] Request textDocument/semanticTokens/full failed.
  Message: Server process for file:///home/matt/foo/Foo.lean crashed, likely due to a stack overflow in user code.
  Code: -32603
[Error - 11:22:34 AM] Request textDocument/documentSymbol failed.
  Message: Server process for file:///home/matt/foo/Foo.lean crashed, likely due to a stack overflow in user code.
  Code: -32603

when the extension attempts auto-complete at F in

inductive Foo where
 | bar : F

Can someone replicate this?

[Mac]

Yep. Auto-completing at F causes the server hang and then after ~1min it crashes with the stack overflow. (I tested it on the 06-14 nightly.)

[Mac]

I would suggest submit this as an issue to the GitHub: https://github.com/leanprover/lean4/issues

[Matthew Ballard]

Thanks. That is the next step - just wanted to make sure nothing idiosyncratic was happening with my machines.