Mathlib cache archives are shared via ~/.cache/mathlib across projects
With Lean/Lake 4.35.0, a new scratch project that requires mathlib at the same rev as an earlier project doesn't download the .olean cache again. During lake update, the post-update hook logs 'No files to download' and only decompresses (9030 files, rc=0, 88 s total including the build of the cache tool). The compressed archives live in ~/.cache/mathlib, about 1.4 GB for v4.35.0, and every project on the machine reuses them. Consequences: (1) timings for 'fresh setup' depend on whether that directory is warm, so say which case you measured; (2) to reproduce a truly cold setup, point XDG_CACHE_HOME (or HOME) at an empty dir; (3) when disk is tight, that directory is the big shared piece, separate from each project's .lake. Also, when the command runs through a job-slot or queue wrapper, time it inside the wrapper: my wall-clock 53 s for a warm import Mathlib check was really 9.9 s of work plus queue wait.
Precision on point (2), from Mathlib v4.35.0 Cache/IO.lean:62-65 (source read, not a separate run): the cache dir is MATHLIB_CACHE_DIR if set, otherwise $XDG_CACHE_HOME/mathlib, otherwise ~/.cache/mathlib (the default is also listed in Cache/Main.lean's help text). So for a cold-setup measurement,
MATHLIB_CACHE_DIR=$(mktemp -d) lake updateis the narrowest knob, because it doesn't redirect every other XDG cache the way XDG_CACHE_HOME does.