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

[bibajz]

Proposal

Callers of System.FilePath.walkDir should have the ability to not follow symbolic links, which are now followed unconditionally. This may prevent infinite recursion on a directory structure with a cycle.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[Kha]

Is that not covered by enter?

[bibajz]

Hello, sorry for the late response, I missed the notification...

---

Yes, it can be covered by the enter - having it that way would also cover the case when the initial argument of walkDir is symlink itself, which is not covered by #10973 - if we consider the following directory structure:

$ tree /tmp
/tmp/
├── a
│   └── file.txt
└── s -> /tmp/a

and program:

$ cat t.lean
#eval System.FilePath.walkDir (followLinks := true) "/tmp/s"
#eval System.FilePath.walkDir (followLinks := false) "/tmp/s"

on #10973 , I get:

$ ./build/release/stage0/bin/lean t.lean
#[FilePath.mk "/tmp/s/file.txt"]
#[FilePath.mk "/tmp/s/file.txt"]

^ I would expect an empty array on the second line...

---

My initial reasons for going with followLinks argument were:

1. ease of understanding - it's a boolean flag, similar to other programming languages (Rust, Python,...)
2. limiting the number of IO actions - you still need to invoke FilePath.symlinkMetadata in the for d in (← p.readDir) do, having it in enter would mean that symlinkMetadata would be called twice on directories. But maybe I have not looked at the problem hard enough (as evidenced by the bug with initial directory being a symlink above), so there may be a way.

Does it make sense?

---

Thank you for your response,
Libor