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.

def Lake.Monitor.spinnerFrames : Array Char

Unicode icons that make up the spinner in animation order.

Equations

• Lake.Monitor.spinnerFrames = #['⣾', '⣷', '⣯', '⣟', '⡿', '⢿', '⣻', '⣽']

structure Lake.MonitorContext : Type

Context of the Lake build monitor.

• jobs : IO.Ref (Array OpaqueJob)
• out : IO.FS.Stream
• outLv : LogLevel
• failLv : LogLevel
• minAction : JobAction
• showOptional : Bool
• useAnsi : Bool
• showProgress : Bool
• showTime : Bool
• updateFrequency : Nat

  How often to poll jobs (in milliseconds).

structure Lake.MonitorState : Type

State of the Lake build monitor.

• jobNo : Nat
• totalJobs : Nat
• didBuild : Bool
• failures : Array String
• resetCtrl : String
• lastUpdate : Nat
• spinnerIdx : Fin Monitor.spinnerFrames.size

@[reducible, inline]

abbrev Lake.MonitorM (α : Type) : Type

Monad of the Lake build monitor.

Equations

• Lake.MonitorM = ReaderT Lake.MonitorContext (StateT Lake.MonitorState BaseIO)

@[inline]

def Lake.MonitorM.run {α : Type} (ctx : MonitorContext) (s : MonitorState) (self : MonitorM α) : BaseIO (α × MonitorState)

Equations

• Lake.MonitorM.run ctx s self = self ctx s

def Lake.Ansi.resetLine : String

The ANSI escape sequence for clearing the current line and resetting the cursor back to the start.

Equations

• Lake.Ansi.resetLine = "\x1b[2K\x0d"

@[inline]

def Lake.flush (out : IO.FS.Stream) : BaseIO PUnit

Like IO.FS.Stream.flush, but ignores errors.

Equations

• Lake.flush out = EIO.catchExceptions out.flush fun (x : IO.Error) => pure ()

@[inline]

def Lake.print! (out : IO.FS.Stream) (s : String) : BaseIO PUnit

Like IO.FS.Stream.putStr, but panics on errors.

Equations

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

@[inline]

def Lake.Monitor.print (s : String) : MonitorM PUnit

Equations

• Lake.Monitor.print s = do let __do_lift ← read liftM (Lake.print! __do_lift.out s)

@[inline]

def Lake.Monitor.flush : MonitorM PUnit

Equations

• Lake.Monitor.flush = do let __do_lift ← read liftM (Lake.flush __do_lift.out)

def Lake.Monitor.renderProgress (running unfinished : Array OpaqueJob) (h : 0 < unfinished.size) : MonitorM PUnit

Equations

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

def Lake.Monitor.reportJob (job : OpaqueJob) : MonitorM PUnit

Equations

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

def Lake.Monitor.reportJob.formatTime (ms : Nat) : String

Equations

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

def Lake.Monitor.poll (unfinished : Array OpaqueJob) : MonitorM (Array OpaqueJob × Array OpaqueJob)

Equations

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

def Lake.Monitor.sleep : MonitorM PUnit

Equations

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

partial def Lake.Monitor.loop (unfinished : Array OpaqueJob) : MonitorM PUnit

def Lake.Monitor.main (init : Array OpaqueJob) : MonitorM PUnit

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)