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

Equations

• Lake.env cmd args = do let __do_lift ← Lake.getAugmentedEnv let x ← liftM (IO.Process.spawn { cmd := cmd, args := args, env := __do_lift }) liftM x.wait

def Lake.exe (name : Lean.Name) (args : Array String := #[]) (buildConfig : BuildConfig := { }) : LakeT IO UInt32

Equations

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

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

Equations

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

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

Equations

• pkg.unpack file = do Lake.logInfo (toString "unpacking " ++ toString file ++ toString "") Lake.untar file pkg.buildDir

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

Equations

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

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

Equations

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

def Lake.Package.test (pkg : Package) (args : List String := []) (buildConfig : BuildConfig := { }) : LakeT IO UInt32

Equations

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

def Lake.Package.lint (pkg : Package) (args : List String := []) (buildConfig : BuildConfig := { }) : LakeT IO UInt32

Equations

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