structure Lake.Module : Type

A buildable Lean module of a LeanLib.

• lib : Lake.LeanLib
• name : Lake.Name
• keyName : Lake.Name

  The name of the module as a key. Used to create private modules (e.g., executable roots).

instance Lake.instHashableModule : Hashable Lake.Module

Equations

• Lake.instHashableModule = { hash := fun (m : Lake.Module) => hash m.keyName }

instance Lake.instBEqModule : BEq Lake.Module

Equations

• Lake.instBEqModule = { beq := fun (m n : Lake.Module) => m.keyName == n.keyName }

@[inline, reducible]

abbrev Lake.ModuleSet : Type

Equations

• Lake.ModuleSet = Lean.HashSet Lake.Module

@[inline]

def Lake.ModuleSet.empty : Lake.ModuleSet

Equations

• Lake.ModuleSet.empty = Lean.HashSet.empty

@[inline, reducible]

abbrev Lake.OrdModuleSet : Type

Equations

• Lake.OrdModuleSet = Lake.OrdHashSet Lake.Module

@[inline]

def Lake.OrdModuleSet.empty : Lake.OrdModuleSet

Equations

• Lake.OrdModuleSet.empty = Lake.OrdHashSet.empty

@[inline, reducible]

abbrev Lake.ModuleMap (α : Type u_1) : Type u_1

Equations

• Lake.ModuleMap α = Lean.RBMap Lake.Module α fun (x x_1 : Lake.Module) => Lean.Name.quickCmp x.name x_1.name

@[inline]

def Lake.ModuleMap.empty {α : Type u_1} : Lake.ModuleMap α

Equations

• Lake.ModuleMap.empty = Lean.RBMap.empty

def Lake.LeanLib.findModule? (mod : Lake.Name) (self : Lake.LeanLib) : Option Lake.Module

Locate the named, buildable module in the library (which implies it is local and importable).

Equations

• Lake.LeanLib.findModule? mod self = if Lake.LeanLib.isBuildableModule mod self = true then some { lib := self, name := mod, keyName := mod } else none

def Lake.Package.findModule? (mod : Lake.Name) (self : Lake.Package) : Option Lake.Module

Locate the named, buildable, importable, local module in the package.

Equations

• Lake.Package.findModule? mod self = Array.findSomeRev? (Lake.Package.leanLibs self) fun (x : Lake.LeanLib) => Lake.LeanLib.findModule? mod x

def Lake.LeanLib.getModuleArray (self : Lake.LeanLib) : IO (Array Lake.Module)

Get an Array of the library's modules (as specified by its globs).

Equations

• One or more equations did not get rendered due to their size.

def Lake.LeanLib.rootModules (self : Lake.LeanLib) : Array Lake.Module

The library's buildable root modules.

Equations

• Lake.LeanLib.rootModules self = Array.filterMap (fun (mod : Lake.Name) => Lake.LeanLib.findModule? mod self) self.config.roots 0

@[inline, reducible]

abbrev Lake.Module.pkg (self : Lake.Module) : Lake.Package

Equations

• Lake.Module.pkg self = self.lib.pkg

@[inline]

def Lake.Module.rootDir (self : Lake.Module) : Lake.FilePath

Equations

• Lake.Module.rootDir self = Lake.LeanLib.rootDir self.lib

@[inline]

def Lake.Module.filePath (dir : Lake.FilePath) (ext : String) (self : Lake.Module) : Lake.FilePath

Equations

• Lake.Module.filePath dir ext self = Lean.modToFilePath dir self.name ext

@[inline]

def Lake.Module.srcPath (ext : String) (self : Lake.Module) : Lake.FilePath

Equations

• Lake.Module.srcPath ext self = Lake.Module.filePath (Lake.LeanLib.srcDir self.lib) ext self

@[inline]

def Lake.Module.leanFile (self : Lake.Module) : Lake.FilePath

Equations

• Lake.Module.leanFile self = Lake.Module.srcPath "lean" self

@[inline]

def Lake.Module.leanLibPath (ext : String) (self : Lake.Module) : Lake.FilePath

Equations

• Lake.Module.leanLibPath ext self = Lake.Module.filePath (Lake.Package.leanLibDir (Lake.Module.pkg self)) ext self

@[inline]

def Lake.Module.oleanFile (self : Lake.Module) : Lake.FilePath

Equations

• Lake.Module.oleanFile self = Lake.Module.leanLibPath "olean" self

@[inline]

def Lake.Module.ileanFile (self : Lake.Module) : Lake.FilePath

Equations

• Lake.Module.ileanFile self = Lake.Module.leanLibPath "ilean" self

@[inline]

def Lake.Module.traceFile (self : Lake.Module) : Lake.FilePath

Equations

• Lake.Module.traceFile self = Lake.Module.leanLibPath "trace" self

