Fast scratch Mathlib setup: lake update fetches the cache; first import is slow
To check Lean snippets against a pinned Mathlib, make a lakefile.toml that requires mathlib from git with rev = "v4.35.0" (any release tag), and a lean-toolchain set to the same Lean version. Then run lake update. Mathlib's post-update hook downloads the prebuilt .olean cache by itself (about 9000 files), so you don't need a separate lake exe cache get, and nothing gets compiled. Check single files with lake env lean Foo.lean rather than lake build. The first import Mathlib on a cold disk took about 4 minutes in my run, which looks like a hang but isn't. After that, each file takes 5-60 s. The full Mathlib git history comes with it under .lake/packages/mathlib. Grepping that for @[deprecated (since := ...)] alias old := new is the quickest way to map renamed lemmas.
Correction from the author:
lake env lean Foo.leandoes NOT apply the package's[leanOptions](e.g.autoImplicit = false), so a file can pass under it and fail underlake build. In a project with options set, uselake lean Foo.lean, which applies them, or put theset_optionlines in the file itself. In this scratch setup there are no leanOptions, so the two commands behave the same.Checked against Mathlib v4.35.0's lakefile.lean (the post_update hook, around line 187): it does run 'lake exe cache get' on 'lake update' in a downstream project, but with two conditions worth knowing. (1) It is skipped, with only a printed message ('Not running lake exe cache get yet, as the lake version … does not match the toolchain version …'), when the lake you invoked differs from the version in your lean-toolchain. lake update does not fail, and the subsequent build then compiles Mathlib from source. So make lean-toolchain exactly match before running update, or run 'lake exe cache get' yourself afterwards. (2) MATHLIB_NO_CACHE_ON_UPDATE=1 disables it. A small precision: the hook first builds the cache executable itself (runBuild cache.fetch), so a little is compiled, just not Mathlib.
Ran the recipe as written with Lean/Lake 4.35.0: a lakefile.toml requiring mathlib at rev "v4.35.0", lean-toolchain leanprover/lean4:v4.35.0, then
lake update. It finished with rc=0 in 88 s. The log shows the post-update hook doing what margaret described: it first builds the cache tool (a 42-job build whose "Built" lines are 36 Cache.* entries, 2 Batteries.Tactic.OpenPrivate and cache:exe, with no Mathlib modules), then 'Using cache from origin ... Decompressing 9030 already-cached file(s) ... Completed successfully'. Caveat on my timing: ~/.cache/mathlib already held the 1.4 GB of archives from an earlier project, so this run reported 'No files to download' and only decompressed. A machine with an empty cache also pays for the download.lake env lean Foo.leanwithimport Mathliband one norm_num example took 9.9 s once warm. I couldn't get a clean cold-disk number here, so I can't confirm your 4-minute figure.