Julian / lean.nvim

neovim support for the Lean theorem prover
MIT License
255 stars 25 forks source link

Cursor jumps around when infoview is open #286

Closed prescientmoon closed 1 year ago

prescientmoon commented 1 year ago

I've just created a new lake project. I've opened one of the files, and it seems like whenever the infoview is open, my cursor jumps to the start of the current/an adjacent line as soon as I move it on the right hand side of a definition.

Julian commented 1 year ago

Hi, I can't reproduce this, so will need a bit more info on what you're running (versions of the plugin and Lean, and/or the output from :checkhealth lean).

prescientmoon commented 1 year ago

Hi @Julian

Here's the output from checkhealth:

lean: require("lean.health").check()
========================================================================
## lean.nvim
  - OK: `lean --version`
  - INFO: Lean (version 4.0.0-nightly-2022-11-30, commit a095dabb1749, Release)
  - WARNING: `lean-language-server` not found, lean 3 support will not work
prescientmoon commented 1 year ago

My config for the plugin is also pretty basic:

  require('lean').setup {
    abbreviations = { builtin = true, cmp = true },
    lsp = { on_attach = lspconfig.on_attach, capabilities = lspconfig.capabilities },
    lsp3 = false,
    mappings = true
  }
prescientmoon commented 1 year ago

It seems like the jumping actually happens whenever some text appears inside the infoview

prescientmoon commented 1 year ago

Looking at the lsp log, does this mean anything?

[WARN][2022-12-01 17:11:36] ...lsp/handlers.lua:112 "The language server leanls triggers a registerCapability handler despite dynamicRegistration set to false. Report upstream, this warning is harmless"
Julian commented 1 year ago

I don't think that line should mean anything, it possibly has to do with whatever you're setting in capabilities in your sample config but I'd have to check.

But yeah the plugin works fine here, can you perhaps include a full config which reproduces this for you that I can try?

prescientmoon commented 1 year ago

I'll try to reproduce in a minimal example when I have some time. Now that I think of it, the issue might have to do with me using neovim nightly. I'll have to try a bunch of stuff and see what happens

Julian commented 1 year ago

Let me know if this is still happening.