Documentation

Lake.Config.LeanLibConfig

  • buildType : Lake.BuildType
  • moreLeanArgs : Array String
  • weakLeanArgs : Array String
  • moreLeancArgs : Array String
  • weakLeancArgs : Array String
  • moreLinkArgs : Array String
  • weakLinkArgs : 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 Glob.one 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
    Equations
    • One or more equations did not get rendered due to their size.

    Whether the given module is considered local to the library.

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

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

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