Skip to content

Commit

Permalink
feat: GitHub cloud releases do not clobber prebuilt artifacts (#6218)
Browse files Browse the repository at this point in the history
This PR makes Lake no longer automatically fetch GitHub cloud releases
if the package build directory is already present (mirroring the
behavior of the Reservoir cache). This prevents the cache from
clobbering existing prebuilt artifacts. Users can still manually fetch
the cache and clobber the build directory by running `lake build
<pkg>:release`.
  • Loading branch information
tydeu authored Nov 26, 2024
1 parent 54c4836 commit 3ece36d
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/lake/Lake/Build/Package.lean
Original file line number Diff line number Diff line change
Expand Up @@ -47,10 +47,10 @@ def Package.optBuildCacheFacetConfig : PackageFacetConfig optBuildCacheFacet :=
def Package.maybeFetchBuildCache (self : Package) : FetchM (BuildJob Bool) := do
let shouldFetch :=
(← getTryCache) &&
!(← self.buildDir.pathExists) && -- do not automatically clobber prebuilt artifacts
(self.preferReleaseBuild || -- GitHub release
((self.scope == "leanprover" || self.scope == "leanprover-community")
&& !(← getElanToolchain).isEmpty
&& !(← self.buildDir.pathExists))) -- Reservoir
&& !(← getElanToolchain).isEmpty)) -- Reservoir
if shouldFetch then
self.optBuildCache.fetch
else
Expand Down

0 comments on commit 3ece36d

Please sign in to comment.