Documentation

Lake.Config.LeanExeConfig

  • 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 executable's Lean source file. Defaults simply to said srcDir.

    (This will be passed to lean as the -R option.)

  • root : Lake.Name

    The root module of the binary executable. Should include a main definition that will serve as the entry point of the program.

    The root is built by recursively building its local imports (i.e., fellow modules of the workspace).

    Defaults to the name of the target.

  • exeName : String

    The name of the binary executable. Defaults to the target name with any . replaced with a -.

  • extraDepTargets : Array Lake.Name

    An Array of target names to build before the executable's modules.

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

  • supportInterpreter : Bool

    Enables the executable to interpret Lean files (e.g., via Lean.Elab.runFrontend) by exposing symbols within the executable to the Lean interpreter.

    Implementation-wise, this passes -rdynamic to the linker when building on non-Windows systems. This increases the size of the binary on Linux, so this feature should only be enabled when necessary.

    Defaults to false.

A Lean executable's declarative configuration.

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