Skip to content

Commit

Permalink
fix: cloud release trace & lake build :release errors (#3248)
Browse files Browse the repository at this point in the history
Fixes a bug with Lake cloud releases where a cloud release would produce
a different trace if the package was the root of the workspace versus a
dependency. Also, an explicit fetch of a cloud release (e.g., via `lake
build :release`) will now error out with a non-zero exit code if it
fails to find, download, and unpack a release.
  • Loading branch information
tydeu authored Feb 17, 2024
1 parent 8f010a6 commit 3fb7262
Show file tree
Hide file tree
Showing 2 changed files with 25 additions and 19 deletions.
11 changes: 11 additions & 0 deletions src/lake/Lake/Build/Job.lean
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,9 @@ abbrev ResultM := OptionIO

namespace Job

@[inline] def try? (self : Job α) : Job (Option α) := do
some <$> self.run

@[inline] def nil : Job Unit :=
pure ()

Expand Down Expand Up @@ -62,6 +65,11 @@ namespace BuildJob

instance : Pure BuildJob := ⟨BuildJob.pure⟩

@[inline] def try? (self : BuildJob α) : BuildJob (Option α) :=
mk <| self.toJob.map fun
| none => some (none, nilTrace)
| some (a, t) => some (some a, t)

@[inline] protected def map (f : α → β) (self : BuildJob α) : BuildJob β :=
mk <| (fun (a,t) => (f a,t)) <$> self.toJob

Expand All @@ -88,6 +96,9 @@ instance : Await BuildJob ResultM := ⟨BuildJob.await⟩
@[inline] def materialize (self : BuildJob α) : ResultM Unit :=
discard <| await self.toJob

def add (t1 : BuildJob α) (t2 : BuildJob β) : BaseIO (BuildJob α) :=
mk <$> seqLeftAsync t1.toJob t2.toJob

def mix (t1 : BuildJob α) (t2 : BuildJob β) : BaseIO (BuildJob Unit) :=
mk <$> seqWithAsync (fun (_,t) (_,t') => ((), mixTrace t t')) t1.toJob t2.toJob

Expand Down
33 changes: 14 additions & 19 deletions src/lake/Lake/Build/Package.lean
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ def Package.recBuildExtraDepTargets (self : Package) : IndexBuildM (BuildJob Uni
job ← job.mix <| ← dep.extraDep.fetch
-- Fetch pre-built release if desired and this package is a dependency
if self.name ≠ (← getWorkspace).root.name ∧ self.preferReleaseBuild then
job ← job.mix <| ← self.release.fetch
job ← job.add (← self.release.fetch).try?
-- Build this package's extra dep targets
for target in self.extraDepTargets do
job ← job.mix <| ← self.fetchTargetJob target
Expand All @@ -49,28 +49,23 @@ def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet :=
def Package.fetchRelease (self : Package) : SchedulerM (BuildJob Unit) := Job.async do
let repo := GitRepo.mk self.dir
let repoUrl? := self.releaseRepo? <|> self.remoteUrl?
let some repoUrl := repoUrl? <|> (← repo.getFilteredRemoteUrl?) | do
logWarning <| s!"{self.name}: wanted prebuilt release, " ++
let some repoUrl := repoUrl? <|> (← repo.getFilteredRemoteUrl?)
| error <| s!"{self.name}: wanted prebuilt release, " ++
"but package's repository URL was not known; it may need to set `releaseRepo?`"
return ((), .nil)
let some tag ← repo.findTag? | do
logWarning <| s!"{self.name}: wanted prebuilt release, " ++
let some tag ← repo.findTag?
| error <| s!"{self.name}: wanted prebuilt release, " ++
"but could not find an associated tag for the package's revision"
return ((), .nil)
let url := s!"{repoUrl}/releases/download/{tag}/{self.buildArchive}"
let logName := s!"{self.name}/{tag}/{self.buildArchive}"
try
let depTrace := Hash.ofString url
let traceFile := FilePath.mk <| self.buildArchiveFile.toString ++ ".trace"
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
return ((), .nil)
let depTrace := Hash.ofString url
let traceFile := FilePath.mk <| self.buildArchiveFile.toString ++ ".trace"
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)

/-- The `PackageFacetConfig` for the builtin `releaseFacet`. -/
def Package.releaseFacetConfig : PackageFacetConfig releaseFacet :=
Expand Down

0 comments on commit 3fb7262

Please sign in to comment.