chore: fix tests & old mode + job actions

src/lake/Lake/Build/Basic.lean

@@ -33,12 +33,38 @@ structure BuildConfig where
   /-- Report build output on `stdout`. Otherwise, Lake uses `stderr`. -/
   useStdout : Bool := false
 
+/-- Information on what this job did. -/
+inductive JobAction
+/-- No information about this job's action is available. -/
+| unknown
+/-- Tried to load a cached build action (set by `buildFileUnlessUpToDate`) -/
+| cache
+/-- Tried to fetch a build from a store (can be set by `buildUnlessUpToDate?`) -/
+| fetch
+/-- Tried to perform a build action (set by `buildUnlessUpToDate?`) -/
+| build
+deriving Inhabited, Repr, DecidableEq, Ord
+
+instance : LT JobAction := ltOfOrd
+instance : LE JobAction := leOfOrd
+instance : Min JobAction := minOfLe
+instance : Max JobAction := maxOfLe
+
+@[inline] def JobAction.merge (a b : JobAction) : JobAction :=
+  max a b
+
+def JobAction.verb (failed : Bool) : JobAction → String
+| .unknown => if failed then "Running" else "Ran"
+| .cache => if failed then "Revisiting" else "Revisited"
+| .fetch => if failed then "Fetching" else "Fetched"
+| .build => if failed then "Building" else "Built"
+
 /-- Mutable state of a Lake job. -/
 structure JobState where
   /-- The job's log. -/
   log : Log := {}
   /-- Tracks whether this job performed any significant build action. -/
-  built : Bool := false
+  action : JobAction := .unknown
 
 /--
 Resets the job state after a checkpoint (e.g., registering the job).
@@ -47,11 +73,11 @@ job-local state that should not be inherited by downstream jobs.
 -/
 @[inline] def JobState.renew (_ : JobState) : JobState where
   log := {}
-  built := false
+  action := .unknown
 
 def JobState.merge (a b : JobState) : JobState where
   log := a.log ++ b.log
-  built := a.built || b.built
+  action := a.action.merge b.action
 
 @[inline] def JobState.modifyLog (f : Log → Log) (s : JobState) :=
   {s with log := f s.log}
@@ -93,9 +119,9 @@ instance : MonadError JobM := ELog.monadError
 instance : Alternative JobM := ELog.alternative
 instance : MonadLift LogIO JobM := ⟨ELogT.takeAndRun⟩
 
-/-- Record that this job has performed some significant build action. -/
-@[inline] def markBuilt : JobM PUnit :=
-  modify fun s => {s with built := true}
+/-- Record that this job is trying to perform some action. -/
+@[inline] def updateAction (action : JobAction) : JobM PUnit :=
+  modify fun s => {s with action := s.action.merge action}
 
 /-- A monad equipped with a Lake build context. -/
 abbrev MonadBuild (m : Type → Type u) :=

src/lake/Lake/Build/Common.lean

@@ -24,13 +24,23 @@ and will be rebuilt on different host platforms.
 -/
 def platformTrace := pureHash System.Platform.target
 
-/-- Check if the `info` is up-to-date by comparing `depTrace` with `traceFile`. -/
+/--
+Checks if the `info` is up-to-date by comparing `depTrace` with `traceFile`.
+If old mode is enabled (e.g., `--old`), uses the modification time of `oldTrace`
+as the point of comparison instead.
+-/
 @[specialize] def BuildTrace.checkUpToDate
   [CheckExists ι] [GetMTime ι]
   (info : ι) (depTrace : BuildTrace) (traceFile : FilePath)
+  (oldTrace := depTrace)
 : JobM Bool := do
   if (← getIsOldMode) then
-    depTrace.checkAgainstTime info
+    if (← oldTrace.checkAgainstTime info) then
+      return true
+    else if let some hash ← Hash.load? traceFile then
+      depTrace.checkAgainstHash info hash
+    else
+      return false
   else
     depTrace.checkAgainstFile info traceFile
 
@@ -42,14 +52,15 @@ Returns whether `info` was already up-to-date.
 @[inline] def buildUnlessUpToDate?
   [CheckExists ι] [GetMTime ι] (info : ι)
   (depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit)
+  (action : JobAction := .build) (oldTrace := depTrace)
 : JobM Bool := do
-  if (← depTrace.checkUpToDate info traceFile) then
+  if (← depTrace.checkUpToDate info traceFile oldTrace) then
     return true
   else if (← getNoBuild) then
     IO.Process.exit noBuildCode.toUInt8
   else
+    updateAction action
     build
-    markBuilt
     depTrace.writeToFile traceFile
     return false
 
@@ -123,6 +134,7 @@ def buildFileUnlessUpToDate
   let logFile := FilePath.mk <| file.toString ++ ".log.json"
   let build := cacheBuildLog logFile build
   if (← buildUnlessUpToDate? file depTrace traceFile build) then
