def Lake.relPathFrom (root path : System.FilePath) : System.FilePath

Returns the portion of path relative to root. If none, returns path verbatim.

def Lake.mkRelPathString (path : System.FilePath) : String

Convert a relative file path to a platform-independent string. Uses / as the path separator, even on Windows.

@[implicit_reducible]

def Lake.instToJsonFilePath_lake : Lean.ToJson System.FilePath

def Lake.joinRelative (a b : System.FilePath) : System.FilePath

Joins a two (potentially) relative paths. If either path is ., this returns the other.

@[implicit_reducible]

def Lake.instDivFilePath_lake : Div System.FilePath

@[implicit_reducible]

def Lake.instHDivFilePathString_lake : HDiv System.FilePath String System.FilePath

@[deprecated "Deprecated without replacement." (since := "2025-08-01")]

def Lake.modOfFilePath (path : System.FilePath) : Lean.Name

Creates a module Name from a file path. The components of the path become string components of the Name. Before conversion, normalizes the path, removes any extensions, and strips a trailing path separator.

Examples:

• modOfFilePath "Foo/Bar" = `Foo.Bar
• modOfFilePath "Foo/Bar/" = `Foo.Bar
• modOfFilePath "Foo/Bar.lean" = `Foo.Bar
• modOfFilePath "Foo/Bar.tar.gz" = `Foo.Bar
• modOfFilePath "Foo/Bar.lean/" = `Foo.«Bar.lean»