diff --git a/src/lake/Lake/Build/Job.lean b/src/lake/Lake/Build/Job.lean index 31eca9a5eacb..85c7a706c7f9 100644 --- a/src/lake/Lake/Build/Job.lean +++ b/src/lake/Lake/Build/Job.lean @@ -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 () @@ -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 @@ -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 diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean index 9b62acfbc293..d985718301af 100644 --- a/src/lake/Lake/Build/Package.lean +++ b/src/lake/Lake/Build/Package.lean @@ -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 @@ -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 :=