Documentation

Lake.Config.TargetConfig

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

A custom target's declarative configuration.

Instances For
    Equations
    • Lake.instInhabitedTargetConfig = { default := { build := default, getJob := default } }
    @[inline]
    def Lake.mkTargetJobConfig {pkgName : Lake.Name} {α : Type} {name : Lake.Name} (build : Lake.NPackage pkgNameLake.IndexBuildM (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
    • One or more equations did not get rendered due to their size.
    Instances For

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

      Instances For
        Equations
        • Lake.OpaqueTargetConfig.instCoeTargetConfigOpaqueTargetConfig = { coe := Lake.OpaqueTargetConfig.mk }
        unsafe def Lake.OpaqueTargetConfig.unsafeMk {pkgName : Lake.Name} {name : Lake.Name} :
        Lake.TargetConfig pkgName nameLake.OpaqueTargetConfig pkgName name
        Equations
        • Lake.OpaqueTargetConfig.unsafeMk = unsafeCast
        Instances For
          Equations
          @[implemented_by Lake.OpaqueTargetConfig.unsafeGet]
          opaque Lake.OpaqueTargetConfig.get {pkgName : Lake.Name} {name : Lake.Name} :
          Lake.OpaqueTargetConfig pkgName nameLake.TargetConfig pkgName name
          Equations
          • Lake.OpaqueTargetConfig.instCoeOpaqueTargetConfigTargetConfig = { coe := Lake.OpaqueTargetConfig.get }
          @[implemented_by Lake.OpaqueTargetConfig.unsafeMk]
          opaque Lake.OpaqueTargetConfig.mk {pkgName : Lake.Name} {name : Lake.Name} :
          Lake.TargetConfig pkgName nameLake.OpaqueTargetConfig pkgName name
          unsafe def Lake.OpaqueTargetConfig.unsafeGet {pkgName : Lake.Name} {name : Lake.Name} :
          Lake.OpaqueTargetConfig pkgName nameLake.TargetConfig pkgName name
          Equations
          • Lake.OpaqueTargetConfig.unsafeGet = unsafeCast
          Instances For

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

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