Skip to content

Commit

Permalink
fix: lake: do not delete path dependencies (#5878)
Browse files Browse the repository at this point in the history
Fixes a serious issue where Lake would delete path dependencies when
attempting to cleanup a dependency required with an incorrect name.

Closes #5876. Originally part of #5684, but also independently
discovered by François.

(cherry picked from commit 4714f84)
  • Loading branch information
tydeu authored and kim-em committed Oct 30, 2024
1 parent 480d731 commit 6d22e0e
Showing 1 changed file with 5 additions and 4 deletions.
9 changes: 5 additions & 4 deletions src/lake/Lake/Load/Resolve.lean
Original file line number Diff line number Diff line change
Expand Up @@ -210,10 +210,11 @@ def updateDep
| .git (inputRev? := some rev) .. => s!" @ {repr rev}"
| _ => ""
logError (stdMismatchError depPkg.name.toString rev)
if let .error e ← IO.FS.removeDirAll depPkg.dir |>.toBaseIO then -- cleanup
-- Deleting git repositories via IO.FS.removeDirAll does not work reliably on Windows
logError s!"'{dep.name}' was downloaded incorrectly; \
you will need to manually delete '{depPkg.dir}': {e}"
if matDep.manifestEntry.src matches .git .. then
if let .error e ← IO.FS.removeDirAll depPkg.dir |>.toBaseIO then -- cleanup
-- Deleting git repositories via IO.FS.removeDirAll does not work reliably on Windows
logError s!"'{dep.name}' was downloaded incorrectly; \
you will need to manually delete '{depPkg.dir}': {e}"
error s!"{pkg.name}: package '{depPkg.name}' was required as '{dep.name}'"
return depPkg

Expand Down

0 comments on commit 6d22e0e

Please sign in to comment.