Build Target Specifiers

structure Lake.BuildSpec : Type

• info : BuildInfo
• buildable : Bool
• format : OutFormat → BuildData self.info.key → String

@[inline]

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

@[inline]

def Lake.mkConfigBuildSpec {facet : Lean.Name} (info : BuildInfo) (config : FacetConfig facet) (h : BuildData info.key = FacetOut facet) : BuildSpec

@[inline]

def Lake.BuildSpec.fetch (self : BuildSpec) : FetchM (Job (BuildData self.info.key))

@[inline]

def Lake.BuildSpec.build (self : BuildSpec) : FetchM OpaqueJob

@[inline]

def Lake.BuildSpec.query (self : BuildSpec) (fmt : OutFormat) : FetchM (Job String)

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

def Lake.querySpecs (specs : Array BuildSpec) (fmt : OutFormat) : FetchM (Job (Array String))

Parsing CLI Build Target Specifiers

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

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

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

def Lake.resolveConfigDeclTarget (ws : Workspace) (pkg : Package) {target : Lean.Name} (decl : NConfigDecl pkg.name target) (facet : Lean.Name) : Except CliError (Array BuildSpec)

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

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

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

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

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

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

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

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

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

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

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

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