From 62ec6c8cea811907433a401136fe822ae6516292 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Tue, 17 Feb 2026 14:51:17 -0500
Subject: [PATCH 1/2] chore: Update Lean to v4.27.0

---
 flake.lock     | 26 +++++++++++++-------------
 flake.nix      |  2 +-
 lakefile.lean  |  2 +-
 lean-toolchain |  2 +-
 4 files changed, 16 insertions(+), 16 deletions(-)

diff --git a/flake.lock b/flake.lock
index bad7814..ed502c7 100644
--- a/flake.lock
+++ b/flake.lock
@@ -3,16 +3,16 @@
     "blake3": {
       "flake": false,
       "locked": {
-        "lastModified": 1745192552,
-        "narHash": "sha256-IABVErXWYQFXZcwsFKfQhm3ox7UZUcW5uzVrGwsSp94=",
+        "lastModified": 1767892649,
+        "narHash": "sha256-aj+fru2saqWxDDiV3mNCZZeZIGTxSgta/X50R87hoko=",
         "owner": "BLAKE3-team",
         "repo": "BLAKE3",
-        "rev": "df610ddc3b93841ffc59a87e3da659a15910eb46",
+        "rev": "8b829b697fa4cfe35de35e9aa8c20b56266cb091",
         "type": "github"
       },
       "original": {
         "owner": "BLAKE3-team",
-        "ref": "refs/tags/1.8.2",
+        "ref": "refs/tags/1.8.3",
         "repo": "BLAKE3",
         "type": "github"
       }
@@ -22,11 +22,11 @@
         "nixpkgs-lib": "nixpkgs-lib"
       },
       "locked": {
-        "lastModified": 1768135262,
-        "narHash": "sha256-PVvu7OqHBGWN16zSi6tEmPwwHQ4rLPU9Plvs8/1TUBY=",
+        "lastModified": 1769996383,
+        "narHash": "sha256-AnYjnFWgS49RlqX7LrC4uA+sCCDBj0Ry/WOJ5XWAsa0=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "80daad04eddbbf5a4d883996a73f3f542fa437ac",
+        "rev": "57928607ea566b5db3ad13af0e57e921e6b12381",
         "type": "github"
       },
       "original": {
@@ -59,11 +59,11 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1768025957,
-        "narHash": "sha256-o9AUUOBq1SKEPGiwjBIP628N9fPNwAjqSm9xXhVEDNY=",
+        "lastModified": 1771204072,
+        "narHash": "sha256-s27Es43FfrMfRXXSll0PM9zRvSer6dDtNZ5WpsIlcyY=",
         "owner": "lenianiva",
         "repo": "lean4-nix",
-        "rev": "ecaa70749083e6a0e6e0814c6a66b7561754b6db",
+        "rev": "de6f06ae44260581d953d485219dcd2bf86aa685",
         "type": "github"
       },
       "original": {
@@ -90,11 +90,11 @@
     },
     "nixpkgs-lib": {
       "locked": {
-        "lastModified": 1765674936,
-        "narHash": "sha256-k00uTP4JNfmejrCLJOwdObYC9jHRrr/5M/a/8L2EIdo=",
+        "lastModified": 1769909678,
+        "narHash": "sha256-cBEymOf4/o3FD5AZnzC3J9hLbiZ+QDT/KDuyHXVJOpM=",
         "owner": "nix-community",
         "repo": "nixpkgs.lib",
-        "rev": "2075416fcb47225d9b68ac469a5c4801a9c4dd85",
+        "rev": "72716169fe93074c333e8d0173151350670b824c",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index 3c0ace3..68e79e4 100644
--- a/flake.nix
+++ b/flake.nix
@@ -6,7 +6,7 @@
     flake-parts.url = "github:hercules-ci/flake-parts";
     lean4-nix.url = "github:lenianiva/lean4-nix";
     blake3 = {
-      url = "github:BLAKE3-team/BLAKE3?ref=refs/tags/1.8.2";
+      url = "github:BLAKE3-team/BLAKE3?ref=refs/tags/1.8.3";
       flake = false;
     };
   };
diff --git a/lakefile.lean b/lakefile.lean
index 0e529fa..cfe0b95 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -12,7 +12,7 @@ lean_lib Blake3 where
 lean_exe Blake3Test
 
 abbrev blake3RepoURL := "https://github.com/BLAKE3-team/BLAKE3"
-abbrev blake3RepoTag := "1.8.2"
+abbrev blake3RepoTag := "1.8.3"
 
 target cloneBlake3 pkg : GitRepo := do
   let repoDir : GitRepo := pkg.dir / "blake3"
diff --git a/lean-toolchain b/lean-toolchain
index e59446d..5249182 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.26.0
+leanprover/lean4:v4.27.0

From d886ce88c55eb210ff664c38f8c8782f1156b0b2 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Fri, 20 Feb 2026 11:50:07 -0500
Subject: [PATCH 2/2] Use temporary fork

---
 flake.lock | 11 ++++++-----
 flake.nix  |  4 ++--
 2 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/flake.lock b/flake.lock
index ed502c7..28baf16 100644
--- a/flake.lock
+++ b/flake.lock
@@ -59,15 +59,16 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1771204072,
-        "narHash": "sha256-s27Es43FfrMfRXXSll0PM9zRvSer6dDtNZ5WpsIlcyY=",
-        "owner": "lenianiva",
+        "lastModified": 1771604035,
+        "narHash": "sha256-35kZxaGTpP0mGHaxKzb7WXQD2hkw5z/kGxIJ/bE+7cA=",
+        "owner": "argumentcomputer",
         "repo": "lean4-nix",
-        "rev": "de6f06ae44260581d953d485219dcd2bf86aa685",
+        "rev": "6ba23dd08cfcdf92c4e2aaae7952088a739d3bca",
         "type": "github"
       },
       "original": {
-        "owner": "lenianiva",
+        "owner": "argumentcomputer",
+        "ref": "lake-config",
         "repo": "lean4-nix",
         "type": "github"
       }
diff --git a/flake.nix b/flake.nix
index 68e79e4..6ccf66f 100644
--- a/flake.nix
+++ b/flake.nix
@@ -4,7 +4,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?ref=lake-config";
     blake3 = {
       url = "github:BLAKE3-team/BLAKE3?ref=refs/tags/1.8.3";
       flake = false;
@@ -46,7 +46,7 @@
             name = "Blake3";
             buildLibrary = true;
             postInstall = ''
-              cp -P ./blake3 $out
+              cp -rP ./blake3 $out
             '';
           });
         blake3Test = lake2nix.mkPackage (commonArgs