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.

@[reducible, inline]

abbrev Lake.RecBuildM (α : Type) : Type

A recursive build of a Lake build store that may encounter a cycle.

Equations

• Lake.RecBuildM = Lake.CallStackT Lake.BuildKey (Lake.BuildT (Lake.ELogT (StateT Lake.BuildStore BaseIO)))

instance Lake.instMonadLiftLogIORecBuildM : MonadLift Lake.LogIO Lake.RecBuildM

Equations

• Lake.instMonadLiftLogIORecBuildM = { monadLift := fun {α : Type} => Lake.ELogT.takeAndRun }

@[inline]

def Lake.RecBuildM.runJobM {α : Type} (x : Lake.JobM α) : Lake.RecBuildM α

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.

instance Lake.instMonadLiftJobMRecBuildM : MonadLift Lake.JobM Lake.RecBuildM

Equations

• Lake.instMonadLiftJobMRecBuildM = { monadLift := fun {α : Type} => Lake.RecBuildM.runJobM }

@[inline]

def Lake.RecBuildM.run {α : Type} (stack : Lake.CallStack Lake.BuildKey) (store : Lake.BuildStore) (build : Lake.RecBuildM α) : Lake.CoreBuildM (α × Lake.BuildStore)

Run a recursive build.

Equations

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

@[inline]

def Lake.RecBuildM.run' {α : Type} (build : Lake.RecBuildM α) : Lake.CoreBuildM α

Run a recursive build in a fresh build store.

Equations

• build.run' = (fun (x : α × Lake.BuildStore) => x.fst) <$> Lake.RecBuildM.run ∅ ∅ build

@[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.

instance Lake.instMonadCycleOfBuildKeyRecBuildM : Lake.MonadCycleOf Lake.BuildKey Lake.RecBuildM

Equations

• Lake.instMonadCycleOfBuildKeyRecBuildM = Lake.MonadCycleOf.mk fun {α : Type} => Lake.buildCycleError

@[reducible, inline]

abbrev Lake.IndexBuildFn (m : Type → Type v) : Type v

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

Equations

• Lake.IndexBuildFn m = ((info : Lake.BuildInfo) → m (Lake.BuildData info.key))

@[reducible, inline]

abbrev Lake.IndexT (m : Type → Type v) (α : Type) : Type v

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

Equations

• Lake.IndexT m = Lake.EquipT (Lake.IndexBuildFn m) m

@[reducible, inline]

abbrev Lake.FetchM (α : Type) : Type

The top-level monad for Lake build functions.

Equations

• Lake.FetchM = Lake.IndexT Lake.RecBuildM

@[reducible, inline, deprecated Lake.FetchM]

abbrev Lake.IndexBuildM (α : Type) : Type

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

Equations

• Lake.IndexBuildM = Lake.FetchM

@[reducible, inline, deprecated Lake.FetchM]

abbrev Lake.BuildM (α : Type) : Type

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

Equations

• Lake.BuildM = Lake.BuildT Lake.LogIO

@[inline]

def Lake.BuildInfo.fetch {α : Type} (self : Lake.BuildInfo) [Lake.FamilyOut Lake.BuildData self.key α] : Lake.FetchM α

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

Equations

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

def Lake.ensureJob {α : Type} (x : Lake.FetchM (Lake.Job α)) : Lake.FetchM (Lake.Job α)

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 : Bool := false) : Lake.FetchM (Lake.Job α)

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 : Bool := false) : Lake.FetchM (Lake.Job α)

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

• Lake.withRegisterJob caption x optional = do let job ← Lake.ensureJob x Lake.registerJob caption job optional

@[inline]

def Lake.maybeRegisterJob {α : Type} (caption : String) (job : Lake.Job α) : Lake.FetchM (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

• Lake.maybeRegisterJob caption job = if job.caption.isEmpty = true then Lake.registerJob caption job else pure job