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

@@ -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

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

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

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