Help with lean.nvim

Stream: new members

[Simon Jacobsson]

I am trying to use the lean.nvim plugin for Neovim (0.7), but when typing :LeanGoal in Neovim, I get an error message "LSP server not connected".

I have followed this guide for setting up the plugin, and then also, since I didn't have a "preferred setup which includes LSP key mappings and (auto)completion", I have followed this guide for setting up my lean.lua.

One guess is that there is something wrong with my lean-language-server. If I type lean-language-server into the terminal, I get the following message back:

simon@orvar:~$ lean-language-server
/usr/local/lib/node_modules/lean-language-server/node_modules/vscode-languageserver/lib/node/main.js:185
        throw new Error('Connection input stream is not set. ' + commandLineMessage);
        ^

Error: Connection input stream is not set. Use arguments of createConnection or set command line parameters: '--node-ipc', '--stdio' or '--socket={number}'
    at _createConnection (/usr/local/lib/node_modules/lean-language-server/node_modules/vscode-languageserver/lib/node/main.js:185:15)
    at Object.createConnection (/usr/local/lib/node_modules/lean-language-server/node_modules/vscode-languageserver/lib/node/main.js:132:12)
    at Object.<anonymous> (/usr/local/lib/node_modules/lean-language-server/lib/index.js:17:27)
    at Module._compile (node:internal/modules/cjs/loader:1105:14)
    at Module._extensions..js (node:internal/modules/cjs/loader:1159:10)
    at Module.load (node:internal/modules/cjs/loader:981:32)
    at Module._load (node:internal/modules/cjs/loader:827:12)
    at Function.executeUserEntryPoint [as runMain] (node:internal/modules/run_main:77:12)
    at node:internal/main/run_main_module:17:47

Node.js v18.2.0

Possibly related, I get an error message when typing <LocalLeader>s in Neovim:

E5108: Error executing lua ...n/.vim/plugged_for_nvim_0.7/lean.nvim/lua/lean/sorry.lua:25: bad
argument #1 to 'pairs' (table expected, got nil)
stack traceback:
        [C]: in function 'pairs'
        ...n/.vim/plugged_for_nvim_0.7/lean.nvim/lua/lean/sorry.lua:25: in function 'fill'
        [string ":lua"]:1: in main chunk

Below is the init.vim I'm using.

let g:plugged_home = '~/.vim/plugged_for_nvim_0.7'

call plug#begin(g:plugged_home)
    Plug 'Julian/lean.nvim'
    Plug 'neovim/nvim-lspconfig'
    Plug 'nvim-lua/plenary.nvim'
    Plug 'hrsh7th/nvim-compe'
call plug#end()

autocmd FileType lean let maplocalleader="+"

[Simon Jacobsson]

@Julian Berman

[Julian Berman]

The lean-language-server error seems fine, unfortunately language servers occasionally have this tendency to be pretty unhelpful if you run them interactively and don't know what the right way to invoke them is. In this case, one needs to run lean-language-server --stdio, which neovim is going to do.

[Julian Berman]

I'm about to jump on a call, so I may have to come back, but just to confirm, you're running :LeanGoal after having opened a lean file right?

[Julian Berman]

Not just from an empty buffer?

[Julian Berman]

Before I run, a possible problem from the crystal ball :P is you're probably opening a single file somewhere? That works fine, but the default version of Lean will be Lean 4 in that case, which you may not have installed. If I'm correct and you're just doing nvim foo.lean, either try first opening a file in a mathlib clone (follow the leanproject get instructions from the site), and if that works, we'll either be able to tell lean.nvim you want Lean 3 by default or you should create a project with leanproject new, which lean.nvim will then realize means you're using Lean 3.

[Julian Berman]

And if all the above is wrong, I'll help later.

[Julian Berman]

Also idly, you don't want to set maplocalleader in an autocmd like that -- I'm not even 100% sure it'll work, the way localleader works is via this funny macro expansion, so it's probably going to be defined too late -- but also, you almost certainly want to use the same local leader key for all your filetypes

[Julian Berman]

So just do it globally, e.g.: https://github.com/Julian/dotfiles/blob/main/.config/nvim/init.vim#L4

[Simon Jacobsson]

Julian Berman said:

The lean-language-server error seems fine, unfortunately language servers occasionally have this tendency to be pretty unhelpful if you run them interactively and don't know what the right way to invoke them is. In this case, one needs to run lean-language-server --stdio, which neovim is going to do.

Yes, running 'lean-language-server --stdio' didn't give me any error messages.

[Simon Jacobsson]

Julian Berman said:

Before I run, a possible problem from the crystal ball :P is you're probably opening a single file somewhere? That works fine, but the default version of Lean will be Lean 4 in that case, which you may not have installed. If I'm correct and you're just doing nvim foo.lean, either try first opening a file in a mathlib clone (follow the leanproject get instructions from the site), and if that works, we'll either be able to tell lean.nvim you want Lean 3 by default or you should create a project with leanproject new, which lean.nvim will then realize means you're using Lean 3.

You were right!
I ranleanproject get tutorials and opened a file from there. Now I get the continuous compilation and I can go to definitions. <LocalLeader>s now also does what it should.

[Simon Jacobsson]

thanks alot :D

I did not know about leanproject but it seems like a sane tool.

[Julian Berman]

Great, glad to hear it. Enjoy.