Lake configuration file

lakefile.toml, the .toml configuration file for Lake, the package manager of the Lean programming language and theorem prover

Type object
File match lakefile.toml
Schema URL https://catalog.lintel.tools/schemas/schemastore/lake-configuration-file/latest.json
Source https://raw.githubusercontent.com/leanprover/lean4/refs/heads/master/src/lake/schemas/lakefile-toml-schema.json

Validate with Lintel

npx @lintel/lintel check
Type: object

Configuration file for Lean's build system, Lake

All of

1. leanConfig
2. object object
name string required

The name of the package.

version string

The package version. Versions have the form:

v!"<major>.<minor>.<patch>[-<specialDescr>]" A version with a - suffix is considered a "prerelease".

Lake suggest the following guidelines for incrementing versions:

  • Major version increment (e.g., v1.3.0 → v2.0.0) Indicates significant breaking changes in the package. Package users are not expected to update to the new version without manual intervention.

  • Minor version increment (e.g., v1.3.0 → v1.4.0) Denotes notable changes that are expected to be generally backwards compatible. Package users are expected to update to this version automatically and should be able to fix any breakages and/or warnings easily.

  • Patch version increment (e.g., v1.3.0 → v1.3.1) Reserved for bug fixes and small touchups. Package users are expected to update automatically and should not expect significant breakage, except in the edge case of users relying on the behavior of patched bugs.

Note that backwards-incompatible changes may occur at any version increment. The is because the current nature of Lean (e.g., transitive imports, rich metaprogramming, reducibility in proofs), makes it infeasible to define a completely stable interface for a package. Instead, the different version levels indicate a change's intended significance and how difficult migration is expected to be.

Versions of form the 0.x.x are considered development versions prior to first official release. Like prerelease, they are not expected to closely follow the above guidelines.

Packages without a defined version default to 0.0.0.

versionTags string | object | array

Git tags of this package's repository that should be treated as versions. Package indices (e.g., Reservoir) can make use of this information to determine the Git revisions corresponding to released versions.

Defaults to tags that are "version-like". That is, start with a v followed by a digit.

Format: Either "*", an array of all version strings that are a match, or a recursive object with one of the following properties at every layer:

  • preset: Denotes the name of a preset-matcher as a string. Currently, the only preset-mater is verLike.
  • startsWith: Denotes a prefix string of all version strings that are a match.
  • endsWith: Denotes a suffix string of all version strings that are a match.
  • not: Negate a version string pattern.
  • any: Match any of an array of version string patterns.
  • all: Match all of an array of version string patterns.
Default: "*"
description string

A short description for the package (e.g., for Reservoir).

keywords string[]

Custom keywords associated with the package. Reservoir can make use of a package's keywords to group related packages together and make it easier for users to discover them.

Good keywords include the domain (e.g., math, software-verification, devtool), specific subtopics (e.g., topology, cryptology), and significant implementation details (e.g., dsl, ffi, cli). For instance, Lake's keywords could be devtool, cli, dsl, package-manager, and build-system.

Default:
[]
homepage string

A URL to information about the package.

Reservoir will already include a link to the package's GitHub repository (if the package is sourced from there). Thus, users are advised to specify something else for this (if anything).

license string

The package's license (if one). Should be a valid [SPDX License Expression][1].

Reservoir requires that packages uses an OSI-approved license to be included in its index, and currently only supports single identifier SPDX expressions. For, a list of OSI-approved SPDX license identifiers, see the [SPDX LIcense List][2].

[1]: https://spdx.github.io/spdx-spec/v3.0/annexes/SPDX-license-expressions/ [2]: https://spdx.org/licenses/

licenseFiles string[]

Files containing licensing information for the package.

These should be the license files that users are expected to include when distributing package sources, which may be more then one file for some licenses. For example, the Apache 2.0 license requires the reproduction of a NOTICE file along with the license (if such a file exists).

Default:
[
  "LICENSE"
]
readmeFile string

The path to the package's README.

A README should be a Markdown file containing an overview of the package. Reservoir displays the rendered HTML of this file on a package's page. A nonstandard location can be used to provide a different README for Reservoir and GitHub.

Default: "README.md"
reservoir boolean

Whether Reservoir should include the package in its index. When set to false, Reservoir will not add the package to its index and will remove it if it was already there (when Reservoir is next updated).

Default: true
libPrefixOnWindows boolean

Whether native libraries (of this package) should be prefixed with lib on Windows.

Unlike Unix, Windows does not require native libraries to start with lib and, by convention, they usually do not. However, for consistent naming across all platforms, users may wish to enable this.

Default: false
allowImportAll boolean

Whether downstream packages can import all modules of this package.

