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