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.

structure Lake.ModuleDeps : Type

• dynlibs : Array Dynlib
• plugins : Array Dynlib

instance Lake.instInhabitedModuleDeps : Inhabited ModuleDeps

Equations

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

instance Lake.instReprModuleDeps : Repr ModuleDeps

Equations

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

Module Facets

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

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

Equations

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

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

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

Equations

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

instance Lake.instFamilyDefNameFacetOutMkStr2ModuleDeps : FamilyDef FacetOut `module.deps ModuleDeps

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

@[simp]

axiom Lake.FacetOut.module.deps : FacetOut `module.deps = ModuleDeps

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ModuleDeps : FamilyDef FacetOut (`module ++ `deps) ModuleDeps

@[simp]

axiom Lake.FacetOut.module.leanArts : FacetOut `module.leanArts = Unit

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit : FamilyDef FacetOut (`module ++ `leanArts) Unit

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

instance Lake.instFamilyDefNameFacetOutMkStr2Unit : FamilyDef FacetOut `module.leanArts Unit

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath : FamilyDef FacetOut (`module ++ `olean) System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath : FamilyDef FacetOut `module.olean System.FilePath

@[simp]

axiom Lake.FacetOut.module.olean : FacetOut `module.olean = System.FilePath

@[reducible]

def Lake.Module.oleanFacet : Lean.Name

The olean file produced by lean.

Equations

• Lake.Module.oleanFacet = `module.olean

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_1 : FamilyDef FacetOut (`module ++ `ilean) System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_1 : FamilyDef FacetOut `module.ilean System.FilePath

@[reducible]

def Lake.Module.ileanFacet : Lean.Name

The ilean file produced by lean.

Equations

• Lake.Module.ileanFacet = `module.ilean

@[simp]

axiom Lake.FacetOut.module.ilean : FacetOut `module.ilean = System.FilePath

@[reducible]

def Lake.Module.cFacet : Lean.Name

The C file built from the Lean file via lean.

Equations

• Lake.Module.cFacet = `module.c

@[simp]

axiom Lake.FacetOut.module.c : FacetOut `module.c = System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_2 : FamilyDef FacetOut (`module ++ `c) System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_2 : FamilyDef FacetOut `module.c System.FilePath

@[simp]

axiom Lake.FacetOut.module.bc : FacetOut `module.bc = System.FilePath

@[reducible]

def Lake.Module.bcFacet : Lean.Name

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

Equations

• Lake.Module.bcFacet = `module.bc

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_3 : FamilyDef FacetOut (`module ++ `bc) System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_3 : FamilyDef FacetOut `module.bc System.FilePath

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

@[simp]

axiom Lake.FacetOut.module.c.o : FacetOut `module.c.o = System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath : FamilyDef FacetOut `module.c.o System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath : FamilyDef FacetOut (`module ++ `c.o) System.FilePath

@[simp]

axiom Lake.FacetOut.module.c.o.export : FacetOut `module.c.o.export = System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr4FilePath : FamilyDef FacetOut `module.c.o.export System.FilePath

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

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr3FilePath : FamilyDef FacetOut (`module ++ `c.o.export) System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr3FilePath_1 : FamilyDef FacetOut (`module ++ `c.o.noexport) System.FilePath

@[simp]

axiom Lake.FacetOut.module.c.o.noexport : FacetOut `module.c.o.noexport = System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr4FilePath_1 : FamilyDef FacetOut `module.c.o.noexport System.FilePath

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

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath_1 : FamilyDef FacetOut (`module ++ `bc.o) System.FilePath

@[simp]

axiom Lake.FacetOut.module.bc.o : FacetOut `module.bc.o = System.FilePath

@[reducible]

def Lake.Module.bcoFacet : Lean.Name

The object file .bc.o built from bc.

Equations

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

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath_1 : FamilyDef FacetOut `module.bc.o System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_4 : FamilyDef FacetOut (`module ++ `o) System.FilePath

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

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_4 : FamilyDef FacetOut `module.o System.FilePath

@[simp]

axiom Lake.FacetOut.module.o : FacetOut `module.o = System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath_2 : FamilyDef FacetOut `module.o.export System.FilePath

@[simp]

axiom Lake.FacetOut.module.o.export : FacetOut `module.o.export = System.FilePath

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

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath_2 : FamilyDef FacetOut (`module ++ `o.export) System.FilePath

