Documentation

Lake.Config.LeanConfig

source
inductive Lake.BuildType :
Type
  • debug: Lake.BuildType

    Debug optimization, asserts enabled, custom debug code enabled, and debug info included in executable (so you can step through the code with a debugger and have address to source-file:line-number translation). For example, passes -Og -g when compiling C code.

  • relWithDebInfo: Lake.BuildType

    Optimized, with debug info, but no debug code or asserts (e.g., passes -O3 -g -DNDEBUG when compiling C code).

  • minSizeRel: Lake.BuildType

    Same as release but optimizing for size rather than speed (e.g., passes -Os -DNDEBUG when compiling C code).

  • release: Lake.BuildType

    High optimization level and no debug info, code, or asserts (e.g., passes -O3 -DNDEBUG when compiling C code).

Lake equivalent of CMake's CMAKE_BUILD_TYPE.

Instances For
    source
    instance Lake.instInhabitedBuildType :
    Inhabited Lake.BuildType
    source
    instance Lake.instReprBuildType :
    Repr Lake.BuildType
    source
    instance Lake.instDecidableEqBuildType :
    DecidableEq Lake.BuildType
    source
    instance Lake.instOrdBuildType :
    Ord Lake.BuildType
    source
    instance Lake.instLTBuildType :
    LT Lake.BuildType
    source
    instance Lake.instLEBuildType :
    LE Lake.BuildType
    source
    instance Lake.instMinBuildType :
    Min Lake.BuildType
    source
    instance Lake.instMaxBuildType :
    Max Lake.BuildType
    source
    def Lake.BuildType.leancArgs :
    Lake.BuildType → Array String

    The arguments to pass to leanc based on the build type.

    Instances For
      source
      structure Lake.LeanConfig :
      Type
      • buildType : Lake.BuildType

        The mode in which the modules should be built (e.g., debug, release). Defaults to release.

      • moreLeanArgs : Array String

        Additional arguments to pass to lean when compiling a module's Lean source files.

      • weakLeanArgs : Array String

        Additional arguments to pass to lean when compiling a module's Lean source files.

        Unlike moreLeanArgs, these arguments do not affect the trace of the build result, so they can be changed without triggering a rebuild.

      • moreLeancArgs : Array String

        Additional arguments to pass to leanc when compiling a module's C source files generated by lean.

        Lake already passes some flags based on the buildType, but you can change this by, for example, adding -O0 and -UNDEBUG.

      • moreLinkArgs : Array String

        Additional arguments to pass to leanc when linking (e.g., for shared libraries or binary executables). These will come after the paths of external libraries.

      Configuration options common to targets that build modules.

      Instances For
        source
        instance Lake.instInhabitedLeanConfig :
        Inhabited Lake.LeanConfig
        source
        instance Lake.instReprLeanConfig :
        Repr Lake.LeanConfig