From c6e2321245f56e0ce80a2ab87deb397c9ed0e822 Mon Sep 17 00:00:00 2001
From: Julian Berman <Julian@GrayVines.com>
Date: Sat, 5 Feb 2022 22:13:39 -0500
Subject: feat(leanls): start the LSP via lake serve (#1698)

Enables workspace symbols for the Lean 4 LSP.

Older versions of Lake (and Lean 4) lack a serve command,
so on those we fallback to the old behavior by directly starting
the LSP.

Closes: Julian/lean.nvim#229
Refs: leanprover/lake#46
---
 lua/lspconfig/server_configurations/leanls.lua | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

(limited to 'lua')

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,
-- 
cgit v1.2.3-70-g09d2