DSL for Targets & Facets

Macros for declaring Lake targets and facets.

def Lake.DSL.buildDeclSig : Lean.ParserDescr

Equations

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

Facet Declarations

@[reducible, inline]

abbrev Lake.DSL.mkModuleFacetDecl (α : Type) (facet : Lake.Name) [Lake.FamilyDef Lake.ModuleData facet (Lake.BuildJob α)] (f : Lake.Module → Lake.FetchM (Lake.BuildJob α)) : Lake.ModuleFacetDecl

Equations

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

def Lake.DSL.moduleFacetDecl : Lean.ParserDescr

Define a new module facet. Has one form:

module_facet «facet-name» (mod : Module) : α :=
  /- build term of type `FetchM (BuildJob α)` -/

The mod parameter (and its type specifier) is optional.

Equations

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

@[reducible, inline]

abbrev Lake.DSL.mkPackageFacetDecl (α : Type) (facet : Lake.Name) [Lake.FamilyDef Lake.PackageData facet (Lake.BuildJob α)] (f : Lake.Package → Lake.FetchM (Lake.BuildJob α)) : Lake.PackageFacetDecl

Equations

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

def Lake.DSL.packageFacetDecl : Lean.ParserDescr

Define a new package facet. Has one form:

package_facet «facet-name» (pkg : Package) : α :=
  /- build term of type `FetchM (BuildJob α)` -/

The pkg parameter (and its type specifier) is optional.

Equations

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

@[reducible, inline]

abbrev Lake.DSL.mkLibraryFacetDecl (α : Type) (facet : Lake.Name) [Lake.FamilyDef Lake.LibraryData facet (Lake.BuildJob α)] (f : Lake.LeanLib → Lake.FetchM (Lake.BuildJob α)) : Lake.LibraryFacetDecl

Equations

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

def Lake.DSL.libraryFacetDecl : Lean.ParserDescr

Define a new library facet. Has one form:

library_facet «facet-name» (lib : LeanLib) : α :=
  /- build term of type `FetchM (BuildJob α)` -/

The lib parameter (and its type specifier) is optional.

Equations

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

Custom Target Declaration

@[reducible, inline]

abbrev Lake.DSL.mkTargetDecl (α : Type) (pkgName : Lake.Name) (target : Lake.Name) [Lake.FamilyDef Lake.CustomData (pkgName, target) (Lake.BuildJob α)] (f : Lake.NPackage pkgName → Lake.FetchM (Lake.BuildJob α)) : Lake.TargetDecl

Equations

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

def Lake.DSL.targetDecl : Lean.ParserDescr

Define a new custom target for the package. Has one form:

target «target-name» (pkg : NPackage _package.name) : α :=
  /- build term of type `FetchM (BuildJob α)` -/

The pkg parameter (and its type specifier) is optional. It is of type NPackage _package.name to provably demonstrate the package provided is the package in which the target is defined.

Equations

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

Lean Library & Executable Target Declarations

def Lake.DSL.leanLibDecl : Lean.ParserDescr

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

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

@[reducible, inline]

abbrev Lake.DSL.LeanLibDecl : Type

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

• Lake.DSL.LeanLibDecl = Lean.TSyntax `Lake.DSL.leanLibDecl

instance Lake.DSL.instCoeLeanLibDeclCommand : Coe Lake.DSL.LeanLibDecl Lean.Command

Equations

• Lake.DSL.instCoeLeanLibDeclCommand = { coe := fun (x : Lake.DSL.LeanLibDecl) => { raw := x.raw } }

def Lake.DSL.leanExeDecl : Lean.ParserDescr

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

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

@[reducible, inline]

abbrev Lake.DSL.LeanExeDecl : Type

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

• Lake.DSL.LeanExeDecl = Lean.TSyntax `Lake.DSL.leanExeDecl

instance Lake.DSL.instCoeLeanExeDeclCommand : Coe Lake.DSL.LeanExeDecl Lean.Command

Equations

• Lake.DSL.instCoeLeanExeDeclCommand = { coe := fun (x : Lake.DSL.LeanExeDecl) => { raw := x.raw } }

External Library Target Declaration

def Lake.DSL.externLibDeclSpec : Lean.ParserDescr

Equations

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

def Lake.DSL.externLibDecl : Lean.ParserDescr

Define a new external library target for the package. Has one form:

extern_lib «target-name» (pkg : NPackage _package.name) :=
  /- build term of type `FetchM (BuildJob FilePath)` -/

The pkg parameter (and its type specifier) is optional. It is of type NPackage _package.name to provably demonstrate the package provided is the package in which the target is defined.

The term should build the external library's static library.

Equations

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