@[reducible, inline]

abbrev Lake.LeanLib : Type

A Lean library -- its package plus its configuration.

Equations

• Lake.LeanLib = Lake.ConfigTarget Lake.LeanLib.configKind

@[inline]

def Lake.Package.leanLibs (self : Package) : Array LeanLib

The Lean libraries of the package (as an Array).

Equations

• self.leanLibs = Lake.Package.configTargets Lake.LeanLib.configKind self

@[inline]

def Lake.Package.findLeanLib? (name : Lean.Name) (self : Package) : Option LeanLib

Try to find a Lean library in the package with the given name.

Equations

• Lake.Package.findLeanLib? name self = Lake.Package.findConfigTarget? Lake.LeanLib.configKind name self

@[inline]

def Lake.LeanLib.config (self : LeanLib) : LeanLibConfig self.name

The library's user-defined configuration.

Equations

• self.config = self.config

@[inline]

def Lake.LeanLib.srcDir (self : LeanLib) : System.FilePath

The package's srcDir joined with the library's srcDir.

Equations

• self.srcDir = self.pkg.srcDir / self.config.srcDir.normalize

@[inline]

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

The library's root directory for lean (i.e., srcDir).

Equations

• self.rootDir = self.srcDir

@[inline]

def Lake.LeanLib.roots (self : LeanLib) : Array Lean.Name

The names of the library's root modules (i.e., the library's roots configuration).

Equations

• self.roots = self.config.roots

@[inline]

def Lake.LeanLib.isLocalModule (mod : Lean.Name) (self : LeanLib) : Bool

Whether the given module is considered local to the library.

Equations

• Lake.LeanLib.isLocalModule mod self = Lake.LeanLibConfig.isLocalModule mod self.config

@[inline]

def Lake.LeanLib.isBuildableModule (mod : Lean.Name) (self : LeanLib) : Bool

Whether the given module is a buildable part of the library.

Equations

• Lake.LeanLib.isBuildableModule mod self = Lake.LeanLibConfig.isBuildableModule mod self.config

@[inline]

def Lake.LeanLib.libPrefixOnWindows (self : LeanLib) : Bool

Whether this library's native binaries should be prefixed with lib on Windows.

Equations

• self.libPrefixOnWindows = (self.config.libPrefixOnWindows || self.pkg.libPrefixOnWindows)

def Lake.LeanLib.libName (self : LeanLib) : String

The name of the native library (e.g., what is passed to -l).

Equations

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

@[inline]

def Lake.LeanLib.staticLibFileName (self : LeanLib) : System.FilePath

The file name of the library's static binary (i.e., its .a)

Equations

• self.staticLibFileName = { toString := Lake.nameToStaticLib self.libName }

@[inline]

def Lake.LeanLib.staticLibFile (self : LeanLib) : System.FilePath

The path to the static library in the package's libDir.

Equations

• self.staticLibFile = self.pkg.staticLibDir / self.staticLibFileName

@[inline]

def Lake.LeanLib.staticExportLibFile (self : LeanLib) : System.FilePath

The path to the static library (with exported symbols) in the package's libDir.

Equations

• self.staticExportLibFile = self.pkg.staticLibDir / self.staticLibFileName.addExtension "export"

@[inline]

def Lake.LeanLib.sharedLibFileName (self : LeanLib) : System.FilePath

The file name of the library's shared binary (i.e., its dll, dylib, or so) .

Equations

• self.sharedLibFileName = { toString := Lake.nameToSharedLib self.libName }

@[inline]

def Lake.LeanLib.sharedLibFile (self : LeanLib) : System.FilePath

The path to the shared library in the package's libDir.

Equations

• self.sharedLibFile = self.pkg.sharedLibDir / self.sharedLibFileName

def Lake.LeanLib.isPlugin (self : LeanLib) : Bool

Whether the shared binary of this library is a valid plugin.

Equations

• self.isPlugin = if h : self.roots.size = 1 then self.libName == Lean.mkModuleInitializationStem self.roots[0] self.pkg.id? else false

@[inline]

def Lake.LeanLib.extraDepTargets (self : LeanLib) : Array Lean.Name

The library's extraDepTargets configuration.

Equations

• self.extraDepTargets = self.config.extraDepTargets

@[inline]

def Lake.LeanLib.precompileModules (self : LeanLib) : Bool

Whether to precompile the library's modules. Is true if either the package or the library have precompileModules set.

Equations

• self.precompileModules = (self.pkg.precompileModules || self.config.precompileModules)

@[inline]

def Lake.LeanLib.precompileImports (self : LeanLib) : Bool

Whether to precompile the imports of the library's modules. Is true if either the package or the library have precompileImports set, or if the library's modules are precompiled.

Equations

• self.precompileImports = (self.precompileModules || self.pkg.precompileImports || self.config.precompileImports)

@[inline]

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

Whether to precompile the library for importers. Is true if the library has precompileLibrary set or its modules are precompiled.

Equations

• self.shouldPrecompile = (self.precompileModules || self.config.precompileLibrary)

@[inline]

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

Whether to the library's Lean code is platform-independent. Returns the library's platformIndependent configuration if non-none. Otherwise, falls back to the package's.

Equations

