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.

source

structure Lake.ModuleDeps :

Type

dynlibs : Array Dynlib
plugins : Array Dynlib

Instances For

source

instance Lake.instInhabitedModuleDeps :

Inhabited ModuleDeps

Equations

Lake.instInhabitedModuleDeps = { default := { dynlibs := default, plugins := default } }

source

instance Lake.instReprModuleDeps :

Repr ModuleDeps

Equations

Lake.instReprModuleDeps = { reprPrec := Lake.reprModuleDeps✝ }

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

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

Repr (ModuleFacet α✝)

Equations

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

source

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

FamilyDef FacetOut facet.name α

source

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

CoeDep Lean.Name facet (ModuleFacet α)

Equations

Lake.instCoeDepNameModuleFacetOfFamilyOutFacetOut = { coe := { name := facet, data_eq := ⋯ } }

source

instance Lake.instFamilyDefNameFacetOutMkStr2ModuleDeps :

FamilyDef FacetOut `module.deps ModuleDeps

source

@[reducible]

def Lake.Module.depsFacet :

Lean.Name

The facet which builds all of a module's dependencies (i.e., transitive local imports and --load-dynlib shared libraries). Returns the list of shared libraries to load along with their search path.

Equations

Lake.Module.depsFacet = `module.deps

source

@[simp]

axiom Lake.FacetOut.module.deps :

FacetOut `module.deps = ModuleDeps

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ModuleDeps :

FamilyDef FacetOut (`module ++ `deps) ModuleDeps

source

@[simp]

axiom Lake.FacetOut.module.leanArts :

FacetOut `module.leanArts = Unit

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit :

FamilyDef FacetOut (`module ++ `leanArts) Unit

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

Equations

Lake.Module.leanArtsFacet = `module.leanArts

source

instance Lake.instFamilyDefNameFacetOutMkStr2Unit :

FamilyDef FacetOut `module.leanArts Unit

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath :

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

source

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath :

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.

Equations

Lake.Module.oleanFacet = `module.olean

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_1 :

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

source

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_1 :

FamilyDef FacetOut `module.ilean System.FilePath

source

@[reducible]

def Lake.Module.ileanFacet :

Lean.Name

The ilean file produced by lean.

Equations

Lake.Module.ileanFacet = `module.ilean

source

@[simp]

axiom Lake.FacetOut.module.ilean :

FacetOut `module.ilean = System.FilePath

source

@[reducible]

def Lake.Module.cFacet :

Lean.Name

The C file built from the Lean file via lean.

Equations

Lake.Module.cFacet = `module.c

source

@[simp]

axiom Lake.FacetOut.module.c :

FacetOut `module.c = System.FilePath

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_2 :

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

source

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_2 :

FamilyDef FacetOut `module.c System.FilePath

source

@[simp]

axiom Lake.FacetOut.module.bc :

FacetOut `module.bc = System.FilePath

source

@[reducible]

def Lake.Module.bcFacet :

Lean.Name

The LLVM BC file built from the Lean file via lean.

Equations

Lake.Module.bcFacet = `module.bc

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_3 :

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

source

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_3 :

FamilyDef FacetOut `module.bc 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).

Equations

Lake.Module.coFacet = `module.c.o

source

@[simp]

axiom Lake.FacetOut.module.c.o :

FacetOut `module.c.o = System.FilePath

source

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath :

FamilyDef FacetOut `module.c.o System.FilePath

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath :

FamilyDef FacetOut (`module ++ `c.o) 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).

Equations

Lake.Module.coExportFacet = `module.c.o.export

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr3FilePath :

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

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr3FilePath_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

instance Lake.instFamilyDefNameFacetOutMkStr4FilePath_1 :

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

Equations

Lake.Module.coNoExportFacet = `module.c.o.noexport

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath_1 :

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

source

@[simp]

axiom Lake.FacetOut.module.bc.o :

FacetOut `module.bc.o = System.FilePath

source

@[reducible]

def Lake.Module.bcoFacet :

Lean.Name

The object file .bc.o built from bc.

Equations

Lake.Module.bcoFacet = `module.bc.o

source

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath_1 :

FamilyDef FacetOut `module.bc.o System.FilePath

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_4 :

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.

Equations

Lake.Module.oFacet = `module.o

source

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_4 :

FamilyDef FacetOut `module.o System.FilePath

source

@[simp]

axiom Lake.FacetOut.module.o :

FacetOut `module.o = System.FilePath

source

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath_2 :

FamilyDef FacetOut `module.o.export System.FilePath

source

@[simp]

axiom Lake.FacetOut.module.o.export :

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

Equations

Lake.Module.oExportFacet = `module.o.export

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath_2 :

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

source

@[simp]

axiom Lake.FacetOut.module.o.noexport :

FacetOut `module.o.noexport = System.FilePath

