neovim stalled by strange errors…

Stream: general

[Antoine Chambert-Loir]

I get a lot of errors like this tonight, which end up stalling neovim… What could happen?

Error executing vim.schedule lua callback: ...ambert/.local/share/nvim/lazy/lean.nvim/lua/lean/lsp.lua:274: Invalid 'end_col': out of range
stack traceback:
        [C]: in function 'nvim_buf_set_extmark'
        ...ambert/.local/share/nvim/lazy/lean.nvim/lua/lean/lsp.lua:274: in function 'f'
        ...Cellar/neovim/0.11.0/share/nvim/runtime/lua/vim/iter.lua:207: in function 'filter'
        ...ambert/.local/share/nvim/lazy/lean.nvim/lua/lean/lsp.lua:254: in function 'handler'
        .../neovim/0.11.0/share/nvim/runtime/lua/vim/lsp/client.lua:1109: in function ''
        vim/_editor.lua: in function <vim/_editor.lua:0>

[Julian Berman]

Does it happen with any file, or if not anything you can share to help me reproduce?

[Antoine Chambert-Loir]

It happens with the file Mathlib/RingTheory/Polynomial/Eisenstein/Generalized.lean of #23710

[Julian Berman]

I can't reproduce with that file yet -- could I ask if you could double check you're up to date on lean.nvim? Is there anything in particular I should do? Or it happens for you just from moving around?

[Julian Berman]

Meanwhile I'll also try to do it with your dotfiles that you shared.

[Matthew Ballard]

I am getting this over and over now. It seems pretty sporadic.

[Antoine Chambert-Loir]

Probably not a coincidence : at the same time, top shows that nvim takes 100% of CPU.

[Matthew Ballard]

Does it have something to do with auto-indent? I seem to get it when pushing text to the next line.

[Antoine Chambert-Loir]

It happens very often when I delete lines (dd).

[Matthew Ballard]

Separately, overall performance is more sluggish but I can't tell whether the culprit is the async elab features, nvim, the extension, or else.

[Julian Berman]

Can I confirm both of you are up to date? And I don't suppose either of you has anything that can help me reproduce? Not that I've done a lot of lean (as opposed to lean.nvim dev itself) recently so it's possible it's easy to reproduce and I just need to try. If it's exactly the traceback from above I could put in something to simply make it go away but I would like to avoid doing so if possible in favor of reproducing and seeing what/where the actual issue is :/

[Antoine Chambert-Loir]

The best I can do to claim I'm “up to date” is entering :Lazy, and typing U. Is that OK?

[Julian Berman]

Yes, that should mean you are!

[Matthew Ballard]

I'll give you the commit in my local clone in a 5, 4, 3,...

[Julian Berman]

