From 3ece36de9db7dca9fd1ca2fe514370e305fb600a Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Tue, 26 Nov 2024 17:10:42 -0500 Subject: [PATCH] feat: GitHub cloud releases do not clobber prebuilt artifacts (#6218) 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 :release`. --- src/lake/Lake/Build/Package.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean index 66cb6ae30726..ec8185b0ffc3 100644 --- a/src/lake/Lake/Build/Package.lean +++ b/src/lake/Lake/Build/Package.lean @@ -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