From f9cd63f0d273630c84f5f8f71d53ea7301fc7969 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 12 Aug 2026 16:20:28 +0000 Subject: [PATCH 1/3] chore: Update Lean to v4.33.0 Toolchain and dependencies bumped by lean-update. --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 18640c8..025e595 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.31.0 +leanprover/lean4:v4.33.0 From 20018dc0c29e0fb32b7929979f3884a70957f951 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 12 Aug 2026 12:24:51 -0400 Subject: [PATCH 2/3] nix: Switch to the lean4-nix fork API Upstream lean4-nix stops at Lean v4.32.0 and builds toolchains from source behind an overlay; the fork provides released toolchains as plain derivations and removed the overlay API. The overlay block is replaced by `lib.${system}.fromToolchainFile`, and the Lean sysroot for bindgen and the dev shell take the toolchain derivation directly. --- flake.lock | 10 +++++----- flake.nix | 17 +++++++---------- 2 files changed, 12 insertions(+), 15 deletions(-) diff --git a/flake.lock b/flake.lock index f364e8e..ab30321 100644 --- a/flake.lock +++ b/flake.lock @@ -96,15 +96,15 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1784223297, - "narHash": "sha256-rmEX8SXvtT7Fi8hOZuCXCbpyzno3iTQYnV3WKzsAVHw=", - "owner": "lenianiva", + "lastModified": 1786543565, + "narHash": "sha256-zHMoHO85jizkIXH0OfnvabpNLTl90rR3GCc1h/e2sx4=", + "owner": "argumentcomputer", "repo": "lean4-nix", - "rev": "82993165f5f30879fc9d40734615ec54cb541e61", + "rev": "4026c657eecf16beea7d266ce32933ef3d7db2e5", "type": "github" }, "original": { - "owner": "lenianiva", + "owner": "argumentcomputer", "repo": "lean4-nix", "type": "github" } diff --git a/flake.nix b/flake.nix index 03aa6d5..57b49fb 100644 --- a/flake.nix +++ b/flake.nix @@ -13,7 +13,7 @@ inputs = { nixpkgs.follows = "lean4-nix/nixpkgs"; flake-parts.url = "github:hercules-ci/flake-parts"; - lean4-nix.url = "github:lenianiva/lean4-nix"; + lean4-nix.url = "github:argumentcomputer/lean4-nix"; blake3 = { url = "github:BLAKE3-team/BLAKE3?ref=refs/tags/1.8.4"; flake = false; @@ -29,7 +29,6 @@ }; outputs = inputs @ { - nixpkgs, flake-parts, lean4-nix, blake3, @@ -50,7 +49,10 @@ pkgs, ... }: let - lake2nix = pkgs.callPackage lean4-nix.lake {}; + # Pins the Lean toolchain; a plain derivation, no overlay involved + lean = lean4-nix.lib.${system}.fromToolchainFile ./lean-toolchain; + + lake2nix = pkgs.callPackage lean4-nix.lake {inherit lean;}; # Filter out build directories lakeSrc = pkgs.lib.cleanSourceWith { @@ -95,7 +97,7 @@ strictDeps = true; # `lean-ffi` uses `LEAN_SYSROOT` to locate `lean.h` for bindgen - LEAN_SYSROOT = "${pkgs.lean.lean-all}"; + LEAN_SYSROOT = "${lean}"; # bindgen needs libclang to parse C headers LIBCLANG_PATH = "${pkgs.llvmPackages.libclang.lib}/lib"; @@ -155,11 +157,6 @@ postConfigure = linkRustLib; }; in { - _module.args.pkgs = import nixpkgs { - inherit system; - overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)]; - }; - packages = { default = blake3C; rust = blake3Rust; @@ -186,7 +183,7 @@ LIBCLANG_PATH = "${pkgs.llvmPackages.libclang.lib}/lib"; packages = with pkgs; [ clang - lean.lean-all + lean rustToolchain rust-analyzer ]; From 7acd847fd00a8511dc3acfcfee106ac0947a6e78 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 12 Aug 2026 12:42:14 -0400 Subject: [PATCH 3/3] chore: Move from alejandra to nixfmt Formatting-only, plus the formatter declaration itself; nixfmt-tree wraps nixfmt so `nix fmt .` can still take a directory. --- flake.nix | 296 +++++++++++++++++++++++++++--------------------------- 1 file changed, 150 insertions(+), 146 deletions(-) diff --git a/flake.nix b/flake.nix index 57b49fb..f70dae4 100644 --- a/flake.nix +++ b/flake.nix @@ -28,15 +28,16 @@ crane.url = "github:ipetkov/crane"; }; - outputs = inputs @ { - flake-parts, - lean4-nix, - blake3, - fenix, - crane, - ... - }: - flake-parts.lib.mkFlake {inherit inputs;} { + outputs = + inputs@{ + flake-parts, + lean4-nix, + blake3, + fenix, + crane, + ... + }: + flake-parts.lib.mkFlake { inherit inputs; } { systems = [ "aarch64-darwin" "aarch64-linux" @@ -44,152 +45,155 @@ "x86_64-linux" ]; - perSystem = { - system, - pkgs, - ... - }: let - # Pins the Lean toolchain; a plain derivation, no overlay involved - lean = lean4-nix.lib.${system}.fromToolchainFile ./lean-toolchain; - - lake2nix = pkgs.callPackage lean4-nix.lake {inherit lean;}; - - # Filter out build directories - lakeSrc = pkgs.lib.cleanSourceWith { - src = ./.; - filter = path: type: let - name = builtins.baseNameOf path; - in - name - != "target" - && name != ".lake" - && name - != "build"; - }; - - # Lakefile patches for Nix builds - disableGitClone = '' - substituteInPlace lakefile.lean --replace-fail 'GitRepo.execGit' '--GitRepo.execGit' - ''; - # Don't build the `blake3_rs` static lib with Lake, since we build it with Crane - disableCargoBuild = '' - substituteInPlace lakefile.lean --replace-fail 'proc { cmd := "cargo"' '--proc { cmd := "cargo"' - ''; - linkBlake3Src = '' - ln -s ${blake3.outPath} ./blake3 - ''; - # Copy the `blake3_rs` static lib from Crane to `target/release` so Lake can use it - linkRustLib = '' - mkdir -p rust/target/release - ln -s ${rustPkg}/lib/libblake3_rs.a rust/target/release/ - ''; - - # Pins the Rust toolchain - rustToolchain = fenix.packages.${system}.fromToolchainFile { - file = ./rust-toolchain.toml; - sha256 = "sha256-sqSWJDUxc+zaz1nBWMAJKTAGBuGWP25GCftIOlCEAtA="; - }; - - # Rust package - craneLib = (crane.mkLib pkgs).overrideToolchain rustToolchain; - craneArgs = { - src = craneLib.cleanCargoSource ./rust; - strictDeps = true; - - # `lean-ffi` uses `LEAN_SYSROOT` to locate `lean.h` for bindgen - LEAN_SYSROOT = "${lean}"; - # bindgen needs libclang to parse C headers - LIBCLANG_PATH = "${pkgs.llvmPackages.libclang.lib}/lib"; - - buildInputs = - [] - ++ pkgs.lib.optionals pkgs.stdenv.isDarwin [ - # Additional darwin specific inputs can be set here - pkgs.libiconv - ]; - }; - # Build dependencies once and share them across the package build and - # the clippy check instead of recompiling them per consumer. - cargoArtifacts = craneLib.buildDepsOnly craneArgs; - # doCheck = false: the crate has no Rust unit tests, and the Lean - # `blake3-test` check is where the suite runs. - rustPkg = craneLib.buildPackage ( - craneArgs - // { - inherit cargoArtifacts; - doCheck = false; - } - ); - - blake3C = lake2nix.mkPackage { - name = "Blake3C"; - src = lakeSrc; - buildLibrary = true; - postPatch = disableGitClone; - preConfigure = linkBlake3Src; - postInstall = '' - cp -rP ./blake3 $out + perSystem = + { + system, + pkgs, + ... + }: + let + # Pins the Lean toolchain; a plain derivation, no overlay involved + lean = lean4-nix.lib.${system}.fromToolchainFile ./lean-toolchain; + + lake2nix = pkgs.callPackage lean4-nix.lake { inherit lean; }; + + # Filter out build directories + lakeSrc = pkgs.lib.cleanSourceWith { + src = ./.; + filter = + path: type: + let + name = builtins.baseNameOf path; + in + name != "target" && name != ".lake" && name != "build"; + }; + + # Lakefile patches for Nix builds + disableGitClone = '' + substituteInPlace lakefile.lean --replace-fail 'GitRepo.execGit' '--GitRepo.execGit' ''; - }; - - blake3Rust = lake2nix.mkPackage { - name = "Blake3Rust"; - src = lakeSrc; - postPatch = disableCargoBuild; - postConfigure = linkRustLib; - postInstall = '' - cp -rP rust/target/ $out/rust/target/ + # Don't build the `blake3_rs` static lib with Lake, since we build it with Crane + disableCargoBuild = '' + substituteInPlace lakefile.lean --replace-fail 'proc { cmd := "cargo"' '--proc { cmd := "cargo"' ''; - }; - - blake3Test = lake2nix.mkPackage { - name = "Blake3Test"; - src = lakeSrc; - installArtifacts = false; - # Merge .lake artifacts from both C and Rust library builds - prePatch = '' - rsync -a ${blake3C}/.lake/ .lake/ - rsync -a ${blake3Rust}/.lake/ .lake/ - chmod -R +w .lake + linkBlake3Src = '' + ln -s ${blake3.outPath} ./blake3 + ''; + # Copy the `blake3_rs` static lib from Crane to `target/release` so Lake can use it + linkRustLib = '' + mkdir -p rust/target/release + ln -s ${rustPkg}/lib/libblake3_rs.a rust/target/release/ ''; - postPatch = disableGitClone + disableCargoBuild; - preConfigure = linkBlake3Src; - postConfigure = linkRustLib; - }; - in { - packages = { - default = blake3C; - rust = blake3Rust; - }; - checks = { - # Lint the Rust FFI crate; warnings are errors. - clippy = craneLib.cargoClippy ( + # Pins the Rust toolchain + rustToolchain = fenix.packages.${system}.fromToolchainFile { + file = ./rust-toolchain.toml; + sha256 = "sha256-sqSWJDUxc+zaz1nBWMAJKTAGBuGWP25GCftIOlCEAtA="; + }; + + # Rust package + craneLib = (crane.mkLib pkgs).overrideToolchain rustToolchain; + craneArgs = { + src = craneLib.cleanCargoSource ./rust; + strictDeps = true; + + # `lean-ffi` uses `LEAN_SYSROOT` to locate `lean.h` for bindgen + LEAN_SYSROOT = "${lean}"; + # bindgen needs libclang to parse C headers + LIBCLANG_PATH = "${pkgs.llvmPackages.libclang.lib}/lib"; + + buildInputs = + [ ] + ++ pkgs.lib.optionals pkgs.stdenv.isDarwin [ + # Additional darwin specific inputs can be set here + pkgs.libiconv + ]; + }; + # Build dependencies once and share them across the package build and + # the clippy check instead of recompiling them per consumer. + cargoArtifacts = craneLib.buildDepsOnly craneArgs; + # doCheck = false: the crate has no Rust unit tests, and the Lean + # `blake3-test` check is where the suite runs. + rustPkg = craneLib.buildPackage ( craneArgs // { inherit cargoArtifacts; - cargoClippyExtraArgs = "--all-targets -- -D warnings"; + doCheck = false; } ); - # Run the Lean test suite (exercises both the C and Rust backends) - # at check time so it runs via `nix flake check`. - blake3-test = pkgs.runCommand "blake3-test" {} '' - ${blake3Test}/bin/Blake3Test - touch $out - ''; - }; - devShells.default = pkgs.mkShell { - # Add libclang for FFI with rust-bindgen - LIBCLANG_PATH = "${pkgs.llvmPackages.libclang.lib}/lib"; - packages = with pkgs; [ - clang - lean - rustToolchain - rust-analyzer - ]; - }; - formatter = pkgs.alejandra; - }; + blake3C = lake2nix.mkPackage { + name = "Blake3C"; + src = lakeSrc; + buildLibrary = true; + postPatch = disableGitClone; + preConfigure = linkBlake3Src; + postInstall = '' + cp -rP ./blake3 $out + ''; + }; + + blake3Rust = lake2nix.mkPackage { + name = "Blake3Rust"; + src = lakeSrc; + postPatch = disableCargoBuild; + postConfigure = linkRustLib; + postInstall = '' + cp -rP rust/target/ $out/rust/target/ + ''; + }; + + blake3Test = lake2nix.mkPackage { + name = "Blake3Test"; + src = lakeSrc; + installArtifacts = false; + # Merge .lake artifacts from both C and Rust library builds + prePatch = '' + rsync -a ${blake3C}/.lake/ .lake/ + rsync -a ${blake3Rust}/.lake/ .lake/ + chmod -R +w .lake + ''; + postPatch = disableGitClone + disableCargoBuild; + preConfigure = linkBlake3Src; + postConfigure = linkRustLib; + }; + in + { + packages = { + default = blake3C; + rust = blake3Rust; + }; + + checks = { + # Lint the Rust FFI crate; warnings are errors. + clippy = craneLib.cargoClippy ( + craneArgs + // { + inherit cargoArtifacts; + cargoClippyExtraArgs = "--all-targets -- -D warnings"; + } + ); + # Run the Lean test suite (exercises both the C and Rust backends) + # at check time so it runs via `nix flake check`. + blake3-test = pkgs.runCommand "blake3-test" { } '' + ${blake3Test}/bin/Blake3Test + touch $out + ''; + }; + devShells.default = pkgs.mkShell { + # Add libclang for FFI with rust-bindgen + LIBCLANG_PATH = "${pkgs.llvmPackages.libclang.lib}/lib"; + packages = with pkgs; [ + clang + lean + rustToolchain + rust-analyzer + ]; + }; + + # The treefmt wrapper around `nixfmt`, so `nix fmt .` can take a + # directory; bare `nixfmt` only accepts individual files. + formatter = pkgs.nixfmt-tree; + }; }; }