From 068208091fb87db7f021171c836efa8a5612c41b Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Sat, 12 Oct 2024 18:56:49 -0400 Subject: [PATCH] refactor: lake: restrict cache fetch to leanprover* (#5642) Lake will now only automatically fetch Reservoir build caches for package in the the `leanprover` and `leanprover-community` organizations. We are not planning to expand the Reservoir build cache to other packages until farther in the future. --- src/lake/Lake/Build/Package.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean index 39a1ff261e..40623b0d75 100644 --- a/src/lake/Lake/Build/Package.lean +++ b/src/lake/Lake/Build/Package.lean @@ -44,9 +44,9 @@ def Package.maybeFetchBuildCache (self : Package) : FetchM (BuildJob Bool) := do let shouldFetch := (← getTryCache) && (self.preferReleaseBuild || -- GitHub release - !(self.scope.isEmpty -- no Reservoir - || (← getElanToolchain).isEmpty - || (← self.buildDir.pathExists))) + ((self.scope == "leanprover" || self.scope == "leanprover-community") + && !(← getElanToolchain).isEmpty + && !(← self.buildDir.pathExists))) -- Reservoir if shouldFetch then self.optBuildCache.fetch else