From aeb1cbe41928e66a304a15434ffa051c3f52bdb0 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Sat, 13 Dec 2025 01:03:00 -0500
Subject: [PATCH 1/6] chore: Update lean4-nix

---
 flake.lock         |  61 ++++++++++++-------
 flake.nix          | 146 +++++++++++++++++++++++++++++++++------------
 ix.nix             |  96 -----------------------------
 lake-manifest.json |  16 ++++-
 lakefile.lean      |  13 ++--
 5 files changed, 169 insertions(+), 163 deletions(-)
 delete mode 100644 ix.nix

diff --git a/flake.lock b/flake.lock
index d2aa8952..053dfb56 100644
--- a/flake.lock
+++ b/flake.lock
@@ -19,7 +19,7 @@
     },
     "blake3-lean": {
       "inputs": {
-        "blake3": "blake3",
+        "blake3": "blake3_2",
         "flake-parts": "flake-parts",
         "lean4-nix": "lean4-nix",
         "nixpkgs": [
@@ -28,19 +28,37 @@
         ]
       },
       "locked": {
-        "lastModified": 1761919236,
-        "narHash": "sha256-ZF/+uKH+oLwxm5VTXksBS70Bjt5s9gbSKNjjp2JI2hA=",
+        "lastModified": 1765602345,
+        "narHash": "sha256-FWyiv5M4qHyOzm6E0SeuumQXP+0K1vJVCRb0Tn8NNOc=",
         "owner": "argumentcomputer",
         "repo": "Blake3.lean",
-        "rev": "732daca6c67f3be3ca44837643cfda906503e9ac",
+        "rev": "1dc03fe74d74c2f33303b4aa60736599e9ee8667",
         "type": "github"
       },
       "original": {
         "owner": "argumentcomputer",
+        "ref": "nix-lake",
         "repo": "Blake3.lean",
         "type": "github"
       }
     },
+    "blake3_2": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1745192552,
+        "narHash": "sha256-IABVErXWYQFXZcwsFKfQhm3ox7UZUcW5uzVrGwsSp94=",
+        "owner": "BLAKE3-team",
+        "repo": "BLAKE3",
+        "rev": "df610ddc3b93841ffc59a87e3da659a15910eb46",
+        "type": "github"
+      },
+      "original": {
+        "owner": "BLAKE3-team",
+        "ref": "refs/tags/1.8.2",
+        "repo": "BLAKE3",
+        "type": "github"
+      }
+    },
     "crane": {
       "locked": {
         "lastModified": 1762538466,
@@ -83,11 +101,11 @@
         "nixpkgs-lib": "nixpkgs-lib"
       },
       "locked": {
-        "lastModified": 1754487366,
-        "narHash": "sha256-pHYj8gUBapuUzKV/kN/tR3Zvqc7o6gdFB9XKXIp1SQ8=",
+        "lastModified": 1765495779,
+        "narHash": "sha256-MhA7wmo/7uogLxiewwRRmIax70g6q1U/YemqTGoFHlM=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "af66ad14b28a127c5c0f3bbb298218fc63528a18",
+        "rev": "5635c32d666a59ec9a55cab87e898889869f7b71",
         "type": "github"
       },
       "original": {
@@ -156,15 +174,16 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1761368467,
-        "narHash": "sha256-eEs2YpE84+d6a8VKXCACNJy5czcu8GQCaeSZwR/mFMk=",
-        "owner": "lenianiva",
+        "lastModified": 1765602315,
+        "narHash": "sha256-edzV+L6baLm9gF1Bzxu9DqDcCFA8u/1/eYdc+Tq7kX8=",
+        "owner": "argumentcomputer",
         "repo": "lean4-nix",
-        "rev": "3550873ed1a87d666d633d34921e79abaa4671c1",
+        "rev": "9eda9f3a49e5ee23594b314c6889eb7fa09b6da7",
         "type": "github"
       },
       "original": {
-        "owner": "lenianiva",
+        "owner": "argumentcomputer",
+        "ref": "lake-incremental",
         "repo": "lean4-nix",
         "type": "github"
       }
@@ -175,15 +194,16 @@
         "nixpkgs": "nixpkgs_2"
       },
       "locked": {
-        "lastModified": 1761368467,
-        "narHash": "sha256-eEs2YpE84+d6a8VKXCACNJy5czcu8GQCaeSZwR/mFMk=",
-        "owner": "lenianiva",
+        "lastModified": 1765602315,
+        "narHash": "sha256-edzV+L6baLm9gF1Bzxu9DqDcCFA8u/1/eYdc+Tq7kX8=",
+        "owner": "argumentcomputer",
         "repo": "lean4-nix",
-        "rev": "3550873ed1a87d666d633d34921e79abaa4671c1",
+        "rev": "9eda9f3a49e5ee23594b314c6889eb7fa09b6da7",
         "type": "github"
       },
       "original": {
-        "owner": "lenianiva",
+        "owner": "argumentcomputer",
+        "ref": "lake-incremental",
         "repo": "lean4-nix",
         "type": "github"
       }
