max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: untar cloud release if no build dir (#2928)

Browse source 
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.
This commit is contained in:
Mac Malone 2023-11-27 11:09:58 -05:00 • committed by GitHub
parent 6592df52cc
commit 0249a8c15e
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 19 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/lake/Lake/Build/Common.lean
View file

@ -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

6
src/lake/Lake/Build/Package.lean
View file

@ -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