Documentation

Lake.Build.Library

Library Facet Builds #

Build function definitions for a library's builtin facets.

Build Lean & Static Lib #

source
def Lake.LeanLib.recCollectLocalModules (self : Lake.LeanLib) :
Lake.FetchM (Array Lake.Module)

Collect the local modules of a library. That is, the modules from getModuleArray plus their local transitive imports.

source
partial def Lake.LeanLib.recCollectLocalModules.go (self : Lake.LeanLib) (root : Lake.Module) (mods : Array Lake.Module) (modSet : Lake.ModuleSet) :
Lake.FetchM (Array Lake.Module × Lake.ModuleSet)
source
def Lake.LeanLib.modulesFacetConfig :
Lake.LibraryFacetConfig Lake.LeanLib.modulesFacet

The LibraryFacetConfig for the builtin modulesFacet.

Equations
source
def Lake.LeanLib.recBuildLean (self : Lake.LeanLib) :
Lake.FetchM (Lake.BuildJob Unit)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lake.LeanLib.leanArtsFacetConfig :
Lake.LibraryFacetConfig Lake.LeanLib.leanArtsFacet

The LibraryFacetConfig for the builtin leanArtsFacet.

source
@[specialize #[]]
def Lake.LeanLib.recBuildStatic (self : Lake.LeanLib) (shouldExport : Bool) :
Lake.FetchM (Lake.BuildJob System.FilePath)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lake.LeanLib.staticFacetConfig :
Lake.LibraryFacetConfig Lake.LeanLib.staticFacet

The LibraryFacetConfig for the builtin staticFacet.

source
def Lake.LeanLib.staticExportFacetConfig :
Lake.LibraryFacetConfig Lake.LeanLib.staticExportFacet

The LibraryFacetConfig for the builtin staticExportFacet.

Build Shared Lib #

source
def Lake.LeanLib.recBuildShared (self : Lake.LeanLib) :
Lake.FetchM (Lake.BuildJob System.FilePath)
source
def Lake.LeanLib.sharedFacetConfig :
Lake.LibraryFacetConfig Lake.LeanLib.sharedFacet

The LibraryFacetConfig for the builtin sharedFacet.

Build extraDepTargets #

source
def Lake.LeanLib.recBuildExtraDepTargets (self : Lake.LeanLib) :
Lake.FetchM (Lake.BuildJob Unit)

Build the extraDepTargets for the library and its package.

source
def Lake.LeanLib.extraDepFacetConfig :
Lake.LibraryFacetConfig Lake.LeanLib.extraDepFacet

The LibraryFacetConfig for the builtin extraDepFacet.

Equations
source
def Lake.initLibraryFacetConfigs :
Lake.DNameMap Lake.LibraryFacetConfig

A library facet name to build function map that contains builders for the initial set of Lake library facets (e.g., lean, static, and shared).