Correct the root directory when editing files in .lake/packages

The correct scope is the entire project it sits inside of.

Author: Julian

lsp/leanls.lua

@@ -169,6 +169,16 @@ return {
   root_dir = function(bufnr, on_dir)
     local fname = vim.api.nvim_buf_get_name(bufnr)
     fname = vim.fs.normalize(fname)
+
+    local packages_dir
+    local packages_suffix = '/.lake/packages/'
+    do
+      local _, endpos = fname:find(packages_suffix)
+      if endpos then
+        packages_dir = fname:sub(1, endpos - packages_suffix:len())
+      end
+    end
+
     -- check if inside lean stdlib
     local stdlib_dir
     do
@@ -185,7 +195,8 @@ return {
     end
 
     on_dir(
-      vim.fs.root(fname, { 'lakefile.toml', 'lakefile.lean', 'lean-toolchain' })
+      packages_dir
+        or vim.fs.root(fname, { 'lakefile.toml', 'lakefile.lean', 'lean-toolchain' })
         or stdlib_dir
         or vim.fs.dirname(vim.fs.find('.git', { path = fname, upward = true })[1])
     )

spec/helpers.lua

@@ -93,11 +93,13 @@ function helpers.wait_for_async_elements(iv)
 end
 
 function helpers.wait_for_ready_lsp()
+  local client
   local succeeded, _ = vim.wait(15000, function()
-    local client = lsp.client_for(0)
+    client = lsp.client_for(0)
     return client and client.initialized or false
   end)
   assert.message('LSP server was never ready.').True(succeeded)
+  return client
 end
 
 ---Wait until a window that isn't one of the known ones shows up.

spec/lsp_spec.lua

@@ -29,4 +29,11 @@ describe('LSP', function()
     assert.is.empty(vim.lsp.get_clients { bufnr = 0, name = 'leanls', _uninitialized = true })
     vim.cmd.close { bang = true }
   end)
+
+  it('uses project root dir for files in .lake/packages', function()
+    vim.cmd.edit(fixtures.with_widgets:child '.lake/packages/Qq/Qq.lean')
+    local client = helpers.wait_for_ready_lsp()
+    local project_root = vim.uv.fs_realpath(fixtures.with_widgets._root)
+    assert.is.same(project_root, vim.uv.fs_realpath(client.config.root_dir))
+  end)
 end)