Frequent crashes on recent nightly

Stream: lean4

[Jannis Limperg]

On nightly-2024-02-27, when I type quickly, the Lean server frequently crashes with

libc++abi: terminating due to uncaught exception of type lean::interrupted
[Error - 11:32:48 AM] Request textDocument/completion failed.
  Message: Server process for file:///home/jannis/uni/aesop/work/Aesop/Builder/NormSimp.lean crashed, likely due to a stack overflow or a bug.
  Code: -32902

I don't have a way to reliably reproduce this, but it happens consistently on both VSCode and Emacs. The speed of the typing seems to make a difference. Other than that, I haven't found any specific triggers yet.

I'll try to find the nightly that introduced this, but I'd be curious whether anyone else can reproduce.

lean4#3528

[Henrik Böving]

@Sebastian Ullrich is this the one you fixed here? https://github.com/leanprover/lean4/pull/3500

[Sebastian Ullrich]

Yes!

[Jannis Limperg]

Okay great, thanks!

[Jannis Limperg]

Actually, this patch should be included in 2024-02-27. So this does not yet seem to be fully fixed.

[Jannis Limperg]

I can reproduce the issue on nightly 02-23, but not on 02-22. This makes it seem likely that lean4#3421, which was first included in 02-23, is indeed the culprit. I can still reproduce the issue on 02-27, which includes the PR lean4#3500 that should have fixed it.

I've been using the file Std/Data/HashMap/WF.lean from bump/nightly-2024-02-27 for my tests. It seems like you need a non-trivial file for the issue to occur; otherwise I guess elaboration is too fast to get interrupted.

[Sebastian Ullrich]

Okay, I can reproduce using the actual release