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

[kim-em]

This PR names the cache tool's temporary files after the writing process, so two cache runs sharing one cache directory cannot write each other's curl configuration or each other's partial downloads.

The cache directory is per user rather than per checkout (~/.cache/mathlib), which is what lets a machine pool its downloads. Several runs can therefore be in flight in it at once — different projects, several worktrees of one project, or several agents on one host — and both temporary paths inside it were fixed names.

curl.cfg is written, passed to curl, and deleted. A second run overwriting it in the window before curl reads it makes the first run fetch the second's file list; the first run then reports the files it was actually asked for as missing and rebuilds them, which is a full Mathlib compile in the bad case. Whichever run finishes second also throws an uncaught removeFile on a path the first already deleted. <hash>.ltar.part is the more damaging one: two curls writing one path interleave their bytes, and whichever rename lands leaves a corrupt .ltar in the shared cache that every later run finds, trusts, and fails to decompress, until someone deletes it by hand.

Both now carry the process id, so a run only renames or removes files it wrote, and two runs fetching the same hash simply both produce a complete file and the second rename wins. Renaming and remove-on-error key off this process's own suffix rather than a bare .part for the same reason. hashFromFileName still reads an untagged <hash>.ltar.part, since a cache directory written by an earlier version may hold some, and lake exe cache-test covers all three name shapes plus the properties the download monitor relies on.

Verified against the real cache server: a single cache get downloads, renames, and leaves no temporaries behind, and two concurrent cache get- runs of the same 70-file target into one fresh cache directory both exit 0, leave 70 valid .ltar files and no .part or config leftovers, and decompress cleanly afterwards. The failure this fixes is timing-dependent, so the argument for it is the shared fixed paths rather than a deterministic reproduction.

🤖 Prepared with Claude Code

[github-actions]

PR summary 50b5b91641

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ PARTSUFFIX
+ test_tempFileNames

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 50b5b91).

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 50b5b91641
Reference commit caa4dbde35

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).