Documentation

Lake.Build.Fetch

Recursive Building #

This module defines Lake's top-level build monad, FetchM, used for performing recursive builds. A recursive build is a build function which can fetch the results of other (recursive) builds. This is done using the fetch function defined in this module.

Equations
@[inline]

Run a JobM action in RecBuildM (and thus FetchM).

Generally, this should not be done, and instead a job action should be run asynchronously in a Job (e.g., via Job.async).

Equations
  • One or more equations did not get rendered due to their size.
Equations
@[inline]

Run a recursive build.

Equations
  • One or more equations did not get rendered due to their size.
@[inline]

Run a recursive build in a fresh build store.

Equations
@[specialize #[]]
def Lake.buildCycleError {m : Type u_1 → Type u_2} {α : Type u_1} [Lake.MonadError m] (cycle : Lake.Cycle Lake.BuildKey) :
m α

Log build cycle and error.

Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]
abbrev Lake.IndexBuildFn (m : TypeType v) :

A build function for any element of the Lake build index.

Equations
@[reducible, inline]
abbrev Lake.IndexT (m : TypeType v) (α : Type) :

A transformer to equip a monad with a build function for the Lake index.

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

The top-level monad for Lake build functions.

Equations
@[reducible, inline, deprecated Lake.FetchM]
abbrev Lake.IndexBuildM (α : Type) :

The top-level monad for Lake build functions. Renamed FetchM.

Equations
@[reducible, inline, deprecated Lake.FetchM]
abbrev Lake.BuildM (α : Type) :

The old build monad. Uses should generally be replaced by FetchM.

Equations
@[inline]

Fetch the result associated with the info using the Lake build index.

Equations
  • self.fetch build = cast (build self)

Wraps stray I/O, logs, and errors in x into the produced job.

Equations
  • One or more equations did not get rendered due to their size.
def Lake.registerJob {α : Type} (caption : String) (job : Lake.Job α) (optional : optParam Bool false) :

Registers the job for the top-level build monitor, (e.g., the Lake CLI progress UI), assigning it caption.

Equations
  • One or more equations did not get rendered due to their size.
def Lake.withRegisterJob {α : Type} (caption : String) (x : Lake.FetchM (Lake.Job α)) (optional : optParam Bool false) :

Registers the produced job for the top-level build monitor (e.g., the Lake CLI progress UI), assigning it caption.

Stray I/O, logs, and errors produced by x will be wrapped into the job.

Equations
@[inline]
def Lake.maybeRegisterJob {α : Type} (caption : String) (job : Lake.Job α) :

Registers the produced job for the top-level build monitor if it is not already (i.e., it has an empty caption).

Equations