diff options
Diffstat (limited to 'lua')
| -rw-r--r-- | lua/lspconfig/server_configurations/leanls.lua | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/lua/lspconfig/server_configurations/leanls.lua b/lua/lspconfig/server_configurations/leanls.lua index 52d55545..924805eb 100644 --- a/lua/lspconfig/server_configurations/leanls.lua +++ b/lua/lspconfig/server_configurations/leanls.lua @@ -1,8 +1,12 @@ local util = require 'lspconfig.util' +-- Only Lake 3.0+ supports lake serve, so for old enough Lean 4, +-- we fallback to the builtin LSP. +local legacy_cmd = { 'lean', '--server' } + return { default_config = { - cmd = { 'lean', '--server' }, + cmd = { 'lake', 'serve', '--' }, filetypes = { 'lean' }, root_dir = function(fname) -- check if inside elan stdlib @@ -20,6 +24,19 @@ return { or util.find_git_ancestor(fname) end, on_new_config = function(config, root_dir) + local lake_version = '' + local lake_job = vim.fn.jobstart({ 'lake', '--version' }, { + on_stdout = function(_, d, _) + lake_version = table.concat(d, '\n') + end, + stdout_buffered = true, + }) + if lake_job > 0 and vim.fn.jobwait({ lake_job })[1] == 0 then + local major = lake_version:match 'Lake version (%d).' + if major and tonumber(major) < 3 then + config.cmd = legacy_cmd + end + end -- add root dir as command-line argument for `ps aux` table.insert(config.cmd, root_dir) end, |