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, deprecated "Deprecated without replacement." (since := "2025-02-22")]

abbrev Lake.CoreBuildM (α : Type) : Type

The internal core monad of Lake builds. Not intended for user use.

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

@[specialize #[]]

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

Log build cycle and error.

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

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

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

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

@[reducible, inline]

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

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

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

@[reducible, inline]

abbrev Lake.FetchT (m : Type → Type) (α : Type) : Type

The top-level monad transformer for Lake build functions.

@[reducible, inline]

abbrev Lake.FetchM (α : Type) : Type

The top-level monad for Lake build functions.

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

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

Fetch the result of this facet of a module.