@[inline]

def Lake.PartialBuildKey.fetchInCore (defaultPkg : Package) (self : PartialBuildKey) : FetchM ((key : BuildKey) × Job (BuildData key))

For internal use only.

Equations

• Lake.PartialBuildKey.fetchInCore defaultPkg self = Lake.PartialBuildKey.fetchInCoreAux✝ defaultPkg self self true

@[inline]

def Lake.PartialBuildKey.fetchIn (defaultPkg : Package) (self : PartialBuildKey) : FetchM OpaqueJob

Fetches the target specified by this key, resolving gaps as needed.

• A missing package (i.e., Name.anoanmoyus) is filled in with defaultPkg.
• Facets are qualified by the their input target's kind, and missing facets are replaced by their kind's default.
• Package targets ending in moduleTargetIndicator are converted to module package targets.
• Package targets for non-dynamic targets (i.e., non-target) produce their default facet rather than their configuration.

Equations

• Lake.PartialBuildKey.fetchIn defaultPkg self = (fun (x : (key : Lake.BuildKey) × Lake.Job (Lake.BuildData key)) => x.snd.toOpaque) <$> Lake.PartialBuildKey.fetchInCore defaultPkg self

@[inline]

def Lake.BuildKey.fetch {α : Type} (self : BuildKey) [FamilyOut BuildData self α] : FetchM (Job α)

Equations

• self.fetch = cast ⋯ (Lake.BuildKey.fetchCore✝ self self)

def Lake.Target.fetchIn {α : Type} [DataKind α] (defaultPkg : Package) (self : Target α) : FetchM (Job α)

Equations

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

def Lake.TargetArray.fetchIn {α : Type} [DataKind α] (defaultPkg : Package) (self : TargetArray α) (traceCaption : String := "<targets>") : FetchM (Job (Array α))

Equations

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