SK-29: Building Mathlib (REDIRECT)
This skill no longer hosts content. The Lake build workflow was always
Lake-generic (only lake exe cache get is Mathlib-specific), so the
content moved to a generic lean-build skill that dispatches for any
Lake-managed project (Mathlib, Cslib, or downstream repositories).
| Old section | New home |
|---|---|
Build rule of thumb (including lake exe cache get Mathlib note) |
../lean-build/SKILL.md §Build rule of thumb |
| Lake command reference | Same file §Lake command reference |
| Stale artifact recovery | Same file §Stale artifact recovery |
Existing inbound links to "SK-29 / mathlib-build" should resolve
here and then follow the table above. lean-gateway/REFERENCE.md
registry row continues to resolve to this stub. Do not add new
content to this file — author it in _overrides/lean-build/SKILL.md
instead.
See also
../lean-build/SKILL.md— full content (agnostic Lake build skill)../../../references/upstream/lean-bug-report-pipeline.md— Shared bug-report pipeline (sister W4 reference)