Lean 4 Nix

Nix flake build for Lean 4.

Features:

• Build Lean with Nix
• Lean overlay from versions or toolchain files
• Build Lake projects (with executables, libraries, and facets) incrementally with Nix
• Convert lake-manifest.json into Nix dependencies

Example

The default minimal template is for projects requiring manual dependency management:

nix flake new --template github:lenianiva/lean4-nix ./minimal

The .#dependency template shows an example of using lake-manifest.json to fetch dependencies automatically.

nix flake new --template github:lenianiva/lean4-nix#dependency ./dependency

The .#incremental template shows an example of incremental builds.

Caching

This project has CI by Garnix and uses cache.garnix.io for binary caching. To use the cache, there must be a match between the nixpkgs version listed in flake.lock and the downstream project. Only the newest version will be cached.

Flake outputs

Packages

The flake's packages.${system}.lean output contains the Lean and lake executables. The version corresponds to the latest version in the manifests/ directory.

• lean-all: lean and lake
• lean/leanc/lake: Executables
• leanshared: Shared library of Lean
• cacheRoots: Cached derivations to enable binary caching.
• buildLeanPackage: See below

Overlay

The user must decide on a Lean version to use as overlay. The Lean version from nixpkgs will likely not work of the box. The minimal supported version is v4.11.0, since it is the version when Lean's official Nix flake was deprecated. From version v4.22.0 onwards, each Lean build must have both bootstrap and buildLeanPackage functions. There are a couple of ways to get an overlay. Each corresponds to a flake output. Below is a list ranked from the easiest to the hardest to use:

• readToolchainFile { toolchain; binary ? true; }: Reads the toolchain from a file. Due to Nix's pure evaluation principle, this only supports leanprover/lean4:{tag} based lean-toolchain files where the tag refers to a stable version. For any other toolchains, use readRev or readFromGit.
• readToolchain { toolchain; binary ? true };: readToolchainFile but with its contents provided directly.
• readBinaryToolchain manifest: Reads the binary toolchain from a manifest given in the same format as manifests/*.nix.
• tags.{tag}: Lean4 tags. See the available tags in manifests/
• readRev { rev; bootstrap; buildLeanPackage; } : Reads a revision from the official Lean 4 repository
• readFromGit{ args; bootstrap; buildLeanPackage; }: Given parameters to builtins.fetchGit, download a git repository
• readSrc { src; bootstrap; buildLeanPackage; }: Builds Lean from a source folder. A bootstrapping function must be provided.

Then apply the overlay on pkgs:

pkgs = import nixpkgs {
  inherit system;
  overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ];
};

and pkgs.lean will be replaced by the chosen overlay.

Some users may wish to build nightly or release candidate versions without a corresponding manifest in manifests/. In this case, a common solution is to import the bootstrap and buildLeanPackage functions from the nearest major version and feed it to readRev. In cases where there is a major change to the bootstrap/buildLeanPackage function, the user may need to create the function on their own. The user may need to create a custom overlay function to pull in the necessary cadical and other build dependency versions.

pkgs.lean

This attribute set has properties

• lean: The Lean executable
• lean-all: lean, lake, and the Lean library.
• example: Use nix run .#example to see an example of building a Lean program.
• Init, Std, Lean: Lean built-in libraries provided in the same format as buildLeanPackage

and the function buildLeanPackage, which accepts a parameter set { name; roots; deps; src; }. The complete parameter set can be found in the v4.22.0 manifest. In general:

• src: The source directory
• roots: Lean modules at the root of the import tree.
• deps: A list of outputs of other buildLeanPackage calls.

This is a form of manual dependency management.

lake2nix

Use lake2nix = pkgs.callPackage lean4-nix.lake {} to generate the lake utilities.

lake2nix.buildDeps { ... } automatically reads the lake-manifest.json file and builds its dependencies using lake build. The output is an attr set of derivations for each dependency. It takes the following arguments:

• src: The source directory
• manifestFile ? ${src}/lake-manifest.json: Path to the manifest file
• depOverride ? {}: Attr set of any custom arguments to use when building a given dependency, such as buildPhase or preConfigure.
• depOverrideDeriv ? {}: Attr set of derivations to use instead of building dependencies

lake2nix.mkPackage { ... } builds the given build target of the Lake project using lake build, optionally with the dependencies built by buildDeps. The output is a derivation. It takes the following arguments:

• name: The name of the desired target to build
• src: The source directory name from manifestFile
• staticLibDeps ? []: List of static libraries to link with.
• lakeDeps: If provided, use these dependencies instead of calling buildDeps internally
• lakeArtifacts: If provided, copy the .lake artifacts from another derivation for incremental builds
• buildLibrary ? false: Whether to build library facets for the name build target
• installArtifacts ? true: Whether to export .lake artifacts and source in the derivation outPath for incremental builds
• configurePhase: If provided, override the configure phase
• buildPhase: If provided, override the build phase
• installPhase: If provided, override the install phase

buildLeanPackage

The buildLeanPackage function output the built Lean package in a non-derivation format. Generally, the attributes available are:

• executable: Executable
• sharedLib: Shared library
• modRoot: Module root. Set LEAN_PATH to this to provide context for LSP.
• cTree, oTree, iTree: Trees of C files/.o files/.ilean files

Troubleshooting

Only leanprover/lean4:{tag} toolchains are supported

The Lean version is not listed in the manifests/ directory. Use readRev or readFromGit instead.

Cadical Failure

bv-decide.lean:19:2: error: Failed to execute external prover:
could not execute external process 'cadical'

When using the built-from-source overlay, the overlay produces a pinned cadical version. This cadical version should be present in any environment (as nativeBuildInputs).

Development

Use the provided pre-commit config:

prek install

Use nix flake check to check the template builds.

Update the template lean-toolchain files when new Lean versions come out. When a new version is released, execute

nix run .#toolchain-fetch $VERSION [$VERSION_TAG]

to generate new toolchain hashes. Supply $VERSION_TAG to address any version tag mismatches (e.g. 4.20.1 incorrectly tagged as 4.20.0).

All code must be formatted with alejandra before merging into main. To use it, execute

nix fmt .