Lake.Config.Module

source

structure Lake.Module :

Type

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

A buildable Lean module of a LeanLib.

Instances For

source

instance Lake.instHashableModule :

Hashable Lake.Module

source

instance Lake.instBEqModule :

BEq Lake.Module

source

@[inline, reducible]

abbrev Lake.ModuleSet :

Type

Instances For

source

@[inline]

def Lake.ModuleSet.empty :

Lake.ModuleSet

Instances For

source

@[inline, reducible]

abbrev Lake.OrdModuleSet :

Type

Instances For

source

@[inline]

def Lake.OrdModuleSet.empty :

Lake.OrdModuleSet

Instances For

source

@[inline, reducible]

abbrev Lake.ModuleMap (α : Type u_1) :

Type u_1

Instances For

source

@[inline]

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

Lake.ModuleMap α

Instances For

source

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

Option Lake.Module

Locate the named module in the library (if it is buildable and local to it).

Instances For

source

def Lake.LeanLib.getModuleArray (self : Lake.LeanLib) :

IO (Array Lake.Module)

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

Instances For

source

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

Array Lake.Module

The library's buildable root modules.

Instances For

source

@[inline, reducible]

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

Lake.Package

Instances For

source

@[inline]

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

Lake.FilePath

Instances For

source

@[inline]

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

Lake.FilePath

Instances For

source

@[inline]

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

Lake.FilePath

Instances For

source

@[inline]

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

Lake.FilePath

Instances For

source

@[inline]

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

Lake.FilePath

Instances For

source

@[inline]

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

Lake.FilePath

Instances For

source

@[inline]

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

Lake.FilePath

Instances For

source

@[inline]

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

Lake.FilePath

Instances For

source

@[inline]

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

Lake.FilePath

Instances For

source

@[inline]

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

Lake.FilePath

Instances For

source

@[inline]

def Lake.Module.oFile (self : Lake.Module) :

Lake.FilePath

Instances For

source

@[noinline]

def Lake.Module.dynlibSuffix :

String

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

Instances For

source

@[inline]

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

String

Instances For

source

@[inline]

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

Lake.FilePath

Instances For

source

@[inline]

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

Lake.BuildType

Instances For

source

@[inline]

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

Array String

Instances For

source

@[inline]

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

Array String

Instances For

source

@[inline]

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

Array String

Instances For

source

@[inline]

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

Array String

Instances For

source

@[inline]

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

Bool

Instances For

source

@[inline]

def Lake.Module.nativeFacets (self : Lake.Module) :

Array (Lake.ModuleFacet (Lake.BuildJob Lake.FilePath))

Instances For

Trace Helpers #

source

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

IO Lake.MTime

Instances For

source

instance Lake.Module.instGetMTimeModule :

Lake.GetMTime Lake.Module

source

def Lake.Module.computeHash (self : Lake.Module) :

IO Lake.Hash

Instances For

source

instance Lake.Module.instComputeHashModuleIO :

Lake.ComputeHash Lake.Module IO

source

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

BaseIO Bool

Instances For

source

instance Lake.Module.instCheckExistsModule :

Lake.CheckExists Lake.Module