Go to definition not finding some definitions

Stream: lean4

[Andre Knispel]

In this example, I can go to the file containing Bool, but not to the file containing Scope, even though I can print its definition.

import Lean

#print Lean.Elab.Command.Scope
#print Bool

What are the conditions for the lookup to succeed? Looking at the definitions in the language server, it seems like the first thing is to check that the context of RequestM contains the appropriate search path. The logs of the server show a rootPath and a rootUri during init, but I don't know if that actually corresponds to the search path, and how to modify it.

[Sebastian Ullrich]

I can't reproduce this, though I haven't tried with a regular release from elan yet

[Andre Knispel]

This is with whatever version of lean the nix setup decided to give me (master probably?). Could it be that the nix build only provides c++ versions of the Lean library? I've been looking at the derivations in nix and I can find regular lean files for Init (in the dependencies of my package), but for Lean I only find c++ files (in the dependencies of lean itself).

[Sebastian Ullrich]

Oh I see, we're probably not setting up LEAN_SRC_PATH correctly for dependencies in the Nix setup yet

[Sebastian Ullrich]

While I want the Nix setup to be worth the hassle in the future, for now the "standard" setup is probably the safer choice. Especially if you want to use Lake-based packages.

[Andre Knispel]

I strongly prefer nix, and wouldn't mind contributing to ensure it works smoothly

[Sebastian Ullrich]

Cool! So when you nix develop into a flake created using the Lean 4 template, we already make sure that go-to-definition works inside that flake: https://github.com/leanprover/lean4/blob/fd1ae3118cd6b718cfff94164e28ac770be54646/nix/buildLeanPackage.nix#L288

[Sebastian Ullrich]

I think all that's missing is that we should add src for every entry in allExternalDeps to that env var. You would have to re-enter the dev shell whenever you add new dependencies in that case, but that should be a good start.

[Andre Knispel]

I'm a bit confused by this approach. Does the language server not have the same information that lean does to find source files? Having a separate source of truth for this information seems like it'll always be prone to breakage.

[Sebastian Ullrich]

Lean itself never has to find .lean files, only compiled .olean files. Thus there are separate LEAN_PATH and LEAN_SRC_PATH (used by the language server only) variables.

[Andre Knispel]

Ah, I see

[Sebastian Ullrich]

But you're completely right that this feels like the wrong location - in fact, the language server calls a command lake print-paths to find both the binary and source locations of a given set of imports, and we already override that in Nix to point at what roughly looks like the right value: https://github.com/leanprover/lean4/blob/fd1ae3118cd6b718cfff94164e28ac770be54646/nix/buildLeanPackage.nix#L202. So we'd have to investigate why that isn't working.

[Sebastian Ullrich]

So inside your editor you should be able to run lake print-paths Lean and check if the output makes sense

[Andre Knispel]

Hmm, so lake print-paths Lean did build some things and printed a path in the nix store that contains the correct things. What I find curious is that srcPath in the outputs contains the path to the sources twice, not sure if that affects anything.

[Sebastian Ullrich]

I don't think it should

[Andre Knispel]

I also realised something else that might be related, which is that in the lsp debug buffer the rootPath and rootUri don't actually point to the package root, but to a folder containing it, which means I get a prompt whether I want to watch hundreds of files that aren't related.

[Sebastian Ullrich]

The root should be the workspace folder you selected in lsp-mode, e.g. using lsp-workspace-folders-open

[Andre Knispel]

Interesting, that doesn't even let me select anything below the folder it already has selected

[Sebastian Ullrich]

Then you probably need lsp-workspace-folders-add. I don't know why it's that complicated :shrug: .

[Andre Knispel]

Ah, that did actually fix my problem!

[Sebastian Ullrich]

Nice, even though I'm unsure why :big_smile:

[Andre Knispel]

So I assume the whole workspace thing was caused by some unrelated things going on with my machine or emacs setup. Maybe there's at least something to learn or fix so that people won't have this issue in the future?