From efbbb0b230ce95653d25b59c83fd24a51a8bf363 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Tue, 21 Oct 2025 00:19:10 -0400
Subject: [PATCH] fix: lake: recurse directories in `input_dir` (#10861)

This PR fixes `input_dir` tracking to also recurse through
subdirectories. The `filter` of an `input_dir` will be applied to each
file in the directory tree (the path names of directories will not be
checked).

Closes #10827.
---
 src/lake/Lake/Build/Common.lean      | 6 +++---
 tests/lake/tests/inputFile/setup.sh  | 3 ++-
 tests/lake/tests/inputFile/test.lean | 3 +++
 tests/lake/tests/inputFile/test.sh   | 5 +++++
 4 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean
index 6b52575924..daf256e810 100644
--- a/src/lake/Lake/Build/Common.lean
+++ b/src/lake/Lake/Build/Common.lean
@@ -688,9 +688,9 @@ public def inputDir
   (path : FilePath) (text : Bool) (filter : FilePath → Bool)
 : SpawnM (Job (Array FilePath)) := do
   let job ← Job.async do
-    let fs ← path.readDir
-    let ps := fs.filterMap fun f =>
-      if filter f.path then some f.path else none
+    let ps ← (← path.walkDir).filterM fun p =>
+      -- Always filter out directories as they cannot be hashed anyway
+      return !(← p.isDir) && filter p
     -- Makes the order of files consistent across platforms
     let ps := ps.qsort (toString · < toString ·)
     return ps
diff --git a/tests/lake/tests/inputFile/setup.sh b/tests/lake/tests/inputFile/setup.sh
index 3cd26d2156..49b31c459b 100755
--- a/tests/lake/tests/inputFile/setup.sh
+++ b/tests/lake/tests/inputFile/setup.sh
@@ -4,9 +4,10 @@ set -euxo pipefail
 ./clean.sh
 
 # Setup directory
-mkdir -p inputs/barz
+mkdir -p inputs/barz/bam
 echo foo > inputs/foo.txt
 echo bar > inputs/barz/bar.txt
 echo baz > inputs/barz/baz.txt
+echo boo > inputs/barz/bam/boo.txt
 echo untraced > inputs/untraced.txt
 echo untraced > inputs/barz/untraced.txt
diff --git a/tests/lake/tests/inputFile/test.lean b/tests/lake/tests/inputFile/test.lean
index e4c75fc49c..dc067700b0 100644
--- a/tests/lake/tests/inputFile/test.lean
+++ b/tests/lake/tests/inputFile/test.lean
@@ -3,6 +3,7 @@ import Std.Data.HashMap
 def foo := include_str "inputs" / "foo.txt"
 def bar := include_str "inputs" / "barz" / "bar.txt"
 def baz := include_str "inputs" / "barz" / "baz.txt"
+def boo := include_str "inputs" / "barz" / "bam" / "boo.txt"
 def untraced := include_str "inputs" / "untraced.txt"
 def untracedBarz := include_str "inputs" / "barz" / "untraced.txt"
 
@@ -11,6 +12,7 @@ def inputs : Std.HashMap String String :=
   |>.insert "foo" foo
   |>.insert "bar" bar
   |>.insert "baz" baz
+  |>.insert "boo" boo
   |>.insert "untraced" untraced
   |>.insert "untracedBarz" untracedBarz
 
@@ -19,6 +21,7 @@ def main (args : List String) : IO Unit := do
     IO.print foo
     IO.print bar
     IO.print baz
+    IO.print boo
     IO.print untraced
     IO.print untracedBarz
   else
diff --git a/tests/lake/tests/inputFile/test.sh b/tests/lake/tests/inputFile/test.sh
index 42bd75d665..445e900b5a 100755
--- a/tests/lake/tests/inputFile/test.sh
+++ b/tests/lake/tests/inputFile/test.sh
@@ -15,6 +15,7 @@ test_out_diff <(cat << 'EOF'
 foo
 bar
 baz
+boo
 untraced
 untraced
 EOF
@@ -37,6 +38,7 @@ test_cmd diff -u --strip-trailing-cr <(echo foo) "`$LAKE query foo`"
 echo "# TEST: input_dir target"
 test_run query barz
 cat `$LAKE query barz` | diff -u --strip-trailing-cr <(cat << 'EOF'
+boo
 bar
 baz
 EOF
@@ -51,6 +53,8 @@ echo traced > inputs/barz/bar.txt
 test_eq "traced" exe test bar
 echo traced > inputs/barz/baz.txt
 test_eq "traced" exe test baz
+echo traced > inputs/barz/bam/boo.txt
+test_eq "traced" exe test boo
 
 # Test untraced dependencies
 echo "# TEST: Untraced dependencies"
@@ -60,6 +64,7 @@ test_out_diff <(cat << 'EOF'
 traced
 traced
 traced
+traced
 untraced
 untraced
 EOF