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 : LeanLib) :
FetchM (Job (Array Module))

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

Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lake.LeanLib.recCollectLocalModules.go (self : LeanLib) (root : Module) (mods : Array Module) (modSet : ModuleSet) :
FetchM (Array Module × ModuleSet)
source
def Lake.LeanLib.modulesFacetConfig :
LibraryFacetConfig modulesFacet

The LibraryFacetConfig for the builtin modulesFacet.

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

The LibraryFacetConfig for the builtin leanArtsFacet.

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

The LibraryFacetConfig for the builtin staticFacet.

Equations
source
def Lake.LeanLib.staticExportFacetConfig :
LibraryFacetConfig staticExportFacet

The LibraryFacetConfig for the builtin staticExportFacet.

Equations

Build Shared Lib #

source
def Lake.LeanLib.recBuildShared (self : LeanLib) :
FetchM (Job System.FilePath)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lake.LeanLib.sharedFacetConfig :
LibraryFacetConfig sharedFacet

The LibraryFacetConfig for the builtin sharedFacet.

Equations

Build extraDepTargets #

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

Build the extraDepTargets for the library and its package.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lake.LeanLib.extraDepFacetConfig :
LibraryFacetConfig extraDepFacet

The LibraryFacetConfig for the builtin extraDepFacet.

Equations
source
def Lake.initLibraryFacetConfigs :
DNameMap 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).

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