列出目录🔗

列出目录的内容🔗

要列出一个目录的内容，我们对一个 System.FilePath 使用 System.FilePath.readDir 方法。它返回一个 Array IO.FS.DirEntry，其中包含关于每个文件和子目录的信息。

def listDirectory (path : System.FilePath) : IO Unit := do
  let entries ← path.readDir
  for entry in entries do
    IO.println entry.fileName

每个 IO.FS.DirEntry 都包含 fileName（文件或目录本身的名称）及其完整的 path。

递归遍历目录🔗

如果你想递归地列出一个目录树中的所有文件，可以使用 System.FilePath.walkDir 方法。

注：你可以用 System.FilePath.isDir 方法检查一个条目是否是目录。

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

遍历时进行过滤🔗

System.FilePath.walkDir 接受一个可选的 enter 参数——一个函数，用来决定是否递归进入某个给定的子目录。这对于跳过像 .git 或 .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