Build Target Specifiers

structure Lake.BuildSpec : Type

• info : BuildInfo
• getBuildJob : BuildData self.info.key → OpaqueJob

@[inline]

def Lake.BuildData.toJob {k : BuildKey} {α : Type} [FamilyOut BuildData k (Job α)] (data : BuildData k) : OpaqueJob

Equations

• data.toJob = (Lake.ofFamily data).toOpaque

@[inline]

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

Equations

• Lake.mkBuildSpec info = { info := info, getBuildJob := Lake.BuildData.toJob }

@[inline]

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

Equations

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

@[inline]

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

Equations

• self.fetch = do let __do_lift ← self.getBuildJob <$> self.info.fetch Lake.maybeRegisterJob self.info.key.toSimpleString __do_lift

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

Equations

• Lake.buildSpecs specs = do let __do_lift ← Array.mapM (fun (x : Lake.BuildSpec) => x.fetch) specs pure (Lake.Job.mixArray __do_lift)

Parsing CLI Build Target Specifiers

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lake.resolveExeTarget (exe : LeanExe) (facet : Lean.Name) : Except CliError 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 : ExternLib) (facet : Lean.Name) : Except CliError BuildSpec

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lake.resolveDefaultPackageTarget ws pkg = Array.flatMapM (fun (x : Lean.Name) => Lake.resolveTargetInPackage ws pkg x Lean.Name.anonymous) pkg.defaultTargets

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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