From d60b92886bc190768301fe78b2026e103b7742e0 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Fri, 5 Dec 2025 17:30:23 -0500 Subject: [PATCH] chore: Update to Lean 4.26.0 and latest lean4-nix --- .github/workflows/ci.yml | 4 +-- Blake3.lean | 10 +++----- blake3.nix | 55 ---------------------------------------- flake.lock | 18 ++++++------- flake.nix | 44 +++++++++++++++++--------------- lean-toolchain | 2 +- 6 files changed, 39 insertions(+), 94 deletions(-) delete mode 100644 blake3.nix diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index bd19974..fed1cba 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -30,5 +30,5 @@ jobs: with: nix_path: nixpkgs=channel:nixos-unstable github_access_token: ${{ secrets.GITHUB_TOKEN }} - - run: nix build --accept-flake-config - - run: nix run --accept-flake-config + - run: nix build + - run: nix run .#test diff --git a/Blake3.lean b/Blake3.lean index d0691b9..5997baa 100644 --- a/Blake3.lean +++ b/Blake3.lean @@ -1,9 +1,8 @@ /-! Bindings to the BLAKE3 hashing library. -/ -theorem ByteArray.size_of_extract {hash : ByteArray} (hbe : b ≤ e) (h : e ≤ hash.data.size) : +theorem ByteArray.size_of_extract {hash : ByteArray} (h : e ≤ hash.size) : (hash.extract b e).size = e - b := by - simp [ByteArray.size, ByteArray.extract, ByteArray.copySlice, ByteArray.empty, ByteArray.emptyWithCapacity] - rw [Nat.add_comm, Nat.sub_add_cancel hbe, Nat.min_eq_left h] + simp [Nat.min_eq_left h] namespace Blake3 @@ -132,7 +131,6 @@ def squeeze (sponge : Sponge) (length : USize) have sub_e_b_eq_length : e - b = length.toNat := by simp only [b, e] rw [Nat.add_comm _ length.toNat, Nat.add_sub_cancel] - have le_b_e : b ≤ e := by simp only [Nat.le_add_right, e, b] have h_e_bound : e ≤ tmp.size := by simp [e, h] cases System.Platform.numBits_eq with @@ -146,8 +144,8 @@ def squeeze (sponge : Sponge) (length : USize) rwa [h64, Nat.pow_succ] at h_len_bound rw [h64, BLAKE3_OUT_LEN] simp only [Nat.mod_eq_of_lt hbound, Nat.le_refl] - have size_of_extract := ByteArray.size_of_extract le_b_e h_e_bound - ⟨y, by simp only [y, size_of_extract, sub_e_b_eq_length]⟩ + have size_of_extract := ByteArray.size_of_extract h_e_bound + ⟨y, by rw [size_of_extract, sub_e_b_eq_length]⟩ end Sponge diff --git a/blake3.nix b/blake3.nix deleted file mode 100644 index f27e152..0000000 --- a/blake3.nix +++ /dev/null @@ -1,55 +0,0 @@ -{ - pkgs, - lean4-nix, - blake3, -}: let - blake3Flags = pkgs.lib.concatStringsSep " " [ - "-DBLAKE3_NO_SSE2" - "-DBLAKE3_NO_SSE41" - "-DBLAKE3_NO_AVX2" - "-DBLAKE3_NO_AVX512" - "-DBLAKE3_USE_NEON=0" - ]; - blake3Files = [ - "blake3" - "blake3_dispatch" - "blake3_portable" - ]; - buildSteps = - builtins.map (file: "gcc -O3 -Wall -c ${blake3}/c/${file}.c -o ${file}.o ${blake3Flags}") blake3Files - ++ [ - "gcc -O3 -Wall -c ffi.c -o ffi.o -I ${pkgs.lean}/include -I ${blake3}/c" - "ar rcs libblake3.a ${(builtins.concatStringsSep " " (builtins.map (str: "${str}.o") blake3Files))} ffi.o" - ]; - # The `libblake3.a` static library is exposed as the `staticLib` package, as it must be explicitly linked against - # in downstream lean4-nix packages. - blake3-c = pkgs.stdenv.mkDerivation { - name = "blake3-c"; - src = ./.; - buildInputs = [pkgs.gcc pkgs.lean.lean-all]; - buildPhase = builtins.concatStringsSep "\n" buildSteps; - installPhase = '' - mkdir -p $out/lib $out/include - cp libblake3.a $out/lib/ - cp ${blake3}/c/blake3.h $out/include/ - ''; - }; - # The Blake3 library is only used locally for development and to build the test package - # Downstream users should import Blake3.lean in the lakefile and fetch it via `mkPackage` - blake3-lib = pkgs.lean.buildLeanPackage { - name = "blake3-lib"; - src = ./.; - roots = ["Blake3"]; - staticLibDeps = [ "${blake3-c}/lib" ]; - groupStaticLibs = true; - }; - - lib = { - inherit - blake3-c - blake3-lib - ; - }; -in { - inherit lib; -} diff --git a/flake.lock b/flake.lock index 298af9d..477cdf5 100644 --- a/flake.lock +++ b/flake.lock @@ -22,11 +22,11 @@ "nixpkgs-lib": "nixpkgs-lib" }, "locked": { - "lastModified": 1754487366, - "narHash": "sha256-pHYj8gUBapuUzKV/kN/tR3Zvqc7o6gdFB9XKXIp1SQ8=", + "lastModified": 1765835352, + "narHash": "sha256-XswHlK/Qtjasvhd1nOa1e8MgZ8GS//jBoTqWtrS1Giw=", "owner": "hercules-ci", "repo": "flake-parts", - "rev": "af66ad14b28a127c5c0f3bbb298218fc63528a18", + "rev": "a34fae9c08a15ad73f295041fec82323541400a9", "type": "github" }, "original": { @@ -59,11 +59,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1761368467, - "narHash": "sha256-eEs2YpE84+d6a8VKXCACNJy5czcu8GQCaeSZwR/mFMk=", + "lastModified": 1766003746, + "narHash": "sha256-S3e45gKBtTZ4bDqfrddB7A3dxcZb8jY0ROPu6Aw+ZEk=", "owner": "lenianiva", "repo": "lean4-nix", - "rev": "3550873ed1a87d666d633d34921e79abaa4671c1", + "rev": "0bca9d30803e3d65157240e67045badbc547dd45", "type": "github" }, "original": { @@ -90,11 +90,11 @@ }, "nixpkgs-lib": { "locked": { - "lastModified": 1753579242, - "narHash": "sha256-zvaMGVn14/Zz8hnp4VWT9xVnhc8vuL3TStRqwk22biA=", + "lastModified": 1765674936, + "narHash": "sha256-k00uTP4JNfmejrCLJOwdObYC9jHRrr/5M/a/8L2EIdo=", "owner": "nix-community", "repo": "nixpkgs.lib", - "rev": "0f36c44e01a6129be94e3ade315a5883f0228a6e", + "rev": "2075416fcb47225d9b68ac469a5c4801a9c4dd85", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 6fa1ea2..5b72cf1 100644 --- a/flake.nix +++ b/flake.nix @@ -1,15 +1,6 @@ { description = "Blake3 Nix Flake"; - nixConfig = { - extra-substituters = [ - "https://cache.garnix.io" - ]; - extra-trusted-public-keys = [ - "cache.garnix.io:CTFPyKSLcx5RMJKfLo5EEPUObbA78b0YQ2DTCJXqr9g=" - ]; - }; - inputs = { nixpkgs.follows = "lean4-nix/nixpkgs"; flake-parts.url = "github:hercules-ci/flake-parts"; @@ -40,7 +31,27 @@ pkgs, ... }: let - lib = (import ./blake3.nix {inherit pkgs lean4-nix blake3;}).lib; + lake2nix = pkgs.callPackage lean4-nix.lake {}; + commonArgs = { + src = ./.; + postPatch = '' + substituteInPlace lakefile.lean --replace-fail 'GitRepo.execGit' '--GitRepo.execGit' + ''; + preConfigure = '' + ln -s ${blake3.outPath} ./blake3 + ''; + }; + blake3Lib = lake2nix.mkPackage (commonArgs + // { + name = "Blake3"; + buildLibrary = true; + }); + blake3Test = lake2nix.mkPackage (commonArgs + // { + name = "Blake3Test"; + lakeArtifacts = blake3Lib; + installArtifacts = false; + }); in { _module.args.pkgs = import nixpkgs { inherit system; @@ -48,17 +59,8 @@ }; packages = { - default = - ((lean4-nix.lake {inherit pkgs;}).mkPackage { - src = ./.; - roots = ["Blake3Test"]; - deps = [lib.blake3-lib]; - staticLibDeps = ["${lib.blake3-c}/lib"]; - }) - .executable; - # Downstream lean4-nix packages must also link to the static lib using the `staticLibDeps` attribute. - # See https://github.com/argumentcomputer/lean4-nix/blob/dev/templates/dependency/flake.nix for an example - staticLib = lib.blake3-c; + default = blake3Lib; + test = blake3Test; }; devShells.default = pkgs.mkShell { packages = with pkgs; [ diff --git a/lean-toolchain b/lean-toolchain index c00a535..e59446d 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.24.0 +leanprover/lean4:v4.26.0