feat: allow System.FilePath.walkDir to not follow symlinks

This PR introduces a new argument to `System.FilePath.walkDir` - `followLinks` - which allows
the callee to not follow symbolic links and is set to `false` as default.

Rationale:

`System.FilePath.metadata` action follows symlinks, therefore
the branch `| ok { type := .symlink, .. }` was in fact unreachable. We
can leverage the `symlinkMetadata` action introduced in add3e1a
which uses the `lstat(2)` system call and does not follow symlinks.

This gives us the option to not follow symlinks and expose ourselves to
an infinite recursion when traversing a directory structure containing a
cycle - a situation that is currently unavoidable.

---

Rationale for setting the `followLinks := false` default:

I realize that setting the default as `false` is a breaking change, and
I don't know the internal usage of `walkDir` well enough to see if it
breaks anything - from grepping and glancing at the code, not following
symlinks seems OK.

I consulted implementations of `walkDir` in other languages and

* Python stdlib `os.walk` - https://docs.python.org/3/library/os.html#os.walk
    does not follow links by default
* Rust crate `walkdir` - https://docs.rs/walkdir/latest/walkdir/struct.WalkDir.html#method.follow_links
    does not follow links by default
* Go stdlib `filepath/WalkDir` - https://pkg.go.dev/path/filepath#WalkDir
    does not follow links at all.

Author: Libor

src/Init/System/IO.lean

@@ -1143,25 +1143,29 @@ def pathExists (p : FilePath) : BaseIO Bool :=
 
 /--
 Traverses a filesystem starting at the path `p` and exploring directories that satisfy `enter`,
-returning the paths visited.
+returning the paths visited. Symbolic links are not followed by default. This behaviour can be
+changed by setting `followLinks` to `true`.
 
 The traversal is a preorder traversal, in which parent directories occur prior to any of their
-children. Symbolic links are followed.
+children.
+
+Note: `walkDir` does not keep track of already visited directories. It is therefore possible to
+get stuck in an infinite recursion when `followLinks` is set to `true` on a directory structure
+that contains a cycle, for example by containing a symbolic link pointing to its parent directory.
 -/
-partial def walkDir (p : FilePath) (enter : FilePath → IO Bool := fun _ => pure true) : IO (Array FilePath) :=
+partial def walkDir (p : FilePath) (enter : FilePath → IO Bool := fun _ => pure true) (followLinks : Bool := false) : IO (Array FilePath) :=
   Prod.snd <$> StateT.run (go p) #[]
 where
   go p := do
     if !(← enter p) then
       return ()
     for d in (← p.readDir) do
       modify (·.push d.path)
-      match (← d.path.metadata.toBaseIO) with
+      match (← d.path.symlinkMetadata.toBaseIO) with
       | .ok { type := .symlink, .. } =>
-        let p' ← FS.realPath d.path
-        if (← p'.isDir) then
-          -- do not call `enter` on a non-directory symlink
-          if (← enter p) then
+        if followLinks then
+          let p' ← FS.realPath d.path
+          if (← p'.isDir) then
             go p'
       | .ok { type := .dir, .. } => go d.path
       | .ok _ => pure ()

src/runtime/io.cpp

@@ -1130,7 +1130,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_symlink_metadata(b_obj_arg filename) {
         return mk_embedded_nul_error(filename);
     }
     struct stat st;
-    if (lstat(string_cstr(filename), &st) != 0) {
+    if (lstat(fname, &st) != 0) {
         return io_result_mk_error(decode_io_error(errno, filename));
     }
     return metadata_core(st);

tests/lean/run/IO_test.lean

@@ -13,6 +13,14 @@ unless (expected == actual) do
   throw $ IO.userError $
     s!"assertion failure \"{tag}\":\n  expected: {repr expected}\n  actual:   {repr actual}"
 
+def mkEmptyFile (file : System.FilePath) : IO Unit :=
+  writeFile file ""
+
+def removeFileIfExists (file : System.FilePath) : IO Unit :=
+  try removeFile file catch
+    | .noFileOrDirectory .. => pure ()
+    | e => throw e
+
 def test : IO Unit := do
 let xs : ByteArray := ⟨#[1,2,3,4]⟩;
 let fn := "io_test/foo.txt";
@@ -171,3 +179,51 @@ def testHardLink : IO Unit := do
 
 #guard_msgs in
 #eval testHardLink
+
+/-
+`walkDir` with `followLinks := false` yields a subset of entries obtained by `walkDir` which
+follows symlinks.
+-/
+
+def testWalkDir : IO Unit := do
+  let fn := "g.txt"
+  let symlink := "io_test/walkdir/dir/symlink"
+  createDirAll "io_test/walkdir/dir"
+  createDirAll "io_test/walkdir/symlink_target"
+  mkEmptyFile "io_test/walkdir/dir/f.txt"
+  mkEmptyFile s!"io_test/walkdir/symlink_target/{fn}"
+  removeFileIfExists symlink
+
+  unless System.Platform.isWindows do
+    let _ ← IO.Process.run { cmd := "ln", args := #["-s", "../../symlink_target", symlink] }
+    let noSymlinks <- System.FilePath.walkDir "io_test/walkdir/dir" (followLinks := false)
+    let withSymlinks <- System.FilePath.walkDir "io_test/walkdir/dir" (followLinks := true)
+    check_eq "1" (withSymlinks.filter (fun s => !(s.toString.endsWith fn))) noSymlinks
+
+#guard_msgs in
+#eval testWalkDir
+
+/-
+`walkDir` with `followLinks := false` does not throw an exception when encountering a dangling
+symlink. When the dangling symlink is followed, `IO.Error.noFileOrDirectory` exception is thrown.
+-/
+
+def testWalkDirDanglingSymlink : IO Unit := do
+  let symlink := "io_test/walkdir_dangling_symlink/symlink"
+  let nonexistentTarget := "nonexistent-target"
+  createDirAll "io_test/walkdir_dangling_symlink"
+  removeFileIfExists symlink
+
+  unless System.Platform.isWindows do
+    assert! !(← System.FilePath.pathExists nonexistentTarget)
+    let _ ← IO.Process.run { cmd := "ln", args := #["-s", nonexistentTarget, symlink] }
+    let noSymlinks <- System.FilePath.walkDir  "io_test/walkdir_dangling_symlink" (followLinks := false)
+    /- symbolic link was recorded in the array, but not followed -/
+    check_eq "1" noSymlinks.size 1
+
+    match <- (System.FilePath.walkDir  "io_test/walkdir_dangling_symlink" (followLinks := true)).toBaseIO with
+    | .error (.noFileOrDirectory ..) => pure ()
+    | _ => assert! false
+
+#guard_msgs in
+#eval testWalkDirDanglingSymlink