Skip to content

Conversation

@bibajz
Copy link

@bibajz bibajz commented Oct 26, 2025

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


Closes #10972


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

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.
for d in (← p.readDir) do
modify (·.push d.path)
match (← d.path.metadata.toBaseIO) with
match (← d.path.symlinkMetadata.toBaseIO) with
Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Introduced in add3e1a - as per the docstring of IO.FS.FileType :

  /--
  Symbolic links that are pointers to other named files. Note that `System.FilePath.metadata` never
  indicates this type as it follows symlinks; use `System.FilePath.symlinkMetadata` instead.
  -/

it means the symlink branch could never be hit!

Comment on lines +1167 to +1168
let p' ← FS.realPath d.path
if (← p'.isDir) then
Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I do not know if it's a real issue, but these lines suffer from TOC/TOU, the first one is:

  1. realPath after symlinkMetada may fail if the symlink vanished
  2. isDir after realPath may fail if the resolved file vanished

to handle them both, it means we need to cast it to toBaseIO and catch the exceptions individually.

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Oct 26, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 77ddfd49e676cf723912e70f1e97aa860aa095ab --onto 97d63db52cd2fc3353f8a75f48209de0011f1bd3. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-26 18:10:07)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 77ddfd49e676cf723912e70f1e97aa860aa095ab --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-26 18:10:08)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

RFC: Allow System.FilePath.walkDir to not follow symbolic link

3 participants