IO.FS.removeDirAll deletes a symlinked directory's target contents (data loss via dependency update)

Summary

IO.FS.removeDirAll p, when p is itself a symlink to a directory, follows the
symlink and deletes the target's contents, then fails with ENOTDIR on the final
removeDir. The function's internal "Do not follow symlinks" guard protects
symlinked children but not a symlinked root, so calling it on a symlink is
more destructive than rm -rf <symlink> (which removes only the link).

Lake triggers this in its dependency-update path: when a package's on-disk directory
is a symlink (a common shared-build-cache setup), lake update deletes the symlink's
target — which can be a real, live source repository including its .git.

Environment

• Lean / Lake v4.30.0 (the same code shape is present on master:
  Init/System/IO.lean, Lake/Util/IO.lean, Lake/Load/Materialize.lean).
• Linux (POSIX symlinks).

Minimal repro (no Lake needed)

mkdir -p /tmp/repro/precious_repo/src
echo 'do not delete me' > /tmp/repro/precious_repo/src/main.lean
ln -s /tmp/repro/precious_repo /tmp/repro/link_to_repo   # symlink to the dir

cat > /tmp/repro/test.lean <<'EOF'
#eval show IO Unit from do
  try IO.FS.removeDirAll "/tmp/repro/link_to_repo"
  catch e => IO.println s!"threw {e}"
EOF
lean /tmp/repro/test.lean

find /tmp/repro/precious_repo -type f     # EMPTY — main.lean is gone
ls -l /tmp/repro/link_to_repo             # the symlink itself still exists

Output:

threw inappropriate type (error code: 20, not a directory)
  file: /tmp/repro/link_to_repo

and precious_repo/src/main.lean has been deleted.

Expected vs actual

• Expected: removeDirAll <symlink> either removes only the link (like
  rm -rf <symlink>) or refuses — it should not traverse into and empty the
  symlink's target.
• Actual: the target directory's contents are recursively deleted; only the final
  removeDir on the link fails (ENOTDIR).

Root cause

Init/System/IO.lean:

partial def removeDirAll (p : FilePath) : IO Unit := do
  for ent in (← p.readDir) do          -- readDir FOLLOWS p when p is a symlink-to-dir
    -- Do not follow symlinks
    if (← ent.path.symlinkMetadata).type == .dir then   -- guard: children only
      removeDirAll ent.path
    else
      removeFile ent.path
  removeDir p                          -- rmdir on the symlink → ENOTDIR

The symlinkMetadata (lstat) check correctly avoids following symlinks among the
children, but there is no such check on p itself. p.readDir opens the
path, which resolves a symlink root and enumerates the target's entries; those real
entries are then deleted. Lake/Util/IO.lean's removeDirAllIfExists has the
identical structure and the identical flaw.

Lake's update path calls it directly on the package directory, with no symlink check:

-- Lake/Load/Materialize.lean
logInfo s!"{name}: URL has changed; deleting '{repo.dir}' and cloning again"
IO.FS.removeDirAll repo.dir
cloneGitPkg name repo url rev?

If repo.dir is a symlink to a real repo (e.g. .lake/packages/foo -> ../foo for a
shared build cache, with the lakefile now declaring foo as a git dep so the URL
"changed"), this empties ../foo — source and .git.

Impact

Real-world data loss: a sibling repository, symlinked into .lake/packages/ as a
shared build cache, had its entire working tree and .git deleted by a single
lake update, producing exactly the not a directory error above. Because .git
went with it, git could recover nothing.

Suggested fixes (either or both)

1. removeDirAll / removeDirAllIfExists: check the root first —
   if (← p.symlinkMetadata).type == .symlink then removeFile p; return (or throw a
   clear "refusing to recurse into a symlink" error) before p.readDir. This makes
   the root consistent with the existing child guard.
2. Lake Materialize: before removeDirAll repo.dir, verify repo.dir is a real
   directory, not a symlink; if it is a symlink, unlink it (or abort with guidance)
   rather than recursing into its target.

A short note in the removeDirAll docstring that it must not be called on a symlink
would also help until (1) lands.

Related: the FS API redesign RFC #13638.

Start with removeDirAll in Init/System/IO.lean and compare Lake/Util/IO.lean's removeDirAllIfExists, then trace the call in Lake/Load/Materialize.lean. Run the provided Linux reproduction first; done means a symlinked root is not traversed or emptied and the Lake dependency-update path handles such a package directory safely.