Mathlib Build

REDIRECT — Lake build content has been generalised and moved to the new `lean-build` skill (W4 Wave 2 / move A3 of lab/design/07-cluster-workflow.md). The Mathlib-specific `lake exe cache get` note survives in the new skill. This stub preserves the slug for Ctrl-F discoverability and incoming cross-references (per the zero-deletions Chesterton protocol).

r-irbe 4e648f6 2 files · 2.0 KB Updated

File contents

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

r-irbe/proof-skills/tree/main/skills/_overrides/mathlib-build commit 4e648f6ccf

Frequently asked questions

npx skillmds@latest add r-irbe/mathlib-build