@[simp]

axiom Lake.FacetOut.module.o.noexport : FacetOut `module.o.noexport = System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath_3 : FamilyDef FacetOut `module.o.noexport System.FilePath

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

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath_3 : FamilyDef FacetOut (`module ++ `o.noexport) System.FilePath

Package Facets

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Bool : FamilyDef FacetOut (`package ++ `optCache) Bool

instance Lake.instFamilyDefNameFacetOutMkStr2Bool : FamilyDef FacetOut `package.optCache Bool

@[simp]

axiom Lake.FacetOut.package.optCache : FacetOut `package.optCache = Bool

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

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_1 : FamilyDef FacetOut (`package ++ `cache) Unit

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_1 : FamilyDef FacetOut `package.cache Unit

@[simp]

axiom Lake.FacetOut.package.cache : FacetOut `package.cache = Unit

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

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

@[simp]

axiom Lake.FacetOut.package.optBarrel : FacetOut `package.optBarrel = Bool

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Bool_1 : FamilyDef FacetOut (`package ++ `optBarrel) Bool

instance Lake.instFamilyDefNameFacetOutMkStr2Bool_1 : FamilyDef FacetOut `package.optBarrel Bool

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_2 : FamilyDef FacetOut `package.barrel Unit

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

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_2 : FamilyDef FacetOut (`package ++ `barrel) Unit

@[simp]

axiom Lake.FacetOut.package.barrel : FacetOut `package.barrel = Unit

@[simp]

axiom Lake.FacetOut.package.optRelease : FacetOut `package.optRelease = Bool

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

instance Lake.instFamilyDefNameFacetOutMkStr2Bool_2 : FamilyDef FacetOut `package.optRelease Bool

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Bool_2 : FamilyDef FacetOut (`package ++ `optRelease) Bool

@[simp]

axiom Lake.FacetOut.package.release : FacetOut `package.release = Unit

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_3 : FamilyDef FacetOut (`package ++ `release) Unit

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_3 : FamilyDef FacetOut `package.release Unit

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

@[simp]

axiom Lake.FacetOut.package.extraDep : FacetOut `package.extraDep = Unit

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_4 : FamilyDef FacetOut (`package ++ `extraDep) Unit

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_4 : FamilyDef FacetOut `package.extraDep Unit

@[reducible]

def Lake.Package.extraDepFacet : Lean.Name

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

Equations

• Lake.Package.extraDepFacet = `package.extraDep

Target Facets

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_5 : FamilyDef FacetOut (`lean_lib ++ `default) Unit

@[simp]

axiom Lake.FacetOut.lean_lib.default : FacetOut `lean_lib.default = Unit

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

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_5 : FamilyDef FacetOut `lean_lib.default Unit

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

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_6 : FamilyDef FacetOut `lean_lib.leanArts Unit

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_6 : FamilyDef FacetOut (`lean_lib ++ `leanArts) Unit

@[simp]

axiom Lake.FacetOut.lean_lib.leanArts : FacetOut `lean_lib.leanArts = Unit

@[simp]

axiom Lake.FacetOut.lean_lib.static : FacetOut `lean_lib.static = System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_5 : FamilyDef FacetOut (`lean_lib ++ `static) System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_5 : FamilyDef FacetOut `lean_lib.static System.FilePath

@[reducible]

def Lake.LeanLib.staticFacet : Lean.Name

A Lean library's static artifact.

Equations

• Lake.LeanLib.staticFacet = `lean_lib.static

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath_4 : FamilyDef FacetOut `lean_lib.static.export System.FilePath

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

• Lake.LeanLib.staticExportFacet = `lean_lib.static.export

@[simp]

axiom Lake.FacetOut.lean_lib.static.export : FacetOut `lean_lib.static.export = System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath_4 : FamilyDef FacetOut (`lean_lib ++ `static.export) System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Dynlib : FamilyDef FacetOut (`lean_lib ++ `shared) Dynlib

@[simp]

axiom Lake.FacetOut.lean_lib.shared : FacetOut `lean_lib.shared = Dynlib

instance Lake.instFamilyDefNameFacetOutMkStr2Dynlib : FamilyDef FacetOut `lean_lib.shared Dynlib

@[reducible]

def Lake.LeanLib.sharedFacet : Lean.Name

A Lean library's shared artifact.

Equations

• Lake.LeanLib.sharedFacet = `lean_lib.shared

