Simple Builtin Facet Declarations #

This module contains the definitions of most of the builtin facets. The others are defined Build.Info. The facets there require configuration definitions (e.g., Module), and some of the facets here are used in said definitions.

source

structure Lake.Dynlib :

Type

path : Lake.FilePath
Library file path.
name : String
Library name without platform-specific prefix/suffix (for -l).

A dynamic/shared library for linking.

Instances For

source

def Lake.Dynlib.dir? (self : Lake.Dynlib) :

Option Lake.FilePath

Optional library directory (for -L).

Instances For

Module Facets #

source

structure Lake.ModuleFacet (α : Type) :

Type

name : Lake.Name
The name of the module facet.
data_eq : Lake.ModuleData s.name = α
Proof that module's facet build result is of type α.

A module facet name along with proof of its data type.

Instances For

source

instance Lake.instReprModuleFacet :

{α : Type} → [inst : Repr α] → Repr (Lake.ModuleFacet α)

source

instance Lake.instFamilyDefNameModuleDataName {α : Type} (facet : Lake.ModuleFacet α) :

Lake.FamilyDef Lake.ModuleData facet.name α

source

instance Lake.instCoeDepNameModuleFacet {facet : Lake.Name} {α : Type} [Lake.FamilyOut Lake.ModuleData facet α] :

CoeDep Lake.Name facet (Lake.ModuleFacet α)

source

@[inline, reducible]

abbrev Lake.Module.depsFacet :

Lake.Name

The facet which builds all of a module's dependencies (i.e., transitive local imports and --load-dynlib shared libraries). Returns the list of shared libraries to load along with their search path.

Instances For

source

instance Lake.instFamilyDefNameModuleDataMkStrAnonymousBuildJobProdSearchPathArrayFilePath :

Lake.FamilyDef Lake.ModuleData (Lean.Name.mkStr Lean.Name.anonymous "deps") (Lake.BuildJob (Lake.SearchPath × Array Lake.FilePath))

source

@[simp]

axiom Lake.ModuleData.deps :

Lake.ModuleData (Lean.Name.mkStr Lean.Name.anonymous "deps") = Lake.BuildJob (Lake.SearchPath × Array Lake.FilePath)

source

@[inline, reducible]

abbrev Lake.Module.leanBinFacet :

Lake.Name

The core compilation / elaboration of the Lean file via lean, which produce the Lean binaries of the module (i.e., olean, ilean, c). Its trace just includes its dependencies.

Instances For

source

@[simp]

axiom Lake.ModuleData.bin :

Lake.ModuleData (Lean.Name.mkStr Lean.Name.anonymous "bin") = Lake.BuildJob Unit

source

instance Lake.instFamilyDefNameModuleDataMkStrAnonymousBuildJobUnit :

Lake.FamilyDef Lake.ModuleData (Lean.Name.mkStr Lean.Name.anonymous "bin") (Lake.BuildJob Unit)

source

@[inline, reducible]

abbrev Lake.Module.importBinFacet :

Lake.Name

The leanBinFacet combined with the module's trace (i.e., the trace of its olean and ilean). It is the facet used for building a Lean import of a module.

Instances For

source

instance Lake.instFamilyDefNameModuleDataMkStrAnonymousBuildJobUnit_1 :

Lake.FamilyDef Lake.ModuleData (Lean.Name.mkStr Lean.Name.anonymous "importBin") (Lake.BuildJob Unit)

source

@[simp]

axiom Lake.ModuleData.importBin :

Lake.ModuleData (Lean.Name.mkStr Lean.Name.anonymous "importBin") = Lake.BuildJob Unit

source

@[inline, reducible]

abbrev Lake.Module.oleanFacet :

Lake.Name