[hawkrobe]

Setup now downloads only the prebuilt Mathlib files the project's imports reach, instead of all of Mathlib.

Measured (macOS, Lean already installed, empty Mathlib download cache)

	Before	--full (all of Mathlib)	This PR (default)
Project folder	about 12 GB	8.2 GB	2.2 GB
With Lean (2.7 GB in ~/.elan)	about 15 GB	about 11 GB	about 4.9 GB
Prebuilt Mathlib files	all, 6.6 GB unpacked	all, 6.6 GB unpacked	900 files, 0.73 GB unpacked
Mathlib download	448 MB	448 MB	71 MB
Setup time	about 10 min (README)	not measured from scratch	4 min, 3 of them cloning the packages

"Before" is the README's figure from when linglib's release unpacked to 3.5 GB. The --full column is what main does today, now that linglib's v4.34.1 release ships per-module archives (linglib-community/linglib#5034).

What changes

• scripts/get_mathlib.py (Python 3.8+, standard library only): follows import lines from the project's files through linglib and the other packages, and asks Mathlib's download tool for exactly the files reached. --check downloads nothing and exits 1 if any are missing.
• scripts/build.sh <target>: runs that script, then lake build. It stops before building if a needed Mathlib file is missing, so a new import cannot start an hours-long Mathlib compile.
• scripts/setup.sh: sets MATHLIB_NO_CACHE_ON_UPDATE=1, fetches the packages with a command that builds nothing (tried twice, since the Mathlib clone sometimes drops), then runs the script. --full downloads all of Mathlib as before.
• .devcontainer: the same variable for terminals, and Python from the distribution.
• AGENTS.md and README.md: build through scripts/build.sh, what to do if Mathlib starts compiling, Windows commands, new sizes and times.

Tests

• 22 unit tests for the header parsing and the import walk, run without Lean (script-tests).
• setup-script and devcontainer fail if the logs show a Mathlib or linglib file being compiled, and print the disk use.
• new-import adds a file importing Linglib.Semantics.Exhaustification.Finite, checks that --check fails first, builds it through scripts/build.sh, and checks that more Mathlib files arrived (44 locally) and nothing was compiled.
• Against linglib's source: the worked example asks for 52 Mathlib modules and needs 900 files (643 from Mathlib); all of linglib needs 3,650 Mathlib modules.

Not tested: Windows, and the dev container locally (no Docker here; the CI job covers it).