source
@[reducible, inline]
abbrev Lake.LeanLib :
Type

A Lean library -- its package plus its configuration.

Equations

- Lake.LeanLib = Lake.ConfigTarget Lake.LeanLib.configKind

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[inline]
def Lake.LeanLib.config (self : LeanLib) :
LeanLibConfig self.name

The library's user-defined configuration.

Equations

- self.config = self.config

Instances For

source
@[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

Instances For

source
@[inline]
def Lake.LeanLib.rootDir (self : LeanLib) :
System.FilePath

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

Equations

- self.rootDir = self.srcDir

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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)

Instances For

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

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

Equations

- self.libName = if (self.libPrefixOnWindows && System.Platform.isWindows) = true then toString "lib" ++ toString self.config.libName else self.config.libName

Instances For

source
@[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 }

Instances For

source
@[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

Instances For

source
@[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"

Instances For

source
@[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 }

Instances For

source
@[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

Instances For

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

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

Equations

- self.isPlugin = (self.roots == #[self.name] && self.libName == self.name.mangle "")

Instances For

source
@[inline]
def Lake.LeanLib.extraDepTargets (self : LeanLib) :
Array Lean.Name

The library's `extraDepTargets` configuration.

Equations

- self.extraDepTargets = self.config.extraDepTargets

Instances For

source
@[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)

Instances For

source
@[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)

Instances For

source
@[inline]
def Lake.LeanLib.defaultFacets (self : LeanLib) :
Array Lean.Name

The library's `defaultFacets` configuration.

Equations

- self.defaultFacets = self.config.defaultFacets

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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)

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[inline]
def Lake.LeanLib.moreLinkObjs (self : LeanLib) :
TargetArray System.FilePath

Additionl 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

Instances For

source
@[inline]
def Lake.LeanLib.moreLinkLibs (self : LeanLib) :
TargetArray Dynlib
Equations

- self.moreLinkLibs = self.pkg.moreLinkLibs ++ self.config.moreLinkLibs

Instances For

source
@[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

Instances For

source
@[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

Instances For