@@ -206,11 +226,11 @@
     },
     "nixpkgs-lib": {
       "locked": {
-        "lastModified": 1753579242,
-        "narHash": "sha256-zvaMGVn14/Zz8hnp4VWT9xVnhc8vuL3TStRqwk22biA=",
+        "lastModified": 1761765539,
+        "narHash": "sha256-b0yj6kfvO8ApcSE+QmA6mUfu8IYG6/uU28OFn4PaC8M=",
         "owner": "nix-community",
         "repo": "nixpkgs.lib",
-        "rev": "0f36c44e01a6129be94e3ade315a5883f0228a6e",
+        "rev": "719359f4562934ae99f5443f20aa06c2ffff91fc",
         "type": "github"
       },
       "original": {
@@ -276,6 +296,7 @@
     },
     "root": {
       "inputs": {
+        "blake3": "blake3",
         "blake3-lean": "blake3-lean",
         "crane": "crane",
         "fenix": "fenix",
diff --git a/flake.nix b/flake.nix
index d3c4344b..9ed5a795 100644
--- a/flake.nix
+++ b/flake.nix
@@ -15,7 +15,9 @@
     nixpkgs.follows = "lean4-nix/nixpkgs";
 
     # Lean 4 & Lake
-    lean4-nix.url = "github:lenianiva/lean4-nix";
+    #lean4-nix.url = "github:lenianiva/lean4-nix?ref=lake/static";
+    lean4-nix.url = "github:argumentcomputer/lean4-nix?ref=lake-incremental";
+    #lean4-nix.url = "github:lenianiva/lean4-nix?rev=f1e91cf5779d5987c219041daf45eecb00e40b7d";
 
     # Helper: flake-parts for easier outputs
     flake-parts.url = "github:hercules-ci/flake-parts";
@@ -29,9 +31,15 @@
 
     crane.url = "github:ipetkov/crane";
 
-    # Blake3 C dependency for static linking
+    blake3 = {
+      url = "github:BLAKE3-team/BLAKE3?ref=refs/tags/1.8.2";
+      flake = false;
+    };
+
+    # Blake3 C bindings for Lean
     blake3-lean = {
-      url = "github:argumentcomputer/Blake3.lean";
+      url = "github:argumentcomputer/Blake3.lean?ref=nix-lake";
+      #url = "path:/home/sam/repos/argument/Blake3.lean";
       # Follow lean4-nix nixpkgs so we stay in sync
       inputs.nixpkgs.follows = "lean4-nix/nixpkgs";
     };
@@ -43,6 +51,7 @@
     lean4-nix,
     fenix,
     crane,
+    blake3,
     blake3-lean,
     ...
   }:
@@ -60,7 +69,74 @@
         pkgs,
         ...
       }: let
-        lib = (import ./ix.nix {inherit system pkgs fenix crane lean4-nix blake3-lean;}).lib;
+        # Pins the Rust toolchain
+        rustToolchain = fenix.packages.${system}.fromToolchainFile {
+          file = ./rust-toolchain.toml;
+          sha256 = "sha256-SDu4snEWjuZU475PERvu+iO50Mi39KVjqCeJeNvpguU=";
+        };
+
+        # Rust package
+        craneLib = (crane.mkLib pkgs).overrideToolchain rustToolchain;
+        src = craneLib.cleanCargoSource ./.;
+        craneArgs = {
+          inherit src;
+          strictDeps = true;
+
+          buildInputs =
+            [
+              # Add additional build inputs here
+            ]
+            ++ pkgs.lib.optionals pkgs.stdenv.isDarwin [
+              # Additional darwin specific inputs can be set here
+              pkgs.libiconv
+            ];
+        };
+        craneLibLLvmTools = craneLib.overrideToolchain rustToolchain;
+        cargoArtifacts = craneLib.buildDepsOnly craneArgs;
+
+        rustPkg = craneLib.buildPackage (craneArgs
+          // {
+            inherit cargoArtifacts;
+          });
+
+        # Lake package
+        lake2nix = pkgs.callPackage lean4-nix.lake {};
+        lakeArgs = {
+          src = ./.;
+          depOverrideDeriv = {
+            Blake3 = blake3-lean.packages.${system}.default;
+          };
+          # Don't build the `ix_rs` static lib with Lake, since we build it with Crane
+          postPatch = ''
+            substituteInPlace lakefile.lean --replace-fail 'proc { cmd := "cargo"' '--proc { cmd := "cargo"'
+          '';
+          # Copy the `ix_rs` static lib from Crane to `target/release` so Lake can use it
+          postConfigure = ''
+            mkdir -p target/release
+            ln -s ${rustPkg}/lib/libix_rs.a target/release/
+          '';
+        };
+        lakeDeps = lake2nix.buildDeps {
+          src = ./.;
+          depOverrideDeriv = {
+            Blake3 = blake3-lean.packages.${system}.default;
+          };
+        };
+        ixLib = lake2nix.mkPackage (lakeArgs
+          // {
+            name = "Ix";
+          });
+        # Ix CLI
+        ixCLI = lake2nix.mkPackage (lakeArgs
+          // {
+            name = "ix";
+            installArtifacts = false;
+          });
+        ixTest = lake2nix.mkPackage (lakeArgs
+          // {
+            name = "IxTests";
+            installArtifacts = false;
+          });
       in {
         # Lean overlay
         _module.args.pkgs = import nixpkgs {
@@ -69,40 +145,32 @@
         };
 
         packages = {
-          # Ix CLI
-          default = lib.leanPkg.executable;
-
-          # Ix tests
-          test =
-            ((lean4-nix.lake {inherit pkgs;}).mkPackage {
-              src = ./.;
-              roots = ["Tests.Main" "Ix"];
-              deps = [lib.leanPkg];
-              staticLibDeps = ["${lib.rustPkg}/lib" "${lib.cPkg}/lib" "${lib.blake3C}/lib"];
-            }).executable;
-
-          # Ix benches
-          bench-aiur =
-            ((lean4-nix.lake {inherit pkgs;}).mkPackage {
-              src = ./.;
-              roots = ["Benchmarks.Aiur" "Ix"];
-              deps = [lib.leanPkg];
-              staticLibDeps = ["${lib.rustPkg}/lib" "${lib.cPkg}/lib" "${lib.blake3C}/lib"];
-            }).executable;
-
-          bench-blake3 =
-            ((lean4-nix.lake {inherit pkgs;}).mkPackage {
-              src = ./.;
-              roots = ["Benchmarks.Blake3" "Ix"];
-              deps = [lib.leanPkg];
-              staticLibDeps = ["${lib.rustPkg}/lib" "${lib.cPkg}/lib" "${lib.blake3C}/lib"];
-            }).executable;
-
-          # Rust static lib, needed for static linking downstream
-          rustStaticLib = lib.rustPkg;
-
-          # C static lib, needed for static linking downstream
-          cStaticLib = lib.cPkg;
+          default = ixLib;
+          ix = ixCLI;
+          test = ixTest;
+
+          ## Ix benches
+          #bench-aiur =
+          #  ((lean4-nix.lake {inherit pkgs;}).mkPackage {
+          #    src = ./.;
+          #    roots = ["Benchmarks.Aiur" "Ix"];
+          #    deps = [lib.leanPkg];
+          #    staticLibDeps = ["${lib.rustPkg}/lib" "${lib.cPkg}/lib" "${lib.blake3C}/lib"];
+          #  }).executable;
+
+          #bench-blake3 =
+          #  ((lean4-nix.lake {inherit pkgs;}).mkPackage {
+          #    src = ./.;
+          #    roots = ["Benchmarks.Blake3" "Ix"];
+          #    deps = [lib.leanPkg];
+          #    staticLibDeps = ["${lib.rustPkg}/lib" "${lib.cPkg}/lib" "${lib.blake3C}/lib"];
+          #  }).executable;
+
+          ## Rust static lib, needed for static linking downstream
+          #rustStaticLib = lib.rustPkg;
+
+          ## C static lib, needed for static linking downstream
+          #cStaticLib = lib.cPkg;
         };
 
         # Provide a unified dev shell with Lean + Rust
@@ -113,7 +181,7 @@
             ocl-icd
             gcc
             clang
-            lib.rustToolchain
+            rustToolchain
             rust-analyzer
             lean.lean-all # Includes Lean compiler, lake, stdlib, etc.
           ];
diff --git a/ix.nix b/ix.nix
deleted file mode 100644
index d2521413..00000000
--- a/ix.nix
+++ /dev/null
@@ -1,96 +0,0 @@
-{
-  system,
-  pkgs,
-  fenix,
-  crane,
-  lean4-nix,
-  blake3-lean,
-}: let
-  # Pins the Rust toolchain
-  rustToolchain = fenix.packages.${system}.fromToolchainFile {
-    file = ./rust-toolchain.toml;
-    sha256 = "sha256-SDu4snEWjuZU475PERvu+iO50Mi39KVjqCeJeNvpguU=";
-  };
-
-  # Rust package
-  craneLib = (crane.mkLib pkgs).overrideToolchain rustToolchain;
-  src = craneLib.cleanCargoSource ./.;
-  commonArgs = {
-    inherit src;
-    strictDeps = true;
-
-    buildInputs =
-      [
-        # Add additional build inputs here
-      ]
-      ++ pkgs.lib.optionals pkgs.stdenv.isDarwin [
-        # Additional darwin specific inputs can be set here
-        pkgs.libiconv
-      ];
-  };
-  craneLibLLvmTools = craneLib.overrideToolchain rustToolchain;
-  cargoArtifacts = craneLib.buildDepsOnly commonArgs;
-
-  rustPkg = craneLib.buildPackage (commonArgs
-    // {
-      inherit cargoArtifacts;
-    });
-
-  # C Package
-  cPkg = let
-    # Function to get all files in `./c` ending with given extension
-    getFiles = ext: builtins.filter (file: builtins.match (".*" + ext) file != null) (builtins.attrNames (builtins.readDir "${toString ./c}"));
-    # Gets all C files in `./c`, without the extension
-    cFiles = let ext = ".c"; in builtins.map (file: builtins.replaceStrings [ext] [""] file) (getFiles ext);
-    # Creates `gcc -c` command for each C file
-    buildCmd = builtins.map (file: "${pkgs.gcc}/bin/gcc -Wall -Werror -Wextra -c ${file}.c -o ${file}.o") cFiles;
-    # Final `buildPhase` instructions
-    buildSteps =
-      buildCmd
-      ++ [
-        "ar rcs libix_c.a ${builtins.concatStringsSep " " (builtins.map (file: "${file}.o") cFiles)}"
-      ];
-    # Gets all header files in `./c`
-    hFiles = getFiles ".h";
-    # Final `installPhase` instructions
-    installSteps = [
-      "mkdir -p $out/lib $out/include"
-      "cp libix_c.a $out/lib/"
-      "cp ${builtins.concatStringsSep " " hFiles} $out/include/"
-    ];
-  in
-    pkgs.stdenv.mkDerivation {
-      pname = "ix_c";
-      version = "0.1.0";
-      src = ./c;
-      buildInputs = [pkgs.gcc pkgs.lean.lean-all rustPkg];
-      # Builds the C files
-      buildPhase = builtins.concatStringsSep "\n" buildSteps;
-      # Installs the library files
-      installPhase = builtins.concatStringsSep "\n" installSteps;
-    };
-
-  # Blake3.lean C FFI dependency, needed for explicit static lib linking
-  blake3C = blake3-lean.packages.${system}.staticLib;
-
-  # Lean package, builds the Ix binary and links to FFI static libs
-  # Note: downstream users of Ix as a library should import it in the lakefile,
-  # only need to include the static libs as below in the final `mkPackage`
-  leanPkg = (lean4-nix.lake {inherit pkgs;}).mkPackage {
-    src = ./.;
-    roots = ["Ix" "Main"];
-    staticLibDeps = ["${rustPkg}/lib" "${cPkg}/lib" "${blake3C}/lib"];
-  };
-
-  lib = {
-    inherit
-      rustToolchain
-      blake3C
-      rustPkg
-      cPkg
-      leanPkg
-      ;
-  };
-in {
-  inherit lib;
-}
diff --git a/lake-manifest.json b/lake-manifest.json
index 2e51562a..4e76579b 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -8,7 +8,7 @@
    "rev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee",
