diff options
| author | Justin M. Keyes <justinkz@gmail.com> | 2024-10-01 05:39:12 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2024-10-01 05:39:12 -0700 |
| commit | bedb2a0df105f68a624a49b867f269b6d55a2c89 (patch) | |
| tree | 877aa3ef8277575a7ffea1ff8f280eeb69b47489 /lua/lspconfig/configs/leanls.lua | |
| parent | docs: CONTRIBUTING.md cleanup (diff) | |
| download | nvim-lspconfig-bedb2a0df105f68a624a49b867f269b6d55a2c89.tar nvim-lspconfig-bedb2a0df105f68a624a49b867f269b6d55a2c89.tar.gz nvim-lspconfig-bedb2a0df105f68a624a49b867f269b6d55a2c89.tar.bz2 nvim-lspconfig-bedb2a0df105f68a624a49b867f269b6d55a2c89.tar.lz nvim-lspconfig-bedb2a0df105f68a624a49b867f269b6d55a2c89.tar.xz nvim-lspconfig-bedb2a0df105f68a624a49b867f269b6d55a2c89.tar.zst nvim-lspconfig-bedb2a0df105f68a624a49b867f269b6d55a2c89.zip | |
refactor: rename "server_configurations" => "configs" #3330
Problem:
The name `server_configurations` is extremely verbose and irritatingly
formal and dogmatic. This overlong name is a constant nuisance when
reading, writing, and coding.
It's also not even correct: these configurations are just as much
"client" configurations as they are "server" configurations.
Solution:
- Rename to a shorter name.
- Leave placeholder files for any old URLs that link to the old
location.
Diffstat (limited to 'lua/lspconfig/configs/leanls.lua')
| -rw-r--r-- | lua/lspconfig/configs/leanls.lua | 52 |
1 files changed, 52 insertions, 0 deletions
diff --git a/lua/lspconfig/configs/leanls.lua b/lua/lspconfig/configs/leanls.lua new file mode 100644 index 00000000..63349a14 --- /dev/null +++ b/lua/lspconfig/configs/leanls.lua @@ -0,0 +1,52 @@ +local util = require 'lspconfig.util' + +return { + default_config = { + cmd = { 'lake', 'serve', '--' }, + filetypes = { 'lean' }, + root_dir = function(fname) + -- check if inside elan stdlib + fname = util.path.sanitize(fname) + local stdlib_dir + do + local _, endpos = fname:find '/src/lean' + 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 + + return util.root_pattern('lakefile.toml', 'lakefile.lean', 'lean-toolchain')(fname) + or stdlib_dir + or util.find_git_ancestor(fname) + end, + on_new_config = function(config, root_dir) + -- add root dir as command-line argument for `ps aux` + table.insert(config.cmd, root_dir) + end, + single_file_support = true, + }, + docs = { + description = [[ +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`. + ]], + default_config = { + root_dir = [[root_pattern("lakefile.toml", "lakefile.lean", "lean-toolchain", ".git")]], + }, + }, +} |
