structure Lake.Module : Type

A buildable Lean module of a LeanLib.

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

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

Instances For

• Lake.Module.instCheckExists
• Lake.Module.instGetMTime
• Lake.instBEqModule
• Lake.instDataKindModule
• Lake.instFamilyDefNameDataTypeMkStr1Module
• Lake.instHashableModule
• Lake.instToJsonModule
• Lake.instToTextModule

instance Lake.instToTextModule : ToText Module

Equations

• Lake.instToTextModule = { toText := fun (x : Lake.Module) => x.name.toString }

instance Lake.instToJsonModule : Lean.ToJson Module

Equations

• Lake.instToJsonModule = { toJson := fun (x : Lake.Module) => Lean.toJson x.name }

instance Lake.instHashableModule : Hashable Module

Equations

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

instance Lake.instBEqModule : BEq Module

Equations

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

@[reducible, inline]

abbrev Lake.ModuleSet : Type

Equations

• Lake.ModuleSet = Std.HashSet Lake.Module

@[inline]

def Lake.ModuleSet.empty : ModuleSet

Equations

• Lake.ModuleSet.empty = ∅

@[reducible, inline]

abbrev Lake.OrdModuleSet : Type

Equations

• Lake.OrdModuleSet = Lake.OrdHashSet Lake.Module

@[inline]

def Lake.OrdModuleSet.empty : 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} : ModuleMap α

Equations

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

def Lake.LeanLib.findModule? (mod : Lean.Name) (self : LeanLib) : Option 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 } else none

def Lake.Package.findModule? (mod : Lean.Name) (self : Package) : Option 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 : LeanLib) : IO (Array 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 : LeanLib) : Array Module

The library's buildable root modules.

Equations

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

@[reducible, inline]

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

Equations

• self.pkg = self.lib.pkg

@[inline]

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

Equations

• self.rootDir = self.lib.rootDir

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

• Lake.Module.irPath ext self = Lake.Module.filePath self.pkg.irDir ext self

@[inline]

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

Equations

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

@[inline]

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

Equations

• self.coExportFile = Lake.Module.irPath "c.o.export" self

@[inline]

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

Equations

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

@[inline]

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

Equations

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

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

Equations

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

@[inline]

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

Equations

• self.bcoFile = 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 : Module) : String

Equations

• self.dynlibName = self.name.mangle ""

@[inline]

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

Equations

• self.dynlibFile = self.pkg.leanLibDir / { toString := toString "" ++ toString self.dynlibName ++ toString "." ++ toString Lake.sharedLibExt ++ toString "" }

@[inline]

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

Equations

• self.serverOptions = self.lib.serverOptions

@[inline]

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

Equations

• self.buildType = self.lib.buildType

@[inline]

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

Equations

• self.backend = self.lib.backend

@[inline]

def Lake.Module.dynlibs (self : Module) : TargetArray Dynlib

Equations

• self.dynlibs = self.lib.dynlibs

@[inline]

def Lake.Module.plugins (self : Module) : TargetArray Dynlib

Equations

• self.plugins = self.lib.plugins

@[inline]

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

Equations

• self.leanArgs = self.lib.leanArgs

@[inline]

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

Equations

• self.weakLeanArgs = self.lib.weakLeanArgs

@[inline]

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

Equations

• self.leancArgs = self.lib.leancArgs

@[inline]

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

Equations

• self.weakLeancArgs = self.lib.weakLeancArgs

@[inline]

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

Equations

• self.linkArgs = self.lib.linkArgs

@[inline]

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

Equations

• self.weakLinkArgs = self.lib.weakLinkArgs

@[inline]

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

Equations

• self.platformIndependent = self.lib.platformIndependent

@[inline]

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

Equations

• self.shouldPrecompile = self.lib.precompileModules

@[inline]

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

Equations

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

Trace Helpers

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

Equations

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

instance Lake.Module.instGetMTime : GetMTime Module

Equations

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

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

Equations

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

instance Lake.Module.instCheckExists : CheckExists Module

Equations

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