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 Dynlib)
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

Other #

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

Build extra target dependencies of the library (e.g., extraDepTargets, needs).

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.LeanLib.recBuildDefaultFacets (self : LeanLib) :
FetchM (Job Unit)

Build the default facets for the library.

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

The LibraryFacetConfig for the builtin defaultFacet.

Equations
source
def Lake.LeanLib.initFacetConfigs :
DNameMap LeanLibFacetConfig

A name-configuration map for the initial set of Lean library facets (e.g., lean, static, shared).

Equations
  • One or more equations did not get rendered due to their size.
source
@[reducible, inline]
abbrev Lake.initLibraryFacetConfigs :
DNameMap LibraryFacetConfig

A name-configuration map for the initial set of Lean library facets (e.g., lean, static, shared).

Equations