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.

Module Facets #

source

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 : FacetOut self.name = α
Proof that module's facet build result is of type α.

Instances For

source

def Lake.instReprModuleFacet.repr {α✝ : Type} [Repr α✝] :

ModuleFacet α✝ → Nat → Std.Format

Instances For

source

@[implicit_reducible]

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

Repr (ModuleFacet α✝)

source

instance Lake.instFamilyDefNameFacetOutName {α : Type} (facet : ModuleFacet α) :

FamilyDef FacetOut facet.name α

source

@[implicit_reducible]

instance Lake.instCoeDepNameModuleFacetOfFamilyOutFacetOut {facet : Lean.Name} {α : Type} [FamilyOut FacetOut facet α] :

CoeDep Lean.Name facet (ModuleFacet α)

source

@[simp]

axiom Lake.FacetOut.module.lean :

FacetOut `module.lean = System.FilePath

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath :

FamilyDef FacetOut (`module ++ `lean) System.FilePath

source

@[reducible]

def Lake.Module.leanFacet :

Lean.Name

The module's Lean source file.

Instances For

source

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath :

FamilyDef FacetOut `module.lean System.FilePath

source

@[reducible]

def Lake.Module.headerFacet :

Lean.Name

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

Instances For

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ModuleHeader :

FamilyDef FacetOut (`module ++ `header) Lean.ModuleHeader

source

instance Lake.instFamilyDefNameFacetOutMkStr2ModuleHeader :

FamilyDef FacetOut `module.header Lean.ModuleHeader

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ModuleSetup :

FamilyDef FacetOut (`module ++ `setup) Lean.ModuleSetup

source

@[simp]

axiom Lake.FacetOut.module.setup :

FacetOut `module.setup = Lean.ModuleSetup

source

@[reducible]

def Lake.Module.setupFacet :

Lean.Name

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.

Instances For

source

instance Lake.instFamilyDefNameFacetOutMkStr2ModuleSetup :

FamilyDef FacetOut `module.setup Lean.ModuleSetup

source

@[reducible]

def Lake.Module.depsFacet :

Lean.Name

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

Instances For

source

instance Lake.instFamilyDefNameFacetOutMkStr2Opaque :

FamilyDef FacetOut `module.deps Opaque

source

@[simp]

axiom Lake.FacetOut.module.deps :

FacetOut `module.deps = Opaque

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Opaque :

FamilyDef FacetOut (`module ++ `deps) Opaque

source

structure Lake.ModuleImportInfo :

Type

Information about the imports of a module.

directArts : Lean.NameMap Lean.ImportArtifacts
Artifacts directly needed for the imports of the module.
trace : BuildTrace
The trace produced by mixing the traces of directArts with their transitive imports.
transTrace : BuildTrace
Transitive import trace for an import of the module with the module system enabled.
metaTransTrace : BuildTrace
Transitive import trace for a meta import of the module.
allTransTrace : BuildTrace
Transitive import trace for an import all of the module.
legacyTransTrace : BuildTrace
Transitive import trace for an import of the module without the module system enabled.

Instances For

source

def Lake.instInhabitedModuleImportInfo.default :

ModuleImportInfo

Instances For

source

@[implicit_reducible]

instance Lake.instInhabitedModuleImportInfo :

Inhabited ModuleImportInfo

source

instance Lake.instFamilyDefNameFacetOutMkStr2ModuleImportInfo :

FamilyDef FacetOut `module.importInfo ModuleImportInfo

source

@[reducible]

def Lake.Module.importInfoFacet :

Lean.Name

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

Instances For

source

@[simp]

axiom Lake.FacetOut.module.importInfo :

