Lake.Config.TargetConfig

source

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

Type

A custom target's declarative configuration.

build (pkg : Lake.NPackage pkgName) : Lake.FetchM (Lake.CustomData (pkgName, name))
The target's build function.
getJob : Lake.CustomData (pkgName, name) → Lake.BuildJob Unit
The target's resulting build job.

Instances For

source

instance Lake.instInhabitedTargetConfig {a✝ a✝¹ : Lean.Name} :

Inhabited (Lake.TargetConfig a✝ a✝¹)

Equations

Lake.instInhabitedTargetConfig = { default := { build := default, getJob := default } }

source

@[inline]

def Lake.mkTargetJobConfig {pkgName : Lean.Name} {α : Type} {name : Lean.Name} (build : Lake.NPackage pkgName → Lake.FetchM (Lake.BuildJob α)) [h : Lake.FamilyOut Lake.CustomData (pkgName, name) (Lake.BuildJob α)] :

Lake.TargetConfig pkgName name

A smart constructor for target configurations that generate CLI targets.

Equations

Lake.mkTargetJobConfig build = { build := cast ⋯ build, getJob := fun (data : Lake.CustomData (pkgName, name)) => discard (Lake.ofFamily data) }

source

structure Lake.TargetDecl :

Type

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

pkg : Lean.Name
name : Lean.Name
config : Lake.TargetConfig self.pkg self.name

source

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

Inhabited (Lake.OpaqueTargetConfig pkgName name)

Equations

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

source

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

Lake.OpaqueTargetConfig pkgName name → Lake.TargetConfig pkgName name

Equations

Lake.OpaqueTargetConfig.unsafeGet = unsafeCast

source

instance Lake.OpaqueTargetConfig.instCoeNameTargetConfig {pkgName name : Lean.Name} :

Coe (Lake.OpaqueTargetConfig pkgName name) (Lake.TargetConfig pkgName name)

Equations

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

source

instance Lake.OpaqueTargetConfig.instCoeTargetConfigName {pkgName name : Lean.Name} :

Coe (Lake.TargetConfig pkgName name) (Lake.OpaqueTargetConfig pkgName name)

Equations

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

source

@[implemented_by Lake.OpaqueTargetConfig.unsafeMk]

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

Lake.TargetConfig pkgName name → Lake.OpaqueTargetConfig pkgName name

source

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

Lake.TargetConfig pkgName name → Lake.OpaqueTargetConfig pkgName name

Equations

Lake.OpaqueTargetConfig.unsafeMk = unsafeCast

source

@[implemented_by Lake.OpaqueTargetConfig.unsafeGet]

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

Lake.OpaqueTargetConfig pkgName name → Lake.TargetConfig pkgName name

source

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

Option (Lake.TargetConfig self.name name)

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

Equations

Lake.Package.findTargetConfig? name self = Option.map (fun (x : Lake.OpaqueTargetConfig self.config.name name) => x.get) (Lake.DRBMap.find? self.opaqueTargetConfigs name)