structure Lake.Module : Type

A buildable Lean module of a LeanLib.

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

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

instance Lake.instHashableModule : Hashable Lake.Module

instance Lake.instBEqModule : BEq Lake.Module

Equations

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

@[reducible, inline]

abbrev Lake.ModuleSet : Type

@[inline]

def Lake.ModuleSet.empty : Lake.ModuleSet

Equations

• Lake.ModuleSet.empty = Std.HashSet.empty

@[reducible, inline]

abbrev Lake.OrdModuleSet : Type

@[inline]

def Lake.OrdModuleSet.empty : Lake.OrdModuleSet

Equations

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

@[reducible, inline]

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

Equations

• Lake.ModuleMap α = Lean.RBMap Lake.Module α fun (x1 x2 : Lake.Module) => x1.name.quickCmp x2.name

@[inline]

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

Equations

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

def Lake.LeanLib.findModule? (mod : Lean.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 : Lean.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? (fun (x : Lake.LeanLib) => Lake.LeanLib.findModule? mod x) self.leanLibs

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

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

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

The library's buildable root modules.

@[reducible, inline]

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

Equations

• self.pkg = self.lib.pkg

@[inline]

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

@[inline]

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

@[inline]

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

Equations

• Lake.Module.srcPath ext self = Lake.Module.filePath self.lib.srcDir ext self

@[inline]

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

@[inline]

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

Equations

• Lake.Module.leanLibPath ext self = Lake.Module.filePath self.pkg.leanLibDir ext self

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

Equations

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

@[inline]

def Lake.Module.coExportFile (self : Lake.Module) : System.FilePath

@[inline]

def Lake.Module.coNoExportFile (self : Lake.Module) : System.FilePath

Equations

• self.coNoExportFile = Lake.Module.irPath "c.o.noexport" self

@[inline]

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

def Lake.Module.bcFile? (self : Lake.Module) : Option System.FilePath

Equations

• self.bcFile? = if Lean.Internal.hasLLVMBackend () = true then some self.bcFile else none

@[inline]

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

def Lake.Module.dynlibSuffix : String

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

@[inline]

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

Equations

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

@[inline]

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

Equations

• self.dynlibFile = self.pkg.nativeLibDir / { toString := Lake.nameToSharedLib self.dynlibName }

@[inline]

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

Equations

• self.serverOptions = self.lib.serverOptions

@[inline]

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

@[inline]

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

Equations

• self.backend = self.lib.backend

@[inline]

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

@[inline]

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

@[inline]

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

Equations

• self.leancArgs = self.lib.leancArgs

@[inline]

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

Equations

• self.weakLeancArgs = self.lib.weakLeancArgs

@[inline]

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

@[inline]

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

Equations

• self.weakLinkArgs = self.lib.weakLinkArgs

@[inline]

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

Equations

• self.platformIndependent = self.lib.platformIndependent

@[inline]

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

@[inline]

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

Equations

• self.nativeFacets shouldExport = self.lib.nativeFacets shouldExport

Trace Helpers

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

instance Lake.Module.instGetMTime : Lake.GetMTime Lake.Module

Equations

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

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

instance Lake.Module.instCheckExists : Lake.CheckExists Lake.Module