Build Runner

This module defines the top-level functions used to execute a Lake build, monitor its progress, and await the result.

def Lake.mkBuildContext (ws : Workspace) (config : BuildConfig) : BaseIO BuildContext

Create a fresh build context from a workspace and a build configuration.

Equations

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

structure Lake.MonitorResult : Type

• didBuild : Bool
• failures : Array String
• numJobs : Nat

def Lake.monitorJobs (initJobs : Array OpaqueJob) (jobs : IO.Ref (Array OpaqueJob)) (out : IO.FS.Stream) (failLv outLv : LogLevel) (minAction : JobAction) (showOptional useAnsi showProgress showTime : Bool) (resetCtrl : String := "") (initFailures : Array String := #[]) (updateFrequency : Nat := 100) : BaseIO MonitorResult

The job monitor function. An auxiliary definition for runFetchM.

Equations

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

def Lake.Workspace.saveInputs (ws : Workspace) : LogIO Unit

Save input mappings to the local Lake artifact cache (if enabled).

Equations

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

def Lake.noBuildCode : ExitCode

Exit code to return if --no-build is set and a build is required.

Equations

• Lake.noBuildCode = 3

def Lake.Workspace.runFetchM {α : Type} (ws : Workspace) (build : FetchM α) (cfg : BuildConfig := { }) : IO α

Run a build function in the Workspace's context using the provided configuration. Reports incremental build progress and build logs. In quiet mode, only reports failing build jobs (e.g., when using -q or non-verbose --no-build).

Equations

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

@[inline]

def Lake.Workspace.runBuild {α : Type} (ws : Workspace) (build : FetchM (Job α)) (cfg : BuildConfig := { }) : IO α

Run a build function in the Workspace's context and await the result.

Equations

• ws.runBuild build cfg = do let job ← ws.runFetchM build cfg let __discr ← liftM job.wait? match __discr with | some a => pure a | x => Lake.error "build failed"

@[inline]

def Lake.runBuild {α : Type} (build : FetchM (Job α)) (cfg : BuildConfig := { }) : LakeT IO α

Produce a build job in the Lake monad's workspace and await the result.

Equations

• Lake.runBuild build cfg = do let __do_lift ← Lake.getWorkspace liftM (__do_lift.runBuild build cfg)