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.

instance Lake.instInhabitedBuildType : Inhabited Lake.BuildType

Equations

• Lake.instInhabitedBuildType = { default := Lake.BuildType.debug }

instance Lake.instReprBuildType : Repr Lake.BuildType

Equations

• Lake.instReprBuildType = { reprPrec := Lake.reprBuildType✝ }

instance Lake.instDecidableEqBuildType : DecidableEq Lake.BuildType

Equations

• Lake.instDecidableEqBuildType x y = if h : Lake.BuildType.toCtorIdx x = Lake.BuildType.toCtorIdx y then isTrue (_ : x = y) else isFalse (_ : x = y → False)

instance Lake.instOrdBuildType : Ord Lake.BuildType

Equations

• Lake.instOrdBuildType = { compare := Lake.ordBuildType✝ }

instance Lake.instLTBuildType : LT Lake.BuildType

Equations

• Lake.instLTBuildType = ltOfOrd

instance Lake.instLEBuildType : LE Lake.BuildType

Equations

• Lake.instLEBuildType = leOfOrd

instance Lake.instMinBuildType : Min Lake.BuildType

Equations

• Lake.instMinBuildType = minOfLe

instance Lake.instMaxBuildType : Max Lake.BuildType

Equations

• Lake.instMaxBuildType = maxOfLe

def Lake.BuildType.leancArgs : Lake.BuildType → Array String

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

Equations

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

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. They come before moreLeanArgs.

• 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.

• weakLeancArgs : Array String

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

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

• 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.

• weakLinkArgs : 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.

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

Configuration options common to targets that build modules.

instance Lake.instInhabitedLeanConfig : Inhabited Lake.LeanConfig

Equations

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

instance Lake.instReprLeanConfig : Repr Lake.LeanConfig

Equations

• Lake.instReprLeanConfig = { reprPrec := Lake.reprLeanConfig✝ }