emacs lean4-mode hanging

Stream: lean4

[David Renshaw]

When I try to use lean4-mode on mathlib4, the *lean4-lsp::stderr* buffer sees this error message repeating forever:

PANIC at Lean.EnvExtensionInterfaceUnsafe.getState Lean.Environment:236:4: invalid environment extension has been accessed
PANIC at Lean.ScopedEnvExtension.getState Lean.ScopedEnvExtension:157:16: unreachable code has been reached
PANIC at Lean.EnvExtensionInterfaceUnsafe.getState Lean.Environment:236:4: invalid environment extension has been accessed
Error: index out of bounds

The goal view and jump-to-definition are still a little bit usable, but very slow. What am I doing wrong?

[David Renshaw]

I am using lean4-mode at this commit https://github.com/leanprover/lean4-mode/commit/c016c7aeee92564836355083664c49ed57024427
to work around this problem: https://github.com/leanprover/lean4-mode/issues/19 .

[Wojciech Nawrocki]

This is a Lean server bug that was fixed in leanprover/lean4#1259. Updating the nightly should help.

[David Renshaw]

ah, okay. I suppose I just need to wait for https://github.com/leanprover-community/mathlib4/pull/295 to land then