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

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 := ⋯ } }

@[simp]

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

@[reducible]

def Lake.Module.leanFacet : Lean.Name

The module's Lean source file.

Equations

• Lake.Module.leanFacet = `module.lean

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

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

@[simp]

axiom Lake.FacetOut.module.header : FacetOut `module.header = Lean.ModuleHeader

instance Lake.instFamilyDefNameFacetOutMkStr2ModuleHeader : FamilyDef FacetOut `module.header Lean.ModuleHeader

@[reducible]

def Lake.Module.headerFacet : Lean.Name

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

Equations

• Lake.Module.headerFacet = `module.header

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ModuleHeader : FamilyDef FacetOut (`module ++ `header) Lean.ModuleHeader

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ModuleSetup : FamilyDef FacetOut (`module ++ `setup) Lean.ModuleSetup

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

Equations

• Lake.Module.setupFacet = `module.setup

instance Lake.instFamilyDefNameFacetOutMkStr2ModuleSetup : FamilyDef FacetOut `module.setup Lean.ModuleSetup

@[simp]

axiom Lake.FacetOut.module.setup : FacetOut `module.setup = Lean.ModuleSetup

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

Equations

• Lake.Module.depsFacet = `module.deps

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Opaque : FamilyDef FacetOut (`module ++ `deps) Opaque

@[simp]

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

instance Lake.instFamilyDefNameFacetOutMkStr2Opaque : FamilyDef FacetOut `module.deps Opaque

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.

instance Lake.instFamilyDefNameFacetOutMkStr2ModuleImportInfo : FamilyDef FacetOut `module.importInfo ModuleImportInfo

@[reducible]

def Lake.Module.importInfoFacet : Lean.Name

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

Equations

• Lake.Module.importInfoFacet = `module.importInfo

@[simp]

axiom Lake.FacetOut.module.importInfo : FacetOut `module.importInfo = ModuleImportInfo

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ModuleImportInfo : FamilyDef FacetOut (`module ++ `importInfo) ModuleImportInfo

structure Lake.ModuleExportInfo : Type

Information useful to importers of a module.

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

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ModuleExportInfo : FamilyDef FacetOut (`module ++ `exportInfo) ModuleExportInfo

instance Lake.instFamilyDefNameFacetOutMkStr2ModuleExportInfo : FamilyDef FacetOut `module.exportInfo ModuleExportInfo

@[reducible]

def Lake.Module.exportInfoFacet : Lean.Name

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

Equations

• Lake.Module.exportInfoFacet = `module.exportInfo

@[simp]

axiom Lake.FacetOut.module.exportInfo : FacetOut `module.exportInfo = ModuleExportInfo

instance Lake.instFamilyDefNameFacetOutMkStr2ImportArtifacts : FamilyDef FacetOut `module.importArts Lean.ImportArtifacts

@[reducible]

def Lake.Module.importArtsFacet : Lean.Name

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

Equations

• Lake.Module.importArtsFacet = `module.importArts

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ImportArtifacts : FamilyDef FacetOut (`module ++ `importArts) Lean.ImportArtifacts

@[simp]

axiom Lake.FacetOut.module.importArts : FacetOut `module.importArts = Lean.ImportArtifacts

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

Equations

• Lake.Module.importAllArtsFacet = `module.importAllArts

instance Lake.instFamilyDefNameFacetOutMkStr2ImportArtifacts_1 : FamilyDef FacetOut `module.importAllArts Lean.ImportArtifacts

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ImportArtifacts_1 : FamilyDef FacetOut (`module ++ `importAllArts) Lean.ImportArtifacts

@[simp]

axiom Lake.FacetOut.module.importAllArts : FacetOut `module.importAllArts = Lean.ImportArtifacts

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

Equations

• Lake.Module.leanArtsFacet = `module.leanArts

@[simp]

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

instance Lake.instFamilyDefNameFacetOutMkStr2ModuleOutputArtifacts : FamilyDef FacetOut `module.leanArts ModuleOutputArtifacts

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ModuleOutputArtifacts : FamilyDef FacetOut (`module ++ `leanArts) ModuleOutputArtifacts

@[simp]

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

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_1 : FamilyDef 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.instFamilyDefNameFacetOutMkStr2FilePath_1 : FamilyDef FacetOut `module.olean System.FilePath

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

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath : FamilyDef FacetOut `module.olean.server System.FilePath

@[reducible]

def Lake.Module.oleanServerFacet : Lean.Name

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

Equations

• Lake.Module.oleanServerFacet = `module.olean.server

