Get source of file containing name

Stream: lean4

[Adam Topaz]

It's quite easy to obtain the source of the current file within CommandElabM as follows:

import Lean

open Lean Elab Command

def foo : CommandElabM String := return (← readThe Context).fileMap.source

#eval foo

I'm trying to figure out how to do something similar, except that I want the source of a file which contains a declaration with name e : Name. Can someone point me in the right direction?

[Max Nowak 🐉]

You can probably find the module containing the constant by looking at (<- getEnv).allImportedModuleNames, and the declsInModuleIdx and getModuleIdx? functions. Maybe there's some functions which do it more efficiently than just scanning through all modules, but I hope this helps a little bit at least.

[Scott Morrison]

This function is in https://github.com/leanprover-community/mathlib4/pull/3122 (shortly to hit master), as Lean.Name.getModule.

[Scott Morrison]

I suspect after that you'll have to actually read the file from the file system: Lean is not going to have it available like for the current file in fileMap. (And even that is a bit hacky, although sagredo uses the same trick.)

[Sebastian Ullrich]

This is docs4#Lean.findModuleOf?, see also docs4#Lean.Server.locationLinksFromDecl

[Scott Morrison]

Both of those links go to blank pages in my browser?

[Sebastian Ullrich]

Mhh, works on my machine

[Scott Morrison]

Oh, sometime later I went back to those tabs and they had loaded!

[Adam Topaz]

Thanks all! Yes, I figured out how to get a ModuleIdx for the given name, but couldn’t figure out what to actually do with it! Is there some function that gives the module name from the module index? (Edit: answered by looking at the source for the function that Sebastian mentioned)

is there no way to get a term of type docs4#Lean.Module from a module’s name?

[Adam Topaz]

Of course, I could go through the file system to get the source as Scott suggests. Is there some function that gives the path of the root of the current project? That would help with such an approach

[Sebastian Ullrich]

What's wrong with the code in documentUriFromModule?

[Sebastian Ullrich]

Adam Topaz said:

is there no way to get a term of type docs4#Lean.Module from a module’s name?

No, the syntax tree is not persisted

[Adam Topaz]

Sebastian Ullrich said:

What's wrong with the code in documentUriFromModule?

What was wrong is that I didn't know this existed :)

[Adam Topaz]

Thanks!

[Adam Topaz]

hmmm... now I can't seem to find how to get the correct SearchPath. Is there a quick way to get the search path that includes both the the lean system and the current project?