• buildType : Lake.BuildType
  • moreLeanArgs : Array String
  • weakLeanArgs : Array String
  • moreLeancArgs : Array String
  • moreLinkArgs : Array String
  • name : Lake.Name

    The name of the target.

  • srcDir : Lake.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 of Lib) are considered part of the package.

    Defaults to a single root of the library's upper camel case name.

  • An Array of module Globs to build for the library. Defaults to a of each of the library's roots.

    Submodule globs build every source file within their directory. Local imports of glob'ed files (i.e., fellow modules of the workspace) are also recursively built.

  • libName : String

    The name of the library. Used as a base for the file names of its static and dynamic binaries. Defaults to the upper camel case name of the target.

  • extraDepTargets : Array Lake.Name

    An Array of target names to build before the library'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.

  • defaultFacets : Array Lake.Name

    An Array of library facets to build on a bare lake build of the library. For example, #[LeanLib.sharedLib] will build the shared library facet.

  • An Array of module facets to build and combine into the library's static and shared libraries. Defaults to #[Module.oFacet] (i.e., the object file compiled from the Lean source).

A Lean library's declarative configuration.

Instances For

    Whether the given module is considered local to the library.

    Instances For

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

      Instances For