Build Info

This module defines the Lake build info type and related utilities. Build info is what is the data passed to a Lake build function to facilitate the build.

inductive Lake.BuildInfo : Type

The type of Lake's build info.

• target (package : Package) (target : Lean.Name) : BuildInfo
• facet (target : BuildKey) (kind : Lean.Name) (data : DataType kind) (facet : Lean.Name) : BuildInfo

Build Info & Keys

Build Key Helper Constructors

@[reducible, inline]

abbrev Lake.Module.key (self : Module) : BuildKey

Equations

• self.key = Lake.BuildKey.module self.keyName

@[reducible, inline, deprecated Lake.Module.key (since := "2025-03-28")]

abbrev Lake.Module.buildKey (self : Module) : BuildKey

Equations

• self.buildKey = Lake.BuildKey.module self.keyName

@[reducible, inline, deprecated Lake.BuildKey.facet (since := "2025-03-28")]

abbrev Lake.Module.facetBuildKey (facet : Lean.Name) (self : Module) : BuildKey

Equations

• Lake.Module.facetBuildKey facet self = self.key.facet facet

@[reducible, inline]

abbrev Lake.Package.key (self : Package) : BuildKey

Equations

• self.key = Lake.BuildKey.package self.name

@[reducible, inline, deprecated Lake.Package.key (since := "2025-03-28")]

abbrev Lake.Package.buildKey (self : Package) : BuildKey

Equations

• self.buildKey = Lake.BuildKey.package self.name

@[reducible, inline, deprecated Lake.BuildKey.facet (since := "2025-03-28")]

abbrev Lake.Package.facetBuildKey (facet : Lean.Name) (self : Package) : BuildKey

Equations

• Lake.Package.facetBuildKey facet self = self.key.facet facet

@[reducible, inline]

abbrev Lake.Package.targetKey (target : Lean.Name) (self : Package) : BuildKey

Equations

• Lake.Package.targetKey target self = Lake.BuildKey.packageTarget self.name target

@[reducible, inline, deprecated Lake.Package.targetKey (since := "2025-03-28")]

abbrev Lake.Package.targetBuildKey (target : Lean.Name) (self : Package) : BuildKey

Equations

• Lake.Package.targetBuildKey target self = Lake.BuildKey.packageTarget self.name target

@[reducible, inline]

abbrev Lake.ConfigTarget.key {kind : Lean.Name} (self : ConfigTarget kind) : BuildKey

Equations

• self.key = Lake.BuildKey.packageTarget self.pkg.name self.name

@[reducible, inline, deprecated Lake.ConfigTarget.key (since := "2025-03-28")]

abbrev Lake.ConfigTarget.buildKey {kind : Lean.Name} (self : ConfigTarget kind) : BuildKey

Equations

• self.buildKey = Lake.BuildKey.packageTarget self.pkg.name self.name

@[reducible, inline, deprecated Lake.BuildKey.facet (since := "2025-03-28")]

abbrev Lake.ConfigTarget.facetBuildKey {kind : Lean.Name} (self : ConfigTarget kind) (facet : Lean.Name) : BuildKey

Equations

• self.facetBuildKey facet = self.key.facet facet

@[reducible, inline]

abbrev Lake.LeanExe.exeBuildKey (self : LeanExe) : BuildKey

Equations

• self.exeBuildKey = (Lake.ConfigTarget.key self).facet Lake.LeanExe.exeFacet

@[reducible, inline]

abbrev Lake.ExternLib.staticBuildKey (self : ExternLib) : BuildKey

Equations

• self.staticBuildKey = (Lake.ConfigTarget.key self).facet Lake.ExternLib.staticFacet

@[reducible, inline]

abbrev Lake.ExternLib.sharedBuildKey (self : ExternLib) : BuildKey

Equations

• self.sharedBuildKey = (Lake.ConfigTarget.key self).facet Lake.ExternLib.sharedFacet