+   "inputRev": "v4.24.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -25,10 +25,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "732daca6c67f3be3ca44837643cfda906503e9ac",
+   "rev": "0621f140c4ece58efaf61dc73cbf753cb140d99a",
    "name": "Blake3",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "732daca6c67f3be3ca44837643cfda906503e9ac",
+   "inputRev": "nix-lake",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/argumentcomputer/LSpec",
@@ -40,6 +40,16 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": "b05e6b83798bce0887eb5001cb10fdcbe675dde3",
    "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/aesop.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "725ac8cd67acd70a7beaf47c3725e23484c1ef50",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.24.0",
+   "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "ix",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index 88b667dc..013f7777 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -5,7 +5,8 @@ package ix where
   version := v!"0.1.0"
 
 @[default_target]
-lean_lib Ix
+lean_lib Ix where
+  --needs := #[(PartialBuildKey.parse "ix_c").toOption.get!, (PartialBuildKey.parse "ix_rs").toOption.get!]
 
 lean_exe ix where
   root := `Main
@@ -15,25 +16,27 @@ require LSpec from git
   "https://github.com/argumentcomputer/LSpec" @ "b05e6b83798bce0887eb5001cb10fdcbe675dde3"
 
 require Blake3 from git
-  "https://github.com/argumentcomputer/Blake3.lean" @ "732daca6c67f3be3ca44837643cfda906503e9ac"
+  "https://github.com/argumentcomputer/Blake3.lean" @ "nix-lake"
+--require Blake3 from "/home/sam/repos/argument/Blake3.lean"
 
 require Cli from git
   "https://github.com/leanprover/lean4-cli" @ "91c18fa62838ad0ab7384c03c9684d99d306e1da"
 
 require batteries from git
-  "https://github.com/leanprover-community/batteries" @ "8da40b72fece29b7d3fe3d768bac4c8910ce9bee"
+  "https://github.com/leanprover-community/batteries" @ "v4.24.0"
 
 section Tests
 
 lean_lib Tests
 
 @[test_driver]
-lean_exe Tests.Main where
+lean_exe IxTests where
+  root := `Tests.Main
   supportInterpreter := true
 
 end Tests
 
-lean_lib IxTest where
+lean_lib IxTestLib where
   srcDir := "ix_test"
 
 section IxApplications

From 311e7651c6ca3c3c950fe17f0374fe4b856d1fb1 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Wed, 17 Dec 2025 14:01:24 -0500
Subject: [PATCH 2/6] Update

---
 flake.lock | 18 +++++++-------
 flake.nix  | 69 ++++++++++++++++++++----------------------------------
 2 files changed, 34 insertions(+), 53 deletions(-)

diff --git a/flake.lock b/flake.lock
index 053dfb56..d7cf36fe 100644
--- a/flake.lock
+++ b/flake.lock
@@ -28,11 +28,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1765602345,
-        "narHash": "sha256-FWyiv5M4qHyOzm6E0SeuumQXP+0K1vJVCRb0Tn8NNOc=",
+        "lastModified": 1765814129,
+        "narHash": "sha256-Fwa21fGAuUh0RKSAhrZ5RJQGBoOPb2IxuubONaezv4U=",
         "owner": "argumentcomputer",
         "repo": "Blake3.lean",
-        "rev": "1dc03fe74d74c2f33303b4aa60736599e9ee8667",
+        "rev": "f1d8fb2b442a8a60793920fb0818762b6f851238",
         "type": "github"
       },
       "original": {
@@ -174,11 +174,11 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1765602315,
-        "narHash": "sha256-edzV+L6baLm9gF1Bzxu9DqDcCFA8u/1/eYdc+Tq7kX8=",
+        "lastModified": 1765813927,
+        "narHash": "sha256-apHaj2EB85CLX3v4RL7emJS++4e2s6P8gyKOKlfgrcY=",
         "owner": "argumentcomputer",
         "repo": "lean4-nix",
-        "rev": "9eda9f3a49e5ee23594b314c6889eb7fa09b6da7",
+        "rev": "6bee46590ca0a5aef74216f07474d71742881b77",
         "type": "github"
       },
       "original": {
@@ -194,11 +194,11 @@
         "nixpkgs": "nixpkgs_2"
       },
       "locked": {
-        "lastModified": 1765602315,
-        "narHash": "sha256-edzV+L6baLm9gF1Bzxu9DqDcCFA8u/1/eYdc+Tq7kX8=",
+        "lastModified": 1765821102,
+        "narHash": "sha256-XsiGKqQ2b2oZmP1wVd1iVo4XVpMwyZ19fFr80y88cBA=",
         "owner": "argumentcomputer",
         "repo": "lean4-nix",
-        "rev": "9eda9f3a49e5ee23594b314c6889eb7fa09b6da7",
+        "rev": "fbf792ea4241c6364d3fb338413bce6175ba66b5",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index 9ed5a795..d14f726b 100644
--- a/flake.nix
+++ b/flake.nix
@@ -15,9 +15,8 @@
     nixpkgs.follows = "lean4-nix/nixpkgs";
 
     # Lean 4 & Lake
-    #lean4-nix.url = "github:lenianiva/lean4-nix?ref=lake/static";
+    #lean4-nix.url = "github:lenianiva/lean4-nix";
     lean4-nix.url = "github:argumentcomputer/lean4-nix?ref=lake-incremental";
-    #lean4-nix.url = "github:lenianiva/lean4-nix?rev=f1e91cf5779d5987c219041daf45eecb00e40b7d";
 
     # Helper: flake-parts for easier outputs
     flake-parts.url = "github:hercules-ci/flake-parts";
@@ -39,7 +38,6 @@
     # Blake3 C bindings for Lean
     blake3-lean = {
       url = "github:argumentcomputer/Blake3.lean?ref=nix-lake";
-      #url = "path:/home/sam/repos/argument/Blake3.lean";
       # Follow lean4-nix nixpkgs so we stay in sync
       inputs.nixpkgs.follows = "lean4-nix/nixpkgs";
     };
@@ -83,15 +81,12 @@
           strictDeps = true;
 
           buildInputs =
-            [
-              # Add additional build inputs here
-            ]
+            []
             ++ pkgs.lib.optionals pkgs.stdenv.isDarwin [
               # Additional darwin specific inputs can be set here
               pkgs.libiconv
             ];
         };