source

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath_3 :

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

Equations

Lake.Module.oNoExportFacet = `module.o.noexport

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath_3 :

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

Package Facets #

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Bool :

FamilyDef FacetOut (`package ++ `optCache) Bool

source

instance Lake.instFamilyDefNameFacetOutMkStr2Bool :

FamilyDef FacetOut `package.optCache Bool

source

@[simp]

axiom Lake.FacetOut.package.optCache :

FacetOut `package.optCache = Bool

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.

Equations

Lake.Package.optBuildCacheFacet = `package.optCache

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_1 :

FamilyDef FacetOut (`package ++ `cache) Unit

source

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_1 :

FamilyDef FacetOut `package.cache Unit

source

@[simp]

axiom Lake.FacetOut.package.cache :

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.

Equations

Lake.Package.buildCacheFacet = `package.cache

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.

Equations

Lake.Package.optReservoirBarrelFacet = `package.optBarrel

source

@[simp]

axiom Lake.FacetOut.package.optBarrel :

FacetOut `package.optBarrel = Bool

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Bool_1 :

FamilyDef FacetOut (`package ++ `optBarrel) Bool

source

instance Lake.instFamilyDefNameFacetOutMkStr2Bool_1 :

FamilyDef FacetOut `package.optBarrel Bool

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.

Equations

Lake.Package.reservoirBarrelFacet = `package.barrel

source

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_2 :

FamilyDef FacetOut `package.barrel Unit

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_2 :

FamilyDef FacetOut (`package ++ `barrel) Unit

source

@[simp]

axiom Lake.FacetOut.package.barrel :

FacetOut `package.barrel = Unit

source

@[simp]

axiom Lake.FacetOut.package.optRelease :

FacetOut `package.optRelease = Bool

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.

Equations

Lake.Package.optGitHubReleaseFacet = `package.optRelease

source

instance Lake.instFamilyDefNameFacetOutMkStr2Bool_2 :

FamilyDef FacetOut `package.optRelease Bool

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Bool_2 :

FamilyDef FacetOut (`package ++ `optRelease) Bool

source

@[reducible, inline, deprecated Lake.Package.optGitHubReleaseFacet (since := "2024-09-27")]

abbrev Lake.Package.optReleaseFacet :

Lean.Name

Equations

Lake.Package.optReleaseFacet = Lake.Package.optGitHubReleaseFacet

source

@[simp]

axiom Lake.FacetOut.package.release :

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.

Equations

Lake.Package.gitHubReleaseFacet = `package.release

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_3 :

FamilyDef FacetOut (`package ++ `release) Unit

source

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_3 :

FamilyDef FacetOut `package.release Unit

source

@[reducible, inline, deprecated Lake.Package.gitHubReleaseFacet (since := "2024-09-27")]

abbrev Lake.Package.releaseFacet :

Lean.Name

Equations

Lake.Package.releaseFacet = Lake.Package.gitHubReleaseFacet

source

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_4 :

FamilyDef FacetOut `package.extraDep Unit

source

@[reducible]

def Lake.Package.extraDepFacet :

Lean.Name

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

Equations

Lake.Package.extraDepFacet = `package.extraDep

source

@[simp]

axiom Lake.FacetOut.package.extraDep :

FacetOut `package.extraDep = Unit

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_4 :

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

Equations

Lake.LeanLib.defaultFacet = `lean_lib.default

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_5 :

FamilyDef FacetOut (`lean_lib ++ `default) Unit

source

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_5 :

FamilyDef FacetOut `lean_lib.default Unit

source

@[simp]

axiom Lake.FacetOut.lean_lib.default :

FacetOut `lean_lib.default = Unit

source

@[reducible]

def Lake.LeanLib.leanArtsFacet :

Lean.Name

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

Equations

Lake.LeanLib.leanArtsFacet = `lean_lib.leanArts

source

@[simp]

axiom Lake.FacetOut.lean_lib.leanArts :

FacetOut `lean_lib.leanArts = Unit

source

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_6 :

FamilyDef FacetOut `lean_lib.leanArts Unit

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_6 :

FamilyDef FacetOut (`lean_lib ++ `leanArts) Unit

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_5 :

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

source

@[simp]

axiom Lake.FacetOut.lean_lib.static :

FacetOut `lean_lib.static = System.FilePath

source

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_5 :

FamilyDef FacetOut `lean_lib.static System.FilePath

source

@[reducible]

def Lake.LeanLib.staticFacet :

Lean.Name

A Lean library's static artifact.

Equations

Lake.LeanLib.staticFacet = `lean_lib.static

source

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath_4 :

FamilyDef FacetOut `lean_lib.static.export System.FilePath

source

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath_4 :

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.

Equations