@[reducible, inline]

abbrev Lake.ExternLib.dynlibBuildKey (self : ExternLib) : BuildKey

Equations

• self.dynlibBuildKey = (Lake.ConfigTarget.key self).facet Lake.ExternLib.dynlibFacet

Build Info to Key

@[reducible]

def Lake.BuildInfo.key (self : BuildInfo) : BuildKey

The key that identifies the build in the Lake build store.

Equations

• (Lake.BuildInfo.target p t).key = Lake.Package.targetKey t p
• (Lake.BuildInfo.facet t kind data f).key = t.facet f

instance Lake.instToStringBuildInfo : ToString BuildInfo

Equations

• Lake.instToStringBuildInfo = { toString := fun (x : Lake.BuildInfo) => toString x.key }

Instances for deducing data types of BuildInfo keys

@[instance 100]

instance Lake.instFamilyDefBuildKeyBuildDataCustomTargetNameCustomData {n t : Lean.Name} {p : NPackage n} : FamilyDef BuildData (BuildKey.customTarget p.name t) (CustomData n t)

instance Lake.instFamilyDefBuildKeyBuildDataKeyTargetOfFamilyOutNameCustomData {n t : Lean.Name} {α : Type} {p : NPackage n} [FamilyOut (CustomData n) t α] : FamilyDef BuildData (BuildInfo.target p.toPackage t).key α

instance Lake.instFamilyDefBuildKeyBuildDataKeyTargetOfFamilyOutPackageTarget {n t : Lean.Name} {α : Type} {p : NPackage n} [FamilyOut BuildData (BuildKey.packageTarget n t) α] : FamilyDef BuildData (BuildInfo.target p.toPackage t).key α

instance Lake.instFamilyDefBuildKeyBuildDataKeyFacetOfFamilyOutNameFacetOut {f : Lean.Name} {α : Type} {t : BuildKey} {k : Lean.Name} {d : DataType k} [FamilyOut FacetOut f α] : FamilyDef BuildData (BuildInfo.facet t k d f).key α

Build Info & Facets

Complex Builtin Facet Declarations

Additional builtin facets missing from Build.Facets. These are defined here because they need configuration definitions (e.g., Module), whereas the facets there are needed by the configuration definitions.

@[simp]

axiom Lake.DataType.module : DataType `module = Module

instance Lake.instDataKindModule : DataKind Module

Equations

• Lake.instDataKindModule = { name := `module, wf := Lake.instDataKindModule._proof_1 }

instance Lake.instFamilyDefNameDataTypeMkStr1Module : FamilyDef DataType `module Module

instance Lake.instDataKindPackage : DataKind Package

Equations

• Lake.instDataKindPackage = { name := `package, wf := Lake.instDataKindPackage._proof_1 }

@[simp]

axiom Lake.DataType.package : DataType `package = Package

instance Lake.instFamilyDefNameDataTypeMkStr1Package : FamilyDef DataType `package Package

instance Lake.instDataKindLeanLib : DataKind LeanLib

Equations

• Lake.instDataKindLeanLib = { name := `lean_lib, wf := Lake.instDataKindLeanLib._proof_1 }

instance Lake.instFamilyDefNameDataTypeMkStr1LeanLib : FamilyDef DataType `lean_lib LeanLib

@[simp]

axiom Lake.DataType.lean_lib : DataType `lean_lib = LeanLib

@[simp]

axiom Lake.DataType.lean_exe : DataType `lean_exe = LeanExe

instance Lake.instFamilyDefNameDataTypeMkStr1LeanExe : FamilyDef DataType `lean_exe LeanExe

instance Lake.instDataKindLeanExe : DataKind LeanExe

Equations

• Lake.instDataKindLeanExe = { name := `lean_exe, wf := Lake.instDataKindLeanExe._proof_1 }

