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 : Lean.Name) [OptDataKind α] [FormatQuery α] [FamilyDef ModuleData facet α] (f : Module → FetchM (Job α)) : 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 (Job α)` -/

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

Equations

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

def Lake.DSL.expandModuleFacetDecl : Lean.Macro

Equations

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

@[reducible, inline]

abbrev Lake.DSL.mkPackageFacetDecl (α : Type) (facet : Lean.Name) [OptDataKind α] [FormatQuery α] [FamilyDef PackageData facet α] (f : Package → FetchM (Job α)) : 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 (Job α)` -/

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

Equations

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

def Lake.DSL.expandPackageFacetDecl : Lean.Macro

Equations

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

@[reducible, inline]

abbrev Lake.DSL.mkLibraryFacetDecl (α : Type) (facet : Lean.Name) [OptDataKind α] [FormatQuery α] [FamilyDef LibraryData facet α] (f : LeanLib → FetchM (Job α)) : 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 (Job α)` -/

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

Equations

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

def Lake.DSL.expandLibraryFacetDecl : Lean.Macro

Equations

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

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 α)) : TargetDecl

Equations

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

def Lake.DSL.targetCommand : 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 (Job α)` -/

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.

def Lake.DSL.expandTargetCommand : Lean.Macro

Equations

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

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

• Lake.DSL.mkConfigDecl pkg name kind config = { pkg := pkg, name := name, kind := kind, config := config, wf_data := ⋯, kind_eq := ⋯ }

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) : Lean.Elab.Command.CommandElabM Lean.Command

def Lake.DSL.leanLibCommand : 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.

def Lake.DSL.elabLeanLibCommand : Lean.Elab.Command.CommandElab

Equations

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

@[reducible, inline]

abbrev Lake.DSL.LeanLibCommand : 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.LeanLibCommand = Lean.TSyntax `Lake.DSL.leanLibCommand

Instances For

• Lake.DSL.instCoeLeanLibCommandCommand

instance Lake.DSL.instCoeLeanLibCommandCommand : Coe LeanLibCommand Lean.Command

Equations

• Lake.DSL.instCoeLeanLibCommandCommand = { coe := fun (x : Lake.DSL.LeanLibCommand) => { raw := x.raw } }

def Lake.DSL.leanExeCommand : 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.

def Lake.DSL.elabLeanExeCommand : Lean.Elab.Command.CommandElab

Equations

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

@[reducible, inline]

abbrev Lake.DSL.LeanExeCommand : 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.LeanExeCommand = Lean.TSyntax `Lake.DSL.leanExeCommand

Instances For

• Lake.DSL.instCoeLeanExeCommandCommand

instance Lake.DSL.instCoeLeanExeCommandCommand : Coe LeanExeCommand Lean.Command

Equations

• Lake.DSL.instCoeLeanExeCommandCommand = { coe := fun (x : Lake.DSL.LeanExeCommand) => { raw := x.raw } }

def Lake.DSL.inputFileCommand : Lean.ParserDescr

Define a new input file target for the package. Can optionally be provided with a configuration of type InputFileConfig.

Equations

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

def Lake.DSL.elabInputfileCommand : Lean.Elab.Command.CommandElab

Equations

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

@[reducible, inline]

abbrev Lake.DSL.InputFileCommand : Type

Define a new input file target for the package. Can optionally be provided with a configuration of type InputFileConfig.

Equations

• Lake.DSL.InputFileCommand = Lean.TSyntax `Lake.DSL.inputFileCommand

Instances For

• Lake.DSL.instCoeInputFileCommandCommand

instance Lake.DSL.instCoeInputFileCommandCommand : Coe InputFileCommand Lean.Command

Equations

• Lake.DSL.instCoeInputFileCommandCommand = { coe := fun (x : Lake.DSL.InputFileCommand) => { raw := x.raw } }

def Lake.DSL.inputDirCommand : Lean.ParserDescr

Define a new input directory target for the package. Can optionally be provided with a configuration of type InputDirConfig.

Equations

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

def Lake.DSL.elabInputDirCommand : Lean.Elab.Command.CommandElab

Equations

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

@[reducible, inline]

abbrev Lake.DSL.InputDirCommand : Type

Define a new input directory target for the package. Can optionally be provided with a configuration of type InputDirConfig.

Equations

• Lake.DSL.InputDirCommand = Lean.TSyntax `Lake.DSL.inputDirCommand

Instances For

• Lake.DSL.instCoeInputDirCommandCommand

instance Lake.DSL.instCoeInputDirCommandCommand : Coe InputDirCommand Lean.Command

Equations

• Lake.DSL.instCoeInputDirCommandCommand = { coe := fun (x : Lake.DSL.InputDirCommand) => { raw := x.raw } }

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)] : ExternLibDecl

Equations

• Lake.DSL.mkExternLibDecl pkgName name = Lake.DSL.mkConfigDecl pkgName name Lake.ExternLib.configKind { getPath := cast ⋯ }

def Lake.DSL.externLibDeclSpec : Lean.ParserDescr

Equations

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

def Lake.DSL.externLibCommand : 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 (Job 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.

def Lake.DSL.expandExternLibCommand : Lean.Macro

Equations

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