Deprecation

On 2 Aug., Sebastian Ullrich (an author of Lean) deprecated the official Nix build for Lean 4. I understand the decision but I don’t agree with it, since the official repository will continue to use Nix-based builds. In the past there has been multiple times where the Nix flake build was broken for MacOS and it was not promptly maintained: case 1, case 2.

The Flake Build

Since 2 of my projects (Pantograph and Trillium) rely on this feature, I decided to roll out my own Nix flake for Lean 4 with the goal of completely supporting every major version. Eventually I hope this flake will be integrated into leanprover-community.

However, I don’t plan to provide support for building the Emacs and VSCode plugins from this flake.

The flake should provide

• A Lean overlay
• buildLeanPackage
• “lake2nix”: Automatically read dependencies from lake-manifest.json

Usage

The flake README.md should be self-explanatory. Execute

nix flake new --template github:lenianiva/lean4-nix ./lean4-flake-example
cd lean4-flake-example
nix run

and it will build and run a Lean project.

For a more advanced example, see Pantograph’s Nix Flake.