instance Lake.instFamilyDefNameDataTypeMkStr1ExternLib : FamilyDef DataType `extern_lib ExternLib

@[simp]

axiom Lake.DataType.extern_lib : DataType `extern_lib = ExternLib

instance Lake.instDataKindExternLib : DataKind ExternLib

Equations

• Lake.instDataKindExternLib = { name := `extern_lib, wf := Lake.instDataKindExternLib._proof_1 }

instance Lake.instFamilyDefNameDataTypeMkStr1InputFile : FamilyDef DataType `input_file InputFile

@[simp]

axiom Lake.DataType.input_file : DataType `input_file = InputFile

instance Lake.instDataKindInputFile : DataKind InputFile

Equations

• Lake.instDataKindInputFile = { name := `input_file, wf := Lake.instDataKindInputFile._proof_1 }

instance Lake.instFamilyDefNameDataTypeMkStr1InputDir : FamilyDef DataType `input_dir InputDir

@[simp]

axiom Lake.DataType.input_dir : DataType `input_dir = InputDir

instance Lake.instDataKindInputDir : DataKind InputDir

Equations

• Lake.instDataKindInputDir = { name := `input_dir, wf := Lake.instDataKindInputDir._proof_1 }

structure Lake.ModuleImportextends Lean.Import : Type

An import statement with its resolved module within the workspace.

• module : Name
• importAll : Bool
• isExported : Bool
• isMeta : Bool
• module? : Option Module

structure Lake.ModuleInput : Type

A module's source file path plus its parsed header.

• path : System.FilePath
• header : Lean.ModuleHeader
• imports : Array ModuleImport

@[simp]

axiom Lake.FacetOut.module.input : FacetOut `module.input = ModuleInput

instance Lake.instFamilyDefNameFacetOutMkStr2ModuleInput : FamilyDef FacetOut `module.input ModuleInput

@[reducible]

def Lake.Module.inputFacet : Lean.Name

The module's processed Lean source file. Combines tracing the file with parsing its header.

Equations

• Lake.Module.inputFacet = `module.input

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ModuleInput : FamilyDef FacetOut (`module ++ `input) ModuleInput

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ArrayModule : FamilyDef FacetOut (`module ++ `imports) (Array Module)

@[simp]

axiom Lake.FacetOut.module.imports : FacetOut `module.imports = Array Module

instance Lake.instFamilyDefNameFacetOutMkStr2ArrayModule : FamilyDef FacetOut `module.imports (Array Module)

@[reducible]

def Lake.Module.importsFacet : Lean.Name

The direct local imports of the Lean module.

Equations

• Lake.Module.importsFacet = `module.imports

@[reducible]

def Lake.Module.transImportsFacet : Lean.Name

The transitive local imports of the Lean module.

Equations

• Lake.Module.transImportsFacet = `module.transImports

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ArrayModule_1 : FamilyDef FacetOut (`module ++ `transImports) (Array Module)

@[simp]

axiom Lake.FacetOut.module.transImports : FacetOut `module.transImports = Array Module

instance Lake.instFamilyDefNameFacetOutMkStr2ArrayModule_1 : FamilyDef FacetOut `module.transImports (Array Module)

instance Lake.instFamilyDefNameFacetOutMkStr2ArrayModule_2 : FamilyDef FacetOut `module.precompileImports (Array Module)

@[reducible]

def Lake.Module.precompileImportsFacet : Lean.Name

The transitive local imports of the Lean module.

Equations

• Lake.Module.precompileImportsFacet = `module.precompileImports

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ArrayModule_2 : FamilyDef FacetOut (`module ++ `precompileImports) (Array Module)

@[simp]

axiom Lake.FacetOut.module.precompileImports : FacetOut `module.precompileImports = Array Module

@[simp]

axiom Lake.FacetOut.module.dynlib : FacetOut `module.dynlib = Dynlib

instance Lake.instFamilyDefNameFacetOutMkStr2Dynlib_2 : FamilyDef FacetOut `module.dynlib Dynlib

@[reducible]

def Lake.Module.dynlibFacet : Lean.Name

Shared library for --load-dynlib.

Equations

• Lake.Module.dynlibFacet = `module.dynlib

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Dynlib_2 : FamilyDef FacetOut (`module ++ `dynlib) Dynlib

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ArrayModule_3 : FamilyDef FacetOut (`lean_lib ++ `modules) (Array Module)

@[reducible]

def Lake.LeanLib.modulesFacet : Lean.Name

A Lean library's Lean modules.

Equations

• Lake.LeanLib.modulesFacet = `lean_lib.modules

@[simp]

axiom Lake.FacetOut.lean_lib.modules : FacetOut `lean_lib.modules = Array Module

instance Lake.instFamilyDefNameFacetOutMkStr2ArrayModule_3 : FamilyDef FacetOut `lean_lib.modules (Array Module)

@[simp]

axiom Lake.FacetOut.package.deps : FacetOut `package.deps = Array Package

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ArrayPackage : FamilyDef FacetOut (`package ++ `deps) (Array Package)

instance Lake.instFamilyDefNameFacetOutMkStr2ArrayPackage : FamilyDef FacetOut `package.deps (Array Package)

@[reducible]

def Lake.Package.depsFacet : Lean.Name

The package's array of dependencies.

Equations

• Lake.Package.depsFacet = `package.deps

@[reducible]

def Lake.Package.transDepsFacet : Lean.Name

The package's complete array of transitive dependencies.

Equations

• Lake.Package.transDepsFacet = `package.transDeps

instance Lake.instFamilyDefNameFacetOutMkStr2ArrayPackage_1 : FamilyDef FacetOut `package.transDeps (Array Package)

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ArrayPackage_1 : FamilyDef FacetOut (`package ++ `transDeps) (Array Package)

@[simp]

axiom Lake.FacetOut.package.transDeps : FacetOut `package.transDeps = Array Package

Facet Build Info Helper Constructors

Definitions to easily construct BuildInfo values for module, package, and target facets.

Module Infos

@[reducible, inline]

abbrev Lake.Module.facetCore (facet : Lean.Name) (self : Module) : BuildInfo

Build info for applying the specified facet to the module. It is the user's obiligation to ensure the facet in question is a module facet.

Equations

• Lake.Module.facetCore facet self = Lake.BuildInfo.facet self.key Lake.Module.facetKind (Lake.toFamily self) facet

@[reducible, inline]

abbrev Lake.Module.facet (facet : Lean.Name) (self : Module) : BuildInfo

Build info for a module facet.

Equations

• Lake.Module.facet facet self = Lake.Module.facetCore (Lake.Module.facetKind ++ facet) self

@[reducible, inline, deprecated Lake.Module.facetCore (since := "2025-03-04")]

abbrev Lake.BuildInfo.moduleFacet (module : Module) (facet : Lean.Name) : BuildInfo

Equations

• Lake.BuildInfo.moduleFacet module facet = Lake.Module.facetCore facet module

@[reducible, inline]

abbrev Lake.Module.input (self : Module) : BuildInfo

The module's processed Lean source file. Combines tracing the file with parsing its header.

Equations

• self.input = Lake.Module.facetCore Lake.Module.inputFacet self

@[reducible, inline]

abbrev Lake.Module.lean (self : Module) : BuildInfo

The module's Lean source file.

Equations

• self.lean = Lake.Module.facetCore Lake.Module.leanFacet self

@[reducible, inline]

abbrev Lake.Module.header (self : Module) : BuildInfo

The parsed module header of the module's source file.

Equations

• self.header = Lake.Module.facetCore Lake.Module.headerFacet self

@[reducible, inline]

abbrev Lake.Module.imports (self : Module) : BuildInfo

The direct local imports of the Lean module.

Equations

• self.imports = Lake.Module.facetCore Lake.Module.importsFacet self

@[reducible, inline]

abbrev Lake.Module.transImports (self : Module) : BuildInfo

The transitive local imports of the Lean module.

Equations

• self.transImports = Lake.Module.facetCore Lake.Module.transImportsFacet self

@[reducible, inline]

abbrev Lake.Module.precompileImports (self : Module) : BuildInfo

The transitive local imports of the Lean module.

Equations

• self.precompileImports = Lake.Module.facetCore Lake.Module.precompileImportsFacet self

@[reducible, inline]

abbrev Lake.Module.setup (self : Module) : BuildInfo

The computed configuration of a module for Lean.

In the process, this facet will build all of a module's dependencies, including transitive imports, plugins, and those specified by needs.

Equations

• self.setup = Lake.Module.facetCore Lake.Module.setupFacet self

@[reducible, inline]

abbrev Lake.Module.deps (self : Module) : BuildInfo

This facet builds all of a module's dependencies, including transitive imports, plugins, and those specified by needs.

Equations

• self.deps = Lake.Module.facetCore Lake.Module.depsFacet self

@[reducible, inline]

abbrev Lake.Module.importInfo (self : Module) : BuildInfo

For internal use only. Information about the imports of this module.

Equations

• self.importInfo = Lake.Module.facetCore Lake.Module.importInfoFacet self

@[reducible, inline]

abbrev Lake.Module.exportInfo (self : Module) : BuildInfo

For internal use only. Information useful to importers of this module.

Equations

• self.exportInfo = Lake.Module.facetCore Lake.Module.exportInfoFacet self

@[reducible, inline]

abbrev Lake.Module.importArts (self : Module) : BuildInfo

Artifacts directly needed for an import of this module with the module system enabled.

Equations

• self.importArts = Lake.Module.facetCore Lake.Module.importArtsFacet self

@[reducible, inline]

abbrev Lake.Module.importAllArts (self : Module) : BuildInfo

Artifacts directly needed for an import of this module from a module without the module system enabled or import all of this module from a module with it enabled.

Equations

• self.importAllArts = Lake.Module.facetCore Lake.Module.importAllArtsFacet self

@[reducible, inline]

abbrev Lake.Module.leanArts (self : Module) : BuildInfo

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

Equations

• self.leanArts = Lake.Module.facetCore Lake.Module.leanArtsFacet self

@[reducible, inline]

abbrev Lake.Module.olean (self : Module) : BuildInfo

The olean file produced by lean.

Equations

• self.olean = Lake.Module.facetCore Lake.Module.oleanFacet self

@[reducible, inline]

abbrev Lake.Module.oleanServer (self : Module) : BuildInfo

The olean.server file produced by lean (with the module system enabled).

Equations

• self.oleanServer = Lake.Module.facetCore Lake.Module.oleanServerFacet self

@[reducible, inline]

abbrev Lake.Module.oleanPrivate (self : Module) : BuildInfo

The olean.private file produced by lean (with the module system enabled).

Equations

• self.oleanPrivate = Lake.Module.facetCore Lake.Module.oleanPrivateFacet self

@[reducible, inline]

abbrev Lake.Module.ilean (self : Module) : BuildInfo

The ilean file produced by lean.

Equations

• self.ilean = Lake.Module.facetCore Lake.Module.ileanFacet self

@[reducible, inline]

abbrev Lake.Module.ir (self : Module) : BuildInfo

The ir file produced by lean (with the module system enabled).

Equations

• self.ir = Lake.Module.facetCore Lake.Module.irFacet self

@[reducible, inline]

abbrev Lake.Module.c (self : Module) : BuildInfo

The C file produced by lean.

Equations

• self.c = Lake.Module.facetCore Lake.Module.cFacet self

@[reducible, inline]

abbrev Lake.Module.bc (self : Module) : BuildInfo

The C file produced by lean.

Equations

• self.bc = Lake.Module.facetCore Lake.Module.bcFacet self

@[reducible, inline]

abbrev Lake.Module.o (self : Module) : BuildInfo

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

• self.o = Lake.Module.facetCore Lake.Module.oFacet self

@[reducible, inline]

abbrev Lake.Module.oExport (self : Module) : BuildInfo

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

Equations

• self.oExport = Lake.Module.facetCore Lake.Module.oExportFacet self

@[reducible, inline]

abbrev Lake.Module.oNoExport (self : Module) : BuildInfo

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

Equations

• self.oNoExport = Lake.Module.facetCore Lake.Module.oNoExportFacet self

@[reducible, inline]

abbrev Lake.Module.co (self : Module) : BuildInfo

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

Equations

• self.co = Lake.Module.facetCore Lake.Module.coFacet self

@[reducible, inline]

abbrev Lake.Module.coExport (self : Module) : BuildInfo

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

Equations

• self.coExport = Lake.Module.facetCore Lake.Module.coExportFacet self

@[reducible, inline]

abbrev Lake.Module.coNoExport (self : Module) : BuildInfo

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

Equations

• self.coNoExport = Lake.Module.facetCore Lake.Module.coNoExportFacet self

@[reducible, inline]

abbrev Lake.Module.bco (self : Module) : BuildInfo

The object file .bc.o built from bc.

Equations

• self.bco = Lake.Module.facetCore Lake.Module.bcoFacet self

@[reducible, inline]

abbrev Lake.Module.dynlib (self : Module) : BuildInfo

Shared library for --load-dynlib.

Equations

• self.dynlib = Lake.Module.facetCore Lake.Module.dynlibFacet self

Package Infos

@[reducible, inline]

abbrev Lake.Package.target (target : Lean.Name) (self : Package) : BuildInfo

Build info for a package target (e.g., a library, executable, or custom target).

Equations

• Lake.Package.target target self = Lake.BuildInfo.target self target

@[reducible, inline]

abbrev Lake.Package.facetCore (facet : Lean.Name) (self : Package) : BuildInfo

Equations

• Lake.Package.facetCore facet self = Lake.BuildInfo.facet self.key Lake.Package.facetKind (Lake.toFamily self) facet

@[reducible, inline]

abbrev Lake.Package.facet (facet : Lean.Name) (self : Package) : BuildInfo

Build info for a package facet.

Equations

• Lake.Package.facet facet self = Lake.Package.facetCore (Lake.Package.facetKind ++ facet) self

@[reducible, inline, deprecated Lake.Package.facetCore (since := "2025-03-04")]

abbrev Lake.BuildInfo.packageFacet (package : Package) (facet : Lean.Name) : BuildInfo

Equations

• Lake.BuildInfo.packageFacet package facet = Lake.Package.facetCore facet package

@[reducible, inline]

abbrev Lake.Package.buildCache (self : Package) : BuildInfo

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

• self.buildCache = Lake.Package.facetCore Lake.Package.buildCacheFacet self

@[reducible, inline]

abbrev Lake.Package.optBuildCache (self : Package) : BuildInfo

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

• self.optBuildCache = Lake.Package.facetCore Lake.Package.optBuildCacheFacet self

@[reducible, inline]

abbrev Lake.Package.reservoirBarrel (self : Package) : BuildInfo

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

Equations

• self.reservoirBarrel = Lake.Package.facetCore Lake.Package.reservoirBarrelFacet self

@[reducible, inline]

abbrev Lake.Package.optReservoirBarrel (self : Package) : BuildInfo

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

Equations

• self.optReservoirBarrel = Lake.Package.facetCore Lake.Package.optReservoirBarrelFacet self

@[reducible, inline]

abbrev Lake.Package.gitHubRelease (self : Package) : BuildInfo

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

Equations

• self.gitHubRelease = Lake.Package.facetCore Lake.Package.gitHubReleaseFacet self

@[reducible, inline]

abbrev Lake.Package.optGitHubRelease (self : Package) : BuildInfo

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

• self.optGitHubRelease = Lake.Package.facetCore Lake.Package.optGitHubReleaseFacet self

@[reducible, inline]

abbrev Lake.Package.extraDep (self : Package) : BuildInfo

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

Equations

• self.extraDep = Lake.Package.facetCore Lake.Package.extraDepFacet self

@[reducible, inline]

abbrev Lake.Package.deps (self : Package) : BuildInfo

The package's array of dependencies.

Equations

• self.deps = Lake.Package.facetCore Lake.Package.depsFacet self

@[reducible, inline]

abbrev Lake.Package.transDeps (self : Package) : BuildInfo

The package's complete array of transitive dependencies.

Equations

• self.transDeps = Lake.Package.facetCore Lake.Package.transDepsFacet self

Lean Library Infos

@[reducible, inline]

abbrev Lake.LeanLib.facetCore (facet : Lean.Name) (self : LeanLib) : BuildInfo

Equations

• Lake.LeanLib.facetCore facet self = Lake.BuildInfo.facet (Lake.ConfigTarget.key self) Lake.LeanLib.facetKind (Lake.toFamily self) facet

@[reducible, inline]

abbrev Lake.LeanLib.facet (facet : Lean.Name) (self : LeanLib) : BuildInfo

Build info for a facet of a Lean library.

Equations

• Lake.LeanLib.facet facet self = Lake.LeanLib.facetCore (Lake.LeanLib.facetKind ++ facet) self

@[reducible, inline, deprecated Lake.LeanLib.facetCore (since := "2025-03-04")]

abbrev Lake.BuildInfo.libraryFacet (lib : LeanLib) (facet : Lean.Name) : BuildInfo

Equations

• Lake.BuildInfo.libraryFacet lib facet = Lake.LeanLib.facetCore facet lib

@[reducible, inline]

abbrev Lake.LeanLib.modules (self : LeanLib) : BuildInfo

A Lean library's Lean modules.

Equations

• self.modules = Lake.LeanLib.facetCore Lake.LeanLib.modulesFacet self

@[reducible, inline]

abbrev Lake.LeanLib.leanArts (self : LeanLib) : BuildInfo

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

Equations

• self.leanArts = Lake.LeanLib.facetCore Lake.LeanLib.leanArtsFacet self

@[reducible, inline]

abbrev Lake.LeanLib.static (self : LeanLib) : BuildInfo

A Lean library's static artifact.

Equations

• self.static = Lake.LeanLib.facetCore Lake.LeanLib.staticFacet self

@[reducible, inline]

abbrev Lake.LeanLib.staticExport (self : LeanLib) : BuildInfo

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

Static libraries with explicit exports are built as thin libraries. Such libraries are usually used as part of the local build process of some shared artifact and not publicly distributed. Standard static libraries are much better for distribution.

Equations

• self.staticExport = Lake.LeanLib.facetCore Lake.LeanLib.staticExportFacet self

@[reducible, inline]

abbrev Lake.LeanLib.shared (self : LeanLib) : BuildInfo

A Lean library's shared artifact.

Equations

• self.shared = Lake.LeanLib.facetCore Lake.LeanLib.sharedFacet self

@[reducible, inline]

abbrev Lake.LeanLib.extraDep (self : LeanLib) : BuildInfo

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

Equations

• self.extraDep = Lake.LeanLib.facetCore Lake.LeanLib.extraDepFacet self

Lean Executable Infos

@[reducible, inline]

abbrev Lake.LeanExe.facetCore (facet : Lean.Name) (self : LeanExe) : BuildInfo

Equations

• Lake.LeanExe.facetCore facet self = Lake.BuildInfo.facet (Lake.ConfigTarget.key self) Lake.LeanExe.facetKind (Lake.toFamily self) facet

@[reducible, inline]

abbrev Lake.LeanExe.exe (self : LeanExe) : BuildInfo

Build info of the Lean executable.

Equations

• self.exe = Lake.LeanExe.facetCore Lake.LeanExe.exeFacet self

@[reducible, inline, deprecated Lake.LeanExe.exe (since := "2025-03-04")]

abbrev Lake.BuildInfo.leanExe (exe : LeanExe) : BuildInfo

Equations

• Lake.BuildInfo.leanExe exe = exe.exe

External Library Infos

@[reducible, inline]

abbrev Lake.ExternLib.facetCore (facet : Lean.Name) (self : ExternLib) : BuildInfo

Equations

• Lake.ExternLib.facetCore facet self = Lake.BuildInfo.facet (Lake.ConfigTarget.key self) Lake.ExternLib.facetKind (Lake.toFamily self) facet

@[reducible, inline]

abbrev Lake.ExternLib.static (self : ExternLib) : BuildInfo

Build info of the external library's static binary.

Equations

• self.static = Lake.ExternLib.facetCore Lake.ExternLib.staticFacet self

@[reducible, inline, deprecated Lake.ExternLib.static (since := "2025-03-04")]

abbrev Lake.BuildInfo.staticExternLib (lib : ExternLib) : BuildInfo

Equations

• Lake.BuildInfo.staticExternLib lib = Lake.ExternLib.facetCore Lake.ExternLib.staticFacet lib

@[reducible, inline]

abbrev Lake.ExternLib.shared (self : ExternLib) : BuildInfo

Build info of the external library's shared binary.

Equations

• self.shared = Lake.ExternLib.facetCore Lake.ExternLib.sharedFacet self

@[reducible, inline, deprecated Lake.ExternLib.shared (since := "2025-03-04")]

abbrev Lake.BuildInfo.sharedExternLib (lib : ExternLib) : BuildInfo

Equations

• Lake.BuildInfo.sharedExternLib lib = Lake.ExternLib.facetCore Lake.ExternLib.sharedFacet lib

@[reducible, inline]

abbrev Lake.ExternLib.dynlib (self : ExternLib) : BuildInfo

Build info of the external library's dynlib.

Equations

• self.dynlib = Lake.ExternLib.facetCore Lake.ExternLib.dynlibFacet self

@[reducible, inline, deprecated Lake.ExternLib.dynlib (since := "2025-03-04")]

abbrev Lake.BuildInfo.dynlibExternLib (lib : ExternLib) : BuildInfo

Equations

• Lake.BuildInfo.dynlibExternLib lib = Lake.ExternLib.facetCore Lake.ExternLib.dynlibFacet lib

Input File & Directory Infos

@[reducible, inline]

abbrev Lake.InputFile.facetCore (facet : Lean.Name) (self : InputFile) : BuildInfo

Equations

• Lake.InputFile.facetCore facet self = Lake.BuildInfo.facet (Lake.ConfigTarget.key self) Lake.InputFile.facetKind (Lake.toFamily self) facet

@[reducible, inline]

abbrev Lake.InputFile.default (self : InputFile) : BuildInfo

Build info of the input file's default facet.

Equations

• self.default = Lake.InputFile.facetCore Lake.InputFile.defaultFacet self

@[reducible, inline]

abbrev Lake.InputDir.facetCore (facet : Lean.Name) (self : InputDir) : BuildInfo

Equations

• Lake.InputDir.facetCore facet self = Lake.BuildInfo.facet (Lake.ConfigTarget.key self) Lake.InputDir.facetKind (Lake.toFamily self) facet

@[reducible, inline]

abbrev Lake.InputDir.default (self : InputDir) : BuildInfo

Build info of the input directory's default facet.

Equations

• self.default = Lake.InputDir.facetCore Lake.InputDir.defaultFacet self