source
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

Instances For

source
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 (ex : IO.Error) => match ex with | IO.Error.noFileOrDirectory filename osCode details => pure () | e => throw e

Instances For

source
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

Instances For

source
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.

Instances For

source
@[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)

Instances For