FacetOut `module.importInfo = ModuleImportInfo

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ModuleImportInfo :

FamilyDef FacetOut (`module ++ `importInfo) ModuleImportInfo

source

structure Lake.ModuleExportInfo :

Type

Information useful to importers of a module.

srcTrace : BuildTrace
The trace of the module's source file.
arts : Lean.ImportArtifacts
Artifacts directly needed for an import of the module with the module system enabled.
artsTrace : BuildTrace
The trace of the module's public olean.
metaArtsTrace : BuildTrace
The trace of the module's public olean and IR.
allArts : Lean.ImportArtifacts
Artifacts directly needed for an import of the module from a module without the module system enabled or import all of the module from a module with it enabled.
allArtsTrace : BuildTrace
The trace produced by mixing the traces of allArts.
transTrace : BuildTrace
Transitive import trace for an import of the module with the module system enabled.
metaTransTrace : BuildTrace
Transitive import trace for a meta import of the module.
allTransTrace : BuildTrace
Transitive import trace for an import all of the module.
legacyTransTrace : BuildTrace
Transitive import trace for an import of the module without the module system enabled.

Instances For

source

def Lake.instInhabitedModuleExportInfo.default :

ModuleExportInfo

Instances For

source

@[implicit_reducible]

instance Lake.instInhabitedModuleExportInfo :

Inhabited ModuleExportInfo

source

instance Lake.instFamilyDefNameFacetOutMkStr2ModuleExportInfo :

FamilyDef FacetOut `module.exportInfo ModuleExportInfo

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ModuleExportInfo :

FamilyDef FacetOut (`module ++ `exportInfo) ModuleExportInfo

source

@[reducible]

def Lake.Module.exportInfoFacet :

Lean.Name

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

Instances For

source

@[simp]

axiom Lake.FacetOut.module.exportInfo :

FacetOut `module.exportInfo = ModuleExportInfo

source

instance Lake.instFamilyDefNameFacetOutMkStr2ImportArtifacts :

FamilyDef FacetOut `module.importArts Lean.ImportArtifacts

source

@[simp]

axiom Lake.FacetOut.module.importArts :

FacetOut `module.importArts = Lean.ImportArtifacts

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ImportArtifacts :

FamilyDef FacetOut (`module ++ `importArts) Lean.ImportArtifacts

source

@[reducible]

def Lake.Module.importArtsFacet :

Lean.Name

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

Instances For

source

instance Lake.instFamilyDefNameFacetOutMkStr2ImportArtifacts_1 :

FamilyDef FacetOut `module.importAllArts Lean.ImportArtifacts

source

@[reducible]

def Lake.Module.importAllArtsFacet :

Lean.Name

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.

Instances For

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ImportArtifacts_1 :

FamilyDef FacetOut (`module ++ `importAllArts) Lean.ImportArtifacts

source

@[simp]

axiom Lake.FacetOut.module.importAllArts :

FacetOut `module.importAllArts = Lean.ImportArtifacts

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ModuleOutputArtifacts :

FamilyDef FacetOut (`module ++ `leanArts) ModuleOutputArtifacts

source

instance Lake.instFamilyDefNameFacetOutMkStr2ModuleOutputArtifacts :

FamilyDef FacetOut `module.leanArts ModuleOutputArtifacts

source

@[reducible]

def 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 (e.g., olean, ilean, c). Its trace just includes its dependencies.

Instances For

source

@[simp]

axiom Lake.FacetOut.module.leanArts :

FacetOut `module.leanArts = ModuleOutputArtifacts

source

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_1 :

FamilyDef FacetOut `module.olean System.FilePath

source

@[simp]

axiom Lake.FacetOut.module.olean :

FacetOut `module.olean = System.FilePath

source

@[reducible]

def Lake.Module.oleanFacet :

Lean.Name

The olean file produced by lean.

Instances For

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_1 :

FamilyDef FacetOut (`module ++ `olean) System.FilePath

source

@[reducible]

def Lake.Module.oleanServerFacet :

Lean.Name

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

Instances For

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath :

FamilyDef FacetOut (`module ++ `olean.server) System.FilePath

source

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath :

FamilyDef FacetOut `module.olean.server System.FilePath

source

@[simp]

axiom Lake.FacetOut.module.olean.server :

FacetOut `module.olean.server = System.FilePath

source

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath_1 :

FamilyDef FacetOut `module.olean.private System.FilePath

source

@[simp]

axiom Lake.FacetOut.module.olean.private :

FacetOut `module.olean.private = System.FilePath

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath_1 :

FamilyDef FacetOut (`module ++ `olean.private) System.FilePath

source

@[reducible]

def Lake.Module.oleanPrivateFacet :

Lean.Name

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

Instances For

source

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_2 :

FamilyDef FacetOut `module.ilean System.FilePath

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_2 :

FamilyDef FacetOut (`module ++ `ilean) System.FilePath

source

@[simp]

axiom Lake.FacetOut.module.ilean :

