Goto definition failing with multiple libraries

Description

In a configuration with multiple libraries, "go to definition" fails in some circumstances.

Context

I had noticed intermittent failures of "go to definition" while working on Verso. Another user experienced them, so I took the time to minimize it and produce a bug report.

Steps to Reproduce

1. Check out the branch goto-def-minimized of Verso
2. Open the file verso-blog/Verso/Genre/Blog/Template.lean
3. Try to use "go to definition" on the occurrence of MonadPath on line 13

Expected behavior:

A jump to the definition of MonadPath

(or, alternatively, I would expect a "variable out of scope" error message, but the file elaborates without errors)

Actual behavior:

It fails to do so in Codium:

and also Emacs:

so I suspect the language server is at fault, rather than the editor plugin.

Versions

I can reproduce this in the following Lean versions:

• leanprover/lean4:nightly-2024-08-08
• leanprover/lean4:v4.11.0-rc1
• leanprover/lean4:v4.10.0
• leanprover/lean4:v4.9.0
• leanprover/lean4:v4.8.0
• leanprover/lean4:v4.1.0

I didn't try the intervening versions.

Additional Information

Editing the Lakefile to remove the first library and restarting the language server:

import Lake
open Lake DSL

package verso where


@[default_target]
lean_lib VersoBlog where
  srcDir := "src/verso-blog"
  roots := #[`Verso.Genre.Blog]

makes it so that the feature works correctly.

I suspected that the problem might be from one library's roots containing another, but the following Lakefile still exhibits the bug:

import Lake
open Lake DSL

package verso where

@[default_target]
lean_lib Verso where
  srcDir := "src/verso"
  roots := #[`Verso.A]

@[default_target]
lean_lib VersoBlog where
  srcDir := "src/verso-blog"
  roots := #[`Verso.Genre.Blog]

as does one in which the library is renamed to VersoA.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Reproduce the failure using the goto-def-minimized Verso branch, opening verso-blog/Verso/Genre/Blog/Template.lean and targeting MonadPath on line 13. Compare behavior with the reduced Lakefiles in the report and inspect the language-server handling of multiple libraries. Done means go-to-definition reaches Verso/Genre/Blog/Site.lean, or reports a clear out-of-scope error.