@[inline]

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

For internal use only.

@[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.

@[inline]

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

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

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