feat: lake: inherit restoreAllArtifacts from workspace (#12837)

This PR changes the default behavior of the `restoreAllArtifacts`
package configuration to mirror that of the workspace. If the workspace
also has it unset, the default remains the same (`false`).

src/lake/Lake/Build/Common.lean

@@ -655,7 +655,7 @@ public def buildArtifactUnlessUpToDate
         return some art
     let art ← id do
       if (← pkg.isArtifactCacheWritable) then
-        let restore := restore || pkg.restoreAllArtifacts
+        let restore := restore || (← pkg.restoreAllArtifacts)
         if let some art ← fetchArt? restore then
           return art
         else

src/lake/Lake/Build/Module.lean

@@ -803,14 +803,15 @@ private def Module.recBuildLean (mod : Module) : FetchM (Job ModuleOutputArtifac
         some <$> mod.restoreNeededArtifacts arts
     let arts ← id do
       if (← mod.pkg.isArtifactCacheWritable) then
-        if let some arts ← fetchArtsFromCache? mod.pkg.restoreAllArtifacts then
+        let restore ← mod.pkg.restoreAllArtifacts
+        if let some arts ← fetchArtsFromCache? restore then
           return arts
         else
           let status ← savedTrace.replayIfUpToDate' (oldTrace := srcTrace.mtime) mod depTrace
           unless status.isUpToDate do
             discard <| mod.buildLean depTrace srcFile setup
           if status.isCacheable then
-            let arts ← mod.cacheOutputArtifacts setup.isModule mod.pkg.restoreAllArtifacts
+            let arts ← mod.cacheOutputArtifacts setup.isModule restore
             (← getLakeCache).writeOutputs mod.pkg.cacheScope inputHash arts.descrs
             return arts
           else

src/lake/Lake/Config/Monad.lean

@@ -172,6 +172,16 @@ deprecated "Deprecated without replacelement." (since := "2025-03-04")]
 public def getArtifact? [Bind m] [MonadLiftT BaseIO m] (descr : ArtifactDescr) : m (Option Artifact) :=
   getLakeCache >>= (·.getArtifact? descr)
 
+/--
+Returns whether the package should restore its artifacts from the Lake artifact cache.
+
+If the package has not configured this option itself through
+{lean}`Package.restoreAllArtifacts?`, this will default to the workspace configuration.
+If not configured at all, this defaults to {lean}`false`.
+-/
+@[inline] public def Package.restoreAllArtifacts [MonadWorkspace m] (self : Package) : m Bool :=
+  (self.restoreAllArtifacts? <|> ·.restoreAllArtifacts? |>.getD false) <$> getWorkspace
+
 /--
 Returns whether the package should retrieve its artifacts from the Lake artifact cache.
 

src/lake/Lake/Config/Package.lean

@@ -384,9 +384,9 @@ The package's `buildDir` joined with its `nativeLibDir` configuration.
 @[inline] public def enableArtifactCache? (self : Package) : Option Bool :=
   self.config.enableArtifactCache?
 
-/-- The package's `restoreAllArtifacts` configuration. -/
-@[inline] public def restoreAllArtifacts (self : Package) : Bool :=
-  self.config.restoreAllArtifacts
+/-- The package's `restoreAllArtifacts?` configuration. -/
+@[inline] public def restoreAllArtifacts? (self : Package) : Option Bool :=
+  self.config.restoreAllArtifacts?
 
 /-- The directory within the Lake cache were package-scoped files are stored. -/
 public def cacheScope (self : Package) : String :=

src/lake/Lake/Config/PackageConfig.lean

@@ -303,9 +303,10 @@ public configuration PackageConfig (p : Name) (n : Name) extends WorkspaceConfig
   artifacts into the build directory. This ensures the build results are available
   to external consumers who expect them in the build directory.
 
-  Defaults to `false`.
+  If `none` (the default), this will follow the workspace's `restoreAllArtifacts` configuration
+  (if set and this package is a dependency). If that is also unset, this will default to `false`.
   -/
-  restoreAllArtifacts : Bool := false
+  restoreAllArtifacts?, restoreAllArtifacts : Option Bool := none
 
   /--
   Whether native libraries (of this package) should be prefixed with `lib` on Windows.

src/lake/Lake/Config/Workspace.lean

@@ -105,6 +105,10 @@ public def isRootArtifactCacheWritable (ws : Workspace) : Bool :=
 public abbrev isRootArtifactCacheEnabled (ws : Workspace) : Bool :=
   ws.isRootArtifactCacheWritable
 
+/-- Whether artifacts should be restored by default from the Lake cache for packages in the workspace. -/
+@[inline] public def restoreAllArtifacts? (ws : Workspace) : Option Bool :=
+  ws.root.restoreAllArtifacts?
+
 /-- Returns the toolchain identifier for the Lake cache corresponding the workspace's toolchain. -/
 @[inline] public def cacheToolchain (ws : Workspace) : CacheToolchain :=
   ws.lakeEnv.cacheToolchain