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.ModuleDeps : Type

• dynlibs : Array System.FilePath
• plugins : Array System.FilePath

instance Lake.instInhabitedModuleDeps : Inhabited ModuleDeps

Equations

• Lake.instInhabitedModuleDeps = { default := { dynlibs := default, plugins := default } }

instance Lake.instReprModuleDeps : Repr ModuleDeps

Equations

• Lake.instReprModuleDeps = { reprPrec := Lake.reprModuleDeps✝ }

Module Facets

structure Lake.ModuleFacet (α : Type) : Type

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

• name : Lean.Name

  The name of the module facet.

• data_eq : ModuleData self.name = α

  Proof that module's facet build result is of type α.

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

Equations

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

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

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

Equations

• Lake.instCoeDepNameModuleFacetOfFamilyOutModuleData = { coe := { name := facet, data_eq := ⋯ } }

@[reducible, inline]

abbrev Lake.Module.depsFacet : Lean.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

@[simp]

axiom Lake.ModuleData.deps : ModuleData `deps = ModuleDeps

instance Lake.instFamilyDefNameModuleDataMkStr1ModuleDeps : FamilyDef ModuleData `deps ModuleDeps

@[reducible, inline]

abbrev Lake.Module.leanArtsFacet : Lean.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 : ModuleData `leanArts = Unit

instance Lake.instFamilyDefNameModuleDataMkStr1Unit : FamilyDef ModuleData `leanArts Unit

@[reducible, inline]

abbrev Lake.Module.oleanFacet : Lean.Name

The olean file produced by lean.

Equations

• Lake.Module.oleanFacet = `olean

@[simp]

axiom Lake.ModuleData.olean : ModuleData `olean = System.FilePath

instance Lake.instFamilyDefNameModuleDataMkStr1FilePath : FamilyDef ModuleData `olean System.FilePath

@[reducible, inline]

abbrev Lake.Module.ileanFacet : Lean.Name

The ilean file produced by lean.

Equations

• Lake.Module.ileanFacet = `ilean

@[simp]

axiom Lake.ModuleData.ilean : ModuleData `ilean = System.FilePath

instance Lake.instFamilyDefNameModuleDataMkStr1FilePath_1 : FamilyDef ModuleData `ilean System.FilePath

@[reducible, inline]

abbrev Lake.Module.cFacet : Lean.Name

The C file built from the Lean file via lean.

Equations

• Lake.Module.cFacet = `c

@[simp]

axiom Lake.ModuleData.c : ModuleData `c = System.FilePath

instance Lake.instFamilyDefNameModuleDataMkStr1FilePath_2 : FamilyDef ModuleData `c System.FilePath

@[reducible, inline]

abbrev Lake.Module.bcFacet : Lean.Name

The LLVM BC file built from the Lean file via lean.

Equations

• Lake.Module.bcFacet = `bc

@[simp]

axiom Lake.ModuleData.bc : ModuleData `bc = System.FilePath

instance Lake.instFamilyDefNameModuleDataMkStr1FilePath_3 : FamilyDef ModuleData `bc System.FilePath

@[reducible, inline]

abbrev Lake.Module.coFacet : Lean.Name

The object file .c.o built from c. On Windows, this is c.o.noexport, on other systems it is c.o.export).

Equations

• Lake.Module.coFacet = `c.o

@[simp]

axiom Lake.ModuleData.c.o : ModuleData `c.o = System.FilePath

instance Lake.instFamilyDefNameModuleDataMkStr2FilePath : FamilyDef ModuleData `c.o System.FilePath

@[reducible, inline]

abbrev Lake.Module.coExportFacet : Lean.Name

The object file .c.o.export built from c (with -DLEAN_EXPORTING).

Equations

• Lake.Module.coExportFacet = `c.o.export

instance Lake.instFamilyDefNameModuleDataMkStr3FilePath : FamilyDef ModuleData `c.o.export System.FilePath

@[simp]

axiom Lake.ModuleData.c.o.export : ModuleData `c.o.export = System.FilePath

@[reducible, inline]

abbrev Lake.Module.coNoExportFacet : Lean.Name

The object file .c.o.noexport built from c (without -DLEAN_EXPORTING).

Equations

• Lake.Module.coNoExportFacet = `c.o.noexport

@[simp]

axiom Lake.ModuleData.c.o.noexport : ModuleData `c.o.noexport = System.FilePath

instance Lake.instFamilyDefNameModuleDataMkStr3FilePath_1 : FamilyDef ModuleData `c.o.noexport System.FilePath

@[reducible, inline]

abbrev Lake.Module.bcoFacet : Lean.Name

The object file .bc.o built from bc.

Equations

• Lake.Module.bcoFacet = `bc.o

