feat: lake: use trace mtime for arts when possible

src/lake/Lake/Build/Common.lean

@@ -227,13 +227,15 @@ Checks if the `info` is up-to-date by comparing `depTrace` with `depHash`.
 If old mode is enabled (e.g., `--old`), uses the `oldTrace` modification time
 as the point of comparison instead.
 -/
-@[inline] public def checkHashUpToDate
+@[inline, deprecated "Deprecated without replacement." (since := "2025-03-04")]
+public def checkHashUpToDate
   [CheckExists ι] [GetMTime ι]
   (info : ι) (depTrace : BuildTrace) (depHash : Option Hash)
   (oldTrace := depTrace.mtime)
 : JobM Bool := (·.isUpToDate) <$> checkHashUpToDate' info depTrace depHash oldTrace
 
 /--
+**Ror internal use only.**
 Checks whether `info` is up-to-date with the trace.
 If so, replays the log of the trace if available.
 -/
@@ -265,7 +267,7 @@ If so, replays the log of the trace if available.
 : JobM Bool := (·.isUpToDate) <$> savedTrace.replayIfUpToDate' info depTrace oldTrace
 
 /--
-Returns if the saved trace exists and its hash matches `inputHash`.
+Returns `true` if the saved trace exists and its hash matches `inputHash`.
 
 If up-to-date, replays the saved log from the trace and sets the current
 build action to `replay`. Otherwise, if the log is empty and trace is synthetic,
@@ -540,36 +542,35 @@ public def resolveArtifact
 : JobM Artifact := do
   let ws ← getWorkspace
   let path := ws.lakeCache.artifactDir / descr.relPath
-  if let some art ← computeArtifact? descr path then
-    return art
-  else if let some service := service? then
-    if let some service := ws.findCacheService? service.toString then
-      let some scope := scope?
-        | error s!"artifact with associated cache service but no scope"
-      let url := service.artifactUrl descr.hash scope
-      logVerbose s!"\
-        downloaded artifact {descr.hash}\
-        \n  local path: {path}\
-        \n  remote URL: {url}"
-      liftM <| downloadArtifactCore descr.hash url path
-      let r := {read := true, write := false, execution := exe}
-      if let .error e ← IO.setAccessRights path ⟨r, r, r⟩ |>.toBaseIO then
-        logWarning s!"could not mark downloaded artifact read-only: {e}"
-      let some art ← computeArtifact? descr path
-        | error s!"downloaded succeeded, but artifact failed to resolve:\n  {path}"
-      return art
-    else
-      error s!"artifact cache service is not configured: {service}"
-  else
-    error s!"artifact not found in cache:\n  {path}"
-where
-  computeArtifact? descr path : BaseIO (Option Artifact) := do
-    if let .ok mtime ← getMTime path |>.toBaseIO then
-      return some {descr, path, mtime}
-    else if (← path.pathExists) then
-      return some {descr, path, mtime := 0}
+  match (← getMTime path |>.toBaseIO) with
+  | .ok mtime =>
+    return {descr, path, mtime}
+  | .error (.noFileOrDirectory ..) =>
+    -- we redownload artifacts on any error
+    if let some service := service? then
+      if let some service := ws.findCacheService? service.toString then
+        let some scope := scope?
+          | error s!"artifact with associated cache service but no scope"
+        let url := service.artifactUrl descr.hash scope
+        logVerbose s!"\
+          downloaded artifact {descr.hash}\
+          \n  local path: {path}\
+          \n  remote URL: {url}"
+        liftM <| downloadArtifactCore descr.hash url path
+        let r := {read := true, write := false, execution := exe}
+        if let .error e ← IO.setAccessRights path ⟨r, r, r⟩ |>.toBaseIO then
+          logWarning s!"could not mark downloaded artifact read-only: {e}"
+        match (← getMTime path |>.toBaseIO) with
+        | .ok mtime =>
+          return {descr, path, mtime}
+        | .error e =>
+          error s!"downloaded succeeded, but artifact failed to resolve: {e}"
+      else
+        error s!"artifact cache service is not configured: {service}"
     else
-      return none
+      error s!"artifact not found in cache:\n  {path}"
+  | .error e =>
+    error s!"failed to retrieve artifact from cache: {e}"
 
 def resolveArtifactOutput
   (out : Json) (service? : Option CacheServiceName) (scope? : Option CacheServiceScope)
@@ -676,15 +677,15 @@ public def buildArtifactUnlessUpToDate
     if let some outputsRef := pkg.outputsRef? then
       outputsRef.insert inputHash art.descr
     setTrace art.trace
