Find a Lean file on the Lean Path

Stream: lean4

[Julian Berman]

I want to open the file which corresponds to the Lean module Foo.Bar which is somewhere on the Lean path. Is there some Lake CLI API for telling me where that file lives so I can directly open whatever path it ends up being without needing to go via the language server?

[Julian Berman]

I guess lake lean will do this for me if I know the answer for Lean itself. So maybe this reduces to a question about the lean CLI.

[Julian Berman]

(Now that the reference is back up, hooray) I guess concretely I want Lake.findModule? but where the return value is a SystemPath not the module? And scanning the rest of what's there I don't see that, so unless I've missed it I'll pick between my 3 options (1: stop wanting this entirely, 2: use a temporary file with import Foo.Bar + gotodefinition to get there in 2 steps since anyways that's what I'm going to do with the path, 3: manually search the search path given Foo.Bar is a fixed module in my case.)

[Jannis Limperg]

findLean should be the function you're looking for. lake env should set the right LEAN_SRC_PATH for you, which you can get via getSrcSearchPath.

[Julian Berman]

Ah that's perfect! Looks like it doesn't show up in the reference yet. Thanks @Jannis Limperg .