If enabled, downstream users will be able to access the private internals of modules, including definition bodies not marked as @[expose]. This may also, in the future, prevent compiler optimization which rely on private definitions being inaccessible outside their own package.

Default: false
fixedToolchain boolean

Whether this package is expected to only function on a single toolchain (the package's toolchain).

This informs Lake's toolchain update procedure (in lake update) to prioritize this package's toolchain. It also avoids the need to separate input-to-output mappings for this package by toolchain version in the Lake cache.

Default: false
enableArtifactCache boolean

Whether to enables Lake's local, offline artifact cache for the package.

Artifacts (i.e., build products) of packages will be shared across local copies by storing them in a cache associated with the Lean toolchain. This can significantly reduce initial build times and disk space usage when working with multiple copies of large projects or large dependencies.

As a caveat, build targets which support the artifact cache will not be stored in their usual location within the build directory. Thus, projects with custom build scripts that rely on specific location of artifacts may wish to disable this feature.

If none (the default), this will fallback to (in order):

  • The LAKE_ARTIFACT_CACHE environment variable (if set).
  • The workspace root's enableArtifactCache configuration (if set and this package is a dependency).
  • Lake's default: The package can use artifacts from the cache, but cannot write to it.
restoreAllArtifacts boolean

Whether, when the local artifact cache is enabled, Lake should copy all cached artifacts into the build directory. This ensures the build results are available to external consumers who expect them in the build directory.

srcDir string

The directory containing the package's Lean source files. Defaults to the package's directory.

(This will be passed to lean as the -R option.)

Default: "."
buildDir string

The directory to which Lake should output the package's build results.

Default: ".lake/build"
leanLibDir string

The build subdirectory to which Lake should output the package's binary Lean libraries (e.g., .olean, .ilean files).

Default: "lib/lean"
nativeLibDir string

The build subdirectory to which Lake should output the package's native libraries (e.g., .a, .so, .dll files).

Default: "lib"
binDir string

The build subdirectory to which Lake should output the package's binary executable.

Default: "bin"
irDir string

The build subdirectory to which Lake should output the package's intermediary results (e.g., .c and .o files).

Default: "ir"
packagesDir string

The directory to which Lake should download remote dependencies.

Default: ".lake/packages"
extraDepTargets string[]

An array of target names to build whenever the package is used.

Default:
[]
precompileModules boolean

Whether to compile each of the package's module into a native shared library that is loaded whenever the module is imported. This speeds up evaluation of metaprograms and enables the interpreter to run functions marked @[extern].

Default: "false"
defaultTargets string[]

The names of the package's targets to build by default (i.e., on a bare lake build of the package).

Default:
[]
moreGlobalServerArgs string[]

Additional arguments to pass to the Lean language server launched by lake serve, both for this package and also for any packages browsed from this one in the same session.

Default:
[]
testDriver string

The name of the script, executable, or library by lake test when this package is the workspace root. To point to a definition in another package, use the syntax <pkg>/<def>.

A script driver will be run by lake test with the arguments configured in testDriverArgs followed by any specified on the CLI (e.g., via lake lint -- <args>...). An executable driver will be built and then run like a script. A library will just be built.

testDriverArgs string[]

Arguments to pass to the package's test driver. These arguments will come before those passed on the command line via lake test -- <args>....

Default:
[]
lintDriver string

The name of the script or executable used by lake lint when this package is the workspace root. To point to a definition in another package, use the syntax <pkg>/<def>.

A script driver will be run by lake lint with the arguments configured in lintDriverArgs followed by any specified on the CLI (e.g., via lake lint -- <args>...). An executable driver will be built and then run like a script.

lintDriverArgs string[]

Arguments to pass to the package's linter. These arguments will come before those passed on the command line via lake lint -- <args>....

Default:
[]
releaseRepo string

The URL of the GitHub repository to upload and download releases of this package. If not set, for downloads, Lake uses the URL the package was download from (if it is a dependency) and for uploads, uses gh's default.

buildArchive string

A custom name for the build archive for the GitHub cloud release. If not set, Lake defaults to {(pkg-)name}-{System.Platform.target}.tar.gz.

preferReleaseBuild boolean

Whether to prefer downloading a prebuilt release (from GitHub) rather than building this package from the source when this package is used as a dependency.

Default: "false"
require array

Dependencies of a package, each of which specifies both the name and the source of each package. There are three kinds of sources:

  • Reservoir, or an alternative package registry
  • Git repositories, which may be local paths or URLs
  • Local paths
lean_lib leanLibConfig[]

Library targets of a package.

lean_exe leanExeConfig[]

Executable targets of a package.

input_file inputFileConfig[]

Input files of a package.

input_dir inputDirConfig[]

Input directories of a package.

Definitions

leanOptionValue Record<string, string | boolean | integer | object>

A set_option string / boolean / natural number configuration value.

leanConfig
buildType string

The mode in which the modules should be built.

Default: "release"
Values: "debug" "Debug" "relWithDebInfo" "RelWithDebInfo" "minSizeRel" "MinSizeRel" "release" "Release"
leanOptions Record<string, string | boolean | integer | object>

Additional set_option options to pass to both the Lean language server launched by lake serve and to lean when compiling a module's Lean source files.

Default:
{}
moreServerOptions Record<string, string | boolean | integer | object>

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

Default:
{}
moreLeanArgs string[]

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

Default:
[]
weakLeanArgs string[]

Additional command-line 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.

Default:
[]
moreLeancArgs string[]

Additional command-line 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.

Default:
[]
weakLeancArgs string[]

Additional command-line 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.

Default:
[]
moreLinkObjs string[]

Build key identifiers of additional target objects to use when linking (both static and shared).

Format: <target>[:<facet>]*, where:

  • <target> is of the form @<package>, @<package>/<targetName>, +or@/+`,
  • <package> may be empty to reference the default package,
  • <facet> is the name of a target facet.

Build key identifiers come after the paths of native facets.

Default:
[]
moreLinkLibs string[]

Build key identifiers of additional target libraries to pass to leanc when linking (e.g., for shared libraries or binary executables).

Format: <target>[:<facet>]*, where:

  • <target> is of the form @<package>, @<package>/<targetName>, +or@/+`,
  • <package> may be empty to reference the default package,
  • <facet> is the name of a target facet.

These come after the paths of other link objects.

Default:
[]
moreLinkArgs string[]

Additional command-line arguments to pass to leanc when linking (e.g., for shared libraries or binary executables). These come after the paths of the linked objects.

Default:
[]
weakLinkArgs string[]

Additional command-line arguments to pass to leanc when linking (e.g., for shared libraries or binary executables). These 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.

Default:
[]
backend string

Compiler backend that modules should be built with (C or LLVM). default corresponds to C.

Default: "default"
Values: "default" "c" "llvm"
platformIndependent boolean

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 not set, 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.

dynlibs string[]

Build key identifiers of dynamic library targets to load during the elaboration of a module (via lean --load-dynlib).

Format: <target>[:<facet>]*, where:

  • <target> is of the form @<package>, @<package>/<targetName>, +or@/+`,
  • <package> may be empty to reference the default package,
  • <facet> is the name of a target facet.
Default:
[]
plugins string[]

Build key identifiers of Lean plugin targets to load during the elaboration of a module (via lean --plugin).

Format: <target>[:<facet>]*, where:

  • <target> is of the form @<package>, @<package>/<targetName>, +or@/+`,
  • <package> may be empty to reference the default package,
  • <facet> is the name of a target facet.
Default:
[]
leanLibConfig
leanExeConfig
inputFileConfig object
name string required

The name of the input file.

path string

The path to the input file (relative to the package root).

Defaults to the name of the target.

text boolean

Whether this is a text file. If so, Lake normalize line endings for its trace. This avoids rebuilds across platforms with different line endings.

Default: false
inputDirConfig object
name string required

The name of the input directory.

path string

The path to the input directory (relative to the package root).

Defaults to the name of the target.

text boolean

Whether the directory is composed of text files. If so, Lake normalize line endings for their traces. This avoids rebuilds across platforms with different line endings.

Default: false
filter string | object

Includes only the files from the directory whose paths satisfy this pattern.

Format: Either "*", or a recursive object with one of the following properties at every layer:

  • path: String pattern matching the path.
  • extension: String pattern matching the extension of the file in the path.
  • fileName: String pattern matching the name of the file in the path.
  • not: Negate a path pattern.
  • any: Match any of an array of path patterns.
  • all: Match all of an array of path patterns.

String patterns have the following format: Either "*", an array of all strings that are a match, or a recursive object with one of the following properties at every layer:

  • startsWith: Denotes a prefix string of all strings that are a match.
  • endsWith: Denotes a suffix string of all strings that are a match.
  • not: Negate a string pattern.
  • any: Match any of an array of string patterns.
  • all: Match all of an array of string patterns.
Default: "*"
dependencyConfig object
name string required

The package name of the dependency. This name must match the one declared in its configuration file, as that name is used to index its target data types. For this reason, the package name must also be unique across packages in the dependency graph.

path string

A dependency on the local filesystem, specified by its path.

git string | object

A dependency in a Git repository, specified by its URL.

Default: ""
subDir string

The subdirectory of a Git repository (as specified by git) that contains the package's source code.

rev string

For Git dependencies, this field specifies the Git revision, which may be a branch name, a tag name, or a specific hash.

scope string

An additional qualifier used to distinguish packages of the same name in a Lake registry. On Reservoir, this is the package owner.