FacetOut `module.ilean = System.FilePath

source

@[reducible]

def Lake.Module.ileanFacet :

Lean.Name

The ilean file produced by lean.

Instances For

source

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_3 :

FamilyDef FacetOut `module.ir System.FilePath

source

@[simp]

axiom Lake.FacetOut.module.ir :

FacetOut `module.ir = System.FilePath

source

@[reducible]

def Lake.Module.irFacet :

Lean.Name

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

Instances For

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_3 :

FamilyDef FacetOut (`module ++ `ir) System.FilePath

source

@[simp]

axiom Lake.FacetOut.module.c :

FacetOut `module.c = System.FilePath

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_4 :

FamilyDef FacetOut (`module ++ `c) System.FilePath

source

@[reducible]

def Lake.Module.cFacet :

Lean.Name

The C file produced by lean.

Instances For

source

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_4 :

FamilyDef FacetOut `module.c System.FilePath

source

@[reducible]

def Lake.Module.bcFacet :

Lean.Name

The LLVM bitcode (bc) file produced by lean.

Instances For

source

@[simp]

axiom Lake.FacetOut.module.bc :

FacetOut `module.bc = System.FilePath

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_5 :

FamilyDef FacetOut (`module ++ `bc) System.FilePath

source

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_5 :

FamilyDef FacetOut `module.bc System.FilePath

source

@[simp]

axiom Lake.FacetOut.module.c.o :

FacetOut `module.c.o = System.FilePath

source

@[reducible]

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

Instances For

source

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath_2 :

FamilyDef FacetOut `module.c.o System.FilePath

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath_2 :

FamilyDef FacetOut (`module ++ `c.o) System.FilePath

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr3FilePath :

FamilyDef FacetOut (`module ++ `c.o.export) System.FilePath

source

@[simp]

axiom Lake.FacetOut.module.c.o.export :

FacetOut `module.c.o.export = System.FilePath

source

instance Lake.instFamilyDefNameFacetOutMkStr4FilePath :

FamilyDef FacetOut `module.c.o.export System.FilePath

source

@[reducible]

def Lake.Module.coExportFacet :

Lean.Name

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

Instances For

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr3FilePath_1 :

FamilyDef FacetOut (`module ++ `c.o.noexport) System.FilePath

source

instance Lake.instFamilyDefNameFacetOutMkStr4FilePath_1 :

FamilyDef FacetOut `module.c.o.noexport System.FilePath

source

@[simp]

axiom Lake.FacetOut.module.c.o.noexport :

FacetOut `module.c.o.noexport = System.FilePath

source

@[reducible]

def Lake.Module.coNoExportFacet :

Lean.Name

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

Instances For

source

@[reducible]

def Lake.Module.bcoFacet :

Lean.Name

The object file .bc.o built from bc.

Instances For

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath_3 :

FamilyDef FacetOut (`module ++ `bc.o) System.FilePath

source

@[simp]

axiom Lake.FacetOut.module.bc.o :

FacetOut `module.bc.o = System.FilePath

source

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath_3 :

FamilyDef FacetOut `module.bc.o System.FilePath

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_6 :

FamilyDef FacetOut (`module ++ `o) System.FilePath

source

@[simp]

axiom Lake.FacetOut.module.o :

FacetOut `module.o = System.FilePath

source

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_6 :

FamilyDef FacetOut `module.o System.FilePath

source

@[reducible]

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

Instances For

source

@[simp]

axiom Lake.FacetOut.module.o.export :

FacetOut `module.o.export = System.FilePath

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath_4 :

FamilyDef FacetOut (`module ++ `o.export) System.FilePath

source

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath_4 :

FamilyDef FacetOut `module.o.export System.FilePath

source

@[reducible]

def Lake.Module.oExportFacet :

Lean.Name

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

Instances For

source

@[simp]

axiom Lake.FacetOut.module.o.noexport :

FacetOut `module.o.noexport = System.FilePath

source

@[reducible]

def Lake.Module.oNoExportFacet :

Lean.Name

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

Instances For

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath_5 :

FamilyDef FacetOut (`module ++ `o.noexport) System.FilePath

source

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath_5 :

