Documentation

Lake.Build.Run

Build Runner #

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

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.

Unicode icons that make up the spinner in animation order.

Equations

Context of the Lake build monitor.

State of the Lake build monitor.

@[reducible, inline]
abbrev Lake.MonitorM (α : Type) :

Monad of the Lake build monitor.

Equations
@[inline]
def Lake.MonitorM.run {α : Type} (ctx : MonitorContext) (s : MonitorState) (self : MonitorM α) :
Equations

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

Equations
@[inline]

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

Equations
@[inline]

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

Equations
  • One or more equations did not get rendered due to their size.
@[inline]
Equations
@[inline]
Equations
def Lake.Monitor.renderProgress (running unfinished : Array OpaqueJob) (h : 0 < unfinished.size) :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
def Lake.monitorJobs (jobs : Array OpaqueJob) (out : IO.FS.Stream) (failLv outLv : LogLevel) (minAction : JobAction) (showOptional useAnsi showProgress : Bool) (resetCtrl : String := "") (initFailures : Array String := #[]) (totalJobs : Nat := jobs.size) (updateFrequency : Nat := 100) :

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.runFetchM {α : Type} (ws : Workspace) (build : FetchM α) (cfg : BuildConfig := { oldMode := false, trustHash := true, noBuild := false, verbosity := Verbosity.normal, failLv := LogLevel.error, outLv := Verbosity.normal.minLogLv, out := OutStream.stderr, ansiMode := AnsiMode.auto }) :
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 := { oldMode := false, trustHash := true, noBuild := false, verbosity := Verbosity.normal, failLv := LogLevel.error, outLv := Verbosity.normal.minLogLv, out := OutStream.stderr, ansiMode := AnsiMode.auto }) :
IO α

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

Equations
  • ws.runBuild build cfg = do let jobws.runFetchM build cfg let __discrliftM job.wait? match __discr with | some a => pure a | x => Lake.error "build failed"
@[inline]
def Lake.runBuild {α : Type} (build : FetchM (Job α)) (cfg : BuildConfig := { oldMode := false, trustHash := true, noBuild := false, verbosity := Verbosity.normal, failLv := LogLevel.error, outLv := Verbosity.normal.minLogLv, out := OutStream.stderr, ansiMode := AnsiMode.auto }) :

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

Equations