Zulip Chat Archive

Stream: lean4

Topic: Go to definition not finding some definitions


Andre Knispel (Sep 25 2022 at 22:00):

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 (Sep 26 2022 at 07:52):

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

Andre Knispel (Sep 26 2022 at 11:25):

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 (Sep 26 2022 at 11:59):

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

Sebastian Ullrich (Sep 26 2022 at 12:03):

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 (Sep 26 2022 at 12:05):

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

Sebastian Ullrich (Sep 26 2022 at 12:09):

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 (Sep 26 2022 at 12:11):

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 (Sep 26 2022 at 12:18):

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 (Sep 26 2022 at 12:20):

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 (Sep 26 2022 at 12:21):

Ah, I see

Sebastian Ullrich (Sep 26 2022 at 12:22):

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 (Sep 26 2022 at 12:24):

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

Andre Knispel (Sep 26 2022 at 12:54):

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 (Sep 26 2022 at 12:54):

I don't think it should

Andre Knispel (Sep 26 2022 at 12:57):

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 (Sep 26 2022 at 13:00):

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

Andre Knispel (Sep 26 2022 at 13:05):

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

Sebastian Ullrich (Sep 26 2022 at 13:06):

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

Andre Knispel (Sep 26 2022 at 13:08):

Ah, that did actually fix my problem!

Sebastian Ullrich (Sep 26 2022 at 13:10):

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

Andre Knispel (Sep 26 2022 at 13:11):

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?


Last updated: Dec 20 2023 at 11:08 UTC