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

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

Equations

• Lake.relPathFrom root path = match path.toString.dropPrefix? root.toString with | some relPath => { toString := (relPath.drop 1).toString } | x => path

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.

Equations

• Lake.mkRelPathString path = if System.Platform.isWindows = true then String.map (fun (c : Char) => if c = '\\' then '/' else c) path.toString else path.toString

def Lake.instToJsonFilePath_lake : Lean.ToJson System.FilePath

Equations

• Lake.instToJsonFilePath_lake = { toJson := fun (path : System.FilePath) => Lean.toJson (Lake.mkRelPathString path) }

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

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

Equations

• Lake.joinRelative a b = if (b == { toString := "." }) = true then a else if (a == { toString := "." }) = true then b else inline System.FilePath.join a b

def Lake.instDivFilePath_lake : Div System.FilePath

Equations

• Lake.instDivFilePath_lake = { div := Lake.joinRelative }

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

Equations

• Lake.instHDivFilePathString_lake = { hDiv := fun (p : System.FilePath) (sub : String) => Lake.joinRelative p { toString := sub } }

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»

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def Lake.modOfFilePath.removeExts (s : String) (i e : String.Pos := s.endPos) : String

Equations

• One or more equations did not get rendered due to their size.