I was about to tell you to just show me checkhealth lean, but I see the version info there is... broken :( so I am fixing that now too

[Matthew Ballard]

ddb881407213d27

[Matthew Ballard]

It is from March 30 so let me update

[Antoine Chambert-Loir]

lean.nvim (v4.19.0-rc3-72-g6c1b01338c) ~
- OK Neovim is new enough.
- `vim.version()`:  0.11.0
- OK Lake is runnable.
- `lake --version`:  Lake version 5.0.0-045d07d (Lean version 4.19.0-rc3)

[Adam Topaz]

FWIW I have also noticed speed issues in nvim primarily when jumping to a definition which lands me in the middle of some large file.

[Matthew Ballard]

Hmm. Packer is telling me things are not very much out of date but the local clone is way off... I might be looking the wrong place. Either way I should be up to date now. I will report back if I see more issues.

[Julian Berman]

OK, I'll also follow up with some instructions on how to collect a profile shortly, but one of the two things I'm trying to get finished right now is some memoization, so there's not much point doing so until I'm done given that's a source of slowness that I'm already aware of and is affecting things.

[Matthew Ballard]

Still there -- dd is triggering it

[Julian Berman]

So open some random file and dd and you get a traceback?

[Antoine Chambert-Loir]

By opening a random file, do you wish that I open /dev/random?

[Antoine Chambert-Loir]

typically, yes.

[Julian Berman]

No sorry I just meant arbitrary

[Antoine Chambert-Loir]

It has to be a lean file. I don't get this otherwise.

[Matthew Ballard]

Error executing vim.schedule lua callback: ...e/nvim/site/pack/packer/start/lean.nvim/lua/lean/lsp.lua:219: Invalid 'end_col': out of range
stack traceback:
        [C]: in function 'nvim_buf_set_extmark'
        ...e/nvim/site/pack/packer/start/lean.nvim/lua/lean/lsp.lua:219: in function 'f'
        ...Cellar/neovim/0.11.0/share/nvim/runtime/lua/vim/iter.lua:207: in function 'filter'
        ...e/nvim/site/pack/packer/start/lean.nvim/lua/lean/lsp.lua:199: in function 'handler'
        .../neovim/0.11.0/share/nvim/runtime/lua/vim/lsp/client.lua:1109: in function ''
        vim/_editor.lua: in function <vim/_editor.lua:0>

Same as above

[Julian Berman]

As in you deterministically are getting a traceback if you open any old Mathlib file and delete a line?

[Antoine Chambert-Loir]

Yes.

[Matthew Ballard]

Line 79 in Mathlib.RingTheory.Valuation.ValuationSubring

[Julian Berman]

So strange, that definitely does not happen to me, so I really would love to know what's different. Let me try that file.

[Antoine Chambert-Loir]

I didn't expect it to be deterministic. But I just open Mathlib/GroupTheory/Abelianization.lean, I'm at line 39, and 8dd, followed by u, triggers it (at undo).

[Matthew Ballard]

I did it 5 or so times in a row

[Matthew Ballard]

Cursor positioned in the first column

[Julian Berman]

Aha! Perfect, that does it! Thank you (both of you)!

[Matthew Ballard]

God forbid you dd and then u

[Julian Berman]

Of course it happened once and now has not happened again the next 5 times, but OK at least I have seen it once.

[Antoine Chambert-Loir]

Sometimes I get one of these error messages, and sometimes a full screen of them. (10 times the same stuff, more or less…)

[Matthew Ballard]

Yes, I thought I had crashed the editor but enough returns got me back

[Matthew Ballard]

I did a few more times. It is not 100% but still happens more often than not

[Julian Berman]

OK I put in a fix (at least I haven't seen a traceback leak through now in 10 tries). Please update again and let me know if you still see them!

[Julian Berman]

(None of this will have anything to do with stalling unfortunately)

[Antoine Chambert-Loir]

I still have it. Line 51 of Abelianization, 8dd/u.

[Julian Berman]

Can you show me what the traceback looks like now?

[Antoine Chambert-Loir]

Error executing vim.schedule lua callback: ...ambert/.local/share/nvim/lazy/lean.nvim/lua/lean/lsp.lua:219: Invalid 'end_col': out of range
stack traceback:
        [C]: in function 'nvim_buf_set_extmark'
        ...ambert/.local/share/nvim/lazy/lean.nvim/lua/lean/lsp.lua:219: in function 'f'
        ...Cellar/neovim/0.11.0/share/nvim/runtime/lua/vim/iter.lua:207: in function 'filter'
        ...ambert/.local/share/nvim/lazy/lean.nvim/lua/lean/lsp.lua:199: in function 'handler'
        .../neovim/0.11.0/share/nvim/runtime/lua/vim/lsp/client.lua:1109: in function ''
        vim/_editor.lua: in function <vim/_editor.lua:0>

[Julian Berman]

OK, one more try then... Lazy update and cross our fingers.

[Antoine Chambert-Loir]

Same…

Error executing vim.schedule lua callback: ...ambert/.local/share/nvim/lazy/lean.nvim/lua/lean/lsp.lua:219: Invalid 'end_col': out of range
stack traceback:
        [C]: in function 'nvim_buf_set_extmark'
        ...ambert/.local/share/nvim/lazy/lean.nvim/lua/lean/lsp.lua:219: in function 'f'
        ...Cellar/neovim/0.11.0/share/nvim/runtime/lua/vim/iter.lua:207: in function 'filter'
        ...ambert/.local/share/nvim/lazy/lean.nvim/lua/lean/lsp.lua:199: in function 'handler'
        .../neovim/0.11.0/share/nvim/runtime/lua/vim/lsp/client.lua:1109: in function ''
        vim/_editor.lua: in function <vim/_editor.lua:0>

and if I press Enter, the same message repeats over and over.

[Antoine Chambert-Loir]

image.png

[Antoine Chambert-Loir]

A new error message, from satellite (Major Tom to Ground Control…)

error(satellite.nvim): handler=gitsigns buf=6 row=20 opts={ id = 21, priority = 20, sign_hl_group = "SatelliteGitSignsChange", sign_text = " │" }, err="Invalid 'line':
error(satellite.nvim): handler=gitsigns buf=6 row=20 opts={ id = 21, priority = 20, sign_hl_group = "SatelliteGitSignsChange", sign_text = " │" }, err="Invalid 'line':
error(satellite.nvim): handler=gitsigns buf=6 row=20 opts={ id = 21, priority = 20, sign_hl_group = "SatelliteGitSignsAdd", sign_text = " │" }, err="Invalid 'line': ou
error(satellite.nvim): handler=gitsigns buf=6 row=20 opts={ id = 21, priority = 20, sign_hl_group = "SatelliteGitSignsChange", sign_text = " │" }, err="Invalid 'line':
 out of range"

[Julian Berman]

:/ -- But something is strange because the line numbers are off there from what's on main after my commits I think. Can you show me :checkhealth lean now?

[Julian Berman]

You're sure you ran Lazy update again right?

[Antoine Chambert-Loir]

lean.nvim (v2024.12.2-193-gf1d9e79)

[Julian Berman]

That's correct :/ OK, back to the drawing board then, even though I have not seen this again yet, will keep trying.