PR comments

Author: marcelolynch

.github/workflows/build_template.yml

@@ -424,7 +424,7 @@ jobs:
         if: ${{ steps.build.outcome == 'success' }}
         shell: bash
         run: |
-          if find cache-staging -type f -name '*.ltar' -print -quit | grep -q .; then
+          if find cache-staging -type f -name '*.ltar' -print -quit | grep -q .;
             echo "has_files=true" >> "$GITHUB_OUTPUT"
           else
             echo "has_files=false" >> "$GITHUB_OUTPUT"
@@ -437,17 +437,6 @@ jobs:
           name: cache-staging
           path: cache-staging/
 
-      # - name: upload artifact containing contents of pr-branch
-      #   # TODO: We should probably only upload the artifacts needed by the cache
-      #   uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0
-      #   with:
-      #     name: mathlib4_artifact
-      #     include-hidden-files: true
-      #     # we exclude .git since there may be secrets in there
-      #     path: |
-      #       pr-branch/
-      #       !pr-branch/.git/
-
       - name: Check if building Archive or Counterexamples failed
         if: steps.archive.outcome == 'failure' || steps.counterexamples.outcome == 'failure'
         run: |
@@ -639,7 +628,7 @@ jobs:
           echo "CACHE_BIN=$CACHE_BIN" >> "$GITHUB_ENV"
 
       - name: Download cache staging artifact
-        uses: actions/download-artifact@v4
+        uses: actions/download-artifact@@37930b1c2abaa49bbe596cd826c3c89aef350131 # v7.0.0
         with:
           name: cache-staging
           path: cache-staging

Cache/Requests.lean

@@ -561,7 +561,7 @@ end Put
 section Stage
 def copyCmd : String := if System.Platform.isWindows then "COPY" else "cp"
 
-/-- Moves cached files to a directory, intended for 'staging' -/
+/-- Copies cached files to a directory, intended for 'staging' -/
 def stageFiles
   (destinationPath : String) (fileNames : Array String)
   : IO Unit := do
@@ -570,7 +570,7 @@ def stageFiles
     IO.FS.createDirAll destinationPath
     let paths := fileNames.map (fun (f : String) => s!"{(IO.CACHEDIR / f)}")
     let args := paths ++ #[destinationPath]
-    IO.println s!"Moving to {size} file(s) to {destinationPath}"
+    IO.println s!"Copying {size} file(s) to {destinationPath}"
     discard <| IO.runCmd copyCmd args
   else IO.println "No files to stage"