structure Lake.Module : Type

A buildable Lean module of a LeanLib.

• lib : LeanLib
• name : Lean.Name

@[reducible, inline, deprecated Lake.Module.name (since := "2025-11-13")]

abbrev Lake.Module.keyName (self : Module) : Lean.Name

@[implicit_reducible]

instance Lake.instToJsonModule : Lean.ToJson Module

@[implicit_reducible]

instance Lake.instToStringModule : ToString Module

@[implicit_reducible]

instance Lake.instHashableModule : Hashable Module

@[implicit_reducible]

instance Lake.instBEqModule : BEq Module

@[reducible, inline]

abbrev Lake.ModuleSet : Type

@[inline]

def Lake.ModuleSet.empty : ModuleSet

@[reducible, inline]

abbrev Lake.OrdModuleSet : Type

@[inline]

def Lake.OrdModuleSet.empty : OrdModuleSet

@[reducible, inline]

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

@[inline]

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

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

def Lake.LeanLib.findModuleBySrc? (path : System.FilePath) (self : LeanLib) : Option Module

Returns the buildable module in the library whose source file or directory is path.

For example, in a library with a source directory of src, src/Foo/Bar.lean and src/Foo/Bar/ will both resolve to the module Foo.Bar.

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

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

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

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

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

The library's buildable root modules.

@[reducible, inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

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

@[inline]

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

def Lake.Module.dynlibSuffix : String

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

@[inline]

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

@[inline]

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

@[inline]

def Lake.Module.serverOptions (self : Module) : Lean.LeanOptions

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

def Lake.Module.leanOptions (self : Module) : Lean.LeanOptions

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

Trace Helpers

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

@[implicit_reducible]

instance Lake.Module.instGetMTime : GetMTime Module

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

@[implicit_reducible]

instance Lake.Module.instCheckExists : CheckExists Module