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 : Lake.Name) (build : Lake.IndexBuildM α) [h : Lake.FamilyOut Lake.TargetData facet α] : Lake.IndexBuildM (Lake.TargetData facet)

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

Equations

• Lake.mkTargetFacetBuild facet build = cast (_ : Lake.IndexBuildM α = Lake.IndexBuildM (Lake.TargetData facet)) build

def Lake.ExternLib.recBuildStatic (lib : Lake.ExternLib) : Lake.IndexBuildM (Lake.BuildJob Lake.FilePath)

Equations

• Lake.ExternLib.recBuildStatic lib = lib.config.getJob <$> Lake.fetch (Lake.Package.target (Lake.ExternLib.staticTargetName lib) lib.pkg)

def Lake.ExternLib.recBuildShared (lib : Lake.ExternLib) : Lake.IndexBuildM (Lake.BuildJob Lake.FilePath)

Equations

• Lake.ExternLib.recBuildShared lib = do let __do_lift ← Lake.fetch (Lake.ExternLib.static lib) liftM (Lake.buildLeanSharedLibOfStatic __do_lift (Lake.ExternLib.linkArgs lib) #[])

def Lake.ExternLib.recComputeDynlib (lib : Lake.ExternLib) : Lake.IndexBuildM (Lake.BuildJob Lake.Dynlib)

Equations

• Lake.ExternLib.recComputeDynlib lib = do let __do_lift ← Lake.fetch (Lake.ExternLib.shared lib) liftM (Lake.computeDynlibOfShared __do_lift)

Topologically-based Recursive Build Using the Index

def Lake.recBuildWithIndex (info : Lake.BuildInfo) : Lake.IndexBuildM (Lake.BuildData (Lake.BuildInfo.key info))

Recursive build function for anything in the Lake build index.

Equations

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

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

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

Equations

• Lake.IndexBuildM.run build = build (Lake.recFetchMemoize Lake.BuildInfo.key Lake.recBuildWithIndex)

def Lake.buildIndexTop' (info : Lake.BuildInfo) : Lake.RecBuildM (Lake.BuildData (Lake.BuildInfo.key info))

Recursively build the given info using the Lake build index and a topological / suspending scheduler.

Equations

• Lake.buildIndexTop' info = Lake.recFetchMemoize Lake.BuildInfo.key Lake.recBuildWithIndex info

@[macro_inline]

def Lake.buildIndexTop {α : Type} (info : Lake.BuildInfo) [Lake.FamilyOut Lake.BuildData (Lake.BuildInfo.key info) α] : Lake.RecBuildM α

Recursively build the given info using the Lake build index and a topological / suspending scheduler and return the dynamic result.

Equations

• Lake.buildIndexTop info = cast (_ : Lake.RecBuildM (Lake.BuildData (Lake.BuildInfo.key info)) = Lake.RecBuildM α) (Lake.buildIndexTop' info)

@[inline]

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

Build the given Lake target in a fresh build store.

Equations

• Lake.build self = Lake.RecBuildM.run (Lake.buildIndexTop self)

Lean Executable Builds

@[inline]

def Lake.LeanExe.build (self : Lake.LeanExe) : Lake.BuildM (Lake.BuildJob Lake.FilePath)

Equations

• Lake.LeanExe.build self = Lake.build (Lake.LeanExe.exe self)

@[inline]

def Lake.LeanExeConfig.build (self : Lake.LeanExeConfig) : Lake.BuildM (Lake.BuildJob Lake.FilePath)

Equations

• Lake.LeanExeConfig.build self = do let __do_lift ← Lake.LeanExeConfig.get self Lake.LeanExe.build __do_lift

@[inline]

def Lake.LeanExe.fetch (self : Lake.LeanExe) : Lake.IndexBuildM (Lake.BuildJob Lake.FilePath)

Equations

• Lake.LeanExe.fetch self = Lake.fetch (Lake.LeanExe.exe self)