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.

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.

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

Optional library directory (for -L).

Equations

• Lake.Dynlib.dir? self = System.FilePath.parent self.path

Module Facets

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.

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

Equations

• Lake.instReprModuleFacet = { reprPrec := Lake.reprModuleFacet✝ }

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

Equations

• @Lake.instFamilyDefNameModuleDataName = @Lake.instFamilyDefNameModuleDataName.proof_1

instance Lake.instCoeDepNameModuleFacet {facet : Lake.Name} {α : Type} [Lake.FamilyOut Lake.ModuleData facet α] : CoeDep Lake.Name facet (Lake.ModuleFacet α)

Equations

• Lake.instCoeDepNameModuleFacet = { coe := { name := facet, data_eq := (_ : Lake.ModuleData facet = α) } }

@[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.

Equations

• Lake.Module.depsFacet = `deps

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

Equations

• Lake.instFamilyDefNameModuleDataMkStrAnonymousBuildJobProdSearchPathArrayFilePath = Lake.instFamilyDefNameModuleDataMkStrAnonymousBuildJobProdSearchPathArrayFilePath.proof_1

@[simp]

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

@[inline, reducible]

abbrev Lake.Module.leanArtsFacet : Lake.Name

The core build facet of a Lean file. Elaborates the Lean file via lean and produces all the Lean artifacts of the module (i.e., olean, ilean, c). Its trace just includes its dependencies.

Equations

• Lake.Module.leanArtsFacet = `leanArts

@[simp]

axiom Lake.ModuleData.leanArts : Lake.ModuleData (Lean.Name.mkStr Lean.Name.anonymous "leanArts") = Lake.BuildJob Unit

instance Lake.instFamilyDefNameModuleDataMkStrAnonymousBuildJobUnit : Lake.FamilyDef Lake.ModuleData (Lean.Name.mkStr Lean.Name.anonymous "leanArts") (Lake.BuildJob Unit)

Equations

• Lake.instFamilyDefNameModuleDataMkStrAnonymousBuildJobUnit = Lake.instFamilyDefNameModuleDataMkStrAnonymousBuildJobUnit.proof_1

@[inline, reducible]

abbrev Lake.Module.oleanFacet : Lake.Name

The olean file produced by lean.

Equations

• Lake.Module.oleanFacet = `olean

@[simp]

axiom Lake.ModuleData.olean : Lake.ModuleData (Lean.Name.mkStr Lean.Name.anonymous "olean") = Lake.BuildJob Lake.FilePath

instance Lake.instFamilyDefNameModuleDataMkStrAnonymousBuildJobFilePath : Lake.FamilyDef Lake.ModuleData (Lean.Name.mkStr Lean.Name.anonymous "olean") (Lake.BuildJob Lake.FilePath)

Equations

• Lake.instFamilyDefNameModuleDataMkStrAnonymousBuildJobFilePath = Lake.instFamilyDefNameModuleDataMkStrAnonymousBuildJobFilePath.proof_1

@[inline, reducible]

abbrev Lake.Module.ileanFacet : Lake.Name

The ilean file produced by lean.

Equations

• Lake.Module.ileanFacet = `ilean

instance Lake.instFamilyDefNameModuleDataMkStrAnonymousBuildJobFilePath_1 : Lake.FamilyDef Lake.ModuleData (Lean.Name.mkStr Lean.Name.anonymous "ilean") (Lake.BuildJob Lake.FilePath)

Equations

• Lake.instFamilyDefNameModuleDataMkStrAnonymousBuildJobFilePath_1 = Lake.instFamilyDefNameModuleDataMkStrAnonymousBuildJobFilePath_1.proof_1

@[simp]

axiom Lake.ModuleData.ilean : Lake.ModuleData (Lean.Name.mkStr Lean.Name.anonymous "ilean") = Lake.BuildJob Lake.FilePath

@[inline, reducible]

abbrev Lake.Module.cFacet : Lake.Name

The C file built from the Lean file via lean.

Equations

• Lake.Module.cFacet = `c

instance Lake.instFamilyDefNameModuleDataMkStrAnonymousBuildJobFilePath_2 : Lake.FamilyDef Lake.ModuleData (Lean.Name.mkStr Lean.Name.anonymous "c") (Lake.BuildJob Lake.FilePath)

Equations

• Lake.instFamilyDefNameModuleDataMkStrAnonymousBuildJobFilePath_2 = Lake.instFamilyDefNameModuleDataMkStrAnonymousBuildJobFilePath_2.proof_1

@[simp]

axiom Lake.ModuleData.c : Lake.ModuleData (Lean.Name.mkStr Lean.Name.anonymous "c") = Lake.BuildJob Lake.FilePath

@[inline, reducible]

abbrev Lake.Module.oFacet : Lake.Name

The object file built from c.

Equations

• Lake.Module.oFacet = `o

@[simp]

axiom Lake.ModuleData.o : Lake.ModuleData (Lean.Name.mkStr Lean.Name.anonymous "o") = Lake.BuildJob Lake.FilePath

instance Lake.instFamilyDefNameModuleDataMkStrAnonymousBuildJobFilePath_3 : Lake.FamilyDef Lake.ModuleData (Lean.Name.mkStr Lean.Name.anonymous "o") (Lake.BuildJob Lake.FilePath)

Equations

• Lake.instFamilyDefNameModuleDataMkStrAnonymousBuildJobFilePath_3 = Lake.instFamilyDefNameModuleDataMkStrAnonymousBuildJobFilePath_3.proof_1

Package Facets

@[inline, reducible]

abbrev Lake.Package.releaseFacet : Lake.Name

A package's cloud build release.

Equations

• Lake.Package.releaseFacet = `release

instance Lake.instFamilyDefNamePackageDataMkStrAnonymousBuildJobUnit : Lake.FamilyDef Lake.PackageData (Lean.Name.mkStr Lean.Name.anonymous "release") (Lake.BuildJob Unit)

Equations

• Lake.instFamilyDefNamePackageDataMkStrAnonymousBuildJobUnit = Lake.instFamilyDefNamePackageDataMkStrAnonymousBuildJobUnit.proof_1

@[simp]

axiom Lake.PackageData.release : Lake.PackageData (Lean.Name.mkStr Lean.Name.anonymous "release") = Lake.BuildJob Unit

@[inline, reducible]

abbrev Lake.Package.extraDepFacet : Lake.Name

A package's extraDepTargets mixed with its transitive dependencies'.

Equations

• Lake.Package.extraDepFacet = `extraDep

instance Lake.instFamilyDefNamePackageDataMkStrAnonymousBuildJobUnit_1 : Lake.FamilyDef Lake.PackageData (Lean.Name.mkStr Lean.Name.anonymous "extraDep") (Lake.BuildJob Unit)

Equations

• Lake.instFamilyDefNamePackageDataMkStrAnonymousBuildJobUnit_1 = Lake.instFamilyDefNamePackageDataMkStrAnonymousBuildJobUnit_1.proof_1

@[simp]

axiom Lake.PackageData.extraDep : Lake.PackageData (Lean.Name.mkStr Lean.Name.anonymous "extraDep") = Lake.BuildJob Unit

Target Facets

@[inline, reducible]

abbrev Lake.LeanLib.leanArtsFacet : Lake.Name

A Lean library's Lean artifacts (i.e., olean, ilean, c).

Equations

• Lake.LeanLib.leanArtsFacet = `leanArts

@[simp]

axiom Lake.TargetData.leanLib.leanArts : Lake.TargetData (`leanLib ++ Lean.Name.mkStr Lean.Name.anonymous "leanArts") = Lake.BuildJob Unit

