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.

def Lake.Workspace.evalLeanFile (ws : Workspace) (leanFile : System.FilePath) (moreArgs : Array String := #[]) (buildConfig : BuildConfig := { }) : IO UInt32

Run lean on file using configuration from the workspace.

Additional arguments can be passed to lean via moreArgs and the building of dependencies can be further configured via buildConfig.

Equations

• ws.evalLeanFile leanFile moreArgs buildConfig = do let spawnArgs ← ws.runBuild (Lake.prepareLeanCommand leanFile moreArgs) buildConfig let child ← IO.Process.spawn spawnArgs child.wait