instance Lake.instFamilyDefNameFacetOutMkStr2Unit_7 : FamilyDef FacetOut `lean_lib.extraDep Unit

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_7 : FamilyDef FacetOut (`lean_lib ++ `extraDep) Unit

@[reducible]

def Lake.LeanLib.extraDepFacet : Lean.Name

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

Equations

• Lake.LeanLib.extraDepFacet = `lean_lib.extraDep

@[simp]

axiom Lake.FacetOut.lean_lib.extraDep : FacetOut `lean_lib.extraDep = Unit

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_6 : FamilyDef FacetOut (`lean_exe ++ `default) System.FilePath

@[simp]

axiom Lake.FacetOut.lean_exe.default : FacetOut `lean_exe.default = System.FilePath

@[reducible]

def Lake.LeanExe.defaultFacet : Lean.Name

The executable's default facet (i.e., an alias for exe)

Equations

• Lake.LeanExe.defaultFacet = `lean_exe.default

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_6 : FamilyDef FacetOut `lean_exe.default System.FilePath

@[reducible]

def Lake.LeanExe.exeFacet : Lean.Name

A Lean binary executable.

Equations

• Lake.LeanExe.exeFacet = `lean_exe.exe

@[simp]

axiom Lake.FacetOut.lean_exe.exe : FacetOut `lean_exe.exe = System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_7 : FamilyDef FacetOut `lean_exe.exe System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_7 : FamilyDef FacetOut (`lean_exe ++ `exe) System.FilePath

@[reducible]

def Lake.ExternLib.defaultFacet : Lean.Name

The external library's default facet (i.e., an alias for static)

Equations

• Lake.ExternLib.defaultFacet = `extern_lib.default

@[simp]

axiom Lake.FacetOut.extern_lib.default : FacetOut `extern_lib.default = System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_8 : FamilyDef FacetOut `extern_lib.default System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_8 : FamilyDef FacetOut (`extern_lib ++ `default) System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_9 : FamilyDef FacetOut (`extern_lib ++ `static) System.FilePath

@[reducible]

def Lake.ExternLib.staticFacet : Lean.Name

A external library's static binary.

Equations

• Lake.ExternLib.staticFacet = `extern_lib.static

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_9 : FamilyDef FacetOut `extern_lib.static System.FilePath

@[simp]

axiom Lake.FacetOut.extern_lib.static : FacetOut `extern_lib.static = System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_10 : FamilyDef FacetOut `extern_lib.shared System.FilePath

@[simp]

axiom Lake.FacetOut.extern_lib.shared : FacetOut `extern_lib.shared = System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_10 : FamilyDef FacetOut (`extern_lib ++ `shared) System.FilePath

@[reducible]

def Lake.ExternLib.sharedFacet : Lean.Name

A external library's shared binary.

Equations

• Lake.ExternLib.sharedFacet = `extern_lib.shared

@[simp]

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

instance Lake.instFamilyDefNameFacetOutMkStr2Dynlib_1 : FamilyDef FacetOut `extern_lib.dynlib Dynlib

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Dynlib_1 : FamilyDef FacetOut (`extern_lib ++ `dynlib) Dynlib

@[reducible]

def Lake.ExternLib.dynlibFacet : Lean.Name

A external library's dynlib.

Equations

• Lake.ExternLib.dynlibFacet = `extern_lib.dynlib

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_11 : FamilyDef FacetOut `input_file.default System.FilePath

@[simp]

axiom Lake.FacetOut.input_file.default : FacetOut `input_file.default = System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_11 : FamilyDef FacetOut (`input_file ++ `default) System.FilePath

@[reducible]

def Lake.InputFile.defaultFacet : Lean.Name

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

Equations

• Lake.InputFile.defaultFacet = `input_file.default

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ArrayFilePath : FamilyDef FacetOut (`input_dir ++ `default) (Array System.FilePath)

@[reducible]

def Lake.InputDir.defaultFacet : Lean.Name

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

Equations

• Lake.InputDir.defaultFacet = `input_dir.default

@[simp]

axiom Lake.FacetOut.input_dir.default : FacetOut `input_dir.default = Array System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr2ArrayFilePath : FamilyDef FacetOut `input_dir.default (Array System.FilePath)