def Lake.createParentDirs (path : System.FilePath) : IO Unit

Creates any missing parent directories of path.

Equations

• Lake.createParentDirs path = match path.parent with | some dir => IO.FS.createDirAll dir | x => pure PUnit.unit

def Lake.removeFileIfExists (path : System.FilePath) : IO Unit

Remove the file at path if it exists.

Equations

• Lake.removeFileIfExists path = tryCatch (IO.FS.removeFile path) fun (x : IO.Error) => match x with | IO.Error.noFileOrDirectory filename osCode details => pure () | e => throw e

def Lake.writeFileIfNew (path : System.FilePath) (content : String) : IO Unit

Write the UTF-8 encoded string content to path. If the file already exists, does nothing.

Equations

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

def Lake.writeBinFileIfNew (path : System.FilePath) (content : ByteArray) : IO Unit

Write the bytes of content to path. If the file already exists, does nothing.

Equations

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

partial def Lake.removeDirAllIfExists (path : System.FilePath) : IO Unit

Remove a directory and all its contents. Like IO.FS.removeDirAll, but does not fail if path does not exist or if a file is first deleted by a racing process.

def Lake.copyFile (src dst : System.FilePath) : IO Unit

Copy a file from src to dst.

Equations

• Lake.copyFile src dst = do let contents ← IO.FS.readBinFile src IO.FS.writeBinFile dst contents

def Lake.resolvePath (path : System.FilePath) : BaseIO System.FilePath

Returns the normalized real path of a file if it exists. Otherwise, returns "".

Equations

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

@[inline]

def Lake.resolvePath? (path : System.FilePath) : BaseIO (Option System.FilePath)

Returns the normalized real path of a file if and only if it exists.

Equations

• Lake.resolvePath? path = do let path ← Lake.resolvePath path pure (if path.toString.isEmpty = true then none else some path)