Complete Lake Package Configuration Options Reference

Lake packages are configured through a lakefile at the package root. The file can be written in TOML (lakefile.toml) or Lean DSL (lakefile.lean). Both formats support the same fields; this page documents each field with side-by-side examples.

TOML
Lean DSL

name = "mypackage"
version = "0.2.0"
description = "A demonstration package"
keywords = ["demo", "lean4"]
license = "Apache-2.0"
defaultTargets = ["mypackage"]

srcDir = "src"

[[lean_lib]]
name = "MyPackage"

[[lean_exe]]
name = "mypackage"
root = "Main"

import Lake
open Lake DSL

package "mypackage" where
  version := v!"0.2.0"
  description := "A demonstration package"
  keywords := #["demo", "lean4"]
  license := "Apache-2.0"
  srcDir := "src"

lean_lib MyPackage

@[default_target]
lean_exe mypackage where
  root := `Main

Metadata

These fields describe the package to the Reservoir package registry and to humans reading the configuration file. None of them affect the build.

name

string

required

The name of the package. In TOML this is a top-level string field. In a Lean lakefile it is set by the package "<name>" declaration.

name = "hello"

package "hello"

version

string

default:"0.0.0"

The package version. Must follow the form <major>.<minor>.<patch> with an optional -<suffix> for pre-releases.

version = "0.1.0"
version = "1.2.3-alpha"

version := v!"0.1.0"
version := v!"1.2.3-alpha"

Lake’s versioning guidelines:

Major increment — significant breaking changes; manual migration expected.
Minor increment — notable but generally backwards-compatible changes.
Patch increment — bug fixes and small touchups only.

description

string

A short human-readable description of the package. Used by Reservoir to index and display the package.

description = "A verified sorting library for Lean 4"

keywords

string[]

default:"[]"

An array of keywords that help Reservoir users discover the package. Good keywords include the domain (e.g. math, devtool), subtopics (e.g. topology), and notable implementation details (e.g. ffi, cli, dsl).

keywords = ["devtool", "cli", "package-manager"]

keywords := #["devtool", "cli", "package-manager"]

homepage

string

A URL to more information about the package. Reservoir already links to the GitHub repository, so this field is best used for documentation sites or other resources.

homepage = "https://myproject.example.com"

license

string

An SPDX license identifier for the package’s license. Reservoir requires an OSI-approved license to index a package.

license = "Apache-2.0"
license = "MIT"

licenseFiles

string[]

default:"[\"LICENSE\"]"

An array of files that contain licence information. For Apache 2.0, this should include both LICENSE and NOTICE if a NOTICE file exists.

licenseFiles = ["LICENSE", "NOTICE"]

licenseFiles := #["LICENSE", "NOTICE"]

readmeFile

string

default:"README.md"

The relative path to the package’s README file. Reservoir renders this file as HTML on the package’s page.

readmeFile = "docs/README.md"

reservoir

boolean

default:"true"

Whether Reservoir should include this package in its index. Set to false to opt out.

reservoir = false

versionTags

string | string[]

default:"\"version-like tags\""

Git tag patterns that Reservoir treats as version releases. Defaults to tags that start with v followed by a digit.

versionTags = ["v*"]

Layout

These fields control the top-level directory structure of the package and its build outputs.

packagesDir

string

default:".lake/packages"

The directory where Lake downloads remote dependencies.

packagesDir = ".lake/packages"

srcDir

string

default:"."

The directory containing the package’s Lean source files. Passed to lean as the -R option. All library and executable srcDir fields are relative to this.

srcDir = "src"

srcDir := "src"

buildDir

string

default:".lake/build"

The top-level directory for all build outputs.

buildDir = ".lake/build"

leanLibDir

string

default:"lib/lean"

Build subdirectory for binary Lean libraries (.olean, .ilean files).

leanLibDir = "lib/lean"

nativeLibDir

string

default:"lib"

Build subdirectory for native libraries (.a, .so, .dll files).

nativeLibDir = "lib"

binDir

string

default:"bin"

Build subdirectory for binary executables.

binDir = "bin"

irDir

string

default:"ir"

Build subdirectory for intermediate results (.c, .o files).

irDir = "ir"

Build & Run

These fields configure how code is compiled and run.

defaultTargets

string[]

default:"[]"

The names of package targets to build on a bare lake build. In the Lean DSL, use the @[default_target] attribute instead.

defaultTargets = ["hello", "MyLib"]

precompileModules

boolean

default:"false"

When true, each module is compiled into a native shared library that is loaded whenever the module is imported. This speeds up metaprogram evaluation and enables the interpreter to call @[extern] functions.

precompileModules = true

precompileModules := true

extraDepTargets

string[]

default:"[]"

An array of target names to build whenever the package is used (as a dependency or directly).

extraDepTargets = ["NativeLib"]

extraDepTargets := #[`NativeLib]

moreServerOptions

object

default:"{}"

Additional set_option-style options to pass to the Lean language server (lean --server) launched by lake serve, for this package only.

[moreServerOptions]
"pp.all" = false

moreServerOptions := #[⟨`pp.all, false⟩]

moreGlobalServerArgs

string[]

default:"[]"

Additional arguments passed to lean --server that apply to this package and to any packages browsed from the same editor session (e.g. via go-to-definition into dependencies).

moreGlobalServerArgs = ["--memory=4096"]

buildType

string

default:"release"

