Lake.Config.LeanConfig

source

inductive Lake.Backend :

Type

Compiler backend with which to compile Lean.

c : Backend
Force the C backend.
llvm : Backend
Force the LLVM backend.
default : Backend
Use the default backend. Can be overridden by more specific configuration.

Instances For

source

def Lake.instReprBackend.repr :

Backend → Nat → Std.Format

Equations

Lake.instReprBackend.repr Lake.Backend.c prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.Backend.c")).group prec✝
Lake.instReprBackend.repr Lake.Backend.llvm prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.Backend.llvm")).group prec✝
Lake.instReprBackend.repr Lake.Backend.default prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.Backend.default")).group prec✝

Instances For

source

instance Lake.instReprBackend :

Repr Backend

Equations

Lake.instReprBackend = { reprPrec := Lake.instReprBackend.repr }

source

instance Lake.instDecidableEqBackend :

DecidableEq Backend

Equations

Lake.instDecidableEqBackend x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance Lake.Backend.instInhabited :

Inhabited Backend

Equations

Lake.Backend.instInhabited = { default := Lake.Backend.default }

source

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

Option 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

Instances For

source

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

String

Equations

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

Instances For

source

def Lake.Backend.orPreferLeft :

Backend → Backend → 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✝¹

Instances For

source

inductive Lake.BuildType :

Type

Lake equivalent of CMake's CMAKE_BUILD_TYPE.

debug : 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 : BuildType
Optimized, with debug info, but no debug code or asserts (e.g., passes -O3 -g -DNDEBUG when compiling C code).
minSizeRel : BuildType
Same as release but optimizing for size rather than speed (e.g., passes -Os -DNDEBUG when compiling C code).
release : BuildType
High optimization level and no debug info, code, or asserts (e.g., passes -O3 -DNDEBUG when compiling C code).

Instances For

source

instance Lake.instInhabitedBuildType :

Inhabited BuildType

Equations

Lake.instInhabitedBuildType = { default := Lake.instInhabitedBuildType.default }

source

def Lake.instInhabitedBuildType.default :

BuildType

Equations

Lake.instInhabitedBuildType.default = Lake.BuildType.debug

Instances For

source

instance Lake.instReprBuildType :

Repr BuildType

Equations

Lake.instReprBuildType = { reprPrec := Lake.instReprBuildType.repr }

source

def Lake.instReprBuildType.repr :

BuildType → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.
Lake.instReprBuildType.repr Lake.BuildType.debug prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.BuildType.debug")).group prec✝
Lake.instReprBuildType.repr Lake.BuildType.minSizeRel prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.BuildType.minSizeRel")).group prec✝
Lake.instReprBuildType.repr Lake.BuildType.release prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.BuildType.release")).group prec✝

Instances For

source

instance Lake.instDecidableEqBuildType :

DecidableEq BuildType

Equations

Lake.instDecidableEqBuildType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Lake.instOrdBuildType.ord :

BuildType → BuildType → Ordering

Equations

Lake.instOrdBuildType.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

Instances For

source

instance Lake.instOrdBuildType :

Ord BuildType

Equations

Lake.instOrdBuildType = { compare := Lake.instOrdBuildType.ord }

source

instance Lake.BuildType.instLT :

LT BuildType

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

Equations

Lake.BuildType.instLT = ltOfOrd

source

instance Lake.BuildType.instLE :

LE BuildType

Equations

Lake.BuildType.instLE = leOfOrd

source

instance Lake.BuildType.instMin :

Min BuildType

Equations

Lake.BuildType.instMin = minOfLe

source

instance Lake.BuildType.instMax :

Max BuildType

Equations

Lake.BuildType.instMax = maxOfLe

source

def Lake.BuildType.leancArgs :

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"]

Instances For

source

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

Option BuildType

Equations

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

Instances For

source

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

String

Equations

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

Instances For

source

instance Lake.BuildType.instToString :

ToString BuildType

Equations

Lake.BuildType.instToString = { toString := Lake.BuildType.toString }

source

def Lake.BuildType.leanOptions :

BuildType → Lean.LeanOptions

The options to pass to lean based on the build type.

Equations

Lake.BuildType.debug.leanOptions = { values := Lake.NameMap.empty.insert `debugAssertions (Lean.LeanOptionValue.ofBool true) }
x✝.leanOptions = ∅

Instances For

source

def Lake.BuildType.leanArgs (t : BuildType) :

Array String

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

Equations

t.leanArgs = #[]

Instances For

source

structure Lake.LeanConfig :

Type

Configuration options common to targets that build modules.

buildType : BuildType
The mode in which the modules should be built (e.g., debug, release). Defaults to release.
leanOptions : Array LeanOption
An Array of 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 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.
moreLinkObjs : TargetArray System.FilePath
Additional target objects to use when linking (both static and shared). These will come after the paths of native facets.
moreLinkLibs : TargetArray Dynlib
Additional target libraries to pass to leanc when linking (e.g., for shared libraries or binary executables). These will come after the paths of other link objects.
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 the linked objects.
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 the linked objects.
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 : 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.
dynlibs : TargetArray Dynlib
plugins : TargetArray Dynlib