# Build Keys, Infos, & Facets #

This module defines the shorthand definitions for build keys, infos, and facets on the various target types.

### Build Key Helper Constructors #

source
@[reducible, inline]
abbrev Lake.Module.key (self : Module) :
BuildKey
Equations

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

Instances For

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

Instances For

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

Instances For

source
@[reducible, inline]
abbrev Lake.ConfigTarget.key {kind : Lean.Name} (self : ConfigTarget kind) :
BuildKey
Equations

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

Instances For

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

Instances For

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

Instances For

source
@[reducible, inline]
abbrev Lake.LeanExe.exeBuildKey (self : LeanExe) :
BuildKey
Equations

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

Instances For

source
@[reducible, inline]
abbrev Lake.ExternLib.staticBuildKey (self : ExternLib) :
BuildKey
Equations

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

Instances For

source
@[reducible, inline]
abbrev Lake.ExternLib.sharedBuildKey (self : ExternLib) :
BuildKey
Equations

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

Instances For

source
@[reducible, inline]
abbrev Lake.ExternLib.dynlibBuildKey (self : ExternLib) :
BuildKey
Equations

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

Instances For

### 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.

source
instance Lake.instDataKindModule :
DataKind Module
Equations

- Lake.instDataKindModule = { name := `module, wf := Lake.instDataKindModule._proof_2 }

source
instance Lake.instFamilyDefNameDataTypeMkStr1Module :
FamilyDef DataType `module Module
source
@[simp]
axiom Lake.DataType.module :
DataType `module = Module
source
instance Lake.instDataKindPackage :
DataKind Package
Equations

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

source
instance Lake.instFamilyDefNameDataTypeMkStr1Package :
FamilyDef DataType `package Package
source
@[simp]
axiom Lake.DataType.package :
DataType `package = Package
source
instance Lake.instFamilyDefNameDataTypeMkStr1LeanLib :
FamilyDef DataType `lean_lib LeanLib
source
instance Lake.instDataKindLeanLib :
DataKind LeanLib
Equations

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

source
@[simp]
axiom Lake.DataType.lean_lib :
DataType `lean_lib = LeanLib
source
instance Lake.instDataKindLeanExe :
DataKind LeanExe
Equations

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

source
instance Lake.instFamilyDefNameDataTypeMkStr1LeanExe :
FamilyDef DataType `lean_exe LeanExe
source
@[simp]
axiom Lake.DataType.lean_exe :
DataType `lean_exe = LeanExe
source
instance Lake.instDataKindExternLib :
DataKind ExternLib
Equations

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

source
instance Lake.instFamilyDefNameDataTypeMkStr1ExternLib :
FamilyDef DataType `extern_lib ExternLib
source
@[simp]
axiom Lake.DataType.extern_lib :
DataType `extern_lib = ExternLib
source
instance Lake.instFamilyDefNameDataTypeMkStr1InputFile :
FamilyDef DataType `input_file InputFile
source
instance Lake.instDataKindInputFile :
DataKind InputFile
Equations

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

source
@[simp]
axiom Lake.DataType.input_file :
DataType `input_file = InputFile
source
instance Lake.instFamilyDefNameDataTypeMkStr1InputDir :
FamilyDef DataType `input_dir InputDir
source
instance Lake.instDataKindInputDir :
DataKind InputDir
Equations

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

source
@[simp]
axiom Lake.DataType.input_dir :
DataType `input_dir = InputDir
source
structure Lake.ModuleImport extends Lean.Import :
Type

An import statement with its resolved module within the workspace.

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

Instances For

source
structure Lake.ModuleInput :
Type

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

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

Instances For

source
instance Lake.instFamilyDefNameFacetOutMkStr2ModuleInput :
FamilyDef FacetOut `module.input ModuleInput
source
instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ModuleInput :
FamilyDef FacetOut (`module ++ `input) ModuleInput
source
@[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

Instances For

source
@[simp]
axiom Lake.FacetOut.module.input :
FacetOut `module.input = ModuleInput
source
@[simp]
axiom Lake.FacetOut.module.imports :
FacetOut `module.imports = Array Module
source
instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ArrayModule :
FamilyDef FacetOut (`module ++ `imports) (Array Module)
source
instance Lake.instFamilyDefNameFacetOutMkStr2ArrayModule :
FamilyDef FacetOut `module.imports (Array Module)
source
@[reducible]
def Lake.Module.importsFacet :
Lean.Name

The direct local imports of the Lean module.

Equations

- Lake.Module.importsFacet = `module.imports

Instances For

source
instance Lake.instFamilyDefNameFacetOutMkStr2ArrayModule_1 :
FamilyDef FacetOut `module.transImports (Array Module)
source
@[simp]
axiom Lake.FacetOut.module.transImports :
FacetOut `module.transImports = Array Module
source
@[reducible]
def Lake.Module.transImportsFacet :
Lean.Name

The transitive local imports of the Lean module.

Equations

- Lake.Module.transImportsFacet = `module.transImports

Instances For

source
instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ArrayModule_1 :
FamilyDef FacetOut (`module ++ `transImports) (Array Module)
source
instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ArrayModule_2 :
FamilyDef FacetOut (`module ++ `precompileImports) (Array Module)
source
instance Lake.instFamilyDefNameFacetOutMkStr2ArrayModule_2 :
FamilyDef FacetOut `module.precompileImports (Array Module)
source
@[simp]
axiom Lake.FacetOut.module.precompileImports :
FacetOut `module.precompileImports = Array Module
source
@[reducible]
def Lake.Module.precompileImportsFacet :
Lean.Name

The transitive local imports of the Lean module.

Equations

- Lake.Module.precompileImportsFacet = `module.precompileImports

Instances For

source
instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Dynlib_2 :
FamilyDef FacetOut (`module ++ `dynlib) Dynlib
source
@[reducible]
def Lake.Module.dynlibFacet :
Lean.Name

Shared library for `--load-dynlib`.

Equations

- Lake.Module.dynlibFacet = `module.dynlib

Instances For

source
@[simp]
axiom Lake.FacetOut.module.dynlib :
FacetOut `module.dynlib = Dynlib
source
instance Lake.instFamilyDefNameFacetOutMkStr2Dynlib_2 :
FamilyDef FacetOut `module.dynlib Dynlib
source
@[simp]
axiom Lake.FacetOut.lean_lib.modules :
FacetOut `lean_lib.modules = Array Module
source
instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ArrayModule_3 :
FamilyDef FacetOut (`lean_lib ++ `modules) (Array Module)
source
@[reducible]
def Lake.LeanLib.modulesFacet :
Lean.Name

A Lean library's Lean modules.

Equations

- Lake.LeanLib.modulesFacet = `lean_lib.modules

Instances For

source
instance Lake.instFamilyDefNameFacetOutMkStr2ArrayModule_3 :
FamilyDef FacetOut `lean_lib.modules (Array Module)
source
@[reducible]
def Lake.Package.depsFacet :
Lean.Name

The package's array of dependencies.

Equations

- Lake.Package.depsFacet = `package.deps

Instances For

source
@[simp]
axiom Lake.FacetOut.package.deps :
FacetOut `package.deps = Array Package
source
instance Lake.instFamilyDefNameFacetOutMkStr2ArrayPackage :
FamilyDef FacetOut `package.deps (Array Package)
source
instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ArrayPackage :
FamilyDef FacetOut (`package ++ `deps) (Array Package)
source
@[simp]
axiom Lake.FacetOut.package.transDeps :
FacetOut `package.transDeps = Array Package
source
instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ArrayPackage_1 :
FamilyDef FacetOut (`package ++ `transDeps) (Array Package)
source
instance Lake.instFamilyDefNameFacetOutMkStr2ArrayPackage_1 :
FamilyDef FacetOut `package.transDeps (Array Package)
source
@[reducible]
def Lake.Package.transDepsFacet :
Lean.Name

The package's complete array of transitive dependencies.

Equations

- Lake.Package.transDepsFacet = `package.transDeps

Instances For

### Facet Build Info Helper Constructors #

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

#### Module Infos #

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
@[reducible, inline]
abbrev Lake.Module.dynlib (self : Module) :
BuildInfo

Shared library for `--load-dynlib`.

Equations

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

Instances For

#### Package Infos #

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

#### Lean Library Infos #

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

#### Lean Executable Infos #

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

Instances For

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

Instances For

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

- Lake.BuildInfo.leanExe exe = exe.exe

Instances For

#### External Library Infos #

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

#### Input File & Directory Infos #

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

Instances For

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

Instances For

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

Instances For

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

Instances For