The Lake Build Index

The Lake build index is the complete map of Lake build keys to Lake build functions, which is used by Lake to build any Lake build info.

This module leverages the index to perform topologically-based recursive builds.

@[macro_inline]

def Lake.mkTargetFacetBuild {α : Type} (facet : Lean.Name) (build : FetchM (Job α)) [h : FamilyOut TargetData facet α] : FetchM (Job (TargetData facet))

Converts a conveniently-typed target facet build function into its dynamically-typed equivalent.

Equations

• Lake.mkTargetFacetBuild facet build = cast ⋯ build

def Lake.ExternLib.recBuildStatic (lib : ExternLib) : FetchM (Job System.FilePath)

Equations

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

def Lake.ExternLib.recBuildShared (lib : ExternLib) : FetchM (Job System.FilePath)

Equations

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

def Lake.ExternLib.recComputeDynlib (lib : ExternLib) : FetchM (Job Dynlib)

Equations

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

Topologically-based Recursive Build Using the Index

def Lake.recBuildWithIndex (info : BuildInfo) : FetchM (Job (BuildData info.key))

Recursive build function for anything in the Lake build index.

Equations

• One or more equations did not get rendered due to their size.
• Lake.recBuildWithIndex (Lake.BuildInfo.leanExe exe) = Lake.mkTargetFacetBuild Lake.LeanExe.exeFacet exe.recBuildExe
• Lake.recBuildWithIndex (Lake.BuildInfo.staticExternLib lib) = Lake.mkTargetFacetBuild Lake.ExternLib.staticFacet lib.recBuildStatic
• Lake.recBuildWithIndex (Lake.BuildInfo.sharedExternLib lib) = Lake.mkTargetFacetBuild Lake.ExternLib.sharedFacet lib.recBuildShared
• Lake.recBuildWithIndex (Lake.BuildInfo.dynlibExternLib lib) = Lake.mkTargetFacetBuild Lake.ExternLib.dynlibFacet lib.recComputeDynlib

def Lake.recFetchWithIndex (info : BuildInfo) : RecBuildM (Job (BuildData info.key))

Recursive build function with memoization.

Equations

• Lake.recFetchWithIndex = inline (Lake.recFetchMemoize Lake.BuildInfo.key Lake.recBuildWithIndex)

@[inline]

def Lake.FetchT.run {m : Type → Type} {α : Type} (x : FetchT m α) : RecBuildT m α

Run a recursive Lake build using the Lake build index and a topological / suspending scheduler.

Equations

• x.run = x Lake.recFetchWithIndex