structure Lake.TargetConfig (pkgName name : Lean.Name) : Type

A custom target's declarative configuration.

• fetchFn (pkg : NPackage pkgName) : FetchM (Job (CustomData pkgName name))

  The target's fetch function.

• format : OutFormat → CustomData pkgName name → String

  Format the target's output (e.g., for lake query).

Instances For

• Lake.OpaqueTargetConfig.instCoeNameTargetConfig
• Lake.OpaqueTargetConfig.instCoeTargetConfigName
• Lake.instInhabitedTargetConfig

instance Lake.instInhabitedTargetConfig {a✝ a✝¹ : Lean.Name} : Inhabited (TargetConfig a✝ a✝¹)

Equations

• Lake.instInhabitedTargetConfig = { default := { fetchFn := default, format := default } }

@[inline]

def Lake.mkTargetJobConfig {α : Type} {pkgName name : Lean.Name} [FormatQuery α] [h : FamilyOut (CustomData pkgName) name α] (fetch : NPackage pkgName → FetchM (Job α)) : TargetConfig pkgName name

A smart constructor for target configurations that generate CLI targets.

Equations

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

instance Lake.OpaqueTargetConfig.instInhabitedNameOfTargetConfig {pkgName name : Lean.Name} [Inhabited (TargetConfig pkgName name)] : Inhabited (OpaqueTargetConfig pkgName name)

Equations

• Lake.OpaqueTargetConfig.instInhabitedNameOfTargetConfig = { default := Lake.OpaqueTargetConfig.mk default }

unsafe def Lake.OpaqueTargetConfig.unsafeMk {pkgName name : Lean.Name} : TargetConfig pkgName name → OpaqueTargetConfig pkgName name

Equations

• Lake.OpaqueTargetConfig.unsafeMk = unsafeCast

instance Lake.OpaqueTargetConfig.instCoeNameTargetConfig {pkgName name : Lean.Name} : Coe (OpaqueTargetConfig pkgName name) (TargetConfig pkgName name)

Equations

• Lake.OpaqueTargetConfig.instCoeNameTargetConfig = { coe := Lake.OpaqueTargetConfig.get }

instance Lake.OpaqueTargetConfig.instCoeTargetConfigName {pkgName name : Lean.Name} : Coe (TargetConfig pkgName name) (OpaqueTargetConfig pkgName name)

Equations

• Lake.OpaqueTargetConfig.instCoeTargetConfigName = { coe := Lake.OpaqueTargetConfig.mk }

unsafe def Lake.OpaqueTargetConfig.unsafeGet {pkgName name : Lean.Name} : OpaqueTargetConfig pkgName name → TargetConfig pkgName name

Equations

• Lake.OpaqueTargetConfig.unsafeGet = unsafeCast

@[implemented_by Lake.OpaqueTargetConfig.unsafeMk]

opaque Lake.OpaqueTargetConfig.mk {pkgName name : Lean.Name} : TargetConfig pkgName name → OpaqueTargetConfig pkgName name

@[implemented_by Lake.OpaqueTargetConfig.unsafeGet]

opaque Lake.OpaqueTargetConfig.get {pkgName name : Lean.Name} : OpaqueTargetConfig pkgName name → TargetConfig pkgName name

@[inline]

def Lake.NConfigDecl.targetConfig {p n : Lean.Name} (self : NConfigDecl p n) (h : self.kind.isAnonymous = true) : TargetConfig p n

Equations

• self.targetConfig h = (self.opaqueTargetConfig h).get

@[inline]

def Lake.NConfigDecl.targetConfig? {p n : Lean.Name} (self : NConfigDecl p n) : Option (TargetConfig p n)

Equations

• self.targetConfig? = Option.map (fun (x : Lake.OpaqueTargetConfig p n) => x.get) self.opaqueTargetConfig?

@[reducible, inline]

abbrev Lake.TargetDecl : Type

A dependently typed configuration based on its registered package and name.

Equations

• Lake.TargetDecl = Lake.KConfigDecl Lean.Name.anonymous

def Lake.Package.findTargetConfig? (name : Lean.Name) (self : Package) : Option (TargetConfig self.name name)

Try to find a target configuration in the package with the given name .

Equations

• Lake.Package.findTargetConfig? name self = (Lake.DRBMap.find? self.targetDeclMap name).bind fun (x : Lake.NConfigDecl self.name name) => x.targetConfig?