Zulip Chat Archive

Stream: lean4

Topic: get filename + pos


Johan Commelin (Jan 28 2023 at 09:43):

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 (Jan 28 2023 at 09:57):

Found it:

let r  declRangeExt.find? env n

Johan Commelin (Jan 28 2023 at 09:58):

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

Johan Commelin (Jan 28 2023 at 10:15):

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 (Jan 28 2023 at 11:32):

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

Eric Wieser (Oct 11 2023 at 21:42):

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

Eric Wieser (Oct 11 2023 at 21:44):

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

Eric Wieser (Oct 11 2023 at 21:50):

Ah, docs#Lean.findOLean

Utensil Song (Oct 12 2023 at 07:00):

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 (Oct 12 2023 at 07:01):

to pass base to docs#Lean.findOLean needs this

Utensil Song (Oct 12 2023 at 07:02):

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

Scott Morrison (Oct 12 2023 at 07:36):

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 (Oct 12 2023 at 08:08):

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 (Oct 12 2023 at 08:15):

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

Utensil Song (Oct 12 2023 at 08:15):

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 (Oct 12 2023 at 08:16):

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

Utensil Song (Oct 12 2023 at 08:18):

Ah I see, Lean only has olean :man_facepalming:

Utensil Song (Oct 12 2023 at 08:21):

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

Sebastian Ullrich (Oct 12 2023 at 09:19):

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

Utensil Song (Oct 12 2023 at 09:33):

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 (Oct 12 2023 at 09:51):

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 (Oct 12 2023 at 10:03):

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 (Oct 12 2023 at 10:04):

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


Last updated: Dec 20 2023 at 11:08 UTC