neovim error message

Stream: general

[Antoine Chambert-Loir]

I'm trying to test lean with vim, and I get an error message I don't understand.

LSP[leanls]: Error ON_ATTACH_ERROR: "vim/keymap.lua:0: rhs: expected string|function, got nil"

(I just followed the instructions about how to install it from lean.nvim, and I used vim-plug.)

[Matthew Ballard]

vim or nvim?

[Antoine Chambert-Loir]

nvim, indeed.

[Matthew Ballard]

Do you already have an on_attach function? If not, here is the one I copied into my init.lua. (I have no organization in .config/nvim/)

[Matthew Ballard]

Also, I am not sure if this should "just work" now. My initial install is long in the past.

[Julian Berman]

(Hooray, another vulnerable convert :smiling_devil:)

That error message would sound like somewhere you have vim.keymap.set('n', 'bla', nil)

[Julian Berman]

Can you share your setup Antoine?

[Antoine Chambert-Loir]

I'm on MacOS (12.7.5), running nvimversion v0.10.1.
I downloaded plug.vim to $(HOME)/.vim/autoload, added the suggested lines, launched `:PlugUpdate after restarting nvim, and added a long ~/.config/nvim/plugin/lean.lua that starts with require('lean').setup{ mappings = true }.

[Julian Berman]

Are there any vim.keymap lines in the lean.lua file?

[Antoine Chambert-Loir]

I added what Matthew suggested above from here hence I have such a line in the definition of on_attach, but I'm not even sure that file is loaded.

[Antoine Chambert-Loir]

What surprises me is that when I do :healthcheck, I get an error message from $HOME/.local/share/nvim/plugged/lean.nvim/lua/lean/_util.luaat line 74:

"lean" exited with non-zero exit status 1.

[Julian Berman]

You can put print("HELLO") at the top of the file if you want to see whether it's loaded, you should then see that when you start nvim -- but could you perhaps pastebin its entire contents, I'm not sure whether you're saying you have require('lean').setup{ mappings = true } in it once or twice (it should be only once).

[Julian Berman]

Antoine Chambert-Loir said:

What surprises me is that when I do :healthcheck, I get an error message from $HOME/.local/share/nvim/plugged/lean.nvim/lua/lean/_util.luaat line 74:

"lean" exited with non-zero exit status 1.

that would sound interesting too yeah, what happens if you run :!lean --version from within neovim?

[Antoine Chambert-Loir]

:!lean --version
error: toolchain 'leanprover/lean4:v4.7.0-rc1' is not installed
info: caused by: not a directory: '/Users/chambert/.elan/toolchains/leanprover--lean4---v4.7.0-rc1'

Oops…

[Antoine Chambert-Loir]

I have the exact content of the file there. (Before your remark, I had the mappings = true twice, but that doesn't change anything…)

[Antoine Chambert-Loir]

lean.lua

[Julian Berman]

Antoine Chambert-Loir said:

:!lean --version
error: toolchain 'leanprover/lean4:v4.7.0-rc1' is not installed
info: caused by: not a directory: '/Users/chambert/.elan/toolchains/leanprover--lean4---v4.7.0-rc1'

Oops…

I assume you're using elan right? I don't have elan handy, does it actually exit with nonzero status for lean --version if it hasn't yet installed the toolchain? Can you try lean --version; echo $? in a shell in that same project perhaps? That would be slightly surprising behavior, but if so probably nothing to worry about, as when it's really time to start the language server I assume then it would download it and all would be fine.

[Antoine Chambert-Loir]

I solved that. (In the main directory,the default version of lean was that obsolete one I had deleted, but I made it to a stable one.

(16:22) pro-acl > elan show
installed toolchains

---

leanprover/lean4:stable (default)
leanprover/lean4:v4.10.0
leanprover/lean4:v4.10.0-rc2
leanprover/lean4:v4.7.0
leanprover/lean4:v4.8.0-rc2

active toolchain

---

leanprover/lean4:stable (default)
Lean (version 4.6.1, x86_64-apple-darwin21.6.0, commit dac66e47e32f, Release)

[Julian Berman]

Antoine Chambert-Loir said:

lean.lua

OK yeah that doesn't seem like anything is wrong there. I am going to take my puppy out and make some coffee and then be back -- can you try perhaps removing the body of the on_attach function (or otherwise removing lines) until the error message goes away? Just keep the lean.setup{} line. If that works we can add it back.

[Antoine Chambert-Loir]

The error message disappeared after commenting out the body of on_attach.

[Julian Berman]

Oh! Your file differs from what Matthew shared.

[Julian Berman]

Probably it was from before I fixed it for newer neovims like 0.10.

[Julian Berman]

Specifically you have cmd('n', '<leader>q', vim.lsp.diagnostic.set_loclist) -- but that's now called vim.diagnostic.setloclist

[Antoine Chambert-Loir]

what?!

[Julian Berman]

If you make that change to cmd('n', '<leader>q', vim.diagnostic.setloclist) all should work

[Antoine Chambert-Loir]

Yeah! thanks!

[Julian Berman]

Great, please provide any feedback :) -- including now you're going to motivate me to get back to writing a bit more of https://github.com/Julian/lean.nvim/wiki/The-lean.nvim-Manual to replace that Getting Started page.

[Antoine Chambert-Loir]

I use vim for all the rest of my editing tasks and I was fed up of vscode for day 1. Moreover, my computer is not so fast for new software (it's a 2015 MacBook Pro), and I observe that lean with nvimis much more reactive. (Also, the vim plugin in vscode is not good enough for me.)

[Antoine Chambert-Loir]

To add feedback: I still don't understand how to have the hover stuff, nor how to use the output of apply?, or simp?. (Still, I can copy-paste)

[Julian Berman]

For hover, the mapping is K. So put your cursor somewhere and hit K and you should see a popup with the same as what you'd see in VSCode. (This K mapping is nvim-wide and should work in any language server).

[Julian Berman]

(Of course you can add another one if you prefer something else -- or you can add an autocmd which automatically shows the hover if you leave your cursor in the same spot. Let me know if you want instructions for that.)

[Antoine Chambert-Loir]

I'm not sure that's useful for me. Automatically hovering windows are sometimes a nuisance, I'll try to see if Kis sufficient for me.

[Julian Berman]

(I agree FWIW.)

[Julian Berman]

Antoine Chambert-Loir said:

nor how to use the output of apply?, or simp?.

These are called code actions -- and it looks like we didn't add a mapping in the page you were using. I'll be sure to both update that as well as update the new manual page. You can add:

      cmd('n', '<leader>a', vim.lsp.buf.code_action)
      cmd('i', '<C-a>', vim.lsp.buf.code_action)

at which point you then can activate them with <leader>a in normal mode or ctrl-a in insert mode.

[Julian Berman]

neovim 0.11 will bind some keys by default to do this, I think the new mapping will live on gra, but I like my suggestion better :)

[Julian Berman]

Also, I quite like https://github.com/aznhe21/actions-preview.nvim, so you might look at that as well -- basically it will show you what apply? etc. will replace as a diff, before you actually select which one you want. (That uses telescope, so you'd be adding telescope to your setup as well if you haven't already.) But of course none of that is required if you're happy with the simple UI that vim.lsp.buf.code_action() has by default.

[Matthew Ballard]

I've only got

  vim.api.nvim_buf_set_keymap(bufnr, 'n', '<leader>ca', '<cmd>lua vim.lsp.buf.code_action()<CR>', opts)

and it seems enough for me.

K is something I use all the time. You can also use return in the infoview (or at least I can and I can't see where I set it).

Another thing I use all the time is jumping to the next trace/warning/error:

vim.api.nvim_set_keymap('n', '[d', '<cmd>lua vim.diagnostic.goto_prev()<CR>', { noremap = true, silent = true })
vim.api.nvim_set_keymap('n', ']d', '<cmd>lua vim.diagnostic.goto_next()<CR>', { noremap = true, silent = true })

Though maybe these are already standard. I should probably clean my key mappings up.

[Matthew Ballard]

For apply?, the buffer gets pretty crowded with all the choices.

[Julian Berman]

That nvim_buf_set_keymap is basically equivalent -- looks like you have only a normal mode mapping -- whether you want an insert mode one too is obviously up to you, but I think it's useful e.g. when you're typing out a structure and you know that the skeleton expansion code action exists, so you don't need to exit insert mode to trigger it.

[Julian Berman]

The ]d mappings are yeah now automatic in 0.10 though there's no harm in keeping that.

[Julian Berman]

I think telescope (via the thing I linked) helps a bit with the crowding, as you can then type to filter the choices further.

[Julian Berman]

Also since you mentioned it, my ]d mapping is a bit more nuanced so maybe someone will like that -- https://github.com/Julian/dotfiles/blob/96340aa51972ec1bf5fa6f3e2d91309780b16723/.config/nvim/init.lua#L357-L370 it does what yours does (what the default does) but it only shows a popup if the diagnostic isn't just likely to be what you already see in the virtual text, which is a bit pointless to show twice for short Lean (or whatever) diagnostics.

[Matthew Ballard]

While we’re here, is there a filler for the diagnostics returning only the errors?

[Julian Berman]

vim.diagnostic.goto_next{ severity = vim.diagnostic.severity.ERROR }

[Matthew Ballard]

Is there a default binding for that now?

[Julian Berman]

Nope -- the ones that exist are https://github.com/neovim/neovim/blob/fd1d84c705128372dc25e3a833e9a1dc6b9e81e0/runtime/lua/vim/_defaults.lua#L177-L208

[Julian Berman]

(That's for 0.11 / nightly, to be clear.)

[Matthew Ballard]

Thanks!

[Antoine Chambert-Loir]

New questions: in the default install I came up to yesterday, there's supposed to be a way to go the next/prev line with a diagnostic message, but I can't understand what <leader> has been assigned to.

-- <leader>n will jump to the next Lean line with a diagnostic message on it
-- <leader>N will jump backwards
cmd('n', '<leader>n', function() vim.diagnostic.goto_next{popup_opts = {show_header = false}} end)
cmd('n', '<leader>N', function() vim.diagnostic.goto_prev{popup_opts = {show_header = false}} end)

[Matthew Ballard]

Space?

[Antoine Chambert-Loir]

You mean, I just type ' n', and it goes to the next Lean line with a diagnostic message?

[Markus Himmel]

<leader> is a general vim concept not specific to Lean. You can show the leader you have configured using :show mapleader. If it is undefined, then the default value is \. So typing \n should jump to the next diagnostic message.

[Julian Berman]

Yeah -- \ is pretty awkward to type (probably on both US and AIUI french keyboards) so space is usually what I'd recommend. You can add vim.g.mapleader = ' ' to the top of your init.lua to change that to space if so.

[Julian Berman]

Also, like Matthew mentioned elsewhere, neovim now also automatically defines ]d and [dfor this by default as well, so those keyboard shortcuts may work for you too (I use them now).

[Antoine Chambert-Loir]

Thanks!

[Antoine Chambert-Loir]

By the way, I just got a bizarre error message :

Error executing vim.schedule lua callback: vim/inspect.lua:0: attempt to compare number with nil
stack traceback:
vim/inspect.lua: in function 'putValue'
vim/inspect.lua: in function 'putValue'
vim/inspect.lua: in function 'putValue'
vim/inspect.lua: in function 'putValue'
vim/inspect.lua: in function 'inspect'
...lar/neovim/0.10.1/share/nvim/runtime/lua/vim/lsp/rpc.lua:292: in function 'notify'
.../neovim/0.10.1/share/nvim/runtime/lua/vim/lsp/client.lua:784: in function 'notify'
...ert/.local/share/nvim/plugged/lean.nvim/lua/lean/rpc.lua:101: in function 'release_now'
...ert/.local/share/nvim/plugged/lean.nvim/lua/lean/rpc.lua:117: in function ''
vim/_editor.lua: in function ''
vim/_editor.lua: in function <vim/_editor.lua:0>

[Antoine Chambert-Loir]

LSP[leanls]: Error NO_RESULT_CALLBACK_FOUND: {
error = {
code = -32601,
message = "No RPC method 'Lean.Widget.getInteractiveDiagnostics' found"
},
id = 443278,
jsonrpc = "2.0"
}

[Matthew Ballard]

I get the last one (or something similar) if I let things sit around too long untouched

[Antoine Chambert-Loir]

That's OK. I'll try to think and type faster.

[Matthew Ballard]

I mean ~ 30 minutes of inactivity.

[Julian Berman]

Yeah I've seen that one too and haven't looked into it carefully, let's see now if I can either reproduce or fix it.

[Matthew Ballard]

Julian Berman said:

Also, I quite like https://github.com/aznhe21/actions-preview.nvim, so you might look at that as well -- basically it will show you what apply? etc. will replace as a diff, before you actually select which one you want.

Ooo. This is nice.

[Julian Berman]

It's in the readme, and I mentioned it in the other thread, but let me know if you have suggestions for more effective ways to announce that sort of thing. I guess at some point hopefully I'll write up lean.nvim release notes, and do this "pRoPerLY" which will make it easier to mention nice new things.

[Antoine Chambert-Loir]

There's an annoying behaviour at end of lines: if I enter <return> just after a character, neovim tries to complete, which forces me to enter <space>, bringing trailing spaces at end of lines, or <shift-return>, which I'm not used to.
Is there a possibility to match <tab> for autocompletion and have <enter> just
pass to the next line?

[Julian Berman]

This is with cmp presumably?

[Antoine Chambert-Loir]

presumably, and in the init.lua file, I just made this modification

  ['<Tab>'] = cmp.mapping.confirm({ select = true }),

and it seems to do what I expected.

[Patrick Massot]

There is tension here that I understand very well. Like Antoine, I’ve been using vim for all my editing for more than twenty years. So it is very frustrating to use VSCode for Lean, and we expect that lean.nvim will be very easy to use for us. But we are old school vim users who don’t know much about the modern (and much better!) vim style that is used here. I spent some time investing in learning a bit about modern vim, and I don’t regret it. It made vim even better also for my old uses.

Something that does not change with modern vim is that vim is still an editor for people who like to customize their editing experience. This is partly unavoidable because of the emphasis on keyboard use. There are simply too many things people could want to do vim their vim, so there is no way to assign default keybindings to everything (whereas you can always add menu item in mouse-based software like VSCode). Note however that more and more people try to package pre-configured vim that are meant to be usable out of the box. For instance lazyvim, nvchad, LunarVim, AstroVim… But for some reason they don’t seem to have realized yet that lean.nvim should be part of their story.

[Patrick Massot]

Antoine, something else you can explore is starting from someone else’s config. GitHub is full of those. Julian’s one can be found at https://github.com/Julian/dotfiles/tree/main/.config/nvim, mine is at https://github.com/PatrickMassot/neovim_config. The issue with that strategy is that it can be hard to untangle what you are interested in from stuff you don’t need (or even stuff that would clash with your other settings).

[Patrick Massot]

Julian Berman said:

Also, I quite like https://github.com/aznhe21/actions-preview.nvim, so you might look at that as well -- basically it will show you what apply? etc. will replace as a diff, before you actually select which one you want. (That uses telescope, so you'd be adding telescope to your setup as well if you haven't already.) But of course none of that is required if you're happy with the simple UI that vim.lsp.buf.code_action() has by default.

The issue is this is obviously not Lean aware. It will show you what the tactic script would become, but in many cases (for instance after a apply?, you are mostly interested in what the tactic state would become.