Skip to content

Commit

Permalink
Add lean4ls and improve Lean root directory search.
Browse files Browse the repository at this point in the history
  • Loading branch information
rish987 committed Jun 2, 2021
1 parent 29ea30f commit e6cc39c
Show file tree
Hide file tree
Showing 2 changed files with 43 additions and 2 deletions.
32 changes: 32 additions & 0 deletions lua/lspconfig/lean4ls.lua
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
local configs = require 'lspconfig/configs'
local util = require 'lspconfig/util'

local function find_toml(startpath)
return util.search_ancestors(util.path.dirname(startpath), function(path)
local toml_file = util.path.join(path, "leanpkg.toml")
if util.path.is_file(toml_file) then
return toml_file
end
end)
end

configs.lean4ls = {
default_config = {
cmd = {"lean4", "--server"};

This comment has been minimized.

Copy link
@gebner

gebner Jun 2, 2021

Contributor

The executable name is lean, not lean4.

This comment has been minimized.

Copy link
@mjlbach

mjlbach Jun 2, 2021

Contributor

This comment has been minimized.

Copy link
@mjlbach

mjlbach Jun 2, 2021

Contributor

Ah, I see, is this someone's fork? Not sure how I'm getting notifications for this.

This comment has been minimized.

Copy link
@gebner

gebner Jun 2, 2021

Contributor

No, Rishikesh is working on improving the neovim plugin for Lean and he plans to PR this soon so I'm commenting here. This is the lean.nvim PR: Julian/lean.nvim#35

filetypes = {"lean4"};
root_dir = function(fname)
return find_toml(fname) or util.find_git_ancestor(fname) or vim.loop.os_homedir()
end;
};
docs = {
package_json = "https://raw.githubusercontent.com/leanprover-community/vscode-lean4/master/package.json",

This comment has been minimized.

Copy link
@gebner

gebner Jun 2, 2021

Contributor

This just looks wrong, there's no relation at all to the vscode extension. But apparently the configuration files for the other languages also link to corresponding vscode extensions....

This comment has been minimized.

Copy link
@mjlbach

mjlbach Jun 2, 2021

Contributor

We use this for docgen to parse the settings for the language server, most of the time this works, but I try to verify the settings match the language server (and not the extension).

This comment has been minimized.

Copy link
@gebner

gebner Jun 2, 2021

Contributor

So every configuration option of the vscode extension is listed on https://github.com/neovim/nvim-lspconfig/blob/master/CONFIG.md?

This is just completely wrong (at least for vscode-lean4). Every single configuration option there is for the vscode extension, and has nothing at all to do with the LSP server. (These are literally the options that vscode shows in the settings dialog; they are not passed to the LSP server.)

This comment has been minimized.

Copy link
@mjlbach

mjlbach Jun 2, 2021

Contributor

Yep, so if that's the case it shouldn't be included. RA for example includes the RA settings (not just the vscode settings) in the package.json (and many other servers do) which is why you see it for other servers.

This comment has been minimized.

Copy link
@gebner

gebner Jun 2, 2021

Contributor

@rish987 I think you should remove the package_json line. ^^ (also in the Lean 3 file)

description = [[
The Lean 4 language server is built-in with a Lean 4 install,
and can be run with, e.g., "lean4 --server".

This comment has been minimized.

Copy link
@gebner

gebner Jun 2, 2021

Contributor

Same here, it's lean not lean4.

]];
default_config = {
root_dir = [[find_toml() or root_pattern(".git") or os_homedir]];
};
};
}
-- vim:et ts=2 sw=2
13 changes: 11 additions & 2 deletions lua/lspconfig/leanls.lua
Original file line number Diff line number Diff line change
@@ -1,12 +1,21 @@
local configs = require 'lspconfig/configs'
local util = require 'lspconfig/util'

local function find_toml(startpath)
return util.search_ancestors(util.path.dirname(startpath), function(path)
local toml_file = util.path.join(path, "leanpkg.toml")
if util.path.is_file(toml_file) then
return toml_file
end
end)
end

configs.leanls = {
default_config = {
cmd = {"lean-language-server", "--stdio"};
filetypes = {"lean"};
root_dir = function(fname)
return util.find_git_ancestor(fname) or vim.loop.os_homedir()
return find_toml(fname) or util.find_git_ancestor(fname) or vim.loop.os_homedir()
end;
};
docs = {
Expand All @@ -17,7 +26,7 @@ https://github.com/leanprover/lean-client-js/tree/master/lean-language-server
Lean language server.
]];
default_config = {
root_dir = [[root_pattern(".git") or os_homedir]];
root_dir = [[find_toml() or root_pattern(".git") or os_homedir]];
};
};
}
Expand Down

0 comments on commit e6cc39c

Please sign in to comment.