Build Target Specifiers

structure Lake.BuildSpec : Type

• info : Lake.BuildInfo
• getBuildJob : Lake.BuildData self.info.key → Lake.BuildJob Unit

@[inline]

def Lake.BuildData.toBuildJob {k : Lake.BuildKey} {α : Type} [Lake.FamilyOut Lake.BuildData k (Lake.BuildJob α)] (data : Lake.BuildData k) : Lake.BuildJob Unit

@[inline]

def Lake.mkBuildSpec {α : Type} (info : Lake.BuildInfo) [Lake.FamilyOut Lake.BuildData info.key (Lake.BuildJob α)] : Lake.BuildSpec

@[inline]

def Lake.mkConfigBuildSpec {Fam : Lean.Name → Type} {ι : Type} {facet : Lean.Name} (facetType : String) (info : Lake.BuildInfo) (config : Lake.FacetConfig Fam ι facet) (h : Lake.BuildData info.key = Fam facet) : Except Lake.CliError Lake.BuildSpec

@[inline]

def Lake.BuildSpec.fetch (self : Lake.BuildSpec) : Lake.FetchM (Lake.BuildJob Unit)

def Lake.buildSpecs (specs : Array Lake.BuildSpec) : Lake.FetchM (Lake.BuildJob Unit)

Parsing CLI Build Target Specifiers

def Lake.parsePackageSpec (ws : Lake.Workspace) (spec : String) : Except Lake.CliError Lake.Package

def Lake.resolveModuleTarget (ws : Lake.Workspace) (mod : Lake.Module) (facet : Lean.Name := Lean.Name.anonymous) : Except Lake.CliError Lake.BuildSpec

Equations

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

def Lake.resolveLibTarget (ws : Lake.Workspace) (lib : Lake.LeanLib) (facet : Lean.Name := Lean.Name.anonymous) : Except Lake.CliError (Array Lake.BuildSpec)

def Lake.resolveLibTarget.resolveFacet (ws : Lake.Workspace) (lib : Lake.LeanLib) (facet : Lean.Name) : Except Lake.CliError Lake.BuildSpec

def Lake.resolveExeTarget (exe : Lake.LeanExe) (facet : Lean.Name) : Except Lake.CliError Lake.BuildSpec

Equations

• Lake.resolveExeTarget exe facet = if (facet.isAnonymous || facet == `exe) = true then pure (Lake.mkBuildSpec exe.exe) else throw (Lake.CliError.unknownFacet "executable" facet)

def Lake.resolveExternLibTarget (lib : Lake.ExternLib) (facet : Lean.Name) : Except Lake.CliError Lake.BuildSpec

def Lake.resolveCustomTarget (pkg : Lake.Package) (name facet : Lean.Name) (config : Lake.TargetConfig pkg.name name) : Except Lake.CliError Lake.BuildSpec

Equations

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

def Lake.resolveTargetInPackage (ws : Lake.Workspace) (pkg : Lake.Package) (target facet : Lean.Name) : Except Lake.CliError (Array Lake.BuildSpec)

Equations

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

def Lake.resolveDefaultPackageTarget (ws : Lake.Workspace) (pkg : Lake.Package) : Except Lake.CliError (Array Lake.BuildSpec)

def Lake.resolvePackageTarget (ws : Lake.Workspace) (pkg : Lake.Package) (facet : Lean.Name) : Except Lake.CliError (Array Lake.BuildSpec)

def Lake.resolveTargetInWorkspace (ws : Lake.Workspace) (target facet : Lean.Name) : Except Lake.CliError (Array Lake.BuildSpec)

Equations

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

def Lake.resolveTargetBaseSpec (ws : Lake.Workspace) (spec : String) (facet : Lean.Name) : Except Lake.CliError (Array Lake.BuildSpec)

Equations

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

def Lake.parseExeTargetSpec (ws : Lake.Workspace) (spec : String) : Except Lake.CliError Lake.LeanExe

Equations

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

def Lake.parseTargetSpec (ws : Lake.Workspace) (spec : String) : Except Lake.CliError (Array Lake.BuildSpec)

def Lake.parseTargetSpecs (ws : Lake.Workspace) (specs : List String) : Except Lake.CliError (Array Lake.BuildSpec)

Equations

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