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

@[reducible, inline]

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

@[reducible, inline]

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

@[reducible, inline]

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

@[reducible, inline]

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

@[reducible, inline]

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

@[reducible, inline]

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

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.

@[implicit_reducible]

instance Lake.instDataKindModule : DataKind Module

instance Lake.instFamilyDefNameDataTypeMkStr1Module : FamilyDef DataType `module Module

@[simp]

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

@[implicit_reducible]

instance Lake.instDataKindPackage : DataKind Package

instance Lake.instFamilyDefNameDataTypeMkStr1Package : FamilyDef DataType `package Package

@[simp]

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

@[simp]

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

instance Lake.instFamilyDefNameDataTypeMkStr1LeanLib : FamilyDef DataType `lean_lib LeanLib

@[implicit_reducible]

instance Lake.instDataKindLeanLib : DataKind LeanLib

@[simp]

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

instance Lake.instFamilyDefNameDataTypeMkStr1LeanExe : FamilyDef DataType `lean_exe LeanExe

@[implicit_reducible]

instance Lake.instDataKindLeanExe : DataKind LeanExe

@[implicit_reducible]

instance Lake.instDataKindExternLib : DataKind ExternLib

instance Lake.instFamilyDefNameDataTypeMkStr1ExternLib : FamilyDef DataType `extern_lib ExternLib

@[simp]

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

instance Lake.instFamilyDefNameDataTypeMkStr1InputFile : FamilyDef DataType `input_file InputFile

@[implicit_reducible]

instance Lake.instDataKindInputFile : DataKind InputFile

@[simp]

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

@[implicit_reducible]

instance Lake.instDataKindInputDir : DataKind InputDir

instance Lake.instFamilyDefNameDataTypeMkStr1InputDir : FamilyDef DataType `input_dir InputDir

@[simp]

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

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
• trace : BuildTrace
• header : Lean.ModuleHeader
• imports : Array ModuleImport

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

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

@[simp]

axiom Lake.FacetOut.module.input : 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.

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

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

@[simp]

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

@[reducible]

def Lake.Module.importsFacet : Lean.Name

The direct local imports of the Lean module.

@[reducible]

def Lake.Module.transImportsFacet : Lean.Name

The transitive local imports of the Lean module.

@[simp]

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

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

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

@[simp]

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

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

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

@[reducible]

def Lake.Module.precompileImportsFacet : Lean.Name

The transitive local imports of the Lean module.

@[simp]

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

@[reducible]

def Lake.Module.dynlibFacet : Lean.Name

Shared library for --load-dynlib.

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

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

@[simp]

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

@[reducible]

def Lake.LeanLib.modulesFacet : Lean.Name

A Lean library's Lean modules.

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

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

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

@[reducible]

def Lake.Package.depsFacet : Lean.Name

The package's array of dependencies.

@[simp]

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

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

@[simp]

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

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

@[reducible]

def Lake.Package.transDepsFacet : Lean.Name

The package's complete array of transitive dependencies.

instance Lake.instFamilyDefNameFacetOutMkStr2ArrayPackage_1 : FamilyDef 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 obligation to ensure the facet in question is a module facet.

@[reducible, inline]

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

Build info for a module facet.

@[reducible, inline]

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

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

@[reducible, inline]

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

The module's Lean source file.

@[reducible, inline]

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

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

@[reducible, inline]

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

The direct local imports of the Lean module.

@[reducible, inline]

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

The transitive local imports of the Lean module.

@[reducible, inline]

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

The transitive local imports of the Lean module.

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

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

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

@[reducible, inline]

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

The olean file produced by lean.

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

The ilean file produced by lean.

@[reducible, inline]

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

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

@[reducible, inline]

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

The C file produced by lean.

@[reducible, inline]

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

The C file produced by lean.

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

The object file .bc.o built from bc.

@[reducible, inline]

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

Shared library for --load-dynlib.

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

@[reducible, inline]

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

@[reducible, inline]

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

Build info for a package facet.

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

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

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

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

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

The package's array of dependencies.

@[reducible, inline]

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

The package's complete array of transitive dependencies.

Lean Library Infos

@[reducible, inline]

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

@[reducible, inline]

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

Build info for a facet of a Lean library.

@[reducible, inline]

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

The library's default facets (as specified by its defaultFacets configuration). .

@[reducible, inline]

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

A Lean library's Lean modules.

@[reducible, inline]

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

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

@[reducible, inline]

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

A Lean library's static artifact.

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

@[reducible, inline]

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

A Lean library's shared artifact.

@[reducible, inline]

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

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

Lean Executable Infos

@[reducible, inline]

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

@[reducible, inline]

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

A Lean binary executable.

External Library Infos

@[reducible, inline]

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

@[reducible, inline]

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

A external library's static binary.

@[reducible, inline]

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

A external library's shared binary.

@[reducible, inline]

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

A external library's dynlib.

Input File & Directory Infos

@[reducible, inline]

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

@[reducible, inline]

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

The default facet for an input file. Produces the file path.

@[reducible, inline]

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

@[reducible, inline]

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

The default facet for an input directory. Produces the matching files in the directory.