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.

Author: tydeu

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

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

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."

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
 

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
 

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 isRootArtifactCacheWritable (ws : Workspace) : Bool :=
+  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
+@[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

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",

tests/lake/tests/cache/disabled.toml

@@ -3,3 +3,6 @@ enableArtifactCache = false
 
 [[lean_lib]]
 name = "Test"
+
+[[lean_lib]]
+name = "Ignored"

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

tests/lake/tests/cache/unset.toml

@@ -2,3 +2,6 @@ name = "test"
 
 [[lean_lib]]
 name = "Test"
+
+[[lean_lib]]
+name = "Ignored"