instance Lake.instFamilyDefNameModuleDataMkStr2FilePath_1 : FamilyDef ModuleData `bc.o System.FilePath

@[simp]

axiom Lake.ModuleData.bc.o : ModuleData `bc.o = System.FilePath

@[reducible, inline]

abbrev Lake.Module.oFacet : Lean.Name

The object file built from c/bc. On Windows with the C backend, no Lean symbols are exported. On every other configuration, symbols are exported.

Equations

• Lake.Module.oFacet = `o

instance Lake.instFamilyDefNameModuleDataMkStr1FilePath_4 : FamilyDef ModuleData `o System.FilePath

@[simp]

axiom Lake.ModuleData.o : ModuleData `o = System.FilePath

@[reducible, inline]

abbrev Lake.Module.oExportFacet : Lean.Name

The object file built from c/bc (with Lean symbols exported).

Equations

• Lake.Module.oExportFacet = `o.export

instance Lake.instFamilyDefNameModuleDataMkStr2FilePath_2 : FamilyDef ModuleData `o.export System.FilePath

@[simp]

axiom Lake.ModuleData.o.export : ModuleData `o.export = System.FilePath

@[reducible, inline]

abbrev Lake.Module.oNoExportFacet : Lean.Name

The object file built from c/bc (without Lean symbols exported).

Equations

• Lake.Module.oNoExportFacet = `o.noexport

instance Lake.instFamilyDefNameModuleDataMkStr2FilePath_3 : FamilyDef ModuleData `o.noexport System.FilePath

@[simp]

axiom Lake.ModuleData.o.noexport : ModuleData `o.noexport = System.FilePath

Package Facets

@[reducible, inline]

abbrev Lake.Package.optBuildCacheFacet : Lean.Name

A package's optional cached build archive (e.g., from Reservoir or GitHub). Will NOT cause the whole build to fail if the archive cannot be fetched.

Equations

• Lake.Package.optBuildCacheFacet = `optCache

@[simp]

axiom Lake.PackageData.optCache : PackageData `optCache = Bool

instance Lake.instFamilyDefNamePackageDataMkStr1Bool : FamilyDef PackageData `optCache Bool

@[reducible, inline]

abbrev Lake.Package.buildCacheFacet : Lean.Name

A package's cached build archive (e.g., from Reservoir or GitHub). Will cause the whole build to fail if the archive cannot be fetched.

Equations

• Lake.Package.buildCacheFacet = `cache

instance Lake.instFamilyDefNamePackageDataMkStr1Unit : FamilyDef PackageData `cache Unit

@[simp]

axiom Lake.PackageData.cache : PackageData `cache = Unit

@[reducible, inline]

abbrev Lake.Package.optReservoirBarrelFacet : Lean.Name

A package's optional build archive from Reservoir. Will NOT cause the whole build to fail if the barrel cannot be fetched.

Equations

• Lake.Package.optReservoirBarrelFacet = `optBarrel

instance Lake.instFamilyDefNamePackageDataMkStr1Bool_1 : FamilyDef PackageData `optBarrel Bool

@[simp]

axiom Lake.PackageData.optBarrel : PackageData `optBarrel = Bool

@[reducible, inline]

abbrev Lake.Package.reservoirBarrelFacet : Lean.Name

A package's Reservoir build archive from Reservoir. Will cause the whole build to fail if the barrel cannot be fetched.

Equations

• Lake.Package.reservoirBarrelFacet = `barrel

@[simp]

axiom Lake.PackageData.barrel : PackageData `barrel = Unit

instance Lake.instFamilyDefNamePackageDataMkStr1Unit_1 : FamilyDef PackageData `barrel Unit

@[reducible, inline]

abbrev Lake.Package.optGitHubReleaseFacet : Lean.Name

A package's optional build archive from a GitHub release. Will NOT cause the whole build to fail if the release cannot be fetched.

Equations

• Lake.Package.optGitHubReleaseFacet = `optRelease

@[simp]

axiom Lake.PackageData.optRelease : PackageData `optRelease = Bool

instance Lake.instFamilyDefNamePackageDataMkStr1Bool_2 : FamilyDef PackageData `optRelease Bool

@[reducible, inline, deprecated Lake.Package.optGitHubReleaseFacet (since := "2024-09-27")]

abbrev Lake.Package.optReleaseFacet : Lean.Name

Equations

• Lake.Package.optReleaseFacet = Lake.Package.optGitHubReleaseFacet

@[reducible, inline]

abbrev Lake.Package.gitHubReleaseFacet : Lean.Name

A package's build archive from a GitHub release. Will cause the whole build to fail if the release cannot be fetched.

Equations

• Lake.Package.gitHubReleaseFacet = `release

instance Lake.instFamilyDefNamePackageDataMkStr1Unit_2 : FamilyDef PackageData `release Unit

@[simp]