@[simp]

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

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath_1 : FamilyDef FacetOut `module.olean.private System.FilePath

@[simp]

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

@[reducible]

def Lake.Module.oleanPrivateFacet : Lean.Name

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

Equations

• Lake.Module.oleanPrivateFacet = `module.olean.private

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

@[reducible]

def Lake.Module.ileanFacet : Lean.Name

The ilean file produced by lean.

Equations

• Lake.Module.ileanFacet = `module.ilean

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

@[simp]

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

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

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

@[reducible]

def Lake.Module.irFacet : Lean.Name

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

Equations

• Lake.Module.irFacet = `module.ir

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

@[simp]

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

@[simp]

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

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

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

@[reducible]

def Lake.Module.cFacet : Lean.Name

The C file produced by lean.

Equations

• Lake.Module.cFacet = `module.c

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

@[simp]

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

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

@[reducible]

def Lake.Module.bcFacet : Lean.Name

The LLVM bitcode (bc) file produced by lean.

Equations

• Lake.Module.bcFacet = `module.bc

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

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

@[simp]

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

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath_2 : FamilyDef FacetOut (`module ++ `c.o) 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.instFamilyDefNameFacetOutMkStr4FilePath : FamilyDef FacetOut `module.c.o.export System.FilePath

@[simp]

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

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1MkStr3FilePath : FamilyDef FacetOut (`module ++ `c.o.export) 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

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

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

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

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath_3 : 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.instFamilyDefNameFacetOutHAppendMkStr1FilePath_6 : FamilyDef FacetOut (`module ++ `o) System.FilePath

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_6 : 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

@[simp]

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

@[simp]

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

instance Lake.instFamilyDefNameFacetOutMkStr3FilePath_4 : FamilyDef 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_4 : FamilyDef FacetOut (`module ++ `o.export) 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

@[simp]

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

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

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

Package Facets

@[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.instFamilyDefNameFacetOutMkStr2Bool : FamilyDef FacetOut `package.optCache Bool

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

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

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

@[simp]

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

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

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

@[simp]

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

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

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

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

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

@[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.release : FacetOut `package.release = Unit

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

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

@[simp]

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

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

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_3 : 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

@[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.instFamilyDefNameFacetOutHAppendMkStr1Unit_4 : FamilyDef FacetOut (`lean_lib ++ `default) Unit

@[simp]

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

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

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

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

@[reducible]

def Lake.LeanLib.leanArtsFacet : Lean.Name

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

Equations

• Lake.LeanLib.leanArtsFacet = `lean_lib.leanArts

@[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.instFamilyDefNameFacetOutMkStr2FilePath_7 : FamilyDef FacetOut `lean_lib.static System.FilePath

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_7 : 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.instFamilyDefNameFacetOutHAppendMkStr1MkStr2FilePath_6 : 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.instFamilyDefNameFacetOutMkStr3FilePath_6 : FamilyDef FacetOut `lean_lib.static.export System.FilePath

@[reducible]

def Lake.LeanLib.sharedFacet : Lean.Name

A Lean library's shared artifact.

Equations

• Lake.LeanLib.sharedFacet = `lean_lib.shared

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

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

@[simp]

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

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

@[simp]

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

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Unit_6 : 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

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_8 : FamilyDef 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_8 : FamilyDef FacetOut `lean_exe.default System.FilePath

@[simp]

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

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

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

@[simp]

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

@[reducible]

def Lake.LeanExe.exeFacet : Lean.Name

A Lean binary executable.

Equations

• Lake.LeanExe.exeFacet = `lean_exe.exe

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

@[simp]

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

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_10 : FamilyDef FacetOut (`extern_lib ++ `default) 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

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

@[simp]

axiom Lake.FacetOut.extern_lib.static : 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_11 : FamilyDef FacetOut `extern_lib.static System.FilePath

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

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1FilePath_12 : 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.shared : FacetOut `extern_lib.shared = System.FilePath

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.instFamilyDefNameFacetOutMkStr2Dynlib_1 : FamilyDef FacetOut `extern_lib.dynlib Dynlib

@[simp]

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

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

instance Lake.instFamilyDefNameFacetOutMkStr2FilePath_13 : 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

@[simp]

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

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)