inductive Lake.BuildType : Type

Lake equivalent of CMake's CMAKE_BUILD_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).

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 : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Lake.instOrdBuildType : Ord Lake.BuildType

Equations

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

instance Lake.instLTBuildType : LT Lake.BuildType

Ordering on build types. The ordering is used to determine the minimum build version that is necessary for a build.

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

inductive Lake.Backend : Type

Compiler backend with which to compile Lean.

• c: Lake.Backend

  Force the C backend.

• llvm: Lake.Backend

  Force the LLVM backend.

• default: Lake.Backend

  Use the default backend. Can be overridden by more specific configuration.

instance Lake.instReprBackend : Repr Lake.Backend

Equations

• Lake.instReprBackend = { reprPrec := Lake.reprBackend✝ }

instance Lake.instDecidableEqBackend : DecidableEq Lake.Backend

Equations

• Lake.instDecidableEqBackend x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Lake.instInhabitedBackend : Inhabited Lake.Backend

Equations

• Lake.instInhabitedBackend = { default := Lake.Backend.default }

def Lake.Backend.ofString? (s : String) : Option Lake.Backend

Equations

• Lake.Backend.ofString? "c" = some Lake.Backend.c
• Lake.Backend.ofString? "llvm" = some Lake.Backend.llvm
• Lake.Backend.ofString? "default" = some Lake.Backend.default
• Lake.Backend.ofString? s = none

def Lake.Backend.toString (bt : Lake.Backend) : String

Equations

• Lake.Backend.c.toString = "c"
• Lake.Backend.llvm.toString = "llvm"
• Lake.Backend.default.toString = "default"

instance Lake.instToStringBackend : ToString Lake.Backend

Equations

• Lake.instToStringBackend = { toString := Lake.Backend.toString }

def Lake.Backend.orPreferLeft : Lake.Backend → Lake.Backend → Lake.Backend

If the left backend is default, choose the right one. Otherwise, keep the left one. This is used to implement preferential choice of backends, where the library config can refine the package config. Formally, a left absorbing monoid on {C, LLVM} with Default as the unit.

Equations

• Lake.Backend.default.orPreferLeft x = x
• x✝.orPreferLeft x = x✝

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

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

Equations

• Lake.BuildType.debug.leancArgs = #["-Og", "-g"]
• Lake.BuildType.relWithDebInfo.leancArgs = #["-O3", "-g", "-DNDEBUG"]
• Lake.BuildType.minSizeRel.leancArgs = #["-Os", "-DNDEBUG"]
• Lake.BuildType.release.leancArgs = #["-O3", "-DNDEBUG"]

def Lake.BuildType.ofString? (s : String) : Option Lake.BuildType

Equations

• Lake.BuildType.ofString? "debug" = some Lake.BuildType.debug
• Lake.BuildType.ofString? "relWithDebInfo" = some Lake.BuildType.relWithDebInfo
• Lake.BuildType.ofString? "minSizeRel" = some Lake.BuildType.minSizeRel
• Lake.BuildType.ofString? "release" = some Lake.BuildType.release
• Lake.BuildType.ofString? s = none

def Lake.BuildType.toString (bt : Lake.BuildType) : String

Equations

• Lake.BuildType.debug.toString = "debug"
• Lake.BuildType.relWithDebInfo.toString = "relWithDebInfo"
• Lake.BuildType.minSizeRel.toString = "minSizeRel"
• Lake.BuildType.release.toString = "release"

instance Lake.instToStringBuildType : ToString Lake.BuildType

Equations

• Lake.instToStringBuildType = { toString := Lake.BuildType.toString }

structure Lake.LeanOption : Type

Option that is used by Lean as if it was passed using -D.

• name : Lean.Name
• value : Lean.LeanOptionValue

instance Lake.instInhabitedLeanOption : Inhabited Lake.LeanOption

Equations

• Lake.instInhabitedLeanOption = { default := { name := default, value := default } }

instance Lake.instReprLeanOption : Repr Lake.LeanOption

Equations

• Lake.instReprLeanOption = { reprPrec := Lake.reprLeanOption✝ }

def Lake.LeanOption.asCliArg (o : Lake.LeanOption) : String

Formats the lean option as a CLI argument using the -D flag.

Equations

• o.asCliArg = toString "-D" ++ toString o.name ++ toString "=" ++ toString o.value.asCliFlagValue ++ toString ""

structure Lake.LeanConfig : Type

Configuration options common to targets that build modules.

• buildType : Lake.BuildType

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

• leanOptions : Array Lake.LeanOption

  Additional options to pass to both the Lean language server (i.e., lean --server) launched by lake serve and to lean when compiling a module's Lean source files.

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

• moreServerOptions : Array Lake.LeanOption

  Additional options to pass to the Lean language server (i.e., lean --server) launched by lake serve.

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

• backend : Lake.Backend

  Compiler backend that modules should be built using (e.g., C, LLVM). Defaults to C.

• platformIndependent : Option Bool

  Asserts whether Lake should assume Lean modules are platform-independent.

  • If false, Lake will add System.Platform.target to the module traces within the code unit (e.g., package or library). This will force Lean code to be re-elaborated on different platforms.

  • If true, Lake will exclude platform-dependent elements (e.g., precompiled modules, external libraries) from a module's trace, preventing re-elaboration on different platforms. Note that this will not effect modules outside the code unit in question. For example, a platform-independent package which depends on a platform-dependent library will still be platform-dependent.

  • If none, Lake will construct traces as natural. That is, it will include platform-dependent artifacts in the trace if they module depends on them, but otherwise not force modules to be platform-dependent.

  There is no check for correctness here, so a configuration can lie and Lake will not catch it. Defaults to none.

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✝ }