instance Lake.instFamilyDefNameTargetDataHAppendInstHAppendInstAppendNameMkStr1MkStrAnonymousBuildJobUnit : Lake.FamilyDef Lake.TargetData (`leanLib ++ Lean.Name.mkStr Lean.Name.anonymous "leanArts") (Lake.BuildJob Unit)

Equations

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

@[inline, reducible]

abbrev Lake.LeanLib.staticFacet : Lake.Name

A Lean library's static artifact.

Equations

• Lake.LeanLib.staticFacet = `static

instance Lake.instFamilyDefNameTargetDataHAppendInstHAppendInstAppendNameMkStr1MkStrAnonymousBuildJobFilePath : Lake.FamilyDef Lake.TargetData (`leanLib ++ Lean.Name.mkStr Lean.Name.anonymous "static") (Lake.BuildJob Lake.FilePath)

Equations

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

@[simp]

axiom Lake.TargetData.leanLib.static : Lake.TargetData (`leanLib ++ Lean.Name.mkStr Lean.Name.anonymous "static") = Lake.BuildJob Lake.FilePath

@[inline, reducible]

abbrev Lake.LeanLib.sharedFacet : Lake.Name

A Lean library's shared artifact.

Equations

• Lake.LeanLib.sharedFacet = `shared

instance Lake.instFamilyDefNameTargetDataHAppendInstHAppendInstAppendNameMkStr1MkStrAnonymousBuildJobFilePath_1 : Lake.FamilyDef Lake.TargetData (`leanLib ++ Lean.Name.mkStr Lean.Name.anonymous "shared") (Lake.BuildJob Lake.FilePath)