• self.platformIndependent = (self.config.platformIndependent <|> self.pkg.platformIndependent)

@[inline]

def Lake.LeanLib.defaultFacets (self : LeanLib) : Array Lean.Name

The library's defaultFacets configuration.

Equations

• self.defaultFacets = self.config.defaultFacets

@[inline]

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

The library's nativeFacets configuration.

Equations

• self.nativeFacets shouldExport = self.config.nativeFacets shouldExport

@[inline]

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

The build type for modules of this library. That is, the minimum of package's buildType and the library's buildType.

Equations

• self.buildType = min self.pkg.buildType self.config.buildType

@[inline]

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

The arguments to pass to lean --server when running the Lean language server. serverOptions is the accumulation of:

• the build type's leanOptions
• the package's leanOptions
• the package's moreServerOptions
• the library's leanOptions
• the library's moreServerOptions

Equations

• self.serverOptions = ∅ ++ self.buildType.leanOptions ++ self.pkg.moreServerOptions ++ self.config.leanOptions ++ self.config.moreServerOptions

@[inline]

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

The backend type for modules of this library. Prefer the library's backend configuration, then the package's, then the default (which is C for now).

Equations

• self.backend = self.config.backend.orPreferLeft self.pkg.backend

@[inline]

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

Whether downstream packages can import all modules of this library. Enabled if either the library or the package enables it.

Equations

• self.allowImportAll = (self.config.allowImportAll || self.pkg.allowImportAll)

@[inline]

def Lake.LeanLib.requiresModuleSystem (self : LeanLib) : Bool

Whether modules of this library are designed for use with the module system. Enabled if either the library or the package enables it.

Equations

• self.requiresModuleSystem = (self.config.requiresModuleSystem || self.pkg.requiresModuleSystem)

@[inline]

def Lake.LeanLib.allowNonModules (self : LeanLib) : Bool

Whether modules of this library may be non-module-system files without warning. Enabled if either the library or the package enables it.

Equations

• self.allowNonModules = (self.config.allowNonModules || self.pkg.allowNonModules)

@[inline]

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

The dynamic libraries to load for modules of this library. The targets of the package plus the targets of the library (in that order).

Equations

• self.dynlibs = self.pkg.dynlibs ++ self.config.dynlibs

@[inline]

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

The Lean plugins for modules of this library. The targets of the package plus the targets of the library (in that order).

Equations

• self.plugins = self.pkg.plugins ++ self.config.plugins

@[inline]

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

The arguments to pass to lean when compiling the library's Lean files. leanArgs is the accumulation of:

• the build type's leanOptions
• the package's leanOptions
• the library's leanOptions

Equations

• self.leanOptions = self.buildType.leanOptions ++ self.pkg.leanOptions ++ self.config.leanOptions

@[inline]

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

The arguments to pass to lean when compiling the library's Lean files. leanArgs is the accumulation of:

• the build type's leanArgs
• the package's moreLeanArgs
• the library's moreLeanArgs

Equations

• self.leanArgs = self.buildType.leanArgs ++ self.pkg.moreLeanArgs ++ self.config.moreLeanArgs

@[inline]

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

The arguments to weakly pass to lean when compiling the library's Lean files. That is, the package's weakLeanArgs plus the library's weakLeanArgs.

Equations

• self.weakLeanArgs = self.pkg.weakLeanArgs ++ self.config.weakLeanArgs

@[inline]

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

The arguments to pass to leanc when compiling the library's Lean-produced C files. That is, the build type's leancArgs, the package's moreLeancArgs, and then the library's moreLeancArgs.

Equations

• self.leancArgs = self.buildType.leancArgs ++ self.pkg.moreLeancArgs ++ self.config.moreLeancArgs

@[inline]

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

The arguments to weakly pass to leanc when compiling the library's Lean-produced C files. That is, the package's weakLeancArgs plus the library's weakLeancArgs.

Equations

• self.weakLeancArgs = self.pkg.weakLeancArgs ++ self.config.weakLeancArgs

@[inline]

def Lake.LeanLib.moreLinkObjs (self : LeanLib) : TargetArray System.FilePath

Additional target objects to pass to ar when linking the static library. That is, the package's moreLinkObjs plus the library's moreLinkObjs.

Equations

• self.moreLinkObjs = self.pkg.moreLinkObjs ++ self.config.moreLinkObjs

@[inline]

def Lake.LeanLib.moreLinkLibs (self : LeanLib) : TargetArray Dynlib

Additional target libraries to are linked to the shared library. That is, the package's moreLinkLibs plus the library's moreLinkLibs.

Equations

• self.moreLinkLibs = self.pkg.moreLinkLibs ++ self.config.moreLinkLibs

@[inline]

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

The arguments to pass to leanc when linking the shared library. That is, the package's moreLinkArgs plus the library's moreLinkArgs.

Equations

• self.linkArgs = self.pkg.moreLinkArgs ++ self.config.moreLinkArgs

@[inline]

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

The arguments to weakly pass to leanc when linking the shared library. That is, the package's weakLinkArgs plus the library's weakLinkArgs.

Equations

• self.weakLinkArgs = self.pkg.weakLinkArgs ++ self.config.weakLinkArgs