def Lake.env (cmd : String) (args : Array String := #[]) : Lake.LakeT IO UInt32

Equations

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

def Lake.exe (name : Lean.Name) (args : Array String := #[]) (buildConfig : Lake.BuildConfig := { oldMode := false, trustHash := true, noBuild := false, verbosity := Lake.Verbosity.normal, failLv := Lake.LogLevel.error, outLv := Lake.Verbosity.normal.minLogLv, out := Lake.OutStream.stderr, ansiMode := Lake.AnsiMode.auto }) : Lake.LakeT IO UInt32

Equations

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

def Lake.Package.pack (pkg : Lake.Package) (file : System.FilePath := pkg.buildArchiveFile) : Lake.LogIO Unit

Equations

• pkg.pack file = do Lake.logInfo (toString "packing " ++ toString file ++ toString "") Lake.tar pkg.buildDir file

def Lake.Package.unpack (pkg : Lake.Package) (file : System.FilePath := pkg.buildArchiveFile) : Lake.LogIO Unit

def Lake.Package.uploadRelease (pkg : Lake.Package) (tag : String) : Lake.LogIO Unit

def Lake.Package.resolveDriver (pkg : Lake.Package) (kind driver : String) : Lake.LakeT IO (Lake.Package × String)

Equations

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

def Lake.Package.test (pkg : Lake.Package) (args : List String := []) (buildConfig : Lake.BuildConfig := { oldMode := false, trustHash := true, noBuild := false, verbosity := Lake.Verbosity.normal, failLv := Lake.LogLevel.error, outLv := Lake.Verbosity.normal.minLogLv, out := Lake.OutStream.stderr, ansiMode := Lake.AnsiMode.auto }) : Lake.LakeT IO UInt32

def Lake.Package.lint (pkg : Lake.Package) (args : List String := []) (buildConfig : Lake.BuildConfig := { oldMode := false, trustHash := true, noBuild := false, verbosity := Lake.Verbosity.normal, failLv := Lake.LogLevel.error, outLv := Lake.Verbosity.normal.minLogLv, out := Lake.OutStream.stderr, ansiMode := Lake.AnsiMode.auto }) : Lake.LakeT IO UInt32