FamilyDef FacetOut `module.o.noexport System.FilePath

Package Facets #

source

@[reducible]

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

Instances For

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Bool :

FamilyDef FacetOut (`package ++ `optCache) Bool

source

@[simp]

axiom Lake.FacetOut.package.optCache :

FacetOut `package.optCache = Bool

source

instance Lake.instFamilyDefNameFacetOutMkStr2Bool :

FamilyDef FacetOut `package.optCache Bool

source

@[simp]

axiom Lake.FacetOut.package.cache :

FacetOut `package.cache = Unit

source

instance Lake.instFamilyDefNameFacetOutMkStr2Unit :

FamilyDef FacetOut `package.cache Unit

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit :

FamilyDef FacetOut (`package ++ `cache) Unit

source

@[reducible]

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

Instances For

source

@[simp]

axiom Lake.FacetOut.package.optBarrel :

FacetOut `package.optBarrel = Bool

source

@[reducible]

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

Instances For

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Bool_1 :

FamilyDef FacetOut (`package ++ `optBarrel) Bool

source

instance Lake.instFamilyDefNameFacetOutMkStr2Bool_1 :

FamilyDef FacetOut `package.optBarrel Bool

source

@[simp]

axiom Lake.FacetOut.package.barrel :

FacetOut `package.barrel = Unit

source

@[reducible]

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

Instances For

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_1 :

FamilyDef FacetOut (`package ++ `barrel) Unit

source

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_1 :

FamilyDef FacetOut `package.barrel Unit

source

@[reducible]

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

Instances For

source

@[simp]

axiom Lake.FacetOut.package.optRelease :

FacetOut `package.optRelease = Bool

source

instance Lake.instFamilyDefNameFacetOutMkStr2Bool_2 :

FamilyDef FacetOut `package.optRelease Bool

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Bool_2 :

FamilyDef FacetOut (`package ++ `optRelease) Bool

source

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_2 :

FamilyDef FacetOut `package.release Unit

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_2 :

FamilyDef FacetOut (`package ++ `release) Unit

source

@[reducible]

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

Instances For

source

@[simp]

axiom Lake.FacetOut.package.release :

FacetOut `package.release = Unit

source

@[simp]

axiom Lake.FacetOut.package.extraDep :

FacetOut `package.extraDep = Unit

source

@[reducible]

def Lake.Package.extraDepFacet :

Lean.Name

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

Instances For

source

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_3 :

FamilyDef FacetOut `package.extraDep Unit

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_3 :

FamilyDef FacetOut (`package ++ `extraDep) Unit

Target Facets #

source

@[reducible]

def Lake.LeanLib.defaultFacet :

Lean.Name

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

Instances For

source

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_4 :

FamilyDef FacetOut `lean_lib.default Unit

source

@[simp]

axiom Lake.FacetOut.lean_lib.default :

FacetOut `lean_lib.default = Unit

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_4 :

FamilyDef FacetOut (`lean_lib ++ `default) Unit

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_5 :

FamilyDef FacetOut (`lean_lib ++ `leanArts) Unit

source

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_5 :

FamilyDef FacetOut `lean_lib.leanArts Unit

source

@[simp]

axiom Lake.FacetOut.lean_lib.leanArts :

FacetOut `lean_lib.leanArts = Unit

source

@[reducible]

def Lake.LeanLib.leanArtsFacet :

Lean.Name

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

Instances For

source

@[simp]

axiom Lake.FacetOut.lean_lib.static :

FacetOut `lean_lib.static = System.FilePath

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_7 :

FamilyDef FacetOut (`lean_lib ++ `static) System.FilePath

source

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_7 :

FamilyDef FacetOut `lean_lib.static System.FilePath

source

@[reducible]

def Lake.LeanLib.staticFacet :

Lean.Name

A Lean library's static artifact.

Instances For

source

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath_6 :

FamilyDef FacetOut `lean_lib.static.export System.FilePath

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath_6 :

FamilyDef FacetOut (`lean_lib ++ `static.export) System.FilePath

source

@[reducible]

def Lake.LeanLib.staticExportFacet :

Lean.Name

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.

Instances For

source

@[simp]

axiom Lake.FacetOut.lean_lib.static.export :

FacetOut `lean_lib.static.export = System.FilePath

source

@[simp]

axiom Lake.FacetOut.lean_lib.shared :

FacetOut `lean_lib.shared = Dynlib

source

@[reducible]

def Lake.LeanLib.sharedFacet :