Recursive directory traversal🔗

If you want to list all files in a directory tree recursively, you can use the System.FilePath.walkDir method.

Note: You can use System.FilePath.isDir method to check if an entry is a directory.

def listAllFiles (path : System.FilePath) : IO Unit := do
  let allFiles ← path.walkDir
  for file in allFiles do
    IO.println file

Filtering during traversal🔗

System.FilePath.walkDir takes an optional enter parameter—a function that decides whether to recurse into a given subdirectory. This is useful for skipping large or irrelevant folders like .git or .lake.

def listSourceFiles (path : System.FilePath) : IO Unit := do
  /- Only enter directories that aren't
    hidden or build artifacts -/
  let filter (p : System.FilePath) : IO Bool := do
    let name := p.fileName.getD ""
    return name != ".git" && name != ".lake"

  let files ← path.walkDir (enter := filter)
  for f in files do
    -- Only print files with the .lean extension
    if f.extension == some "lean" then
      IO.println f