Goto definition failing with multiple libraries

david-christiansen commented 2 months ago

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

Check out the branch goto-def-minimized of Verso
Open the file verso-blog/Verso/Genre/Blog/Template.lean
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 :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

Kha commented 2 months ago

Note that in general, Lean assumes different libraries have different module name roots (Verso) (edit: that part is fine, I just didn't expect them to also have different source roots). That doesn't mean the server should also (silently) fail but likely makes this lower prio.

david-christiansen commented 2 months ago

Ah, after all this time I wasn't aware of this assumption! Thanks for the clarification, and I'll reorganize things.

leanprover / lean4