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

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

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

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

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

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

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

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

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.