aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorY. Ding <yuzheng.q.ding@gmail.com>2025-11-18 09:32:54 -0800
committerGitHub <noreply@github.com>2025-11-18 09:32:54 -0800
commit61122cf099681d0c3f6463548327eed1ca6390a3 (patch)
tree7102b16c842b27f84a5c62c77ed4b93c4fb775c3
parentdocs: update configs.md (diff)
downloadnvim-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.lua45
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,
-}