Filenames to `Lean.Name`

Stream: Is there code for X?

[Jireh Loreaux]

Do we have anything to take the filename Mathlib/Algebra/Group/Defs.lean to the docs#Lean.Name Mathlib.Algebra.Group.Defs?

[Jireh Loreaux]

I know it shouldn't be hard to write, but I figure it must already exist.

[Alex J. Best]

docs#moduleNameOfFileName perhaps?

[Jireh Loreaux]

Thanks!

[Anne Baanen]

Is there also a way to go the other way, from Mathlib.Algebra.Group.Defs to Mathlib/Algebra/Group/Defs.lean?

[Scott Morrison]

Lean.findOLean is almost what you want.

[Scott Morrison]

I have a

-- TODO allow finding Lean 4 sources from the toolchain.
def findLean (mod : Name) : IO FilePath := do
  return FilePath.mk ((← findOLean mod).toString.replace "build/lib/" "") |>.withExtension "lean"

in a project.