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.

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

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

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

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.

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.

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.

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

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

Lean Executable Builds

@[inline]

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

@[inline]

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