diff options
| author | Y. Ding <yuzheng.q.ding@gmail.com> | 2025-11-18 09:32:54 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2025-11-18 09:32:54 -0800 |
| commit | 61122cf099681d0c3f6463548327eed1ca6390a3 (patch) | |
| tree | 7102b16c842b27f84a5c62c77ed4b93c4fb775c3 | |
| parent | docs: update configs.md (diff) | |
| download | nvim-lspconfig-61122cf099681d0c3f6463548327eed1ca6390a3.tar nvim-lspconfig-61122cf099681d0c3f6463548327eed1ca6390a3.tar.gz nvim-lspconfig-61122cf099681d0c3f6463548327eed1ca6390a3.tar.bz2 nvim-lspconfig-61122cf099681d0c3f6463548327eed1ca6390a3.tar.lz nvim-lspconfig-61122cf099681d0c3f6463548327eed1ca6390a3.tar.xz nvim-lspconfig-61122cf099681d0c3f6463548327eed1ca6390a3.tar.zst nvim-lspconfig-61122cf099681d0c3f6463548327eed1ca6390a3.zip | |
fix(leanls) : drop outdated config #4177
The old file has compatibility issues with the newest version of the `lean.nvim` plugin.
The `lean.nvim` plugin now handles language server attachment internally and no longer requires `nvim-lspconfig`. However, for users who still need `nvim-lspconfig` installed (e.g., for other languages), the existing file would shadow the newer one, leading to conflicts. This update directly copies the relevant file from `lean.nvim` to resolve this.
| -rw-r--r-- | lsp/leanls.lua | 45 |
1 files changed, 0 insertions, 45 deletions
diff --git a/lsp/leanls.lua b/lsp/leanls.lua deleted file mode 100644 index e5c03fdd..00000000 --- a/lsp/leanls.lua +++ /dev/null @@ -1,45 +0,0 @@ ----@brief ---- https://github.com/leanprover/lean4 ---- ---- Lean installation instructions can be found ---- [here](https://leanprover-community.github.io/get_started.html#regular-install). ---- ---- The Lean language server is included in any Lean installation and ---- does not require any additional packages. ---- ---- Note: that if you're using [lean.nvim](https://github.com/Julian/lean.nvim), ---- that plugin fully handles the setup of the Lean language server, ---- and you shouldn't set up `leanls` both with it and `lspconfig`. - ----@type vim.lsp.Config -return { - cmd = function(dispatchers, config) - local local_cmd = { 'lake', 'serve', '--', config.root_dir } - return vim.lsp.rpc.start(local_cmd, dispatchers) - end, - filetypes = { 'lean' }, - root_dir = function(bufnr, on_dir) - local fname = vim.api.nvim_buf_get_name(bufnr) - fname = vim.fs.normalize(fname) - -- check if inside lean stdlib - local stdlib_dir - do - local _, endpos = fname:find '/lean/library' - if endpos then - stdlib_dir = fname:sub(1, endpos) - end - end - if not stdlib_dir then - local _, endpos = fname:find '/lib/lean' - if endpos then - stdlib_dir = fname:sub(1, endpos) - end - end - - on_dir( - vim.fs.root(fname, { 'lakefile.toml', 'lakefile.lean', 'lean-toolchain' }) - or stdlib_dir - or vim.fs.dirname(vim.fs.find('.git', { path = fname, upward = true })[1]) - ) - end, -} |
