Lean4-nix for building Lean projects

Announcements
1

lean4-nix provides source build and binary build Lean 4 packages, and incremental building of lake projects using Nix.

For example:

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

Building a lake package is as easy as

lake2nix = pkgs.callPackage lean4-nix.lake {};
pkgs = import nixpkgs {
  inherit system;
  overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
};
lake2nix.mkPackage {
  name = "Example";
  src = ./.;
};

Before version 4.11.0, Lean came with its own nix utilities, but it was deprecated and eventually removed. During this time I refactored out the Nix build paths from Lean 4 into lean4-nix. Lean 4’s build system lake occasionally undergoes changes and lean4-nix may take a while to adapt to these changes.

4 Likes