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

A dynamic/shared library for linking.

• path : System.FilePath

  Library file path.

• name : String

  Library name without platform-specific prefix/suffix (for -l).

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

Optional library directory (for -L).

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 : Lake.ModuleData self.name = α

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

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

Equations

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

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

instance Lake.instCoeDepNameModuleFacetOfFamilyOutModuleData {facet : Lean.Name} {α : Type} [Lake.FamilyOut Lake.ModuleData facet α] : CoeDep Lean.Name facet (Lake.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.

theorem Lake.instFamilyDefNameModuleDataMkStr1BuildJobProdSearchPathArrayFilePath : Lake.FamilyDef Lake.ModuleData `deps (Lake.BuildJob (System.SearchPath × Array System.FilePath))

@[simp]

axiom Lake.ModuleData.deps : Lake.ModuleData `deps = Lake.BuildJob (System.SearchPath × Array System.FilePath)

@[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 : Lake.ModuleData `leanArts = Lake.BuildJob Unit

theorem Lake.instFamilyDefNameModuleDataMkStr1BuildJobUnit : Lake.FamilyDef Lake.ModuleData `leanArts (Lake.BuildJob Unit)

@[reducible, inline]

abbrev Lake.Module.oleanFacet : Lean.Name

The olean file produced by lean.

@[simp]

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

theorem Lake.instFamilyDefNameModuleDataMkStr1BuildJobFilePath : Lake.FamilyDef Lake.ModuleData `olean (Lake.BuildJob System.FilePath)

@[reducible, inline]

abbrev Lake.Module.ileanFacet : Lean.Name

The ilean file produced by lean.

theorem Lake.instFamilyDefNameModuleDataMkStr1BuildJobFilePath_1 : Lake.FamilyDef Lake.ModuleData `ilean (Lake.BuildJob System.FilePath)

@[simp]

axiom Lake.ModuleData.ilean : Lake.ModuleData `ilean = Lake.BuildJob 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 : Lake.ModuleData `c = Lake.BuildJob System.FilePath

theorem Lake.instFamilyDefNameModuleDataMkStr1BuildJobFilePath_2 : Lake.FamilyDef Lake.ModuleData `c (Lake.BuildJob 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 : Lake.ModuleData `bc = Lake.BuildJob System.FilePath

theorem Lake.instFamilyDefNameModuleDataMkStr1BuildJobFilePath_3 : Lake.FamilyDef Lake.ModuleData `bc (Lake.BuildJob 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

theorem Lake.instFamilyDefNameModuleDataMkStr2BuildJobFilePath : Lake.FamilyDef Lake.ModuleData `c.o (Lake.BuildJob System.FilePath)

@[simp]

axiom Lake.ModuleData.c.o : Lake.ModuleData `c.o = Lake.BuildJob 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

@[simp]

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

theorem Lake.instFamilyDefNameModuleDataMkStr3BuildJobFilePath : Lake.FamilyDef Lake.ModuleData `c.o.export (Lake.BuildJob 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 : Lake.ModuleData `c.o.noexport = Lake.BuildJob System.FilePath

theorem Lake.instFamilyDefNameModuleDataMkStr3BuildJobFilePath_1 : Lake.FamilyDef Lake.ModuleData `c.o.noexport (Lake.BuildJob System.FilePath)

@[reducible, inline]

abbrev Lake.Module.bcoFacet : Lean.Name

The object file .bc.o built from bc.

Equations

• Lake.Module.bcoFacet = `bc.o

theorem Lake.instFamilyDefNameModuleDataMkStr2BuildJobFilePath_1 : Lake.FamilyDef Lake.ModuleData `bc.o (Lake.BuildJob System.FilePath)

@[simp]

axiom Lake.ModuleData.bc.o : Lake.ModuleData `bc.o = Lake.BuildJob 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.

theorem Lake.instFamilyDefNameModuleDataMkStr1BuildJobFilePath_4 : Lake.FamilyDef Lake.ModuleData `o (Lake.BuildJob System.FilePath)

@[simp]

axiom Lake.ModuleData.o : Lake.ModuleData `o = Lake.BuildJob 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

@[simp]

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

theorem Lake.instFamilyDefNameModuleDataMkStr2BuildJobFilePath_2 : Lake.FamilyDef Lake.ModuleData `o.export (Lake.BuildJob System.FilePath)

@[reducible, inline]

abbrev Lake.Module.oNoExportFacet : Lean.Name

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

@[simp]

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

theorem Lake.instFamilyDefNameModuleDataMkStr2BuildJobFilePath_3 : Lake.FamilyDef Lake.ModuleData `o.noexport (Lake.BuildJob 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

theorem Lake.instFamilyDefNamePackageDataMkStr1BuildJobBool : Lake.FamilyDef Lake.PackageData `optCache (Lake.BuildJob Bool)

@[simp]

axiom Lake.PackageData.optCache : Lake.PackageData `optCache = Lake.BuildJob 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.

@[simp]

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

theorem Lake.instFamilyDefNamePackageDataMkStr1BuildJobUnit : Lake.FamilyDef Lake.PackageData `cache (Lake.BuildJob 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.

theorem Lake.instFamilyDefNamePackageDataMkStr1BuildJobBool_1 : Lake.FamilyDef Lake.PackageData `optBarrel (Lake.BuildJob Bool)

@[simp]

axiom Lake.PackageData.optBarrel : Lake.PackageData `optBarrel = Lake.BuildJob 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.

@[simp]

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

theorem Lake.instFamilyDefNamePackageDataMkStr1BuildJobUnit_1 : Lake.FamilyDef Lake.PackageData `barrel (Lake.BuildJob 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 : Lake.PackageData `optRelease = Lake.BuildJob Bool

theorem Lake.instFamilyDefNamePackageDataMkStr1BuildJobBool_2 : Lake.FamilyDef Lake.PackageData `optRelease (Lake.BuildJob Bool)

@[reducible, inline, deprecated Lake.Package.optGitHubReleaseFacet]

abbrev Lake.Package.optReleaseFacet : Lean.Name

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

@[simp]

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

theorem Lake.instFamilyDefNamePackageDataMkStr1BuildJobUnit_2 : Lake.FamilyDef Lake.PackageData `release (Lake.BuildJob Unit)

@[reducible, inline, deprecated Lake.Package.gitHubReleaseFacet]

abbrev Lake.Package.releaseFacet : Lean.Name

@[reducible, inline]

abbrev Lake.Package.extraDepFacet : Lean.Name

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

Equations

• Lake.Package.extraDepFacet = `extraDep

theorem Lake.instFamilyDefNamePackageDataMkStr1BuildJobUnit_3 : Lake.FamilyDef Lake.PackageData `extraDep (Lake.BuildJob Unit)

@[simp]

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

Target Facets

@[reducible, inline]

abbrev Lake.LeanLib.leanArtsFacet : Lean.Name

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

theorem Lake.instFamilyDefNameTargetDataHAppendMkStr1BuildJobUnit : Lake.FamilyDef Lake.TargetData (`leanLib ++ `leanArts) (Lake.BuildJob Unit)

@[simp]

axiom Lake.TargetData.leanLib.leanArts : Lake.TargetData (`leanLib ++ `leanArts) = Lake.BuildJob 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 : Lake.TargetData (`leanLib ++ `static) = Lake.BuildJob System.FilePath

theorem Lake.instFamilyDefNameTargetDataHAppendMkStr1BuildJobFilePath : Lake.FamilyDef Lake.TargetData (`leanLib ++ `static) (Lake.BuildJob 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 : Lake.TargetData (`leanLib ++ `static.export) = Lake.BuildJob System.FilePath

theorem Lake.instFamilyDefNameTargetDataHAppendMkStr1MkStr2BuildJobFilePath : Lake.FamilyDef Lake.TargetData (`leanLib ++ `static.export) (Lake.BuildJob System.FilePath)

@[reducible, inline]

abbrev Lake.LeanLib.sharedFacet : Lean.Name

A Lean library's shared artifact.

Equations

• Lake.LeanLib.sharedFacet = `shared

theorem Lake.instFamilyDefNameTargetDataHAppendMkStr1BuildJobFilePath_1 : Lake.FamilyDef Lake.TargetData (`leanLib ++ `shared) (Lake.BuildJob System.FilePath)

@[simp]

axiom Lake.TargetData.leanLib.shared : Lake.TargetData (`leanLib ++ `shared) = Lake.BuildJob 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

theorem Lake.instFamilyDefNameTargetDataHAppendMkStr1BuildJobUnit_1 : Lake.FamilyDef Lake.TargetData (`leanLib ++ `extraDep) (Lake.BuildJob Unit)

@[simp]

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

@[reducible, inline]

abbrev Lake.LeanExe.exeFacet : Lean.Name

A Lean binary executable.

Equations

• Lake.LeanExe.exeFacet = `leanExe

theorem Lake.instFamilyDefNameTargetDataMkStr1BuildJobFilePath : Lake.FamilyDef Lake.TargetData `leanExe (Lake.BuildJob System.FilePath)

@[simp]

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

@[reducible, inline]

abbrev Lake.ExternLib.staticFacet : Lean.Name

A external library's static binary.

theorem Lake.instFamilyDefNameTargetDataMkStr2BuildJobFilePath : Lake.FamilyDef Lake.TargetData `externLib.static (Lake.BuildJob System.FilePath)

@[simp]

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

@[reducible, inline]

abbrev Lake.ExternLib.sharedFacet : Lean.Name

A external library's shared binary.

Equations

• Lake.ExternLib.sharedFacet = `externLib.shared

theorem Lake.instFamilyDefNameTargetDataMkStr2BuildJobFilePath_1 : Lake.FamilyDef Lake.TargetData `externLib.shared (Lake.BuildJob System.FilePath)

@[simp]

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

@[reducible, inline]

abbrev Lake.ExternLib.dynlibFacet : Lean.Name

A external library's dynlib.

Equations

• Lake.ExternLib.dynlibFacet = `externLib.dynlib

theorem Lake.instFamilyDefNameTargetDataMkStr2BuildJobDynlib : Lake.FamilyDef Lake.TargetData `externLib.dynlib (Lake.BuildJob Lake.Dynlib)

@[simp]

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