From 39c26fce1da321b24eaf949d0d7d028ba589e4e1 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Sat, 7 Feb 2026 13:07:05 -0500 Subject: [PATCH] feat: lake: disabling the artifact cache also disables fetching (#12300) This PR makes disabling the artifact cache (e.g., via `LAKE_ARTIFACT_CACHE=false` or `enableArtifactCache = false`) now stop Lake from fetching from the cache (whereas it previously only stopped writing to it). There are now 3 possible configuration of the local artifact cache for a package: * `true`: Artifacts will be fetched from the cache before building (if available) and built artifacts will be cached. * `false:`: Lake will neither fetch artifacts from the cache or store them into it. * **default** (no configuration set): Lake will fetch artifacts from the cache but not store them into it. A key motivation for this is to, by default, reuse artifacts downloaded into the cache from a remote service. --- src/lake/Lake/Build/Common.lean | 9 +++++---- src/lake/Lake/Build/Module.lean | 7 ++++--- src/lake/Lake/Build/Run.lean | 2 +- src/lake/Lake/Config/Monad.lean | 19 ++++++++++++++++--- src/lake/Lake/Config/PackageConfig.lean | 6 +++--- src/lake/Lake/Config/Workspace.lean | 18 ++++++++++++++---- src/lake/schemas/lakefile-toml-schema.json | 2 +- tests/lake/tests/cache/disabled.toml | 3 +++ tests/lake/tests/cache/test.sh | 14 +++++++++++++- tests/lake/tests/cache/unset.toml | 3 +++ .../lake/tests/env/disableArtifactCache.toml | 2 ++ tests/lake/tests/env/test.sh | 3 ++- 12 files changed, 67 insertions(+), 21 deletions(-) create mode 100644 tests/lake/tests/env/disableArtifactCache.toml diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean index a25841b58a..2d65b8978e 100644 --- a/src/lake/Lake/Build/Common.lean +++ b/src/lake/Lake/Build/Common.lean @@ -497,7 +497,7 @@ in either the saved trace file or in the cached input-to-content mapping. (inputHash : Hash) (savedTrace : SavedTrace) (cache : Cache) (pkg : Package) : JobM (Option α) := do - let updateCache ← pkg.isArtifactCacheEnabled + let updateCache ← pkg.isArtifactCacheWritable if let some out ← cache.readOutputs? pkg.cacheScope inputHash then match (← resolveOutputs? out) with | .ok arts => @@ -577,7 +577,7 @@ public def buildArtifactUnlessUpToDate else return some art let art ← id do - if (← pkg.isArtifactCacheEnabled) then + if (← pkg.isArtifactCacheWritable) then let restore := restore || pkg.restoreAllArtifacts if let some art ← fetchArt? restore then return art @@ -593,9 +593,10 @@ public def buildArtifactUnlessUpToDate computeArtifact file ext text else if (← savedTrace.replayIfUpToDate file depTrace) then computeArtifact file ext text - else if let some art ← fetchArt? (restore := true) then - return art else + if (← pkg.isArtifactCacheReadable) then + if let some art ← fetchArt? (restore := true) then + return art doBuild depTrace traceFile if let some outputsRef := pkg.outputsRef? then outputsRef.insert inputHash art.descr diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean index 66f6431a83..ad5f3c4ffa 100644 --- a/src/lake/Lake/Build/Module.lean +++ b/src/lake/Lake/Build/Module.lean @@ -761,7 +761,7 @@ private def Module.recBuildLean (mod : Module) : FetchM (Job ModuleOutputArtifac else some <$> mod.restoreNeededArtifacts arts let arts ← id do - if (← mod.pkg.isArtifactCacheEnabled) then + if (← mod.pkg.isArtifactCacheWritable) then if let some arts ← fetchArtsFromCache? mod.pkg.restoreAllArtifacts then return arts else @@ -776,9 +776,10 @@ private def Module.recBuildLean (mod : Module) : FetchM (Job ModuleOutputArtifac mod.computeArtifacts setup.isModule else if (← savedTrace.replayIfUpToDate (oldTrace := srcTrace.mtime) mod depTrace) then mod.computeArtifacts setup.isModule - else if let some arts ← fetchArtsFromCache? true then - return arts else + if (← mod.pkg.isArtifactCacheReadable) then + if let some arts ← fetchArtsFromCache? true then + return arts mod.buildLean depTrace srcFile setup if let some ref := mod.pkg.outputsRef? then ref.insert inputHash arts.descrs diff --git a/src/lake/Lake/Build/Run.lean b/src/lake/Lake/Build/Run.lean index a8bbd2c202..bd0f8fef28 100644 --- a/src/lake/Lake/Build/Run.lean +++ b/src/lake/Lake/Build/Run.lean @@ -263,7 +263,7 @@ def Workspace.saveOutputs [logger : MonadLog BaseIO] (ws : Workspace) (out : IO.FS.Stream) (outputsFile : FilePath) (isVerbose : Bool) : BaseIO Unit := do - unless ws.isRootArtifactCacheEnabled do + unless ws.isRootArtifactCacheWritable do logWarning s!"{ws.root.prettyName}: \ the artifact cache is not enabled for this package, so the artifacts described \ by the mappings produced by `-o` will not necessarily be available in the cache." diff --git a/src/lake/Lake/Config/Monad.lean b/src/lake/Lake/Config/Monad.lean index 91e8382558..cc834f2a94 100644 --- a/src/lake/Lake/Config/Monad.lean +++ b/src/lake/Lake/Config/Monad.lean @@ -171,13 +171,26 @@ public def getArtifact? [Bind m] [MonadLiftT BaseIO m] (descr : ArtifactDescr) : getLakeCache >>= (·.getArtifact? descr) /-- -Returns whether the package the artifact cache is enabled for the package. +Returns whether the package should store its artifacts in the Lake artifact cache. If the package has not configured the artifact cache itself through {lean}`Package.enableArtifactCache?`, this will default to the workspace configuration. -/ -public def Package.isArtifactCacheEnabled [MonadWorkspace m] (self : Package) : m Bool := - (self.enableArtifactCache?.getD ·.enableArtifactCache) <$> getWorkspace +@[inline] public def Package.isArtifactCacheReadable [MonadWorkspace m] (self : Package) : m Bool := + (self.enableArtifactCache? <|> ·.enableArtifactCache? |>.getD true) <$> getWorkspace + +/-- +Returns whether the package should restore its artifacts from the Lake artifact cache. + +If the package has not configured the artifact cache itself through +{lean}`Package.enableArtifactCache?`, this will default to the workspace configuration. +-/ +@[inline] public def Package.isArtifactCacheWritable [MonadWorkspace m] (self : Package) : m Bool := + (self.enableArtifactCache? <|> ·.enableArtifactCache? |>.getD false) <$> getWorkspace + +@[inherit_doc isArtifactCacheWritable, deprecated isArtifactCacheWritable (since := "2026-02-03")] +public abbrev Package.isArtifactCacheEnabled [MonadWorkspace m] (self : Package) : m Bool := + self.isArtifactCacheWritable end diff --git a/src/lake/Lake/Config/PackageConfig.lean b/src/lake/Lake/Config/PackageConfig.lean index 2323adb2ec..bdd1ccd701 100644 --- a/src/lake/Lake/Config/PackageConfig.lean +++ b/src/lake/Lake/Config/PackageConfig.lean @@ -292,9 +292,9 @@ public configuration PackageConfig (p : Name) (n : Name) extends WorkspaceConfig scripts that rely on specific location of artifacts may wish to disable this feature. If `none` (the default), this will fallback to (in order): - * The `LAKE_ARTIFACT_CACHE` environment variable (if set) - * The workspace root's `enableArtifactCache` configuration (if set and this package is a dependency) - * Lake's default: `false` + * The `LAKE_ARTIFACT_CACHE` environment variable (if set). + * The workspace root's `enableArtifactCache` configuration (if set and this package is a dependency). + * **Lake's default**: The package can use artifacts from the cache, but cannot write to it. -/ enableArtifactCache?, enableArtifactCache : Option Bool := none diff --git a/src/lake/Lake/Config/Workspace.lean b/src/lake/Lake/Config/Workspace.lean index 07e90a3ae0..af1cb9e330 100644 --- a/src/lake/Lake/Config/Workspace.lean +++ b/src/lake/Lake/Config/Workspace.lean @@ -87,12 +87,22 @@ namespace Workspace self.root.lakeDir /-- Whether the Lake artifact cache should be enabled by default for packages in the workspace. -/ +@[inline] public def enableArtifactCache? (ws : Workspace) : Option Bool := + ws.lakeEnv.enableArtifactCache? <|> ws.root.enableArtifactCache? + +/-- Whether the Lake artifact cache should be enabled by default for packages in the workspace. -/ +@[deprecated enableArtifactCache? (since := "2026-02-03")] public def enableArtifactCache (ws : Workspace) : Bool := - ws.lakeEnv.enableArtifactCache? <|> ws.root.enableArtifactCache? |>.getD false + ws.enableArtifactCache?.getD false /-- Whether the Lake artifact cache should is enabled for workspace's root package. -/ -public def isRootArtifactCacheEnabled (ws : Workspace) : Bool := - ws.root.enableArtifactCache? <|> ws.lakeEnv.enableArtifactCache? |>.getD false +public def isRootArtifactCacheWritable (ws : Workspace) : Bool := + ws.enableArtifactCache?.getD false + +/-- Whether the Lake artifact cache should is enabled for workspace's root package. -/ +@[deprecated isRootArtifactCacheWritable (since := "2026-02-03")] +public abbrev isRootArtifactCacheEnabled (ws : Workspace) : Bool := + ws.isRootArtifactCacheWritable /-- The path to the workspace's remote packages directory relative to {lean}`dir`. -/ @[inline] public def relPkgsDir (self : Workspace) : FilePath := @@ -302,7 +312,7 @@ to run executables. public def augmentedEnvVars (self : Workspace) : Array (String × Option String) := let vars := self.lakeEnv.baseVars ++ #[ ("LAKE_CACHE_DIR", some self.lakeCache.dir.toString), - ("LAKE_ARTIFACT_CACHE", toString self.enableArtifactCache), + ("LAKE_ARTIFACT_CACHE", if let some b := self.enableArtifactCache? then toString b else ""), ("LEAN_PATH", some self.augmentedLeanPath.toString), ("LEAN_SRC_PATH", some self.augmentedLeanSrcPath.toString), -- Allow the Lean version to change dynamically within core diff --git a/src/lake/schemas/lakefile-toml-schema.json b/src/lake/schemas/lakefile-toml-schema.json index ab5a2c6ba3..0aa9af20a1 100644 --- a/src/lake/schemas/lakefile-toml-schema.json +++ b/src/lake/schemas/lakefile-toml-schema.json @@ -464,7 +464,7 @@ }, "enableArtifactCache": { "type": "boolean", - "description": "Whether to enables Lake's local, offline artifact cache for the package.\n\nArtifacts (i.e., build products) of packages will be shared across local copies by storing them in a cache associated with the Lean toolchain.\nThis can significantly reduce initial build times and disk space usage when working with multiple copies of large projects or large dependencies.\n\nAs a caveat, build targets which support the artifact cache will not be stored in their usual location within the build directory. Thus, projects with custom build scripts that rely on specific location of artifacts may wish to disable this feature.\n\nIf not set, If `none` (the default), this will fallback to (in order):\n* The `LAKE_ARTIFACT_CACHE` environment variable (if set)\n* The workspace root's `enableArtifactCache` configuration (if set and this package is a dependency)\n* Lake's default: `false`" + "description": "Whether to enables Lake's local, offline artifact cache for the package.\n\nArtifacts (i.e., build products) of packages will be shared across local copies by storing them in a cache associated with the Lean toolchain.\nThis can significantly reduce initial build times and disk space usage when working with multiple copies of large projects or large dependencies.\n\nAs a caveat, build targets which support the artifact cache will not be stored in their usual location within the build directory. Thus, projects with custom build scripts that rely on specific location of artifacts may wish to disable this feature.\n\nIf `none` (the default), this will fallback to (in order):\n* The `LAKE_ARTIFACT_CACHE` environment variable (if set).\n* The workspace root's `enableArtifactCache` configuration (if set and this package is a dependency).\n* **Lake's default**: The package can use artifacts from the cache, but cannot write to it." }, "restoreAllArtifacts": { "type": "boolean", diff --git a/tests/lake/tests/cache/disabled.toml b/tests/lake/tests/cache/disabled.toml index 4ce5c0a4b4..9bd7b39f90 100644 --- a/tests/lake/tests/cache/disabled.toml +++ b/tests/lake/tests/cache/disabled.toml @@ -3,3 +3,6 @@ enableArtifactCache = false [[lean_lib]] name = "Test" + +[[lean_lib]] +name = "Ignored" diff --git a/tests/lake/tests/cache/test.sh b/tests/lake/tests/cache/test.sh index 5e3f3b9a04..ba010accb9 100755 --- a/tests/lake/tests/cache/test.sh +++ b/tests/lake/tests/cache/test.sh @@ -1,5 +1,6 @@ #!/usr/bin/env bash source ../common.sh +NO_BUILD_CODE=3 ./clean.sh @@ -83,8 +84,19 @@ check_diff /dev/null <(ls -1 "$CACHE_DIR/*.hash" 2>/dev/null) # Verify that the executable has the right permissions to be run test_run exe test -# Verify that fetching from the cache creates a trace file that does not replay +# Create a test module that can be arbitrarily edited and cached +# The `Test` module's artifacts are more carefully managed throught this test touch Ignored.lean +test_run -v build +Ignored +test_cmd rm -f .lake/build/lib/lean/Ignored.trace + +# Verify that fetching from the cache can be disabled +test_cmd rm -f .lake/build/lib/lean/Ignored.trace +test_status $NO_BUILD_CODE -v -f disabled.toml build +Ignored --no-build +LAKE_ARTIFACT_CACHE=false test_status $NO_BUILD_CODE -v \ + -f unset.toml build +Ignored --no-build + +# Verify that fetching from the cache creates a trace file that does not replay test_out "Fetched Ignored" -v build +Ignored test_exp -f .lake/build/lib/lean/Ignored.trace test_out "Fetched Ignored" -v build +Ignored diff --git a/tests/lake/tests/cache/unset.toml b/tests/lake/tests/cache/unset.toml index 617c0d1b48..d03a4e0ac4 100644 --- a/tests/lake/tests/cache/unset.toml +++ b/tests/lake/tests/cache/unset.toml @@ -2,3 +2,6 @@ name = "test" [[lean_lib]] name = "Test" + +[[lean_lib]] +name = "Ignored" diff --git a/tests/lake/tests/env/disableArtifactCache.toml b/tests/lake/tests/env/disableArtifactCache.toml new file mode 100644 index 0000000000..668845729c --- /dev/null +++ b/tests/lake/tests/env/disableArtifactCache.toml @@ -0,0 +1,2 @@ +name = "test" +enableArtifactCache = false diff --git a/tests/lake/tests/env/test.sh b/tests/lake/tests/env/test.sh index e369d2da2f..6f352d2a93 100755 --- a/tests/lake/tests/env/test.sh +++ b/tests/lake/tests/env/test.sh @@ -46,8 +46,9 @@ LEAN_CC=foo test_eq "foo" env printenv LEAN_CC LAKE_ARTIFACT_CACHE=true test_eq "true" env printenv LAKE_ARTIFACT_CACHE LAKE_ARTIFACT_CACHE=false test_eq "false" env printenv LAKE_ARTIFACT_CACHE LAKE_ARTIFACT_CACHE= test_eq "" env printenv LAKE_ARTIFACT_CACHE -LAKE_ARTIFACT_CACHE= test_eq "false" -d ../../examples/hello env printenv LAKE_ARTIFACT_CACHE +LAKE_ARTIFACT_CACHE= test_eq "" -d ../../examples/hello env printenv LAKE_ARTIFACT_CACHE LAKE_ARTIFACT_CACHE= test_eq "true" -f enableArtifactCache.toml env printenv LAKE_ARTIFACT_CACHE +LAKE_ARTIFACT_CACHE= test_eq "false" -f disableArtifactCache.toml env printenv LAKE_ARTIFACT_CACHE test_cmd rm lake-manifest.json # Test `LAKE_PKG_URL_MAP` setting and errors