Documentation

Lake.Config.LeanLib

structure Lake.LeanLib :

A Lean library -- its package plus its configuration.

@[inline]

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

Equations
@[inline]

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

Equations
@[inline]

The library's well-formed name.

Equations
  • self.name = self.config.name
@[inline]

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

Equations
  • self.srcDir = self.pkg.srcDir / self.config.srcDir
@[inline]

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

Equations
  • self.rootDir = self.srcDir
@[inline]

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

Equations
  • self.roots = self.config.roots
@[inline]

Whether the given module is considered local to the library.

Equations
@[inline]

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

Equations
@[inline]

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

Equations
@[inline]

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

Equations
  • self.staticLibFile = self.pkg.nativeLibDir / self.staticLibFileName
@[inline]

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

Equations
  • self.staticExportLibFile = self.pkg.nativeLibDir / self.staticLibFileName.addExtension "export"
@[inline]

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

Equations
@[inline]

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

Equations
  • self.sharedLibFile = self.pkg.nativeLibDir / self.sharedLibFileName
@[inline]

The library's extraDepTargets configuration.

Equations
  • self.extraDepTargets = self.config.extraDepTargets
@[inline]

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]

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]

The library's defaultFacets configuration.

Equations
  • self.defaultFacets = self.config.defaultFacets
@[inline]

The library's nativeFacets configuration.

Equations
  • self.nativeFacets shouldExport = self.config.nativeFacets shouldExport
@[inline]

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

  • the package's leanOptions
  • the package's moreServerOptions
  • the library's leanOptions
  • the library's moreServerOptions
Equations
  • self.serverOptions = self.pkg.moreServerOptions ++ self.config.leanOptions ++ self.config.moreServerOptions
@[inline]

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]

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]

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

  • the package's leanOptions
  • the package's moreLeanArgs
  • the library's leanOptions
  • the library's moreLeanArgs
Equations
@[inline]

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]

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]

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]

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]

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