# Lean Executable Build #

The build function definition for a Lean executable.

source
def Lake.LeanExe.exeFacetConfig :
LeanExeFacetConfig exeFacet

The facet configuration for the builtin `LeanExe.exeFacet`.

Equations

- Lake.LeanExe.exeFacetConfig = Lake.mkFacetJobConfig Lake.LeanExe.recBuildExe✝

Instances For

source
def Lake.LeanExe.defaultFacetConfig :
LeanExeFacetConfig defaultFacet

The facet configuration for the builtin `ExternLib.dynlibFacet`.

Equations

- Lake.LeanExe.defaultFacetConfig = Lake.mkFacetJobConfig Lake.LeanExe.recBuildDefault✝ true false

Instances For

source
def Lake.LeanExe.initFacetConfigs :
DNameMap LeanExeFacetConfig

A name-configuration map for the initial set of Lean executable facets (e.g., `exe`).

Equations

- Lake.LeanExe.initFacetConfigs = (Std.DTreeMap.insert Lake.DNameMap.empty Lake.LeanExe.defaultFacet Lake.LeanExe.defaultFacetConfig).insert Lake.LeanExe.exeFacet Lake.LeanExe.exeFacetConfig

Instances For