fix(Cache): give each cache process its own temporary file names

Cache/IO.lean

@@ -69,9 +69,31 @@ initialize CACHEDIR : FilePath ← do
       | some path => return path / ".cache" / "mathlib"
       | none => pure ⟨".cache"⟩
 
-/-- Target file path for `curl` configurations -/
+/--
+A tag unique to this `cache` process, mixed into the names of every temporary file it writes into
+`CACHEDIR`.
+
+`CACHEDIR` is shared by design: it defaults to one directory per user
+(`~/.cache/mathlib`), so every checkout, worktree, and CI job on a machine pools its
+downloads there. Two `cache` runs can therefore be in flight in it at once, and until
+they were tagged they wrote each other's files — one run's `curl.cfg` overwritten by the
+other's before curl read it (so it fetched the wrong list, then reported the files it was
+actually asked for as missing and rebuilt them), and, worse, two curls writing one
+`<hash>.ltar.part` and renaming the interleaved result into place, leaving a corrupt
+`.ltar` that every later run would find, trust, and fail to decompress.
+-/
+initialize PROCTAG : String ← toString <$> IO.Process.getPID
+
+/-- Target file path for `curl` configurations. One per process; see `PROCTAG`. -/
 def CURLCFG :=
-  IO.CACHEDIR / "curl.cfg"
+  IO.CACHEDIR / s!"curl-{PROCTAG}.cfg"
+
+/--
+Suffix for a download still in flight, before it is renamed to `<hash>.ltar`. One per process; see
+`PROCTAG`.
+-/
+def PARTSUFFIX :=
+  s!".{PROCTAG}.part"
 
 /-- curl version at https://github.com/leanprover-community/static-curl -/
 def CURLVERSION :=

Cache/README.md

@@ -298,6 +298,11 @@ If your system curl is too old, a static binary is downloaded automatically on L
 |-----------------------------|------------------------------|
 | `~/.cache/mathlib/`         | Default cache directory      |
 | `~/.cache/mathlib/*.ltar`   | Cached build artifacts       |
-| `~/.cache/mathlib/curl.cfg` | Temporary curl configuration |
+| `~/.cache/mathlib/*.ltar.<pid>.part` | Downloads in flight, renamed on success |
+| `~/.cache/mathlib/curl-<pid>.cfg` | Temporary curl configuration |
+
+The cache directory is per user, not per checkout, so several `cache` runs can be
+in flight in it at once. Everything temporary is therefore named with the writing
+process's id, and one run only ever renames or removes its own files.
 | `.lake/build/lib/lean/`     | Unpacked `.olean` files      |
 | `.lake/build/ir/`           | Unpacked `.c` files          |

Cache/Requests.lean

