diff options
| author | Lorenzo Bellina <59364991+TheRealLorenz@users.noreply.github.com> | 2025-04-13 00:15:43 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2025-04-12 15:15:43 -0700 |
| commit | 81a570f58b2113cc2d538efae743ad38d6ab564f (patch) | |
| tree | 74f9691bbb1b303cd7cfaab7b543f82cb0dc6b46 /lsp/lean3ls.lua | |
| parent | refactor: replace vim.loop with vim.uv #3703 (diff) | |
| download | nvim-lspconfig-81a570f58b2113cc2d538efae743ad38d6ab564f.tar nvim-lspconfig-81a570f58b2113cc2d538efae743ad38d6ab564f.tar.gz nvim-lspconfig-81a570f58b2113cc2d538efae743ad38d6ab564f.tar.bz2 nvim-lspconfig-81a570f58b2113cc2d538efae743ad38d6ab564f.tar.lz nvim-lspconfig-81a570f58b2113cc2d538efae743ad38d6ab564f.tar.xz nvim-lspconfig-81a570f58b2113cc2d538efae743ad38d6ab564f.tar.zst nvim-lspconfig-81a570f58b2113cc2d538efae743ad38d6ab564f.zip | |
feat: migrate to vim.lsp.config #3659
Problem:
Nvim 0.11 has vim.lsp.config, which mostly replaces the legacy
nvim-lspconfig "framework".
Solution:
Migrate all configs to `lsp/*` variants. The old configs in
`lua/lspconfig/` are "frozen".
The new configs include these changes:
- `commands` field became raw calls to
`vim.api.nvim_buf_create_user_command` inside `on_attach`.
- `root_dir` became:
- `root_markers` whenever the file list was simple didn't need to mach `*`
- if the logic was complicated, or needed to match something like
'\*.c', it was defined as a vim.lsp.Config `root_dir` callback.
- `on_config_change` became `before_init`. I don't actually know if this
is the correct approach, but looking around the documentation of
`nvim-lspconfig` a saw that it was defined as the function that gets
called as soon as the config have `root_dir`, and so I thought
`before_init` might be the closest alternative.
- `docs.description` became a luadoc `@brief` docstring.
- `single_file_support = false`?
Co-authored-by: Aliou Diallo <aliou@users.noreply.github.com>
Co-authored-by: Justin M. Keyes <justinkz@gmail.com>
Diffstat (limited to 'lsp/lean3ls.lua')
| -rw-r--r-- | lsp/lean3ls.lua | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/lsp/lean3ls.lua b/lsp/lean3ls.lua new file mode 100644 index 00000000..58301588 --- /dev/null +++ b/lsp/lean3ls.lua @@ -0,0 +1,41 @@ +local util = require 'lspconfig.util' + +---@brief +--- +---https://github.com/leanprover/lean-client-js/tree/master/lean-language-server +-- +-- Lean installation instructions can be found +-- [here](https://leanprover-community.github.io/get_started.html#regular-install). +-- +-- Once Lean is installed, you can install the Lean 3 language server by running +-- ```sh +-- npm install -g lean-language-server +-- ``` +-- +-- 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 `lean3ls` both with it and `lspconfig`. +return { + cmd = { 'lean-language-server', '--stdio', '--', '-M', '4096', '-T', '100000' }, + filetypes = { 'lean3' }, + offset_encoding = 'utf-32', + root_dir = function(bufnr, on_dir) + local fname = vim.api.nvim_buf_get_name(bufnr) + fname = vim.fs.normalize(fname) + -- check if inside elan stdlib + local stdlib_dir + do + local _, endpos = fname:find '/lean/library' + if endpos then + stdlib_dir = fname:sub(1, endpos) + end + end + + on_dir( + util.root_pattern 'leanpkg.toml'(fname) + or util.root_pattern 'leanpkg.path'(fname) + or stdlib_dir + or vim.fs.dirname(vim.fs.find('.git', { path = fname, upward = true })[1]) + ) + end, +} |
