From 2776e43ef9ce43b5d83b024d7d5bef3db6cfe12f Mon Sep 17 00:00:00 2001
From: munenick <mune0127@munenick.me>
Date: Wed, 5 Aug 2026 14:07:49 +0900
Subject: [PATCH 1/2] fix: avoid case-insensitive source directory collision

---
 lakefile.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lakefile.lean b/lakefile.lean
index e8900fc..001c61a 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -15,7 +15,7 @@ abbrev blake3RepoURL := "https://github.com/BLAKE3-team/BLAKE3"
 abbrev blake3RepoTag := "1.8.7"
 
 target cloneBlake3 pkg : GitRepo := do
-  let repoDir : GitRepo := pkg.dir / "blake3"
+  let repoDir : GitRepo := pkg.dir / "blake3-source"
 
   -- Clone if it hasn't already been cloned
   let alreadyCloned ← repoDir.dir.pathExists

From a749c4c78900ea55a22f1eb4b94ddee61d09b540 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Sat, 22 Aug 2026 12:54:44 -0400
Subject: [PATCH 2/2] fix: clone BLAKE3 into `.lake` and update the remaining
 paths
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The rename to `blake3-source` only covered `lakefile.lean`, leaving
`.gitignore` and `flake.nix` pointing at the old `blake3` path. The Nix
build relies on that path entirely: `disableGitClone` comments out the
git calls and `linkBlake3Src` symlinks the pinned source in its place,
so a stale path breaks `nix build`.

Move the clone under `.lake` instead of the package root. It is already
untracked there, so the `.gitignore` entry can go away — which also
fixes a latent trap, since git enables `core.ignoreCase` on
case-insensitive filesystems and a root-level `/blake3` pattern then
also matches the `Blake3` source directory, silently ignoring new files
added under it. `lake clean` only clears `.lake/build`, so the clone
survives a clean.

Since lean4-nix installs `.lake` wholesale, `blake3C` no longer needs to
copy the source to `$out` by hand; that copy only existed because the
install rsync filters the package root through `.gitignore`.
`linkBlake3Src` gains `-fn` so it replaces, rather than dereferences,
the symlink that `blake3Test` rsyncs in from the `blake3C` artifacts.
---
 .gitignore    | 2 --
 flake.nix     | 7 +++----
 lakefile.lean | 6 +++++-
 3 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/.gitignore b/.gitignore
index c908d25..2e36d3e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,7 +1,5 @@
 # Lean
 /.lake
-# Local clone for Lake build
-/blake3
 
 # Rust
 **/target
diff --git a/flake.nix b/flake.nix
index b8b4178..67f3a2c 100644
--- a/flake.nix
+++ b/flake.nix
@@ -76,8 +76,10 @@
           disableCargoBuild = ''
             substituteInPlace lakefile.lean --replace-fail 'proc { cmd := "cargo"' '--proc { cmd := "cargo"'
           '';
+          # `-fn` so it overwrites the symlink rsynced in from a prior stage's `.lake`
           linkBlake3Src = ''
-            ln -s ${blake3.outPath} ./blake3
+            mkdir -p .lake
+            ln -sfn ${blake3.outPath} .lake/blake3-source
           '';
           # Copy the `blake3_rs` static lib from Crane to `target/release` so Lake can use it
           linkRustLib = ''
@@ -128,9 +130,6 @@
             buildLibrary = true;
             postPatch = disableGitClone;
             preConfigure = linkBlake3Src;
-            postInstall = ''
-              cp -rP ./blake3 $out
-            '';
           };
 
           blake3Rust = lake2nix.mkPackage {
diff --git a/lakefile.lean b/lakefile.lean
index 001c61a..c8a5fe4 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -15,7 +15,11 @@ abbrev blake3RepoURL := "https://github.com/BLAKE3-team/BLAKE3"
 abbrev blake3RepoTag := "1.8.7"
 
 target cloneBlake3 pkg : GitRepo := do
-  let repoDir : GitRepo := pkg.dir / "blake3-source"
+  -- Under `.lake` rather than the package root: it is already untracked, and a
+  -- sibling `blake3` directory would collide with `Blake3` on case-insensitive
+  -- filesystems (macOS, Windows). `lake clean` only clears `.lake/build`, so the
+  -- clone survives.
+  let repoDir : GitRepo := pkg.lakeDir / "blake3-source"
 
   -- Clone if it hasn't already been cloned
   let alreadyCloned ← repoDir.dir.pathExists