The build optimisation mode. One of debug, relWithDebInfo, minSizeRel, or release.

Value	C flags	Description
`debug`	`-O0 -g`	Debug info, assertions enabled
`relWithDebInfo`	`-O3 -g -DNDEBUG`	Optimised with debug info
`minSizeRel`	`-Os -DNDEBUG`	Size-optimised release
`release`	`-O3 -DNDEBUG`	Full optimisation (default)

buildType = "debug"

buildType := .debug

moreLeanArgs

string[]

default:"[]"

Additional arguments passed to lean when compiling Lean source files. These do affect the build trace; changing them triggers a rebuild.

moreLeanArgs = ["-Dpp.unicode.fun=true"]

moreLeanArgs := #["-Dpp.unicode.fun=true"]

weakLeanArgs

string[]

default:"[]"

Like moreLeanArgs, but do not affect the trace. Changing them will not trigger a rebuild. They are prepended before moreLeanArgs.

weakLeanArgs = ["--load-dynlib=mylib"]

moreLeancArgs

string[]

default:"[]"

Additional arguments passed to leanc when compiling the C files generated by lean. These affect the trace.

moreLeancArgs = ["-O0", "-UNDEBUG"]

weakLeancArgs

string[]

default:"[]"

Like moreLeancArgs but do not affect the trace. Prepended before moreLeancArgs.

moreLinkArgs

string[]

default:"[]"

Additional arguments passed to leanc during linking (for executables and shared libraries). These affect the trace.

moreLinkArgs = ["-lssl"]

moreLinkArgs := #["-lssl"]

weakLinkArgs

string[]

default:"[]"

Like moreLinkArgs but do not affect the trace.

platformIndependent

boolean | null

default:"null (unset)"

Whether Lake should assume modules in this package are platform-independent:

true — exclude platform-dependent elements from traces; prevents re-elaboration on different platforms.
false — force System.Platform.target into traces; always re-elaborate on other platforms.
unset (default) — include platform info only when platform-dependent artefacts are actually used.

platformIndependent = true

platformIndependent := some true

Test & Lint

testDriver

string

default:"\"\""

The name of the script, executable, or library used by lake test. To reference a definition in a dependency, use <pkg>/<name> syntax. In the Lean DSL, tag a definition with @[test_driver] instead.

testDriver = "test"
testDriver = "mathlib/test"  # from a dependency

@[test_driver]
lean_exe test where
  root := `Test.Main

testDriverArgs

string[]

default:"[]"

Arguments prepended before any CLI arguments when the test driver is invoked by lake test.

testDriverArgs = ["--reporter=spec"]

lintDriver

string

default:"\"\""

The name of the script or executable used by lake lint. Libraries cannot be lint drivers. Tag with @[lint_driver] in Lean DSL.

lintDriver = "lint"

@[lint_driver]
lean_exe lint where
  root := `Lint.Main

lintDriverArgs

string[]

default:"[]"

Arguments prepended before any CLI arguments when the lint driver is invoked by lake lint.

lintDriverArgs = ["--strict"]

Cloud Releases

releaseRepo

string

default:"null (auto-detected)"

The URL of the GitHub repository hosting releases of this package. Defaults to the URL the package was downloaded from (for dependencies) or gh’s default (for uploads).

releaseRepo = "https://github.com/myorg/mypackage"

buildArchive

string

default:"\"{name}-{platform}.tar.gz\""

Custom file name for the build archive. Defaults to {name}-{System.Platform.target}.tar.gz.

buildArchive = "mypackage-linux-x86_64.tar.gz"

preferReleaseBuild

boolean

default:"false"

When true and this package is used as a dependency, Lake will attempt to download a prebuilt release archive from GitHub rather than building from source.

preferReleaseBuild = true

preferReleaseBuild := true

Full Example

TOML
Lean DSL

name = "myproject"
version = "1.0.0"
description = "An example Lean 4 project"
keywords = ["math", "verified"]
license = "MIT"
homepage = "https://myproject.example.com"

srcDir = "src"
buildDir = ".lake/build"

precompileModules = false
buildType = "release"

testDriver = "test"
testDriverArgs = ["--verbose"]

lintDriver = "lint"

preferReleaseBuild = false

[[lean_lib]]
name = "MyProject"

[[lean_exe]]
name = "myproject"
root = "Main"

[[lean_exe]]
name = "test"
root = "Test.Main"

import Lake
open Lake DSL

package "myproject" where
  version := v!"1.0.0"
  description := "An example Lean 4 project"
  keywords := #["math", "verified"]
  license := "MIT"
  homepage := "https://myproject.example.com"
  srcDir := "src"
  buildType := .release
  testDriver := "test"
  testDriverArgs := #["--verbose"]
  lintDriver := "lint"

lean_lib MyProject

@[default_target]
lean_exe myproject where
  root := `Main

@[test_driver]
lean_exe test where
  root := `Test.Main

Getting Started with Lake

Configuration

CLI Reference

Complete Lake Package Configuration Options Reference

Metadata

Layout

Build & Run

Test & Lint

Cloud Releases

Full Example

Build docs developers (and LLMs) love

Getting Started with Lake

Configuration

CLI Reference

Documentation Index

​Metadata

​Layout

​Build & Run

​Test & Lint

​Cloud Releases

​Full Example

Build docs developers (and LLMs) love

Metadata

Layout

Build & Run

Test & Lint

Cloud Releases

Full Example