-        craneLibLLvmTools = craneLib.overrideToolchain rustToolchain;
         cargoArtifacts = craneLib.buildDepsOnly craneArgs;
 
         rustPkg = craneLib.buildPackage (craneArgs
@@ -101,7 +96,14 @@
 
         # Lake package
         lake2nix = pkgs.callPackage lean4-nix.lake {};
+        lakeDeps = lake2nix.buildDeps {
+          src = ./.;
+          depOverrideDeriv = {
+            Blake3 = blake3-lean.packages.${system}.default;
+          };
+        };
         lakeArgs = {
+          inherit lakeDeps;
           src = ./.;
           depOverrideDeriv = {
             Blake3 = blake3-lean.packages.${system}.default;
@@ -109,34 +111,33 @@
           # Don't build the `ix_rs` static lib with Lake, since we build it with Crane
           postPatch = ''
             substituteInPlace lakefile.lean --replace-fail 'proc { cmd := "cargo"' '--proc { cmd := "cargo"'
+            cat lakefile.lean
           '';
           # Copy the `ix_rs` static lib from Crane to `target/release` so Lake can use it
           postConfigure = ''
             mkdir -p target/release
+            echo "RUNNING POST CONFIGURE"
+            ls -alh target/release
             ln -s ${rustPkg}/lib/libix_rs.a target/release/
+            echo "LINKED libix_rs.a"
+            ls -alh target/release
           '';
         };
-        lakeDeps = lake2nix.buildDeps {
-          src = ./.;
-          depOverrideDeriv = {
-            Blake3 = blake3-lean.packages.${system}.default;
-          };
-        };
         ixLib = lake2nix.mkPackage (lakeArgs
           // {
             name = "Ix";
+            buildLibrary = true;
           });
-        # Ix CLI
-        ixCLI = lake2nix.mkPackage (lakeArgs
+        lakeBinArgs =
+          lakeArgs
           // {
-            name = "ix";
+            lakeArtifacts = ixLib;
             installArtifacts = false;
-          });
-        ixTest = lake2nix.mkPackage (lakeArgs
-          // {
-            name = "IxTests";
-            installArtifacts = false;
-          });
+          };
+        ixCLI = lake2nix.mkPackage (lakeBinArgs // {name = "ix";});
+        ixTest = lake2nix.mkPackage (lakeBinArgs // {name = "IxTests";});
+        benchAiur = lake2nix.mkPackage (lakeBinArgs // {name = "bench-aiur";});
+        benchBlake3 = lake2nix.mkPackage (lakeBinArgs // {name = "bench-blake3";});
       in {
         # Lean overlay
         _module.args.pkgs = import nixpkgs {
@@ -148,29 +149,9 @@
           default = ixLib;
           ix = ixCLI;
           test = ixTest;
-
           ## Ix benches
-          #bench-aiur =
-          #  ((lean4-nix.lake {inherit pkgs;}).mkPackage {
-          #    src = ./.;
-          #    roots = ["Benchmarks.Aiur" "Ix"];
-          #    deps = [lib.leanPkg];
-          #    staticLibDeps = ["${lib.rustPkg}/lib" "${lib.cPkg}/lib" "${lib.blake3C}/lib"];
-          #  }).executable;
-
-          #bench-blake3 =
-          #  ((lean4-nix.lake {inherit pkgs;}).mkPackage {
-          #    src = ./.;
-          #    roots = ["Benchmarks.Blake3" "Ix"];
-          #    deps = [lib.leanPkg];
-          #    staticLibDeps = ["${lib.rustPkg}/lib" "${lib.cPkg}/lib" "${lib.blake3C}/lib"];
-          #  }).executable;
-
-          ## Rust static lib, needed for static linking downstream
-          #rustStaticLib = lib.rustPkg;
-
-          ## C static lib, needed for static linking downstream
-          #cStaticLib = lib.cPkg;
+          bench-aiur = benchAiur;
+          bench-blake3 = benchBlake3;
         };
 
         # Provide a unified dev shell with Lean + Rust

From 7a1c27f8bede6bab3929f97c0a38f3eb48c949ab Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Sat, 20 Dec 2025 07:33:11 -0500
Subject: [PATCH 3/6] (WIP) chore: Update Lean to v4.26.0

---
 Ix/Address.lean         |   2 +-
 Ix/Benchmark/Bench.lean |   4 +-
 Ix/Common.lean          |   4 +-
 Ix/CompileM.lean        |   2 +-
 Ix/Store.lean           |   8 ++-
 Tests/Ix.lean           |  10 +--
 flake.lock              | 133 ++++++++--------------------------------
 flake.nix               |  58 ++++++++----------
 lake-manifest.json      |  26 +++-----
 lakefile.lean           |  10 ++-
 lean-toolchain          |   2 +-
 11 files changed, 79 insertions(+), 180 deletions(-)

diff --git a/Ix/Address.lean b/Ix/Address.lean
index acdd2228..7c9a6f84 100644
--- a/Ix/Address.lean
+++ b/Ix/Address.lean
@@ -60,7 +60,7 @@ def natOfHex : Char -> Option Nat
 def hexOfByte (b : UInt8) : String :=
   let hi := hexOfNat (UInt8.toNat (b >>> 4))
   let lo := hexOfNat (UInt8.toNat (b &&& 0xF))
-  String.mk [hi.get!, lo.get!]
+  String.ofList [hi.get!, lo.get!]
 
 /-- Convert a ByteArray to a big-endian hexadecimal string. -/
 def hexOfBytes (ba : ByteArray) : String :=
diff --git a/Ix/Benchmark/Bench.lean b/Ix/Benchmark/Bench.lean
index 178017ba..30de8e62 100644
--- a/Ix/Benchmark/Bench.lean
+++ b/Ix/Benchmark/Bench.lean
@@ -333,10 +333,10 @@ def padWhitespace (input : String) (width : Nat) : String :=
   let padWidth := width - input.length 
   let leftPad := padWidth / 2
   let rightPad := padWidth - leftPad
-  String.mk (List.replicate leftPad ' ') ++ input ++ (String.mk (List.replicate rightPad ' '))
+  String.ofList (List.replicate leftPad ' ') ++ input ++ (String.ofList (List.replicate rightPad ' '))
 
 def padDashes (width : Nat) : String :=
-  String.mk (List.replicate width '-')
+  String.ofList (List.replicate width '-')
 
 def mkReportPretty' (columnWidths : ColumnWidths) (reportPretty : String) (row : BenchReport) : String :=
   let functionStr := padWhitespace row.function columnWidths.function
diff --git a/Ix/Common.lean b/Ix/Common.lean
index e5052730..530ec568 100644
--- a/Ix/Common.lean
+++ b/Ix/Common.lean
@@ -38,8 +38,8 @@ deriving instance BEq, Repr, Ord, Hashable for Lean.QuotKind
 deriving instance BEq, Repr, Ord, Hashable for Lean.ReducibilityHints
 deriving instance BEq, Repr, Ord, Hashable for Lean.DefinitionSafety
 deriving instance BEq, Repr, Ord, Hashable for ByteArray
-deriving instance BEq, Repr, Ord, Hashable for String.Pos
-deriving instance BEq, Repr, Ord, Hashable for Substring
+deriving instance BEq, Repr, Ord, Hashable for String.Pos.Raw
+deriving instance BEq, Repr, Ord, Hashable for Substring.Raw
 deriving instance BEq, Repr, Ord, Hashable for Lean.SourceInfo
 deriving instance BEq, Repr, Ord, Hashable for Lean.Syntax.Preresolved
 deriving instance BEq, Repr, Ord, Hashable for Lean.Syntax
diff --git a/Ix/CompileM.lean b/Ix/CompileM.lean
index e21bc3e7..d276bf71 100644
--- a/Ix/CompileM.lean
+++ b/Ix/CompileM.lean
@@ -227,7 +227,7 @@ def compileLevel (lvl: Lean.Level): CompileM MetaAddress := do
       | none   => do throw <| .levelNotFound (<- read).current n lvls s!"compileLevel"
     | l@(.mvar ..) => throw $ .levelMetavariable l
 
-def compileSubstring : Substring -> CompileM Ixon.Substring
+def compileSubstring : Substring.Raw -> CompileM Ixon.Substring
 | ⟨str, startPos, stopPos⟩ => do
     pure ⟨<- storeString str, startPos.byteIdx, stopPos.byteIdx⟩
 
diff --git a/Ix/Store.lean b/Ix/Store.lean
index 9bf05b73..a476a5e3 100644
--- a/Ix/Store.lean
+++ b/Ix/Store.lean
@@ -43,9 +43,11 @@ def storeDir : StoreIO FilePath := do
 def storePath (addr: Address): StoreIO FilePath := do
   let store <- storeDir
   let hex := hexOfBytes addr.hash
-  let dir1 := String.mk [(hex.get ⟨0⟩), (hex.get ⟨1⟩)]
-  let dir2 := String.mk [(hex.get ⟨2⟩), (hex.get ⟨3⟩)]
-  let dir3 := String.mk [(hex.get ⟨4⟩), (hex.get ⟨5⟩)]
+  -- TODO: Use Slice API once it matures
+  let hexChars := hex.toSlice.chars.toList
+  let dir1 := String.ofList [hexChars[0]!, hexChars[1]!]
+  let dir2 := String.ofList [hexChars[2]!, hexChars[3]!]
+  let dir3 := String.ofList [hexChars[4]!, hexChars[5]!]
   let file := hex.drop 6
   let path := store / dir1 / dir2 / dir3
   if !(<- path.pathExists) then
diff --git a/Tests/Ix.lean b/Tests/Ix.lean
index ccef1c14..5db23ab4 100644
--- a/Tests/Ix.lean
+++ b/Tests/Ix.lean
@@ -119,7 +119,7 @@ def parseHex (x : String) : ByteArray :=
   let x :=
     if x.startsWith "0x" || x.startsWith "0X" then x.drop 2 else x
   -- remove underscores
-  let x := String.mk (x.toList.filter (· ≠ '_'))
+  let x := String.ofList (x.toList.filter (· ≠ '_'))
   -- must have an even number of hex digits
   if x.length % 2 = 1 then
     panic! "parseHex: odd number of hex digits"
@@ -128,8 +128,8 @@ def parseHex (x : String) : ByteArray :=
     let rec loop (i : Nat) (acc : ByteArray) : ByteArray :=
       if i < n then
         -- safe since ASCII: `String.get!` indexes by chars
-        let c1 := x.get! ⟨i⟩
-        let c2 := x.get! ⟨i+1⟩
+        let c1 := String.Pos.Raw.get! x ⟨i⟩ 
+        let c2 := String.Pos.Raw.get! x ⟨i+1⟩
         match hexVal? c1, hexVal? c2 with
         | some hi, some lo =>
           let b : UInt8 := (hi <<< 4) ||| lo
@@ -148,8 +148,8 @@ def printHex (ba : ByteArray) : String :=
       let b := ba.get! i
       let hi := (b.toNat / 16)
       let lo := (b.toNat % 16)
-      let acc := acc.push (hexdigits.get! ⟨hi⟩)
-      let acc := acc.push (hexdigits.get! ⟨lo⟩)
+      let acc := acc.push (String.Pos.Raw.get! hexdigits ⟨hi⟩)
+      let acc := acc.push (String.Pos.Raw.get! hexdigits ⟨lo⟩)
       go (i + 1) acc
     else acc
   "0x" ++ go 0 ""
diff --git a/flake.lock b/flake.lock
index d7cf36fe..ac3d9682 100644
--- a/flake.lock
+++ b/flake.lock
@@ -19,46 +19,30 @@
     },
     "blake3-lean": {
       "inputs": {
-        "blake3": "blake3_2",
+        "blake3": "blake3",
         "flake-parts": "flake-parts",
-        "lean4-nix": "lean4-nix",
+        "lean4-nix": [
+          "lean4-nix"
+        ],
         "nixpkgs": [
           "lean4-nix",
           "nixpkgs"
         ]
       },
       "locked": {
-        "lastModified": 1765814129,
-        "narHash": "sha256-Fwa21fGAuUh0RKSAhrZ5RJQGBoOPb2IxuubONaezv4U=",
+        "lastModified": 1766006980,
+        "narHash": "sha256-6o2JzJHKA2TnkxDjRPmYSxvhAom35poLkxrvFx5X0Q0=",
         "owner": "argumentcomputer",
         "repo": "Blake3.lean",
-        "rev": "f1d8fb2b442a8a60793920fb0818762b6f851238",
+        "rev": "c42d5a54a142c195ea8a2643b423bcdf7d61ad9f",
         "type": "github"
       },
       "original": {
         "owner": "argumentcomputer",
-        "ref": "nix-lake",
         "repo": "Blake3.lean",
         "type": "github"
       }
     },
-    "blake3_2": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1745192552,
-        "narHash": "sha256-IABVErXWYQFXZcwsFKfQhm3ox7UZUcW5uzVrGwsSp94=",
-        "owner": "BLAKE3-team",
-        "repo": "BLAKE3",
-        "rev": "df610ddc3b93841ffc59a87e3da659a15910eb46",
-        "type": "github"
-      },
-      "original": {
-        "owner": "BLAKE3-team",
-        "ref": "refs/tags/1.8.2",
-        "repo": "BLAKE3",
-        "type": "github"
-      }
-    },
     "crane": {
       "locked": {
         "lastModified": 1762538466,
@@ -101,11 +85,11 @@
         "nixpkgs-lib": "nixpkgs-lib"
       },
       "locked": {
-        "lastModified": 1765495779,
-        "narHash": "sha256-MhA7wmo/7uogLxiewwRRmIax70g6q1U/YemqTGoFHlM=",
+        "lastModified": 1765835352,
+        "narHash": "sha256-XswHlK/Qtjasvhd1nOa1e8MgZ8GS//jBoTqWtrS1Giw=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "5635c32d666a59ec9a55cab87e898889869f7b71",
+        "rev": "a34fae9c08a15ad73f295041fec82323541400a9",
         "type": "github"
       },
       "original": {
@@ -118,24 +102,6 @@
       "inputs": {
         "nixpkgs-lib": "nixpkgs-lib_2"
       },
-      "locked": {
-        "lastModified": 1727826117,
-        "narHash": "sha256-K5ZLCyfO/Zj9mPFldf3iwS6oZStJcU4tSpiXTMYaaL0=",
-        "owner": "hercules-ci",
-        "repo": "flake-parts",
-        "rev": "3d04084d54bedc3d6b8b736c70ef449225c361b1",
-        "type": "github"
-      },
-      "original": {
-        "owner": "hercules-ci",
-        "repo": "flake-parts",
-        "type": "github"
-      }
-    },
-    "flake-parts_3": {
-      "inputs": {
-        "nixpkgs-lib": "nixpkgs-lib_3"
-      },
       "locked": {
         "lastModified": 1762980239,
         "narHash": "sha256-8oNVE8TrD19ulHinjaqONf9QWCKK+w4url56cdStMpM=",
@@ -150,9 +116,9 @@
         "type": "github"
       }
     },
-    "flake-parts_4": {
+    "flake-parts_3": {
       "inputs": {
-        "nixpkgs-lib": "nixpkgs-lib_4"
+        "nixpkgs-lib": "nixpkgs-lib_3"
       },
       "locked": {
         "lastModified": 1727826117,
@@ -170,41 +136,21 @@
     },
     "lean4-nix": {
       "inputs": {
-        "flake-parts": "flake-parts_2",
+        "flake-parts": "flake-parts_3",
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1765813927,
-        "narHash": "sha256-apHaj2EB85CLX3v4RL7emJS++4e2s6P8gyKOKlfgrcY=",
-        "owner": "argumentcomputer",
+        "lastModified": 1766003746,
+        "narHash": "sha256-S3e45gKBtTZ4bDqfrddB7A3dxcZb8jY0ROPu6Aw+ZEk=",
+        "owner": "lenianiva",
         "repo": "lean4-nix",
-        "rev": "6bee46590ca0a5aef74216f07474d71742881b77",
+        "rev": "0bca9d30803e3d65157240e67045badbc547dd45",
         "type": "github"
       },
       "original": {
-        "owner": "argumentcomputer",
-        "ref": "lake-incremental",
-        "repo": "lean4-nix",
-        "type": "github"
-      }
-    },
-    "lean4-nix_2": {
-      "inputs": {
-        "flake-parts": "flake-parts_4",
-        "nixpkgs": "nixpkgs_2"
-      },
-      "locked": {
-        "lastModified": 1765821102,
-        "narHash": "sha256-XsiGKqQ2b2oZmP1wVd1iVo4XVpMwyZ19fFr80y88cBA=",
-        "owner": "argumentcomputer",
-        "repo": "lean4-nix",
-        "rev": "fbf792ea4241c6364d3fb338413bce6175ba66b5",
-        "type": "github"
-      },
-      "original": {
-        "owner": "argumentcomputer",
-        "ref": "lake-incremental",
+        "owner": "lenianiva",
         "repo": "lean4-nix",
+        "rev": "0bca9d30803e3d65157240e67045badbc547dd45",
         "type": "github"
       }
     },
@@ -226,11 +172,11 @@
     },
     "nixpkgs-lib": {
       "locked": {
-        "lastModified": 1761765539,
-        "narHash": "sha256-b0yj6kfvO8ApcSE+QmA6mUfu8IYG6/uU28OFn4PaC8M=",
+        "lastModified": 1765674936,
+        "narHash": "sha256-k00uTP4JNfmejrCLJOwdObYC9jHRrr/5M/a/8L2EIdo=",
         "owner": "nix-community",
         "repo": "nixpkgs.lib",
-        "rev": "719359f4562934ae99f5443f20aa06c2ffff91fc",
+        "rev": "2075416fcb47225d9b68ac469a5c4801a9c4dd85",
         "type": "github"
       },
       "original": {
@@ -240,18 +186,6 @@
       }
     },
     "nixpkgs-lib_2": {
-      "locked": {
-        "lastModified": 1727825735,
-        "narHash": "sha256-0xHYkMkeLVQAMa7gvkddbPqpxph+hDzdu1XdGPJR+Os=",
-        "type": "tarball",
-        "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
-      },
-      "original": {
-        "type": "tarball",
-        "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
-      }
-    },
-    "nixpkgs-lib_3": {
       "locked": {
         "lastModified": 1761765539,
         "narHash": "sha256-b0yj6kfvO8ApcSE+QmA6mUfu8IYG6/uU28OFn4PaC8M=",
@@ -266,7 +200,7 @@
         "type": "github"
       }
     },
-    "nixpkgs-lib_4": {
+    "nixpkgs-lib_3": {
       "locked": {
         "lastModified": 1727825735,
         "narHash": "sha256-0xHYkMkeLVQAMa7gvkddbPqpxph+hDzdu1XdGPJR+Os=",
@@ -278,30 +212,13 @@
         "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
       }
     },
-    "nixpkgs_2": {
-      "locked": {
-        "lastModified": 1743095683,
-        "narHash": "sha256-gWd4urRoLRe8GLVC/3rYRae1h+xfQzt09xOfb0PaHSk=",
-        "owner": "nixos",
-        "repo": "nixpkgs",
-        "rev": "5e5402ecbcb27af32284d4a62553c019a3a49ea6",
-        "type": "github"
-      },
-      "original": {
-        "owner": "nixos",
-        "ref": "nixos-unstable",
-        "repo": "nixpkgs",
-        "type": "github"
-      }
-    },
     "root": {
       "inputs": {
-        "blake3": "blake3",
         "blake3-lean": "blake3-lean",
         "crane": "crane",
         "fenix": "fenix",
-        "flake-parts": "flake-parts_3",
-        "lean4-nix": "lean4-nix_2",
+        "flake-parts": "flake-parts_2",
+        "lean4-nix": "lean4-nix",
         "nixpkgs": [
           "lean4-nix",
           "nixpkgs"
diff --git a/flake.nix b/flake.nix
index d14f726b..be61f13e 100644
--- a/flake.nix
+++ b/flake.nix
@@ -15,8 +15,7 @@
     nixpkgs.follows = "lean4-nix/nixpkgs";
 
     # Lean 4 & Lake
-    #lean4-nix.url = "github:lenianiva/lean4-nix";
-    lean4-nix.url = "github:argumentcomputer/lean4-nix?ref=lake-incremental";
+    lean4-nix.url = "github:lenianiva/lean4-nix?rev=0bca9d30803e3d65157240e67045badbc547dd45";
 
     # Helper: flake-parts for easier outputs
     flake-parts.url = "github:hercules-ci/flake-parts";
@@ -30,15 +29,11 @@
 
     crane.url = "github:ipetkov/crane";
 
-    blake3 = {
-      url = "github:BLAKE3-team/BLAKE3?ref=refs/tags/1.8.2";
-      flake = false;
-    };
-
     # Blake3 C bindings for Lean
     blake3-lean = {
-      url = "github:argumentcomputer/Blake3.lean?ref=nix-lake";
-      # Follow lean4-nix nixpkgs so we stay in sync
+      url = "github:argumentcomputer/Blake3.lean";
+      # System packages, follows lean4-nix so we stay in sync
+      inputs.lean4-nix.follows = "lean4-nix";
       inputs.nixpkgs.follows = "lean4-nix/nixpkgs";
     };
   };
@@ -49,7 +44,6 @@
     lean4-nix,
     fenix,
     crane,
-    blake3,
     blake3-lean,
     ...
   }:
@@ -96,40 +90,38 @@
 
         # Lake package
         lake2nix = pkgs.callPackage lean4-nix.lake {};
-        lakeDeps = lake2nix.buildDeps {
+        lakeDepArgs = {
           src = ./.;
-          depOverrideDeriv = {
-            Blake3 = blake3-lean.packages.${system}.default;
-          };
         };
-        lakeArgs = {
-          inherit lakeDeps;
+        lakeDeps = lake2nix.buildDeps {
           src = ./.;
           depOverrideDeriv = {
             Blake3 = blake3-lean.packages.${system}.default;
           };
-          # Don't build the `ix_rs` static lib with Lake, since we build it with Crane
-          postPatch = ''
-            substituteInPlace lakefile.lean --replace-fail 'proc { cmd := "cargo"' '--proc { cmd := "cargo"'
-            cat lakefile.lean
-          '';
-          # Copy the `ix_rs` static lib from Crane to `target/release` so Lake can use it
-          postConfigure = ''
-            mkdir -p target/release
-            echo "RUNNING POST CONFIGURE"
-            ls -alh target/release
-            ln -s ${rustPkg}/lib/libix_rs.a target/release/
-            echo "LINKED libix_rs.a"
-            ls -alh target/release
-          '';
         };
-        ixLib = lake2nix.mkPackage (lakeArgs
+        lakeBuildArgs =
+          lakeDepArgs
+          // {
+            inherit lakeDeps;
+            # Don't build the `ix_rs` static lib with Lake, since we build it with Crane
+            postPatch = ''
+              substituteInPlace lakefile.lean --replace-fail "let args := match (ixNoPar, ixNet)" "let _args := match (ixNoPar, ixNet)"
+              substituteInPlace lakefile.lean --replace-fail 'proc { cmd := "cargo"' '--proc { cmd := "cargo"'
+              cat lakefile.lean
+            '';
+            # Copy the `ix_rs` static lib from Crane to `target/release` so Lake can use it
+            postConfigure = ''
+              mkdir -p target/release
+              ln -s ${rustPkg}/lib/libix_rs.a target/release/
+            '';
+          };
+        ixLib = lake2nix.mkPackage (lakeBuildArgs
           // {
             name = "Ix";
             buildLibrary = true;
           });
         lakeBinArgs =
-          lakeArgs
+          lakeBuildArgs
           // {
             lakeArtifacts = ixLib;
             installArtifacts = false;
@@ -149,7 +141,7 @@
           default = ixLib;
           ix = ixCLI;
           test = ixTest;
-          ## Ix benches
+          # Ix benches
           bench-aiur = benchAiur;
           bench-blake3 = benchBlake3;
         };
diff --git a/lake-manifest.json b/lake-manifest.json
index 4e76579b..a75b32c1 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,51 +5,41 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee",
+   "rev": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.24.0",
+   "inputRev": "v4.26.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "91c18fa62838ad0ab7384c03c9684d99d306e1da",
+   "rev": "933fce7e893f65969714c60cdb4bd8376786044e",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "91c18fa62838ad0ab7384c03c9684d99d306e1da",
+   "inputRev": "v4.26.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/argumentcomputer/Blake3.lean",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0621f140c4ece58efaf61dc73cbf753cb140d99a",
+   "rev": "c42d5a54a142c195ea8a2643b423bcdf7d61ad9f",
    "name": "Blake3",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nix-lake",
+   "inputRev": "c42d5a54a142c195ea8a2643b423bcdf7d61ad9f",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/argumentcomputer/LSpec",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b05e6b83798bce0887eb5001cb10fdcbe675dde3",
+   "rev": "fdf848d6cda9f080a09e49e760e2d6f70878800b",
    "name": "LSpec",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "b05e6b83798bce0887eb5001cb10fdcbe675dde3",
+   "inputRev": "fdf848d6cda9f080a09e49e760e2d6f70878800b",
    "inherited": false,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/aesop.git",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "725ac8cd67acd70a7beaf47c3725e23484c1ef50",
-   "name": "aesop",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.24.0",
-   "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "ix",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index 013f7777..a19ccbd7 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -6,24 +6,22 @@ package ix where
 
 @[default_target]
 lean_lib Ix where
-  --needs := #[(PartialBuildKey.parse "ix_c").toOption.get!, (PartialBuildKey.parse "ix_rs").toOption.get!]
 
 lean_exe ix where
   root := `Main
   supportInterpreter := true
 
 require LSpec from git
-  "https://github.com/argumentcomputer/LSpec" @ "b05e6b83798bce0887eb5001cb10fdcbe675dde3"
+  "https://github.com/argumentcomputer/LSpec" @ "fdf848d6cda9f080a09e49e760e2d6f70878800b"
 
 require Blake3 from git
-  "https://github.com/argumentcomputer/Blake3.lean" @ "nix-lake"
---require Blake3 from "/home/sam/repos/argument/Blake3.lean"
+  "https://github.com/argumentcomputer/Blake3.lean" @ "c42d5a54a142c195ea8a2643b423bcdf7d61ad9f"
 
 require Cli from git
-  "https://github.com/leanprover/lean4-cli" @ "91c18fa62838ad0ab7384c03c9684d99d306e1da"
+  "https://github.com/leanprover/lean4-cli" @ "v4.26.0"
 
 require batteries from git
-  "https://github.com/leanprover-community/batteries" @ "v4.24.0"
+  "https://github.com/leanprover-community/batteries" @ "v4.26.0"
 
 section Tests
 
diff --git a/lean-toolchain b/lean-toolchain
index c00a5350..e59446d5 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.24.0
+leanprover/lean4:v4.26.0

From b6f1f9f882e6f84530ff3397c7dff3f1d17691ee Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Thu, 15 Jan 2026 10:33:20 -0500
Subject: [PATCH 4/6] Update lean4-nix and Rust 1.92

---
 flake.lock          | 48 ++++++++++++++++++++++++---------------------
 flake.nix           | 40 ++++++++++++++++---------------------
 lake-manifest.json  |  4 ++--
 lakefile.lean       |  5 +++--
 rust-toolchain.toml |  2 +-
 5 files changed, 49 insertions(+), 50 deletions(-)

diff --git a/flake.lock b/flake.lock
index ac3d9682..1681d1ea 100644
--- a/flake.lock
+++ b/flake.lock
@@ -25,21 +25,23 @@
           "lean4-nix"
         ],
         "nixpkgs": [
+          "blake3-lean",
           "lean4-nix",
           "nixpkgs"
         ]
       },
       "locked": {
-        "lastModified": 1766006980,
-        "narHash": "sha256-6o2JzJHKA2TnkxDjRPmYSxvhAom35poLkxrvFx5X0Q0=",
+        "lastModified": 1768490836,
+        "narHash": "sha256-r98AAunFEidRoXFWTb8kJkjch9nSEcq95w1ZADJm9Dk=",
         "owner": "argumentcomputer",
         "repo": "Blake3.lean",
-        "rev": "c42d5a54a142c195ea8a2643b423bcdf7d61ad9f",
+        "rev": "40469c68dd5629cda700ff8cf00b3362dee81f1a",
         "type": "github"
       },
       "original": {
         "owner": "argumentcomputer",
         "repo": "Blake3.lean",
+        "rev": "40469c68dd5629cda700ff8cf00b3362dee81f1a",
         "type": "github"
       }
     },
@@ -85,11 +87,11 @@
         "nixpkgs-lib": "nixpkgs-lib"
       },
       "locked": {
-        "lastModified": 1765835352,
-        "narHash": "sha256-XswHlK/Qtjasvhd1nOa1e8MgZ8GS//jBoTqWtrS1Giw=",
+        "lastModified": 1768135262,
+        "narHash": "sha256-PVvu7OqHBGWN16zSi6tEmPwwHQ4rLPU9Plvs8/1TUBY=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "a34fae9c08a15ad73f295041fec82323541400a9",
+        "rev": "80daad04eddbbf5a4d883996a73f3f542fa437ac",
         "type": "github"
       },
       "original": {
@@ -121,11 +123,11 @@
         "nixpkgs-lib": "nixpkgs-lib_3"
       },
       "locked": {
-        "lastModified": 1727826117,
-        "narHash": "sha256-K5ZLCyfO/Zj9mPFldf3iwS6oZStJcU4tSpiXTMYaaL0=",
+        "lastModified": 1765835352,
+        "narHash": "sha256-XswHlK/Qtjasvhd1nOa1e8MgZ8GS//jBoTqWtrS1Giw=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "3d04084d54bedc3d6b8b736c70ef449225c361b1",
+        "rev": "a34fae9c08a15ad73f295041fec82323541400a9",
         "type": "github"
       },
       "original": {
@@ -140,27 +142,26 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1766003746,
-        "narHash": "sha256-S3e45gKBtTZ4bDqfrddB7A3dxcZb8jY0ROPu6Aw+ZEk=",
+        "lastModified": 1768025957,
+        "narHash": "sha256-o9AUUOBq1SKEPGiwjBIP628N9fPNwAjqSm9xXhVEDNY=",
         "owner": "lenianiva",
         "repo": "lean4-nix",
-        "rev": "0bca9d30803e3d65157240e67045badbc547dd45",
+        "rev": "ecaa70749083e6a0e6e0814c6a66b7561754b6db",
         "type": "github"
       },
       "original": {
         "owner": "lenianiva",
         "repo": "lean4-nix",
-        "rev": "0bca9d30803e3d65157240e67045badbc547dd45",
         "type": "github"
       }
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1743095683,
-        "narHash": "sha256-gWd4urRoLRe8GLVC/3rYRae1h+xfQzt09xOfb0PaHSk=",
+        "lastModified": 1765779637,
+        "narHash": "sha256-KJ2wa/BLSrTqDjbfyNx70ov/HdgNBCBBSQP3BIzKnv4=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "5e5402ecbcb27af32284d4a62553c019a3a49ea6",
+        "rev": "1306659b587dc277866c7b69eb97e5f07864d8c4",
         "type": "github"
       },
       "original": {
@@ -202,14 +203,17 @@
     },
     "nixpkgs-lib_3": {
       "locked": {
-        "lastModified": 1727825735,
-        "narHash": "sha256-0xHYkMkeLVQAMa7gvkddbPqpxph+hDzdu1XdGPJR+Os=",
-        "type": "tarball",
-        "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
+        "lastModified": 1765674936,
+        "narHash": "sha256-k00uTP4JNfmejrCLJOwdObYC9jHRrr/5M/a/8L2EIdo=",
+        "owner": "nix-community",
+        "repo": "nixpkgs.lib",
+        "rev": "2075416fcb47225d9b68ac469a5c4801a9c4dd85",
+        "type": "github"
       },
       "original": {
-        "type": "tarball",
-        "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
+        "owner": "nix-community",
+        "repo": "nixpkgs.lib",
+        "type": "github"
       }
     },
     "root": {
diff --git a/flake.nix b/flake.nix
index be61f13e..042b7b0e 100644
--- a/flake.nix
+++ b/flake.nix
@@ -15,7 +15,7 @@
     nixpkgs.follows = "lean4-nix/nixpkgs";
 
     # Lean 4 & Lake
-    lean4-nix.url = "github:lenianiva/lean4-nix?rev=0bca9d30803e3d65157240e67045badbc547dd45";
+    lean4-nix.url = "github:lenianiva/lean4-nix";
 
     # Helper: flake-parts for easier outputs
     flake-parts.url = "github:hercules-ci/flake-parts";
@@ -31,10 +31,9 @@
 
     # Blake3 C bindings for Lean
     blake3-lean = {
-      url = "github:argumentcomputer/Blake3.lean";
+      url = "github:argumentcomputer/Blake3.lean?rev=40469c68dd5629cda700ff8cf00b3362dee81f1a";
       # System packages, follows lean4-nix so we stay in sync
       inputs.lean4-nix.follows = "lean4-nix";
-      inputs.nixpkgs.follows = "lean4-nix/nixpkgs";
     };
   };
 
@@ -64,7 +63,7 @@
         # Pins the Rust toolchain
         rustToolchain = fenix.packages.${system}.fromToolchainFile {
           file = ./rust-toolchain.toml;
-          sha256 = "sha256-SDu4snEWjuZU475PERvu+iO50Mi39KVjqCeJeNvpguU=";
+          sha256 = "sha256-sqSWJDUxc+zaz1nBWMAJKTAGBuGWP25GCftIOlCEAtA=";
         };
 
         # Rust package
@@ -90,31 +89,26 @@
 
         # Lake package
         lake2nix = pkgs.callPackage lean4-nix.lake {};
-        lakeDepArgs = {
-          src = ./.;
-        };
         lakeDeps = lake2nix.buildDeps {
           src = ./.;
           depOverrideDeriv = {
             Blake3 = blake3-lean.packages.${system}.default;
           };
         };
-        lakeBuildArgs =
-          lakeDepArgs
-          // {
-            inherit lakeDeps;
-            # Don't build the `ix_rs` static lib with Lake, since we build it with Crane
-            postPatch = ''
-              substituteInPlace lakefile.lean --replace-fail "let args := match (ixNoPar, ixNet)" "let _args := match (ixNoPar, ixNet)"
-              substituteInPlace lakefile.lean --replace-fail 'proc { cmd := "cargo"' '--proc { cmd := "cargo"'
-              cat lakefile.lean
-            '';
-            # Copy the `ix_rs` static lib from Crane to `target/release` so Lake can use it
-            postConfigure = ''
-              mkdir -p target/release
-              ln -s ${rustPkg}/lib/libix_rs.a target/release/
-            '';
-          };
+        lakeBuildArgs = {
+          inherit lakeDeps;
+          src = ./.;
+          # Don't build the `ix_rs` static lib with Lake, since we build it with Crane
+          postPatch = ''
+            substituteInPlace lakefile.lean --replace-fail "let args := match (ixNoPar, ixNet)" "let _args := match (ixNoPar, ixNet)"
+            substituteInPlace lakefile.lean --replace-fail 'proc { cmd := "cargo"' '--proc { cmd := "cargo"'
+          '';
+          # Copy the `ix_rs` static lib from Crane to `target/release` so Lake can use it
+          postConfigure = ''
+            mkdir -p target/release
+            ln -s ${rustPkg}/lib/libix_rs.a target/release/
+          '';
+        };
         ixLib = lake2nix.mkPackage (lakeBuildArgs
           // {
             name = "Ix";
diff --git a/lake-manifest.json b/lake-manifest.json
index a75b32c1..298d8e29 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -25,10 +25,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c42d5a54a142c195ea8a2643b423bcdf7d61ad9f",
+   "rev": "4a3528f2b905854b554b1ae107f543c50611563d",
    "name": "Blake3",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "c42d5a54a142c195ea8a2643b423bcdf7d61ad9f",
+   "inputRev": "4a3528f2b905854b554b1ae107f543c50611563d",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/argumentcomputer/LSpec",
diff --git a/lakefile.lean b/lakefile.lean
index a19ccbd7..92a1be55 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -5,7 +5,7 @@ package ix where
   version := v!"0.1.0"
 
 @[default_target]
-lean_lib Ix where
+lean_lib Ix
 
 lean_exe ix where
   root := `Main
@@ -14,8 +14,9 @@ lean_exe ix where
 require LSpec from git
   "https://github.com/argumentcomputer/LSpec" @ "fdf848d6cda9f080a09e49e760e2d6f70878800b"
 
+-- TODO: Update to latest Blake3 main here and in flake.nix
 require Blake3 from git
-  "https://github.com/argumentcomputer/Blake3.lean" @ "c42d5a54a142c195ea8a2643b423bcdf7d61ad9f"
+  "https://github.com/argumentcomputer/Blake3.lean" @ "4a3528f2b905854b554b1ae107f543c50611563d"
 
 require Cli from git
   "https://github.com/leanprover/lean4-cli" @ "v4.26.0"
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index dccca02c..a5b578d8 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -1,4 +1,4 @@
 [toolchain]
 # The default profile includes rustc, rust-std, cargo, rust-docs, rustfmt and clippy.
 profile = "default"
-channel = "1.91"
+channel = "1.92"

From 663d7a6bbd5002b6d32918a44bd4c408eed5efee Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Thu, 15 Jan 2026 11:01:48 -0500
Subject: [PATCH 5/6] Fix lints

---
 .github/workflows/nix.yml |  2 +-
 deny.toml                 | 67 ++++-----------------------------------
 lakefile.lean             |  4 ++-
 3 files changed, 10 insertions(+), 63 deletions(-)

diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml
index f8f0c867..b7767b65 100644
--- a/.github/workflows/nix.yml
+++ b/.github/workflows/nix.yml
@@ -26,7 +26,7 @@ jobs:
           github_access_token: ${{ secrets.GITHUB_TOKEN }}
       # Ix CLI
       - run: nix build --print-build-logs --accept-flake-config
-      - run: nix run .#default -- --help
+      - run: nix run .#ix -- --help
       # Ix benches
       - run: nix build .#bench-aiur --print-build-logs --accept-flake-config
       - run: nix build .#bench-blake3 --print-build-logs --accept-flake-config
diff --git a/deny.toml b/deny.toml
index 6519dae3..11d7152e 100644
--- a/deny.toml
+++ b/deny.toml
@@ -75,7 +75,6 @@ ignore = [
     "RUSTSEC-2024-0370", # `proc-macro-error` crate is unmaintained
     "RUSTSEC-2023-0089", # `atomic-polyfill` crate is unmaintained
     "RUSTSEC-2025-0141", # `bincode` crate is unmaintained
-
     #{ id = "RUSTSEC-0000-0000", reason = "you can specify a reason the advisory is ignored" },
     #"a-crate-that-is-yanked@0.1.1", # you can also ignore yanked crate versions if you wish
     #{ crate = "a-crate-that-is-yanked@0.1.1", reason = "you can specify why you are ignoring the yanked crate" },
@@ -122,66 +121,12 @@ exceptions = [
 # Some crates don't have (easily) machine readable licensing information,
 # adding a clarification entry for it allows you to manually specify the
 # licensing information
-[[licenses.clarify]]
-crate = "binius_circuits"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_core"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_field"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_hal"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_hash"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_macros"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_math"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_maybe_rayon"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_ntt"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_utils"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
+# [[licenses.clarify]]
+# crate = "binius_circuits"
+# expression = "Apache-2.0"
+# license-files = [
+#   { path = "../../LICENSE.txt", hash = 0 }
+# ]
 # The package spec the clarification applies to
 #crate = "ring"
 # The SPDX expression for the license requirements of the crate
diff --git a/lakefile.lean b/lakefile.lean
index 92a1be55..0185a689 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -144,7 +144,7 @@ script install := do
   return 0
 
 script "check-lean-h-hash" := do
-  let cachedLeanHHash := 1323938820889983873
+  let cachedLeanHHash := 11261383907494897568
 
   let leanIncludeDir ← getLeanIncludeDir
   let includedLeanHPath := leanIncludeDir / "lean" / "lean.h"
@@ -156,6 +156,8 @@ script "check-lean-h-hash" := do
     IO.eprintln   "  1. Double-check changes made to lean/lean.h"
     IO.eprintln s!"  2. Cache {includedLeanHHash} instead"
     return 1
+  else
+    IO.println "lean/lean.h hash matches ✓"
   return 0
 
 script "get-exe-targets" := do

From ad97ce0e621285fe254f685288807027b23ce787 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Mon, 19 Jan 2026 17:17:19 -0500
Subject: [PATCH 6/6] Update Blake3.lean

---
 flake.lock         | 5 ++---
 flake.nix          | 2 +-
 lake-manifest.json | 4 ++--
 lakefile.lean      | 3 +--
 4 files changed, 6 insertions(+), 8 deletions(-)

diff --git a/flake.lock b/flake.lock
index 1681d1ea..b0c5033f 100644
--- a/flake.lock
+++ b/flake.lock
@@ -31,17 +31,16 @@
         ]
       },
       "locked": {
-        "lastModified": 1768490836,
+        "lastModified": 1768515341,
         "narHash": "sha256-r98AAunFEidRoXFWTb8kJkjch9nSEcq95w1ZADJm9Dk=",
         "owner": "argumentcomputer",
         "repo": "Blake3.lean",
-        "rev": "40469c68dd5629cda700ff8cf00b3362dee81f1a",
+        "rev": "f66794edb4612106cd7b04a7fbd04917fb1abb7d",
         "type": "github"
       },
       "original": {
         "owner": "argumentcomputer",
         "repo": "Blake3.lean",
-        "rev": "40469c68dd5629cda700ff8cf00b3362dee81f1a",
         "type": "github"
       }
     },
diff --git a/flake.nix b/flake.nix
index 042b7b0e..f5cb3364 100644
--- a/flake.nix
+++ b/flake.nix
@@ -31,7 +31,7 @@
 
     # Blake3 C bindings for Lean
     blake3-lean = {
-      url = "github:argumentcomputer/Blake3.lean?rev=40469c68dd5629cda700ff8cf00b3362dee81f1a";
+      url = "github:argumentcomputer/Blake3.lean";
       # System packages, follows lean4-nix so we stay in sync
       inputs.lean4-nix.follows = "lean4-nix";
     };
diff --git a/lake-manifest.json b/lake-manifest.json
index 298d8e29..74b38ab6 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -25,10 +25,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "4a3528f2b905854b554b1ae107f543c50611563d",
+   "rev": "f66794edb4612106cd7b04a7fbd04917fb1abb7d",
    "name": "Blake3",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "4a3528f2b905854b554b1ae107f543c50611563d",
+   "inputRev": "f66794edb4612106cd7b04a7fbd04917fb1abb7d",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/argumentcomputer/LSpec",
diff --git a/lakefile.lean b/lakefile.lean
index 0185a689..567d85f3 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -14,9 +14,8 @@ lean_exe ix where
 require LSpec from git
   "https://github.com/argumentcomputer/LSpec" @ "fdf848d6cda9f080a09e49e760e2d6f70878800b"
 
--- TODO: Update to latest Blake3 main here and in flake.nix
 require Blake3 from git
-  "https://github.com/argumentcomputer/Blake3.lean" @ "4a3528f2b905854b554b1ae107f543c50611563d"
+  "https://github.com/argumentcomputer/Blake3.lean" @ "f66794edb4612106cd7b04a7fbd04917fb1abb7d"
 
 require Cli from git
   "https://github.com/leanprover/lean4-cli" @ "v4.26.0"