get filename + pos

Stream: lean4

[Johan Commelin]

I'm looping over the environment, and have a Lean.Name. How can I get access to the file + position where it is declared?

[Johan Commelin]

Found it:

let r ← declRangeExt.find? env n

[Johan Commelin]

At least, that gives the position. Now I still need the filename

[Johan Commelin]

Is this the idiomatic way to get the module name?

let i ← env.getModuleIdxFor? n
let m := env.header.moduleNames.get! i

[Henrik Böving]

I do it like this in doc-gen but idk if it is considered idiomatic

[Eric Wieser]

How do I go from the module name to a file name?

[Eric Wieser]

that is; what's the analog to docs3#environment.decl_olean?

[Eric Wieser]

Ah, docs#Lean.findOLean

[Utensil Song]

You'll need lake related stuff to get the filename from a module Name because of how lake places them in lake-packages

[Utensil Song]

to pass base to docs#Lean.findOLean needs this

[Utensil Song]

The major issue is to locate the package directory when you only have Package root

[Scott Morrison]

I have used

def findLean (mod : Name) : IO FilePath := do
  return FilePath.mk ((← findOLean mod).toString.replace "build/lib/" "") |>.withExtension "lean"

in the past, but I know this does not work for source files from the Lean toolchain.

[Utensil Song]

This my current attempt (~ 250 loc) to minimize deps to revive the Lean 3 declsin blueprint: https://github.com/utensil/LeanBlueprintExample/blob/main/Exe/Decls.lean (as a demonstration of how complicated it is)

I've combined how things are done in doc-gen4 (now it moves to use lake module:facet which is difficult to strip off) and mathlib4 cache (which manually maps package names to package dirs with some assumptions that's why it can be free of lake deps).

By lake deps I mean work in a standalone program using lake as a library dependency, it's way harder than writing things in a lakefile . I'm still fighting lake to get it working, to be free of manual mapping package names to package dirs.

I wonder why the file name information is not available directly as Lean is already compiling the file, why it gives a DeclarationRange but not a file name, and one has to work it out from module name+lake setup, or work out the source location based on where olean is compiled to by Lake (following a relative path mapping) like @Scott Morrison did.

[Sebastian Ullrich]

The correct way is to use docs4#Lean.initSrcSearchPath + docs4#Lean.SearchPath.findModuleWithExt

[Utensil Song]

Maybe docs#Lean.SearchPath.findWithExt do the trick, but it should not be searching the file again as the file is already in the hand of Lean

[Sebastian Ullrich]

For a loaded import the corresponding .lean file is not in the hands of Lean yet

[Utensil Song]

Ah I see, Lean only has olean :man_facepalming:

[Utensil Song]

But how does Lean know DeclarationRange, doesn't it know the file if it knows DeclarationRange?

[Sebastian Ullrich]

The file path is machine-specific, the location isn't. So we only persist the latter in the .olean.

[Utensil Song]

Sebastian Ullrich said:

The correct way is to use docs4#Lean.initSrcSearchPath + docs4#Lean.SearchPath.findModuleWithExt

Performance-wise, this seems to be good enough as I only need to search once for each package, then cache the mapping. The relative part can be inferred.

[Eric Wieser]

Sebastian Ullrich said:

The correct way is to use docs4#Lean.initSrcSearchPath + docs4#Lean.SearchPath.findModuleWithExt

The key thing here is that this finds the source file rather than the olean, I assume?

[Utensil Song]

The key thing is docs#Lean.findOLean (for .olean) and docs4#Lean.SearchPath.findModuleWithExt (for .olean and .lean) both indeed are search which is IO heavy, should not be put into inner loop during processing many files/declarations.

[Utensil Song]

The former calls (the variant of ) the latter internally.