@[inline]

def Lake.Module.irPath (ext : String) (self : Lake.Module) : Lake.FilePath

Equations

• Lake.Module.irPath ext self = Lake.Module.filePath (Lake.Package.irDir (Lake.Module.pkg self)) ext self

@[inline]

def Lake.Module.cFile (self : Lake.Module) : Lake.FilePath

Equations

• Lake.Module.cFile self = Lake.Module.irPath "c" self

@[inline]

def Lake.Module.bcFile (self : Lake.Module) : Lake.FilePath

Equations

• Lake.Module.bcFile self = Lake.Module.irPath "bc" self

@[inline]

def Lake.Module.coFile (self : Lake.Module) : Lake.FilePath

Equations

• Lake.Module.coFile self = Lake.Module.irPath "c.o" self

@[inline]

def Lake.Module.bcoFile (self : Lake.Module) : Lake.FilePath

Equations

• Lake.Module.bcoFile self = Lake.Module.irPath "bc.o" self

def Lake.Module.dynlibSuffix : String

Suffix for single module dynlibs (e.g., for precompilation).

Equations

• Lake.Module.dynlibSuffix = "-1"

@[inline]

def Lake.Module.dynlibName (self : Lake.Module) : String

Equations

• Lake.Module.dynlibName self = Lean.Name.toStringWithSep "-" true self.name ++ Lake.Module.dynlibSuffix

@[inline]

def Lake.Module.dynlibFile (self : Lake.Module) : Lake.FilePath

Equations

• Lake.Module.dynlibFile self = Lake.Package.nativeLibDir (Lake.Module.pkg self) / { toString := Lake.nameToSharedLib (Lake.Module.dynlibName self) }

@[inline]

def Lake.Module.serverOptions (self : Lake.Module) : Array Lake.LeanOption

Equations

• Lake.Module.serverOptions self = Lake.LeanLib.serverOptions self.lib

@[inline]

def Lake.Module.buildType (self : Lake.Module) : Lake.BuildType

Equations

• Lake.Module.buildType self = Lake.LeanLib.buildType self.lib

@[inline]

def Lake.Module.backend (self : Lake.Module) : Lake.Backend

Equations

• Lake.Module.backend self = Lake.LeanLib.backend self.lib

@[inline]

def Lake.Module.leanArgs (self : Lake.Module) : Array String

Equations

• Lake.Module.leanArgs self = Lake.LeanLib.leanArgs self.lib

@[inline]

def Lake.Module.weakLeanArgs (self : Lake.Module) : Array String

Equations

• Lake.Module.weakLeanArgs self = Lake.LeanLib.weakLeanArgs self.lib

@[inline]

def Lake.Module.leancArgs (self : Lake.Module) : Array String

Equations

• Lake.Module.leancArgs self = Lake.LeanLib.leancArgs self.lib

@[inline]

def Lake.Module.weakLeancArgs (self : Lake.Module) : Array String

Equations

• Lake.Module.weakLeancArgs self = Lake.LeanLib.weakLeancArgs self.lib

@[inline]

def Lake.Module.linkArgs (self : Lake.Module) : Array String

Equations

• Lake.Module.linkArgs self = Lake.LeanLib.linkArgs self.lib

@[inline]

def Lake.Module.weakLinkArgs (self : Lake.Module) : Array String

Equations

• Lake.Module.weakLinkArgs self = Lake.LeanLib.weakLinkArgs self.lib

@[inline]

def Lake.Module.platformIndependent (self : Lake.Module) : Option Bool

Equations

• Lake.Module.platformIndependent self = Lake.LeanLib.platformIndependent self.lib

@[inline]

def Lake.Module.shouldPrecompile (self : Lake.Module) : Bool

Equations

• Lake.Module.shouldPrecompile self = Lake.LeanLib.precompileModules self.lib

@[inline]

def Lake.Module.nativeFacets (self : Lake.Module) : Array (Lake.ModuleFacet (Lake.BuildJob Lake.FilePath))

Equations

• Lake.Module.nativeFacets self = Lake.LeanLib.nativeFacets self.lib

Trace Helpers

def Lake.Module.getMTime (self : Lake.Module) : IO Lake.MTime

Equations

• One or more equations did not get rendered due to their size.

instance Lake.Module.instGetMTimeModule : Lake.GetMTime Lake.Module

Equations

• Lake.Module.instGetMTimeModule = { getMTime := Lake.Module.getMTime }

def Lake.Module.checkExists (self : Lake.Module) : BaseIO Bool

Equations

• One or more equations did not get rendered due to their size.

instance Lake.Module.instCheckExistsModule : Lake.CheckExists Lake.Module

Equations

• Lake.Module.instCheckExistsModule = { checkExists := Lake.Module.checkExists }