# 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.

source
def Lake.CurrPackage :
Type

A type alias for `Option Package` that assists monad type class synthesis.

Equations

- Lake.CurrPackage = Option Lake.Package

Instances For

source
@[inline]
def Lake.withCurrPackage? {m : Type → Type u_1} {α : Type} [MonadWithReader CurrPackage m] (pkg? : Option Package) (x : m α) :
m α

Run the action `x` with `pkg?` as the current package or no package if `none`.

Equations

- Lake.withCurrPackage? pkg? x = withReader (fun (x : Option Lake.Package) => pkg?) x

Instances For

source
@[inline]
def Lake.withCurrPackage {m : Type → Type u_1} {α : Type} [MonadWithReader CurrPackage m] (pkg : Package) (x : m α) :
m α

Run the action `x` with `pkg` as the current package.

Equations

- Lake.withCurrPackage pkg x = Lake.withCurrPackage? (some pkg) x

Instances For

source
@[inline]
def Lake.getCurrPackage? {m : Type → Type u_1} [MonadReaderOf CurrPackage m] :
m (Option Package)

Get the package of the context (if any).

Equations

- Lake.getCurrPackage? = read

Instances For

source
@[reducible, inline]
abbrev Lake.RecBuildT (m : Type → Type) (α : Type) :
Type

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

An internal monad. Not intended for user use.

Equations

- Lake.RecBuildT m = ReaderT Lake.CurrPackage (Lake.CallStackT Lake.BuildKey (StateRefT' IO.RealWorld Lake.BuildStore (Lake.BuildT m)))

Instances For

source
def Lake.buildCycleError (cycle : Cycle BuildKey) :
String

Build cycle error message.

Equations

- Lake.buildCycleError cycle = toString "build cycle detected:\n" ++ toString (inline (Lake.formatCycle cycle))

Instances For

source
instance Lake.instMonadCycleOfBuildKeyRecBuildTOfMonadOfMonadError {m : Type → Type} [Monad m] [MonadError m] :
MonadCycleOf BuildKey (RecBuildT m)
Equations

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

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

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

An internal monad. Not intended for user use.

Equations

- Lake.RecBuildM = Lake.RecBuildT Lake.LogIO

Instances For

source
@[inline]
def Lake.RecBuildT.run {m : Type → Type} {α : Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (stack : CallStack BuildKey) (store : BuildStore) (build : RecBuildT m α) :
BuildT m (α × BuildStore)

Run a recursive build.

Equations

- Lake.RecBuildT.run stack store build = (build none stack).run store

Instances For

source
@[inline]
def Lake.RecBuildT.run' {m : Type → Type} {α : Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (build : RecBuildT m α) :
BuildT m α

Run a recursive build in a fresh build store.

Equations

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

Instances For

source
@[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.Job (Lake.BuildData info.key)))

Instances For

source
@[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 Lake.RecBuildM) m

Instances For

source
@[reducible, inline]
abbrev Lake.FetchT (m : Type → Type) (α : Type) :
Type

The top-level monad transformer for Lake build functions.

Equations

- Lake.FetchT m = Lake.IndexT (Lake.RecBuildT m)

Instances For

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

The top-level monad for Lake build functions.

Equations

- Lake.FetchM = Lake.FetchT Lake.LogIO

Instances For

source
@[inline]
def Lake.FetchM.ofFn {α : Type} (f : IndexBuildFn RecBuildM → Option Package → CallStack BuildKey → IO.Ref BuildStore → BuildContext → Log → BaseIO (EResult Log.Pos Log α)) :
FetchM α

Construct a `FetchM` monad from its full functional representation.

Equations

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

Instances For

source
@[inline]
def Lake.FetchM.toFn {α : Type} (self : FetchM α) :
IndexBuildFn RecBuildM → Option Package → CallStack BuildKey → IO.Ref BuildStore → BuildContext → Log → BaseIO (EResult Log.Pos Log α)

Convert a `FetchM` monad to its full functional representation.

Equations

- self.toFn fetch pkg? stack store ctx log = Lake.ELogT.run (Lake.EquipT.run self fetch pkg? stack store ctx) log

Instances For

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

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

Equations

- self.fetch = Lake.EquipT.mk fun (build : Lake.IndexBuildFn Lake.RecBuildM) => cast ⋯ (build self)

Instances For

source
def Lake.ModuleFacet.fetch {α : Type} (self : ModuleFacet α) (mod : Module) :
FetchM (Job α)

Fetch the result of this facet of a module.

Equations

- self.fetch mod = (Lake.Module.facetCore self.name mod).fetch

Instances For