feat(leanls): add support for lakefile.toml-only packages (#3238)

This is partially a bugfix, as such packages would appear to function
correctly because we fell back to `lean --server` -- but that is a lie,
as it means `lake` doesn't control the LSP environment (and specifically
it means that shared objects aren't correctly found for a package which
prebuilds them with prebuildModules).

While we're here, remove said ancient Lean 4 logic for versions no one
has used for years, simplifying the startup (and saving a subprocess).
It'd have been better to fail loudly here rather than falling back to
confusing errors.

1 files changed, 4 insertions, 29 deletions

diff --git a/lua/lspconfig/server_configurations/leanls.lua b/lua/lspconfig/server_configurations/leanls.lua
index 208598af..63349a14 100644
--- a/lua/lspconfig/server_configurations/leanls.lua
+++ b/lua/lspconfig/server_configurations/leanls.lua
@@ -21,36 +21,11 @@ return {
         end
       end
 
-      return util.root_pattern('lakefile.lean', 'lean-toolchain', 'leanpkg.toml')(fname)
+      return util.root_pattern('lakefile.toml', 'lakefile.lean', 'lean-toolchain')(fname)
         or stdlib_dir
         or util.find_git_ancestor(fname)
     end,
-    options = {
-      -- Only Lake 3.0+ supports lake serve, so for old enough Lean 4,
-      -- or core Lean itself, this command (typically using the in-built
-      -- Lean 4 language server) will be used instead.
-      no_lake_lsp_cmd = { 'lean', '--server' },
-    },
     on_new_config = function(config, root_dir)
-      local use_lake_serve = false
-      if util.path.exists(util.path.join(root_dir, 'lakefile.lean')) then
-        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
-            use_lake_serve = true
-          end
-        end
-      end
-      if not use_lake_serve then
-        config.cmd = config.options.no_lake_lsp_cmd
-      end
       -- add root dir as command-line argument for `ps aux`
       table.insert(config.cmd, root_dir)
     end,
@@ -63,15 +38,15 @@ https://github.com/leanprover/lean4
 Lean installation instructions can be found
 [here](https://leanprover-community.github.io/get_started.html#regular-install).
 
-The Lean 4 language server is built-in with a Lean 4 install
-(and can be manually run with, e.g., `lean --server`).
+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.lean", "lean-toolchain", "leanpkg.toml", ".git")]],
+      root_dir = [[root_pattern("lakefile.toml", "lakefile.lean", "lean-toolchain", ".git")]],
     },
   },
 }