fix: lake: do not delete path dependencies (#5878)

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 4714f84fb9)

RELEASES.md

@@ -8,6 +8,11 @@ This file contains work-in-progress notes for the upcoming release, as well as p
 Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
 of each version.
 
+v4.13.0
+----------
+
+Release notes to be written.
+
 v4.12.0
 ----------
 

src/CMakeLists.txt

@@ -10,9 +10,9 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 12)
+set(LEAN_VERSION_MINOR 13)
 set(LEAN_VERSION_PATCH 0)
-set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
+set(LEAN_VERSION_IS_RELEASE 1)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
 set(LEAN_VERSION_STRING "${LEAN_VERSION_MAJOR}.${LEAN_VERSION_MINOR}.${LEAN_VERSION_PATCH}")
 if (LEAN_SPECIAL_VERSION_DESC)

src/Lean/Elab/Command.lean

@@ -528,11 +528,12 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
     let mut msgs := (← get).messages
     for tree in (← getInfoTrees) do
       trace[Elab.info] (← tree.format)
-    if let some snap := (← read).snap? then
-      -- We can assume that the root command snapshot is not involved in parallelism yet, so this
-      -- should be true iff the command supports incrementality
-      if (← IO.hasFinished snap.new.result) then
-        liftCoreM <| Language.ToSnapshotTree.toSnapshotTree snap.new.result.get |>.trace
+    if (← isTracingEnabledFor `Elab.snapshotTree) then
+      if let some snap := (← read).snap? then
+        -- We can assume that the root command snapshot is not involved in parallelism yet, so this
+        -- should be true iff the command supports incrementality
+        if (← IO.hasFinished snap.new.result) then
+          liftCoreM <| Language.ToSnapshotTree.toSnapshotTree snap.new.result.get |>.trace
     modify fun st => { st with
       messages := initMsgs ++ msgs
       infoState := { st.infoState with trees := initInfoTrees ++ st.infoState.trees }

src/Lean/Language/Basic.lean

@@ -243,11 +243,16 @@ instance : ToSnapshotTree SnapshotLeaf where
 structure DynamicSnapshot where
   /-- Concrete snapshot value as `Dynamic`. -/
   val  : Dynamic
-  /-- Snapshot tree retrieved from `val` before erasure. -/
-  tree : SnapshotTree
+  /--
+  Snapshot tree retrieved from `val` before erasure. We do thunk even the first level as accessing
+  it too early can create some unnecessary tasks from `toSnapshotTree` that are otherwise avoided by
+  `(sync := true)` when accessing only after elaboration has finished. Early access can even lead to
+  deadlocks when later forcing these unnecessary tasks on a starved thread pool.
+  -/
+  tree : Thunk SnapshotTree
 
 instance : ToSnapshotTree DynamicSnapshot where
-  toSnapshotTree s := s.tree
+  toSnapshotTree s := s.tree.get
 
 /-- Creates a `DynamicSnapshot` from a typed snapshot value. -/
 def DynamicSnapshot.ofTyped [TypeName α] [ToSnapshotTree α] (val : α) : DynamicSnapshot where

src/lake/Lake/Build/Package.lean

@@ -44,9 +44,9 @@ def Package.maybeFetchBuildCache (self : Package) : FetchM (BuildJob Bool) := do
   let shouldFetch :=
     (← getTryCache) &&
     (self.preferReleaseBuild || -- GitHub release
-      !(self.scope.isEmpty -- no Reservoir
-        || (← getElanToolchain).isEmpty
-        || (← self.buildDir.pathExists)))
+      ((self.scope == "leanprover" || self.scope == "leanprover-community")
+        && !(← getElanToolchain).isEmpty
+        && !(← self.buildDir.pathExists))) -- Reservoir
   if shouldFetch then
     self.optBuildCache.fetch
   else
@@ -79,15 +79,12 @@ def Package.maybeFetchBuildCacheWithWarning (self : Package) := do
 def Package.fetchOptRelease := @maybeFetchBuildCacheWithWarning
 
 /--
-Build the `extraDepTargets` for the package and its transitive dependencies.
-Also fetch pre-built releases for the package's' dependencies.
+Build the `extraDepTargets` for the package.
+Also, if the package is a dependency, maybe fetch its build cache.
 -/
 def Package.recBuildExtraDepTargets (self : Package) : FetchM (BuildJob Unit) :=
   withRegisterJob s!"{self.name}:extraDep" do
   let mut job := BuildJob.nil
-  -- Build dependencies' extra dep targets
-  for dep in self.deps do
-    job := job.mix <| ← dep.extraDep.fetch
   -- Fetch build cache if this package is a dependency
   if self.name ≠ (← getWorkspace).root.name then
     job := job.add <| ← self.maybeFetchBuildCacheWithWarning

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
 

src/lake/tests/noRelease/Test.lean

@@ -0,0 +1 @@
+import Dep

src/lake/tests/noRelease/dep/lakefile.lean

@@ -5,3 +5,5 @@ package dep where
   preferReleaseBuild := true
   releaseRepo := "https://example.com"
   buildArchive := "release.tgz"
+
+lean_lib Dep

src/lake/tests/noRelease/test.sh

@@ -40,9 +40,10 @@ EOF
 
 # Test that an indirect fetch on the release does not cause the build to fail
 $LAKE build Test | diff -u --strip-trailing-cr <(cat << EOF
-⚠ [2/5] Ran dep:extraDep
+⚠ [3/6] Ran dep:extraDep
 warning: building from source; failed to fetch GitHub release (run with '-v' for details)
-✔ [4/5] Built Test
+✔ [4/6] Built Dep
+✔ [5/6] Built Test
 Build completed successfully.
 EOF
 ) -
@@ -56,7 +57,7 @@ mkdir -p .lake/packages/dep/.lake/build
 $LAKE -d .lake/packages/dep pack 2>&1 | grep --color "packing"
 test -f .lake/packages/dep/.lake/release.tgz
 echo 4225503363911572621 > .lake/packages/dep/.lake/release.tgz.trace
-rmdir .lake/packages/dep/.lake/build
+rm -rf .lake/packages/dep/.lake/build
 $LAKE build dep:release -v | grep --color "tar"
 test -d .lake/packages/dep/.lake/build
 

src/lake/tests/online/test.sh

@@ -18,6 +18,9 @@ $LAKE -v -f git.toml build @Cli:extraDep |
 
 ./clean.sh
 $LAKE -f barrel.lean update
+# Test that a barrel is not fetched for an unbuilt dependency
+$LAKE -v -f barrel.lean build @test:extraDep |
+  grep --color "Cli:optBarrel" && exit 1 || true
 # Test that barrels are not fetched after the build directory is created.
 mkdir -p .lake/packages/Cli/.lake/build
 ($LAKE -v -f barrel.lean build @Cli:extraDep) |