chore: Update to Lean 4.26.0 and latest lean4-nix

.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

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
 

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,25 +31,36 @@
         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;
           overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
         };
 
         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; [

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.24.0
+leanprover/lean4:v4.26.0