Closed mdgeorge4153 closed 1 year ago
This appears to pop up every time I move into the RHS of a definition. Note that the info pane does populate.
Hey! I can try to have a look in a bit, so this is just a guess, but are you able to update to neovim 0.8 or newer perhaps and then retry? (Generally neovim itself and most plugins will only support the most recent release, think
Whoops, hit the wrong button, thanks github mobile -- anyways yeah I think this is complaining about us doing vim.cmd.normal
which may be 0.8+ I forget -- if you can update (0.8.1 is out as of a month ago too) let me know if that works, otherwise can have a look when I'm back at a computer.
I pushed a commit which changes doing that line in a way that should work on <0.8, which I think might be the only one breaking your setup, but I'd still encourage updating to 0.8 (and 0.9 is going to be out soon) -- in general neovim itself only supports 2 versions (latest stable and latest nightly), so it's hard to support more than that downstream, but obviously I try not to break anything intentionally especially if the Ubuntu repos haven't caught up. Definitely share any feedback though (about this but in general!)
I have just installed
nvim
,lean
, andlean.nvim
for the first time and am trying to get them set up. While navigating lean source, I encounter the following error:I am using lean 3, and installed the LSP using npm. I have installed
nvim
on ubuntu from the PPA,My
init.vim
is taken from here: https://github.com/Julian/lean.nvim/wiki/Getting-Started#install-leannvim-and-its-dependenciesTo reproduce, open
src/data/finset.lean
in mathlib and move to line 25 (this is the first file I've opened so I don't know how prevalent the problem is).