+    updateAction .cache
     replayBuildLog logFile
     fetchFileTrace file
   else

src/lake/Lake/Build/Module.lean

@@ -154,7 +154,7 @@ def Module.recBuildLean (mod : Module) : FetchM (BuildJob Unit) := do
     let argTrace : BuildTrace := pureHash mod.leanArgs
     let srcTrace : BuildTrace ← computeTrace { path := mod.leanFile : TextFilePath }
     let modTrace := (← getLeanTrace).mix <| argTrace.mix <| srcTrace.mix depTrace
-    let upToDate ← buildUnlessUpToDate? mod modTrace mod.traceFile do
+    let upToDate ← buildUnlessUpToDate? (oldTrace := srcTrace) mod modTrace mod.traceFile do
       let hasLLVM := Lean.Internal.hasLLVMBackend ()
       let bcFile? := if hasLLVM then some mod.bcFile else none
       cacheBuildLog mod.logFile do
@@ -166,6 +166,7 @@ def Module.recBuildLean (mod : Module) : FetchM (BuildJob Unit) := do
       if hasLLVM then
         discard <| cacheFileHash mod.bcFile
     if upToDate then
+      updateAction .cache
       replayBuildLog mod.logFile
     return ((), depTrace)
 

src/lake/Lake/Build/Package.lean

@@ -50,6 +50,7 @@ def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet :=
 
 /-- Download and unpack the package's prebuilt release archive (from GitHub). -/
 def Package.fetchOptRelease (self : Package) : FetchM (BuildJob Bool) := Job.async do
+  updateAction .fetch
   let repo := GitRepo.mk self.dir
   let repoUrl? := self.releaseRepo? <|> self.remoteUrl?
   let some repoUrl := repoUrl? <|> (← repo.getFilteredRemoteUrl?)
@@ -64,7 +65,7 @@ def Package.fetchOptRelease (self : Package) : FetchM (BuildJob Bool) := Job.asy
   let logName := s!"{self.name}/{tag}/{self.buildArchive}"
   let depTrace := Hash.ofString url
   let traceFile := FilePath.mk <| self.buildArchiveFile.toString ++ ".trace"
-  let upToDate ← buildUnlessUpToDate? self.buildArchiveFile depTrace traceFile do
+  let upToDate ← buildUnlessUpToDate? (action := .fetch) self.buildArchiveFile depTrace traceFile do
     logVerbose s!"downloading {logName}"
     download url self.buildArchiveFile
   unless upToDate && (← self.buildDir.pathExists) do

src/lake/Lake/Build/Run.lean

@@ -55,18 +55,15 @@ where
     for h : i in [0:jobs.size] do
       let job := jobs[i]'h.upper
       if (← IO.hasFinished job.task) then
-        let {log, built, ..} := (← job.wait).state
+        let {log, action, ..} := (← job.wait).state
         let maxLv := log.maxLogLevel
         let failed := !log.isEmpty ∧ maxLv ≥ failLv
         if failed then
           modify fun s => {s with failures := s.failures.push job.caption}
         let hasOutput := !log.isEmpty ∧ maxLv ≥ outLv
-        if hasOutput ∨ (showProgress ∧ built) then
+        if hasOutput ∨ (showProgress ∧ action == .build) then
+          let verb := action.verb failed
           let icon := if hasOutput then maxLv.icon else '✔'
-          let verb :=
-            if built then "Built"
-            else if failed then "Building"
-            else "Fetched"
           let jobNo := (totalJobs - jobs.size) + (i - (← get).jobs.size) + 1
           let caption := s!"{icon} [{jobNo}/{totalJobs}] {verb} {job.caption}"
           let caption :=
@@ -154,7 +151,7 @@ def Workspace.runFetchM
       out.putStr s!"Build completed successfully.\n"
     return a
   else
-    out.putStr "Some build steps logged failures:\n"
+    out.putStr "Some builds logged failures:\n"
     failures.forM (out.putStr s!"- {·}\n")
     error "build failed"
 

src/lake/examples/targets/test.sh

@@ -23,25 +23,25 @@ fi
 $LAKE build targets:noexistent && exit 1 || true
 
 # Test custom targets and package, library, and module facets
