DSL for Targets & Facets #
Macros for declaring Lake targets and facets.
Facet Declarations #
@[reducible, inline]
abbrev
Lake.DSL.mkModuleFacetDecl
(α : Type)
(facet : Lean.Name)
[OptDataKind α]
[FormatQuery α]
[FamilyDef ModuleData facet α]
(f : Module → FetchM (Job α))
:
Equations
Instances For
@[reducible, inline]
abbrev
Lake.DSL.mkPackageFacetDecl
(α : Type)
(facet : Lean.Name)
[OptDataKind α]
[FormatQuery α]
[FamilyDef PackageData facet α]
(f : Package → FetchM (Job α))
:
Equations
Instances For
@[reducible, inline]
abbrev
Lake.DSL.mkLibraryFacetDecl
(α : Type)
(facet : Lean.Name)
[OptDataKind α]
[FormatQuery α]
[FamilyDef LibraryData facet α]
(f : LeanLib → FetchM (Job α))
:
Equations
Instances For
Custom Target Declaration #
@[reducible, inline]
abbrev
Lake.DSL.mkTargetDecl
(α : Type)
(pkgName target : Lean.Name)
[OptDataKind α]
[FormatQuery α]
[FamilyDef (CustomData pkgName) target α]
(f : NPackage pkgName → FetchM (Job α))
:
Equations
Instances For
Lean Library & Executable Target Declarations #
@[reducible, inline]
abbrev
Lake.DSL.mkConfigDecl
(pkg name kind : Lean.Name)
(config : ConfigType kind pkg name)
[FamilyDef (CustomData pkg) name (ConfigTarget kind)]
[FamilyDef DataType kind (ConfigTarget kind)]
:
KConfigDecl kind
Equations
Instances For
def
Lake.DSL.mkConfigDeclDef
(tyName attr kind : Lean.Name)
[ConfigInfo tyName]
[delTyName : TypeName (KConfigDecl kind)]
(doc? : Option DocComment)
(attrs? : Option Attributes)
(nameStx? : Option IdentOrStr)
(cfg : OptConfig)
:
Equations
Instances For
@[reducible, inline]
Define a new Lean library target for the package.
Can optionally be provided with a configuration of type LeanLibConfig
.
Has many forms:
lean_lib «target-name»
lean_lib «target-name» { /- config opts -/ }
lean_lib «target-name» where /- config opts -/
Equations
Instances For
@[reducible, inline]
Define a new Lean binary executable target for the package.
Can optionally be provided with a configuration of type LeanExeConfig
.
Has many forms:
lean_exe «target-name»
lean_exe «target-name» { /- config opts -/ }
lean_exe «target-name» where /- config opts -/
Equations
Instances For
@[reducible, inline]
Define a new input file target for the package.
Can optionally be provided with a configuration of type InputFileConfig
.
Equations
Instances For
@[reducible, inline]
Define a new input directory target for the package.
Can optionally be provided with a configuration of type InputDirConfig
.
Equations
Instances For
External Library Target Declaration #
@[reducible, inline]
abbrev
Lake.DSL.mkExternLibDecl
(pkgName name : Lean.Name)
[FamilyDef (CustomData pkgName) (name.str "static") System.FilePath]
[FamilyDef (CustomData pkgName) name (ConfigTarget ExternLib.configKind)]
: