diff --git a/src/lake/Lake/Build/Actions.lean b/src/lake/Lake/Build/Actions.lean index 4be6e4e179..713a7030a0 100644 --- a/src/lake/Lake/Build/Actions.lean +++ b/src/lake/Lake/Build/Actions.lean @@ -77,7 +77,7 @@ def compileExe (name : String) (binFile : FilePath) (linkFiles : Array FilePath) /-- Download a file using `curl`, clobbering any existing file. -/ def download (name : String) (url : String) (file : FilePath) : LogIO PUnit := do - logInfo s!"Downloading {name}" + logVerbose s!"Downloading {name}" if (← file.pathExists) then IO.FS.removeFile file else @@ -91,7 +91,7 @@ def download (name : String) (url : String) (file : FilePath) : LogIO PUnit := d /-- Unpack an archive `file` using `tar` into the directory `dir`. -/ def untar (name : String) (file : FilePath) (dir : FilePath) (gzip := true) : LogIO PUnit := do - logInfo s!"Unpacking {name}" + logVerbose s!"Unpacking {name}" let mut opts := "-x" if (← getIsVerbose) then opts := opts.push 'v' @@ -105,7 +105,7 @@ def untar (name : String) (file : FilePath) (dir : FilePath) (gzip := true) : Lo /-- Pack a directory `dir` using `tar` into the archive `file`. -/ def tar (name : String) (dir : FilePath) (file : FilePath) (gzip := true) (excludePaths : Array FilePath := #[]) : LogIO PUnit := do - logInfo s!"Packing {name}" + logVerbose s!"Packing {name}" createParentDirs file let mut args := #["-c"] if gzip then diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean index 4ad252cc82..dec6f6b3d1 100644 --- a/src/lake/Lake/Build/Package.lean +++ b/src/lake/Lake/Build/Package.lean @@ -16,17 +16,8 @@ namespace Lake /-- Compute a topological ordering of the package's transitive dependencies. -/ def Package.recComputeDeps (self : Package) : IndexBuildM (Array Package) := do - let mut deps := #[] - let mut depSet := PackageSet.empty - for dep in self.deps do - for depDep in (← fetch <| dep.facet `deps) do - unless depSet.contains depDep do - deps := deps.push depDep - depSet := depSet.insert depDep - unless depSet.contains dep do - deps := deps.push dep - depSet := depSet.insert dep - return deps + (·.toArray) <$> self.deps.foldlM (init := OrdPackageSet.empty) fun deps dep => do + return (← fetch <| dep.facet `deps).foldl (·.insert ·) deps |>.insert dep /-- The `PackageFacetConfig` for the builtin `depsFacet`. -/ def Package.depsFacetConfig : PackageFacetConfig depsFacet := @@ -62,10 +53,12 @@ def Package.fetchRelease (self : Package) : SchedulerM (BuildJob Unit) := Job.as let logName := s!"{self.name}/{tag}/{self.buildArchive}" try let depTrace := Hash.ofString url - let trace ← buildFileUnlessUpToDate self.buildArchiveFile depTrace do + let traceFile := FilePath.mk <| self.buildArchiveFile.toString ++ ".trace" + buildUnlessUpToDate self.buildArchiveFile depTrace traceFile do + logStep s!"Fetching {self.name} cloud release" download logName url self.buildArchiveFile untar logName self.buildArchiveFile self.buildDir - return ((), trace) + return ((), .nil) else return ((), .nil) @@ -73,6 +66,20 @@ def Package.fetchRelease (self : Package) : SchedulerM (BuildJob Unit) := Job.as def Package.releaseFacetConfig : PackageFacetConfig releaseFacet := mkFacetJobConfig (·.fetchRelease) +/-- Perform a build job after first checking for a cloud release for the package. -/ +def Package.afterReleaseAsync (self : Package) (build : SchedulerM (Job α)) : IndexBuildM (Job α) := do + if self.preferReleaseBuild ∧ self.name ≠ (← getRootPackage).name then + (← self.release.fetch).bindAsync fun _ _ => build + else + build + +/-- Perform a build after first checking for a cloud release for the package. -/ +def Package.afterReleaseSync (self : Package) (build : BuildM α) : IndexBuildM (Job α) := do + if self.preferReleaseBuild ∧ self.name ≠ (← getRootPackage).name then + (← self.release.fetch).bindSync fun _ _ => build + else + Job.async build + open Package in /-- A package facet name to build function map that contains builders for