-$LAKE build bark | awk '/Building/,/Bark!/' | diff -u --strip-trailing-cr <(cat << 'EOF'
-[1/1] Building targets/bark
+$LAKE build bark | awk '/Ran/,/Bark!/' | diff -u --strip-trailing-cr <(cat << 'EOF'
+ℹ [1/1] Ran targets/bark
 info: Bark!
 EOF
 ) -
-$LAKE build targets/bark_bark | awk '/Building/,0' | diff -u --strip-trailing-cr <(cat << 'EOF'
-[1/2] Building targets/bark
+$LAKE build targets/bark_bark | awk '/Ran/,0' | diff -u --strip-trailing-cr <(cat << 'EOF'
+ℹ [1/2] Ran targets/bark
 info: Bark!
-All builds jobs completed successfully.
+Build completed successfully.
 EOF
 ) -
-$LAKE build targets:print_name | awk '/Building/,/^targets/' | diff -u --strip-trailing-cr <(cat << 'EOF'
-[1/1] Building targets:print_name
+$LAKE build targets:print_name | awk '/Ran/,/^targets/' | diff -u --strip-trailing-cr <(cat << 'EOF'
+ℹ [1/1] Ran targets:print_name
 info: stdout/stderr:
 targets
 EOF
 ) -
-$LAKE build Foo:print_name | awk '/Building/,/^Foo/' | diff -u --strip-trailing-cr <(cat << 'EOF'
-[1/1] Building targets/Foo:print_name
+$LAKE build Foo:print_name | awk '/Ran/,/^Foo/' | diff -u --strip-trailing-cr <(cat << 'EOF'
+ℹ [1/1] Ran targets/Foo:print_name
 info: stdout/stderr:
 Foo
 EOF

src/lake/tests/noRelease/test.sh

@@ -11,19 +11,19 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 
 # Test that a direct invocation fo `lake build *:release` fails
 ($LAKE build dep:release && exit 1 || true) | diff -u --strip-trailing-cr <(cat << 'EOF'
-[1/1] Fetching dep cloud release
+✖ [1/1] Fetching dep:release
 info: dep: wanted prebuilt release, but could not find an associated tag for the package's revision
 error: failed to fetch cloud release
-Some build steps logged failures:
-- Fetching dep cloud release
+Some builds logged failures:
+- dep:release
 EOF
 ) -
 
 # Test that an indirect fetch on the release does not cause the build to fail
 $LAKE build -v test:extraDep | diff -u --strip-trailing-cr <(cat << 'EOF'
-[1/1] Building test:extraDep
+⚠ [1/1] Fetched test:extraDep
 info: dep: wanted prebuilt release, but could not find an associated tag for the package's revision
 warning: failed to fetch cloud release; falling back to local build
-All builds jobs completed successfully.
+Build completed successfully.
 EOF
 ) -

src/lake/tests/old/test.sh

@@ -5,23 +5,39 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 
 ./clean.sh
 
-# Tests the `--old` option for using outdate oleans
-# See https://github.com/leanprover/lake/issues/44
+# Test the `--old` option for using outdate oleans
+# https://github.com/leanprover/lake/issues/44
+# https://github.com/leanprover/lean4/issues/2822
 
 $LAKE new hello
 $LAKE -d hello build
-sleep 0.5 # for some reason, delay needed for `--old` rebuild consistency
-echo 'def hello := "old"' > hello/Hello.lean
-$LAKE -d hello build --old | sed 's/\[.*\] //' | tee produced.out
-echo 'def hello := "normal"' > hello/Hello.lean
-$LAKE -d hello build | sed 's/\[.*\] //' | tee -a produced.out
+sleep 1 # sleep needed to guarantee modification time difference
 
-grep -i main produced.out
-grep -i hello produced.out > produced.out.tmp
-mv produced.out.tmp produced.out
-if [ "$OS" = Windows_NT ]; then
-  sed -i 's/.exe//g' produced.out
-  diff --strip-trailing-cr expected.out produced.out
-else
-  diff expected.out produced.out
-fi
+# Test basic `--old`
+echo 'def hello := "old"' > hello/Hello/Basic.lean
+$LAKE -d hello build --old | sed 's/.*\[.*\] //' | diff -u --strip-trailing-cr <(cat << 'EOF'
+Built Hello.Basic
+Built Hello.Basic:c (without exports)
+Built hello
+Build completed successfully.
+EOF
+) -
+
+# Test a normal build works after an `--old` build
+echo 'def hello := "normal"' > hello/Hello/Basic.lean
+$LAKE -d hello build | sed 's/.*\[.*\] //' | diff -u --strip-trailing-cr <(cat << 'EOF'
+Built Hello.Basic
+Built Hello
+Built Hello.Basic:c (without exports)
+Built Main
+Built hello
+Build completed successfully.
+EOF
+) -
+
+# Test that `--old` does not rebuild touched but unchanged files (lean4#2822)
+touch hello/Hello/Basic.lean
+$LAKE -d hello build --old | sed 's/.*\[.*\] //' | diff -u --strip-trailing-cr <(cat << 'EOF'
+Build completed successfully.
+EOF
+) -

tests/pkg/test_extern/expected.txt

@@ -1,4 +1,4 @@
-error: ././././TestExtern.lean:5:0-5:27: native implementation did not agree with reference implementation!
+error: ././././TestExtern.lean:5:0: native implementation did not agree with reference implementation!
 Compare the outputs of:
 #eval Nat.not_add 4 5
  and