@@ -409,10 +409,11 @@ def mkGetConfigContent (container : Option Container) (repo containerURL : Strin
     -- ```
     -- If this becomes an issue we can implement the curl spec.
 
-    -- Note we append a '.part' to the filenames here,
-    -- which `downloadFiles` then removes when the download is successful.
+    -- Note we append `IO.PARTSUFFIX` to the filenames here, which `downloadFiles` then
+    -- removes when the download is successful. The suffix carries this process's tag, so a
+    -- concurrent `cache` run sharing this `CACHEDIR` writes its own in-flight files, not ours.
     pure <| acc ++ s!"url = {mkFileURL container repo containerURL fileName scope?}\n\
-      -o {(IO.CACHEDIR / (fileName ++ ".part")).toString.quote}\n"
+      -o {(IO.CACHEDIR / (fileName ++ IO.PARTSUFFIX)).toString.quote}\n"
 
 /--
 Whether an HTTP status returned for a single-file read should be treated as a
@@ -448,7 +449,7 @@ def downloadFile (container : Option Container) (repo containerURL : String)
   let fileName := hash.asLTar
   let url := mkFileURL container repo containerURL fileName scope?
   let path := IO.CACHEDIR / fileName
-  let partFileName := fileName ++ ".part"
+  let partFileName := fileName ++ IO.PARTSUFFIX
   let partPath := IO.CACHEDIR / partFileName
   let out ← IO.Process.output
     { cmd := (← IO.getCurl),
@@ -464,12 +465,14 @@ def downloadFile (container : Option Container) (repo containerURL : String)
   return if isCacheMissStatus httpCode treatForbiddenAsMiss then .miss else .failed
 
 /-- Extract hash from filename (e.g., "/path/to/.cache/00012345.ltar" → 0x12345).
-    Handles both `.ltar` and `.ltar.part` files using `FilePath.fileStem`. -/
-def hashFromFileName (path : FilePath) : Option UInt64 := do
-  let some stem := path.fileStem | .none
-  -- For .ltar.part files, fileStem gives "hash.ltar"; apply fileStem again to strip .ltar
-  let stem := (FilePath.mk (toString stem)).fileStem.getD stem
-  (toString stem).parseHexToUInt64?
+    Handles a finished `<hash>.ltar`, an in-flight `<hash>.ltar<PARTSUFFIX>`, and a
+    `<hash>.ltar.part` left in the cache by a version that wrote untagged temporaries. -/
+def hashFromFileName (path : FilePath) : Option UInt64 :=
+  let peel (name : String) := (FilePath.mk name).fileStem.getD name
+  let name := path.fileName.getD path.toString
+  -- Peel one extension at a time — `.part`, this process's tag, `.ltar` — and take the first stem
+  -- that parses as a hash, so all three shapes above resolve without knowing which one this is.
+  [name, peel name, peel (peel name), peel (peel (peel name))].findSome? String.parseHexToUInt64?
 
 /-- Decompress a batch of files using a single leantar invocation -/
 def decompressBatch (files : Array (FilePath × Lean.Name))
@@ -611,8 +614,10 @@ def monitorCurl (args : Array String) (size : Nat)
         | .ok 200
         | .ok 201 =>
           if let .ok fn := result.getObjValAs? String "filename_effective" then
-            if (← System.FilePath.pathExists fn) && fn.endsWith ".part" then
-              let finalPath := (fn.dropEnd 5).copy
+            -- Match this process's own suffix, not a bare `.part`: a concurrent run's
+            -- in-flight file is not ours to rename, and curl only reports our transfers.
+            if (← System.FilePath.pathExists fn) && fn.endsWith IO.PARTSUFFIX then
+              let finalPath := (fn.dropEnd IO.PARTSUFFIX.length).copy
               IO.FS.rename fn finalPath
               let hash? := hashFromFileName finalPath
               if let some hash := hash? then servedRef.modify (·.insert hash)

Cache/Test.lean

@@ -382,26 +382,57 @@ end ExtractPRNumber
 section HashFromFileName
 
 /-- Recovers the UInt64 cache hash from a cached file's path, the inverse of
-`UInt64.asLTar`. The subtle case is `.ltar.part` — the suffix curl writes during
-a download — where `.part` must be stripped before `.ltar`. A regression here
-corrupts cache lookups, so both suffixes and a non-hex stem are covered. -/
+`UInt64.asLTar`. The subtle cases are the in-flight suffixes curl writes during a
+download: today's process-tagged `.ltar.<pid>.part` (see `IO.PARTSUFFIX`) and the
+untagged `.ltar.part` a cache from before tagging may have left in the shared
+directory. A regression here corrupts cache lookups, so every suffix and a
+non-hex stem are covered. -/
 def test_hashFromFileName : IO Unit := do
   IO.println "hashFromFileName:"
   assertTrue "plain .ltar file"
     (hashFromFileName "abc123def.ltar" == String.parseHexToUInt64? "000000abc123def")
-  assertTrue "in-flight .ltar.part file strips both suffixes"
+  assertTrue "in-flight process-tagged .part file strips all three suffixes"
+    (hashFromFileName "abc123def.ltar.31415.part" == String.parseHexToUInt64? "000000abc123def")
+  assertTrue "legacy untagged .ltar.part file strips both suffixes"
     (hashFromFileName "abc123def.ltar.part" == String.parseHexToUInt64? "000000abc123def")
+  assertTrue "the tag this process actually writes round-trips"
+    (hashFromFileName ("abc123def.ltar" ++ IO.PARTSUFFIX) ==
+      String.parseHexToUInt64? "000000abc123def")
   assertTrue "full 16-digit hex stem"
     (hashFromFileName "deadbeef00112233.ltar" == String.parseHexToUInt64? "deadbeef00112233")
   -- A non-hex stem returns none rather than a garbage hash.
   assertTrue "non-hex stem returns none"
     (hashFromFileName "nothexa.ltar" == none)
+  assertTrue "non-hex stem returns none for a tagged part file too"
+    (hashFromFileName "nothexa.ltar.31415.part" == none)
   -- Directory components are ignored; only the basename's stem is parsed.
   assertTrue "leading path is ignored"
     (hashFromFileName "/path/to/abc123def.ltar" == String.parseHexToUInt64? "000000abc123def")
 
 end HashFromFileName
 
+section TempFileNames
+
+/-- Every temporary file `cache` writes into the shared `CACHEDIR` carries this process's
+tag, so two runs in flight in one cache directory cannot write each other's curl
+configuration or each other's partial downloads. The `.part` ending is load-bearing
+beyond uniqueness: the download monitor keys both its rename-on-success and its
+remove-on-error off it. -/
+def test_tempFileNames : IO Unit := do
+  IO.println "temporary file names:"
+  assertTrue "the process tag is non-empty" (!IO.PROCTAG.isEmpty)
+  assertTrue "the in-flight suffix still ends in .part" (IO.PARTSUFFIX.endsWith ".part")
+  assertTrue "the in-flight suffix is tagged, not a bare .part" (IO.PARTSUFFIX != ".part")
+  assertTrue "the in-flight suffix carries the tag" ((IO.PARTSUFFIX.splitOn IO.PROCTAG).length == 2)
+  assertTrue "the curl config carries the tag"
+    ((IO.CURLCFG.toString.splitOn IO.PROCTAG).length == 2)
+  assertTrue "the curl config sits in the cache directory"
+    (IO.CURLCFG.parent == some IO.CACHEDIR)
+  -- The tag must not reintroduce a path separator or a shell/curl-config hazard.
+  assertTrue "the tag is a bare identifier" (IO.PROCTAG.all fun c => c.isAlphanum)
+
+end TempFileNames
+
 section IsRemoteURL
 
 /-- Discriminator: is this string a remote URL (vs a local filesystem path)?
@@ -1062,6 +1093,7 @@ def runAll : IO Unit := do
   test_extractRepoFromUrl
   test_extractPRNumber
   test_hashFromFileName
+  test_tempFileNames
   test_isRemoteURL
   test_UInt64_asLTar
   test_hash_roundtrip