From 4714f84fb9511bebd5ecbdd81e2c35de2bc627d3 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Tue, 29 Oct 2024 22:31:20 -0400 Subject: [PATCH] fix: lake: do not delete path dependencies (#5878) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- src/lake/Lake/Load/Resolve.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/lake/Lake/Load/Resolve.lean b/src/lake/Lake/Load/Resolve.lean index a5681a42da..e92c77d2f7 100644 --- a/src/lake/Lake/Load/Resolve.lean +++ b/src/lake/Lake/Load/Resolve.lean @@ -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