A Lean library's declarative configuration.
- srcDir : System.FilePath
The subdirectory of the package's source directory containing the library's Lean source files. Defaults simply to said
srcDir
.(This will be passed to
lean
as the-R
option.) The root module(s) of the library. Submodules of these roots (e.g.,
Lib.Foo
ofLib
) are considered part of the library. Defaults to a single root of the target's name.- libName : String
The name of the library artifact. Used as a base for the file names of its static and dynamic binaries. Defaults to the mangled name of the target.
- needs : Array PartialBuildKey
An
Array
of targets to build before the executable's modules. - precompileModules : Bool
Whether to compile each of the library's modules into a native shared library that is loaded whenever the module is imported. This speeds up evaluation of metaprograms and enables the interpreter to run functions marked
@[extern]
.Defaults to
false
. An
Array
of library facets to build on a barelake build
of the library. For example,#[LeanLib.sharedLib]
will build the shared library facet.- nativeFacets (shouldExport : Bool) : Array (ModuleFacet System.FilePath)
The module facets to build and combine into the library's static and shared libraries. If
shouldExport
is true, the module facets should export any symbols a user may expect to lookup in the library. For example, the Lean interpreter will use exported symbols in linked libraries.Defaults to a singleton of
Module.oExportFacet
(ifshouldExport
) orModule.oFacet
. That is, the object files compiled from the Lean sources, potentially with exported Lean symbols.
Instances For
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
The library's name.
Equations
Instances For
Whether the given module is considered local to the library.
Equations
Instances For
Whether the given module is a buildable part of the library.