how to setup lean lsp for neovim?

Stream: general

[Cheesehead]

I am a newbie here trying to setup lean. I saw the language server solution for vscode in the documentation. But for other editors, I didn't find instructions for that.
Actually I found 3 possible lsp interface for lean:
lean --server
lake serve
and a npm package named lean-language-server.
Which one should I use and how to enable it in neovim (I use coc.nivm for auto-completion) ?
If anyone can help, I would be very grateful.

[Julian Berman]

Hi there. Have you found the README here: https://github.com/Julian/lean.nvim/#installation

If not have a look and do ask questions if it's not clear enough, you'll find there's a page there that should assume no prior knowledge (but yeah if that's still not clear enough more than happy to fix it and help)

[Siyuan Yan]

Hi, I'm a new lean user. I use neovim too and I actually just set it up yesterday

[Julian Berman]

Nice. Welcome to you both.

[Siyuan Yan]

I'm on Arch Linux and I use the npm package lean-language-server from AUR. but for completion I don't use coc.nvim. I use nvim-cmp instead so my vimrc file probablly won't help you.

[Siyuan Yan]

Are you the Julian of lean.nvim??? @Julian Berman

[Julian Berman]

Depends, did you encounter a bug?

[Siyuan Yan]

image.png
this has perplexed me. I couldn't figure out how to set my local leader to space space.
I tried this:

let mapleader = " "
let localmapleader = "  "

and this:

let mapleader = "\<space>"
let localmapleader = "\<space>\<space>"

leader works but not localmapleader
when I set localmapleader to something like backslash, it works as expected

[Cheesehead]

I saw your project on github. but I it seems to need a lot of other dependencies and I'm not sure if they will be compatible with my existing plugins (especially those lsp related ones).

[Siyuan Yan]

I have a lot of plugins too and lean.nvim has worked wonderfully so far. I don't know coc.nvim but do you have an existing on_attach function? all I did extra in my config file was to pass the function to lean.nvim setup

[Cheesehead]

That sounds great. I'm going to try it out.

[Siyuan Yan]

@Julian Berman yeah I do have a more related question too. A plugin of mine cmp_nvim_lsp instructs me to pass a capabilities thingy when I set up lsps. I don't understand what it does. Should I do that too lean.nvim too? Also I use exclusively lean3, is it safe to comment out lsp = {on_attach = on_attach} line?
here's the relevant part of my config file:

-- Set up lspconfig.
  local capabilities = require('cmp_nvim_lsp').default_capabilities(vim.lsp.protocol.make_client_capabilities())
-- bash language server
require'lspconfig'.bashls.setup{
    on_attach = on_attach,
    capabilities = capabilities
}
-- python language server
require'lspconfig'.jedi_language_server.setup{
    on_attach = on_attach,
    capabilities = capabilities
}

-- lean
require('lean').setup{
  abbreviations = { builtin = true },
-- can I comment out this line?
  lsp = { on_attach = on_attach, capabilities = capabilities },
-- do I need to pass `capabilities`?
  lsp3 = {
      on_attach = on_attach,
      capabilities = capabilities
  },
  mappings = true,
}

[Julian Berman]

Siyuan Yan said:

image.png
this has perplexed me. I couldn't figure out how to set my local leader to space space.
I tried this:

let mapleader = " "
let localmapleader = "  "

and this:

let mapleader = "\<space>"
let localmapleader = "\<space>\<space>"

leader works but not localmapleader
when I set localmapleader to something like backslash, it works as expected

The right way is the second way but you need maplocalleader not localmapleader.

Here's a link to my dotfiles which you can also just copy paste if you'd like: https://github.com/Julian/dotfiles/blob/main/.config/nvim/init.vim#L3-L4

[Siyuan Yan]

@Julian Berman omg, thanks! Also I actually looked into your dotfiles repo yesterday (sorry for being creepy) and did a quick search for lean related configs but found nothing haha

[Julian Berman]

Cheesehead said:

I saw your project on github. but I it seems to need a lot of other dependencies and I'm not sure if they will be compatible with my existing plugins (especially those lsp related ones).

I use... 65+ plugins myself :) -- https://github.com/Julian/dotfiles/blob/main/.config/nvim/init.vim#L35-L117 and no issues, though that's a bit biased since if I encountered one I'd fix lean.nvim -- but certainly if you encounter one we definitely would look at it and try to fix it

[Julian Berman]

Siyuan Yan said:

Julian Berman omg, thanks! Also I actually looked into your dotfiles repo yesterday (sorry for being creepy) and did a quick search for lean related configs but found nothing haha

It's not creepy :) that's why it's public.

[Cheesehead]

I used vim before and just switched to neovim and I don't follow the community trends recently. So neovim is planning to do everything with pure lua? Should I then use a plugin like nvim-cmp to replace what I am using?

[Julian Berman]

Yes, likely you should.

[Julian Berman]

(All these are personal choices, but yes that would be my recommendation)

[Julian Berman]

Re: Lean 4, the community is (hopefully) getting quite close now to Lean 4 being used for mathlib (FSVO "quite close") -- so even if you don't use Lean 4 you maybe should still include that, but if you really don't want to for the next 6 months or whatever, yes you can just leave off that line.

[Siyuan Yan]

(deleted)

[Siyuan Yan]

Julian Berman said:

Re: Lean 4, the community is (hopefully) getting quite close now to Lean 4 being used for mathlib (FSVO "quite close") -- so even if you don't use Lean 4 you maybe should still include that, but if you really don't want to for the next 6 months or whatever, yes you can just leave off that line.

Last time I checked mathlib4 on github (yesterday) it seemed lacking in comparison? I didn't find a Number Theory folder for example, which is what I'm interested in. Is there a website I can compare what's missing in mathlib4?
I'm just saying that this directory of mathlib4 seems to have much few content compared to this directory of mathlib.

[Julian Berman]

It is lacking but there's some very recent progress in the sense that as of the last few days there's now a call for "help port files now, it's ready" in some concrete sense, and @Scott Morrison just did a youtube video last night https://www.youtube.com/watch?v=-Nu0mSeABK0 to help others pitch in so I think hopefully it's about to see lots of increased activity

[Julian Berman]

(I'm on a call otherwise I'd go find the announcement thread with proper details but you can find it in the #mathlib4 stream I think)

[Siyuan Yan]

Ah, good work! If I were a bit more familiar with lean I would definitely help!

[Julian Berman]

(Gone for a bit, but yeah if either of you run into issues with setup or usage do leave bug reports and/or messages.)