leanprover
Definition jumping to a local dependency seems to jump to the wrong path
Prerequisites
- [x] Put an X between the brackets on this line if you have done all of the following:
- Checked that your issue isn't already filed.
- Reduced the issue to a self-contained, reproducible test case.
Description
Given a simple package like the below (also uploaded as a zip, test.zip):
⊙ cat Test.lean julian@Airm ●
import Foo
#check best
~/Desktop/test
⊙ cat foo/Foo.lean julian@Airm ●
def best := 37
~/Desktop/test
⊙ cat lakefile.lean julian@Airm ●
import Lake
open Lake DSL
package Test {
defaultFacet := PackageFacet.oleans,
dependencies := #[{
name := `foo
src := Source.path ("foo")
}]
}
Opening Test.lean in an editor and attempting to jump to the definition of best produces an error like:
[Error - 12:32:25 PM] Request textDocument/definition failed.
Message: no such file or directory (error code: 2)
file: /users/julian/desktop/test/Foo.lean
Code: -32603
where the correct path is /Users/julian/Desktop/test/foo/Foo.lean (in my case this is macOS, so the filesystem is case insensitive, ~~but that doesn't seem directly relevant~~).
Steps to Reproduce
- Open test/Test.lean in an editor
- Jump to the definition of
best
Expected behavior:
We jump to test/foo/Foo.lean.
Actual behavior:
[Error - 12:32:25 PM] Request textDocument/definition failed.
Message: no such file or directory (error code: 2)
file: /users/julian/desktop/test/Foo.lean
Code: -32603
Reproduces how often: Always.
Versions
macOS 12.0.1 (21A559)
⊙ lean --version julian@Airm ●
Lean (version 4.0.0, commit 60934bf1d524, Release)
~/Desktop/test
⊙ lake --version julian@Airm ●
Lake version 3.0.0-pre (Lean version master (4.0.0))
in my case this is macOS, so the filesystem is case insensitive, but that doesn't seem directly relevant
No, that likely is exactly the problem. We had the same issue with the path lake/Lake in this repo. I certainly didn't think of such file systems when implementing the lookup.
We could of course implement our own, case-sensitive check regardless of the actual file system...
Just to be sure to point it out, there's a path component missing, it's not just the case, which is what made me think it was irrelevant -- in the example, the correct path is /Users/julian/Desktop/test/foo/Foo.lean, but the jumped-to path is missing /foo
(If not, sorry for the misdiagnosis)
Yes, Lean thinks test/ is the root of the Foo package because it seems to contains a Foo/ folder.
I just did the following: downloaded the zip file, replaced the two lakefiles with:
import Lake
open Lake DSL
package Test where
require foo from "foo"
lean_lib Test
and:
import Lake
open Lake DSL
package foo where
lean_lib Foo
and set the outer toolchain file to leanprover/lean4:nightly-2024-03-11.
After doing that, and restarting everything as needed, "go to definition" works just fine on best. This is Mac OS.
I am closing this issue for now. Please let me know if it comes up again, and I will re-open it.