Equations

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

@[simp]

axiom Lake.TargetData.leanLib.shared : Lake.TargetData (`leanLib ++ Lean.Name.mkStr Lean.Name.anonymous "shared") = Lake.BuildJob Lake.FilePath

@[inline, reducible]

abbrev Lake.LeanLib.extraDepFacet : Lake.Name

A Lean library's extraDepTargets mixed with its package's.

Equations

• Lake.LeanLib.extraDepFacet = `extraDep

@[simp]

axiom Lake.TargetData.leanLib.extraDep : Lake.TargetData (`leanLib ++ Lean.Name.mkStr Lean.Name.anonymous "extraDep") = Lake.BuildJob Unit

instance Lake.instFamilyDefNameTargetDataHAppendInstHAppendInstAppendNameMkStr1MkStrAnonymousBuildJobUnit_1 : Lake.FamilyDef Lake.TargetData (`leanLib ++ Lean.Name.mkStr Lean.Name.anonymous "extraDep") (Lake.BuildJob Unit)

Equations

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

@[inline, reducible]

abbrev Lake.LeanExe.exeFacet : Lake.Name

A Lean binary executable.

Equations

• Lake.LeanExe.exeFacet = `leanExe

instance Lake.instFamilyDefNameTargetDataMkStrAnonymousBuildJobFilePath : Lake.FamilyDef Lake.TargetData (Lean.Name.mkStr Lean.Name.anonymous "leanExe") (Lake.BuildJob Lake.FilePath)

Equations

• Lake.instFamilyDefNameTargetDataMkStrAnonymousBuildJobFilePath = Lake.instFamilyDefNameTargetDataMkStrAnonymousBuildJobFilePath.proof_1

@[simp]

axiom Lake.TargetData.leanExe : Lake.TargetData (Lean.Name.mkStr Lean.Name.anonymous "leanExe") = Lake.BuildJob Lake.FilePath

@[inline, reducible]

abbrev Lake.ExternLib.staticFacet : Lake.Name

A external library's static binary.

Equations

• Lake.ExternLib.staticFacet = `externLib.static

@[simp]

axiom Lake.TargetData.externLib.static : Lake.TargetData (Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "externLib") "static") = Lake.BuildJob Lake.FilePath

instance Lake.instFamilyDefNameTargetDataMkStrAnonymousBuildJobFilePath_1 : Lake.FamilyDef Lake.TargetData (Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "externLib") "static") (Lake.BuildJob Lake.FilePath)

Equations

• Lake.instFamilyDefNameTargetDataMkStrAnonymousBuildJobFilePath_1 = Lake.instFamilyDefNameTargetDataMkStrAnonymousBuildJobFilePath_1.proof_1

@[inline, reducible]

abbrev Lake.ExternLib.sharedFacet : Lake.Name

A external library's shared binary.

Equations

• Lake.ExternLib.sharedFacet = `externLib.shared

@[simp]

axiom Lake.TargetData.externLib.shared : Lake.TargetData (Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "externLib") "shared") = Lake.BuildJob Lake.FilePath

instance Lake.instFamilyDefNameTargetDataMkStrAnonymousBuildJobFilePath_2 : Lake.FamilyDef Lake.TargetData (Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "externLib") "shared") (Lake.BuildJob Lake.FilePath)

Equations

• Lake.instFamilyDefNameTargetDataMkStrAnonymousBuildJobFilePath_2 = Lake.instFamilyDefNameTargetDataMkStrAnonymousBuildJobFilePath_2.proof_1

@[inline, reducible]

abbrev Lake.ExternLib.dynlibFacet : Lake.Name

A external library's dynlib.

Equations

• Lake.ExternLib.dynlibFacet = `externLib.dynlib

instance Lake.instFamilyDefNameTargetDataMkStrAnonymousBuildJobDynlib : Lake.FamilyDef Lake.TargetData (Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "externLib") "dynlib") (Lake.BuildJob Lake.Dynlib)

Equations

• Lake.instFamilyDefNameTargetDataMkStrAnonymousBuildJobDynlib = Lake.instFamilyDefNameTargetDataMkStrAnonymousBuildJobDynlib.proof_1

@[simp]

axiom Lake.TargetData.externLib.dynlib : Lake.TargetData (Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "externLib") "dynlib") = Lake.BuildJob Lake.Dynlib