Zulip Chat Archive

Stream: general

Topic: how to setup lean lsp for neovim?


Cheesehead (Nov 03 2022 at 16:00):

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 (Nov 03 2022 at 16:02):

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 (Nov 03 2022 at 16:03):

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

Julian Berman (Nov 03 2022 at 16:03):

Nice. Welcome to you both.

Siyuan Yan (Nov 03 2022 at 16:05):

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 (Nov 03 2022 at 16:05):

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

Julian Berman (Nov 03 2022 at 16:06):

Depends, did you encounter a bug?

Siyuan Yan (Nov 03 2022 at 16:07):

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 (Nov 03 2022 at 16:08):

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 (Nov 03 2022 at 16:10):

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 (Nov 03 2022 at 16:14):

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

Siyuan Yan (Nov 03 2022 at 16:16):

@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 (Nov 03 2022 at 16:18):

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 (Nov 03 2022 at 16:19):

@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 (Nov 03 2022 at 16:19):

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 (Nov 03 2022 at 16:20):

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 (Nov 03 2022 at 16:21):

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 (Nov 03 2022 at 16:21):

Yes, likely you should.

Julian Berman (Nov 03 2022 at 16:22):

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

Julian Berman (Nov 03 2022 at 16:23):

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 (Nov 03 2022 at 16:33):

(deleted)

Siyuan Yan (Nov 03 2022 at 16:35):

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 (Nov 03 2022 at 16:35):

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 (Nov 03 2022 at 16:35):

(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 (Nov 03 2022 at 16:36):

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

Julian Berman (Nov 03 2022 at 16:36):

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


Last updated: Dec 20 2023 at 11:08 UTC