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.
A recursive build of a Lake build store that may encounter a cycle.
Instances For
Run a recursive build.
Equations
- Lake.RecBuildM.run stack store build = build stack store
Instances For
Run a recursive build in a fresh build store.
Equations
- build.run' = (fun (x : α × Lake.BuildStore) => x.fst) <$> Lake.RecBuildM.run ∅ ∅ build
Instances For
Log build cycle and error.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lake.instMonadCycleOfBuildKeyRecBuildM = Lake.MonadCycleOf.mk fun {α : Type} => Lake.buildCycleError
A build function for any element of the Lake build index.
Equations
- Lake.IndexBuildFn m = ((info : Lake.BuildInfo) → m (Lake.BuildData info.key))
Instances For
A transformer to equip a monad with a build function for the Lake index.
Equations
- Lake.IndexT m = Lake.EquipT (Lake.IndexBuildFn m) m
Instances For
The top-level monad for Lake build functions.
Equations
Instances For
The top-level monad for Lake build functions. Renamed FetchM
.
Equations
Instances For
The old build monad. Uses should generally be replaced by FetchM
.
Equations
Instances For
Fetch the result associated with the info using the Lake build index.