From 0249a8c15e3686ea67d304aaee0c36d93c527bbf Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Mon, 27 Nov 2023 11:09:58 -0500
Subject: [PATCH] fix: untar cloud release if no build dir (#2928)

Cloud releases will now properly be re-unpacked if the build directory
is removed. This fixes [an issue reported on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Some.20files.20not.20found.20in.20the.20cache/near/402921424)
with the new `.lake` directory that broke Mathlib's ProofWidgets cache.
---
 src/lake/Lake/Build/Common.lean  | 18 +++++++++++++++---
 src/lake/Lake/Build/Package.lean |  6 ++++--
 2 files changed, 19 insertions(+), 5 deletions(-)

diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean
index 3935c6c223..a486d5d1bd 100644
--- a/src/lake/Lake/Build/Common.lean
+++ b/src/lake/Lake/Build/Common.lean
@@ -27,14 +27,26 @@ namespace Lake
 /--
 Build `info` unless it already exists and `depTrace` matches that
 of the `traceFile`. If rebuilt, save the new `depTrace` to the `tracefile`.
+Returns whether `info` was already up-to-date.
 -/
-@[inline] def buildUnlessUpToDate [CheckExists ι] [GetMTime ι] (info : ι)
-(depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit) : JobM PUnit := do
-  unless (← depTrace.checkUpToDate info traceFile) do
+@[inline] def buildUnlessUpToDate' [CheckExists ι] [GetMTime ι] (info : ι)
+(depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit) : JobM Bool := do
+  if (← depTrace.checkUpToDate info traceFile) then
+    return true
+  else
     if (← getNoBuild) then
       IO.Process.exit noBuildCode.toUInt8
     build
     depTrace.writeToFile traceFile
+    return false
+
+/--
+Build `info` unless it already exists and `depTrace` matches that
+of the `traceFile`. If rebuilt, save the new `depTrace` to the `tracefile`.
+-/
+@[inline] def buildUnlessUpToDate [CheckExists ι] [GetMTime ι] (info : ι)
+(depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit) : JobM PUnit := do
+  discard <| buildUnlessUpToDate' info depTrace traceFile build
 
 /-- Fetch the trace of a file that may have its hash already cached in a `.hash` file. -/
 def fetchFileTrace (file : FilePath) : BuildM BuildTrace := do
diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean
index dccbc6b006..9b62acfbc2 100644
--- a/src/lake/Lake/Build/Package.lean
+++ b/src/lake/Lake/Build/Package.lean
@@ -62,9 +62,11 @@ def Package.fetchRelease (self : Package) : SchedulerM (BuildJob Unit) := Job.as
   try
     let depTrace := Hash.ofString url
     let traceFile := FilePath.mk <| self.buildArchiveFile.toString ++ ".trace"
-    buildUnlessUpToDate self.buildArchiveFile depTrace traceFile do
-      logStep s!"Fetching {self.name} cloud release"
+    let upToDate ← buildUnlessUpToDate' self.buildArchiveFile depTrace traceFile do
+      logStep s!"Downloading {self.name} cloud release"
       download logName url self.buildArchiveFile
+    unless upToDate && (← self.buildDir.pathExists) do
+      logStep s!"Unpacking {self.name} cloud release"
       untar logName self.buildArchiveFile self.buildDir
     return ((), .nil)
   else