axiom Lake.PackageData.release : PackageData `release = Unit

@[reducible, inline, deprecated Lake.Package.gitHubReleaseFacet (since := "2024-09-27")]

abbrev Lake.Package.releaseFacet : Lean.Name

Equations

• Lake.Package.releaseFacet = Lake.Package.gitHubReleaseFacet

@[reducible, inline]

abbrev Lake.Package.extraDepFacet : Lean.Name

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

Equations

• Lake.Package.extraDepFacet = `extraDep

@[simp]

axiom Lake.PackageData.extraDep : PackageData `extraDep = Unit

instance Lake.instFamilyDefNamePackageDataMkStr1Unit_3 : FamilyDef PackageData `extraDep Unit

Target Facets

@[reducible, inline]

abbrev Lake.LeanLib.leanArtsFacet : Lean.Name

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

Equations

• Lake.LeanLib.leanArtsFacet = `leanArts

@[simp]

axiom Lake.TargetData.leanLib.leanArts : TargetData (`leanLib ++ `leanArts) = Unit

instance Lake.instFamilyDefNameTargetDataHAppendMkStr1Unit : FamilyDef TargetData (`leanLib ++ `leanArts) Unit

@[reducible, inline]

abbrev Lake.LeanLib.staticFacet : Lean.Name

A Lean library's static artifact.

Equations

• Lake.LeanLib.staticFacet = `static

@[simp]

axiom Lake.TargetData.leanLib.static : TargetData (`leanLib ++ `static) = System.FilePath

instance Lake.instFamilyDefNameTargetDataHAppendMkStr1FilePath : FamilyDef TargetData (`leanLib ++ `static) System.FilePath

@[reducible, inline]

abbrev Lake.LeanLib.staticExportFacet : Lean.Name

A Lean library's static artifact (with exported symbols).

Equations

• Lake.LeanLib.staticExportFacet = `static.export

@[simp]

axiom Lake.TargetData.leanLib.static.export : TargetData (`leanLib ++ `static.export) = System.FilePath

instance Lake.instFamilyDefNameTargetDataHAppendMkStr1MkStr2FilePath : FamilyDef TargetData (`leanLib ++ `static.export) System.FilePath

@[reducible, inline]

abbrev Lake.LeanLib.sharedFacet : Lean.Name

A Lean library's shared artifact.

Equations

• Lake.LeanLib.sharedFacet = `shared

instance Lake.instFamilyDefNameTargetDataHAppendMkStr1FilePath_1 : FamilyDef TargetData (`leanLib ++ `shared) System.FilePath

@[simp]

axiom Lake.TargetData.leanLib.shared : TargetData (`leanLib ++ `shared) = System.FilePath

@[reducible, inline]

abbrev Lake.LeanLib.extraDepFacet : Lean.Name

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

Equations

• Lake.LeanLib.extraDepFacet = `extraDep

instance Lake.instFamilyDefNameTargetDataHAppendMkStr1Unit_1 : FamilyDef TargetData (`leanLib ++ `extraDep) Unit

@[simp]

axiom Lake.TargetData.leanLib.extraDep : TargetData (`leanLib ++ `extraDep) = Unit

@[reducible, inline]

abbrev Lake.LeanExe.exeFacet : Lean.Name

A Lean binary executable.

Equations

• Lake.LeanExe.exeFacet = `leanExe

@[simp]

axiom Lake.TargetData.leanExe : TargetData `leanExe = System.FilePath

instance Lake.instFamilyDefNameTargetDataMkStr1FilePath : FamilyDef TargetData `leanExe System.FilePath

@[reducible, inline]

abbrev Lake.ExternLib.staticFacet : Lean.Name

A external library's static binary.

Equations

• Lake.ExternLib.staticFacet = `externLib.static

@[simp]

axiom Lake.TargetData.externLib.static : TargetData `externLib.static = System.FilePath

instance Lake.instFamilyDefNameTargetDataMkStr2FilePath : FamilyDef TargetData `externLib.static System.FilePath

@[reducible, inline]

abbrev Lake.ExternLib.sharedFacet : Lean.Name

A external library's shared binary.

Equations

• Lake.ExternLib.sharedFacet = `externLib.shared

instance Lake.instFamilyDefNameTargetDataMkStr2FilePath_1 : FamilyDef TargetData `externLib.shared System.FilePath

@[simp]

axiom Lake.TargetData.externLib.shared : TargetData `externLib.shared = System.FilePath

@[reducible, inline]

abbrev Lake.ExternLib.dynlibFacet : Lean.Name

A external library's dynlib.

Equations

• Lake.ExternLib.dynlibFacet = `externLib.dynlib

@[simp]

axiom Lake.TargetData.externLib.dynlib : TargetData `externLib.dynlib = Dynlib

instance Lake.instFamilyDefNameTargetDataMkStr2Dynlib : FamilyDef TargetData `externLib.dynlib Dynlib