-    return art
+    setMTime art traceFile
   else
     let art ←
       if (← savedTrace.replayIfUpToDate file depTrace) then
         computeArtifact file ext text
       else
         doBuild depTrace traceFile
     setTrace art.trace
-    return art
+    setMTime art traceFile
 where
   doBuild depTrace traceFile :=
     inline <| buildAction depTrace traceFile do
@@ -693,6 +694,14 @@ where
       clearFileHash file
       removeFileIfExists traceFile
       computeArtifact file ext text
+  setMTime art traceFile := do
+    match (← getMTime traceFile |>.toBaseIO) with
+    | .ok mtime =>
+      return {art with mtime}
+    | .error (.noFileOrDirectory ..) => -- trace file may not exist
+      return art
+    | .error e =>
+      error s!"failed to retrieve artifact modification time: {e}"
 
 /--
 Build `file` using `build` after `dep` completes if the dependency's

src/lake/Lake/Build/Module.lean

@@ -668,6 +668,49 @@ private def Module.restoreAllArtifacts (mod : Module) (cached : ModuleOutputArti
 where
   @[inline] restoreSome file art? := art?.mapM (restoreArtifact file ·)
 
+public protected def Module.checkExists (self : Module) (isModule : Bool) : BaseIO Bool := do
+  unless (← self.oleanFile.pathExists) do return false
+  unless (← self.ileanFile.pathExists) do return false
+  unless (← self.cFile.pathExists) do return false
+  if Lean.Internal.hasLLVMBackend () then
+    unless (← self.bcFile.pathExists) do return false
+  if isModule then
+    unless (← self.oleanServerFile.pathExists) do return false
+    unless (← self.oleanPrivateFile.pathExists) do return false
+    unless (← self.irFile.pathExists) do return false
+  return true
+
+@[deprecated Module.checkExists (since := "2025-03-04")]
+public instance : CheckExists Module := ⟨Module.checkExists (isModule := false)⟩
+
+public protected def Module.getMTime (self : Module) (isModule : Bool) : IO MTime := do
+  let mut mtime :=
+    (← getMTime self.oleanFile)
+    |> max (← getMTime self.ileanFile)
+    |> max (← getMTime self.cFile)
+  if Lean.Internal.hasLLVMBackend () then
+    mtime := max mtime (← getMTime self.bcFile)
+  if isModule then
+    mtime := mtime
+    |> max (← getMTime self.oleanServerFile)
+    |> max (← getMTime self.oleanPrivateFile)
+    |> max (← getMTime self.irFile)
+  return mtime
+
+@[deprecated Module.getMTime (since := "2025-03-04")]
+public instance : GetMTime Module := ⟨Module.getMTime (isModule := false)⟩
+
+private def ModuleOutputArtifacts.setMTime (self : ModuleOutputArtifacts) (mtime : MTime) : ModuleOutputArtifacts :=
+  {self with
+    olean := {self.olean with mtime}
+    oleanServer? := self.oleanServer?.map ({· with mtime})
+    oleanPrivate? := self.oleanPrivate?.map ({· with mtime})
+    ilean := {self.ilean with mtime}
+    ir? := self.ir?.map ({· with mtime})
+    c := {self.c with mtime}
+    bc? := self.bc?.map ({· with mtime})
+  }
+
 
 private def Module.mkArtifacts (mod : Module) (srcFile : FilePath) (isModule : Bool) : ModuleArtifacts where
   lean? := srcFile
@@ -746,6 +789,8 @@ private def Module.recBuildLean (mod : Module) : FetchM (Job ModuleOutputArtifac
     let depTrace ← getTrace
     let inputHash := depTrace.hash
     let savedTrace ← readTraceFile mod.traceFile
+    have : CheckExists Module := ⟨Module.checkExists (isModule := setup.isModule)⟩
+    have : GetMTime Module := ⟨Module.getMTime (isModule := setup.isModule)⟩
     let fetchArtsFromCache? restoreAll := do
       let some arts ← getArtifacts? inputHash savedTrace mod.pkg
         | return none
@@ -779,7 +824,13 @@ private def Module.recBuildLean (mod : Module) : FetchM (Job ModuleOutputArtifac
         mod.buildLean depTrace srcFile setup
     if let some ref := mod.pkg.outputsRef? then
       ref.insert inputHash arts.descrs
-    return arts
+    match (← getMTime mod.traceFile |>.toBaseIO) with
+    | .ok mtime =>
+      return arts.setMTime mtime
+    | .error (.noFileOrDirectory ..) => -- trace file may not exist
+      return arts
+    | .error e =>
+      error s!"failed to retrieve module artifact modification time: {e}"
 
 /-- The `ModuleFacetConfig` for the builtin `leanArtsFacet`. -/
 public def Module.leanArtsFacetConfig : ModuleFacetConfig leanArtsFacet :=

src/lake/Lake/Config/Artifact.lean

@@ -75,7 +75,7 @@ public structure Artifact extends descr : ArtifactDescr where
   path : FilePath
   /-- The artifact's. This is used, for example, as a caption in traces. -/
   name := path.toString
-  /-- The artifact's modification time (or `0` if unknown). -/
+  /-- The artifact's modification time. -/
   mtime : MTime
   deriving Inhabited, Repr
 

src/lake/Lake/Config/Cache.lean

@@ -351,26 +351,29 @@ namespace Cache
   cache.artifactDir / artifactPath contentHash ext
 
 /-- Returns the artifact in the Lake cache corresponding the given artifact description. -/
+@[deprecated "Deprecated without replacelement." (since := "2025-03-04")]
 public def getArtifact? (cache : Cache) (descr : ArtifactDescr) : BaseIO (Option Artifact) := do
   let path := cache.artifactDir / descr.relPath
-  if let .ok mtime ← getMTime path |>.toBaseIO then
-    return some {descr, path, mtime}
-  else if (← path.pathExists) then
-    return some {descr, path, mtime := 0}
-  else
-    return none
+  let .ok mtime ← getMTime path |>.toBaseIO
+    | return none
+  return some {descr, path, mtime}
 
 /-- Returns the artifact in the Lake cache corresponding the given artifact description. Errors if missing. -/
+@[deprecated "Deprecated without replacelement." (since := "2025-03-04")]
 public def getArtifact (cache : Cache) (descr : ArtifactDescr) : EIO String Artifact := do
   let path := cache.artifactDir / descr.relPath
-  if let .ok mtime ← getMTime path |>.toBaseIO then
+  match (← getMTime path |>.toBaseIO) with
+  | .ok mtime =>
     return {descr, path, mtime}
-  else if (← path.pathExists) then
-    return {descr, path, mtime := 0}
-  else
+  | .error (.noFileOrDirectory ..) =>
     error s!"artifact not found in cache: {path}"
+  | .error e =>
+    error s!"failed to retrieve artifact from cache: {e}"
 
-/-- Returns path to the artifact for each output. Errors if any are missing. -/
+/--
+**For internal use only.**
+Returns path to the artifact for each output. Errors if any are missing.
+-/
 public def getArtifactPaths
   (cache : Cache) (descrs : Array ArtifactDescr)
 : LogIO (Vector FilePath descrs.size) := throwIfLogs do

src/lake/Lake/Config/Module.lean

@@ -199,20 +199,3 @@ public def dynlibSuffix := "-1"
 
 @[inline] public def nativeFacets (self : Module) (shouldExport : Bool) : Array (ModuleFacet FilePath) :=
   self.lib.nativeFacets shouldExport
-
-/-! ## Trace Helpers -/
-
-public protected def getMTime (self : Module) : IO MTime := do
-  return mixTrace (mixTrace (← getMTime self.oleanFile) (← getMTime self.ileanFile)) (← getMTime self.cFile)
-
-public instance : GetMTime Module := ⟨Module.getMTime⟩
-
-public protected def checkExists (self : Module) : BaseIO Bool := do
-  let bcFileExists? ←
-    if Lean.Internal.hasLLVMBackend () then
-      checkExists self.bcFile
-    else
-      pure true
-  return (← checkExists self.oleanFile) && (← checkExists self.ileanFile) && (← checkExists self.cFile) && bcFileExists?
-
-public instance : CheckExists Module := ⟨Module.checkExists⟩

src/lake/Lake/Config/Monad.lean

@@ -166,24 +166,28 @@ public def getLeanArgs : m (Array String) :=
 @[inline] public def getLakeCache : m Cache :=
   (·.lakeCache) <$> getWorkspace
 
-@[inline, inherit_doc Cache.getArtifact?]
+set_option linter.deprecated false in
+@[inline, inherit_doc Cache.getArtifact?,
+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 store its artifacts in the Lake artifact cache.
+Returns whether the package should retrieve 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.
+If not configured at all, this defaults to {lean}`true`.
 -/
 @[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.
+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.
+If not configured at all, this defaults to {lean}`false`.
 -/
 @[inline] public def Package.isArtifactCacheWritable [MonadWorkspace m] (self : Package) : m Bool :=
   (self.enableArtifactCache? <|> ·.enableArtifactCache? |>.getD false) <$> getWorkspace