Mathlib Build
Building Mathlib
MCP get_skill({ skillId: "mathlib-build-ab2f4500" })Use this skill with your agent
Create a free account and connect via MCP
# Building Mathlib Fetch the Mathlib olean cache before build: ```bash lake exe cache get ``` Use `lake exe cache get!` (with `!`) to force re-download if the cache appears corrupt. When building Mathlib reduce verbosity to save on tokens: ```bash lake build -q --log-level=info ``` For merge conflict resolution or small fixes build only the affected files: `lake build Mathlib.Foo.Bar -q --log-level=info`. Often it is fine to leave a complete build to CI. If you need a thorough local build, use `lake build Mathlib MathlibTest Archive Counterexamples && lake exe runLinter`.
Related Skills
More skills in Data, AI & Research
Ablation Planner
Use when main results pass result-to-claim (`claim_supported = yes` or `partial`) and ablation studies are needed for paper submission. A secondary Codex agent designs ablations from a reviewer's perspective; the local executor reviews feasibility and implements.
Ablation Planner
Use when main results pass result-to-claim (claim_supported=yes or partial) and ablation studies are needed for paper submission.
About
Provides information about the bitwize-music plugin, its version, and its creator. Use when the user asks about the plugin, its purpose, version, or capabilities.
Ab Test Analysis
Analyze A/B test results with statistical significance, sample size validation, confidence intervals, and ship/extend/stop recommendations. Use when evaluating experiment results, checking if a test reached significance, interpreting split test data, or deciding whether to ship a variant.
Academic Search
Search and analyze academic literature. Find papers, understand research methodologies, and synthesize academic findings for research projects.
Adaptyv
How to use the Adaptyv Bio Foundry API and Python SDK for protein experiment design, submission, and results retrieval. Use this skill whenever the user mentions Adaptyv, Foundry API, protein binding assays, protein screening experiments, BLI/SPR assays, thermostability assays, or wants to submit protein sequences for experimental characterization. Also trigger when code imports `adaptyv`, `adaptyv_sdk`, or `FoundryClient`, or references `foundry-api-public.adaptyvbio.com`.
Explore Other Categories
Skills from other categories with shared topics
Mathlib PR
PR conventions for leanprover-community/mathlib4. Use when creating pull requests, writing commit messages, or managing labels for Mathlib contributions.
Mathlib Review
Review guidelines for Mathlib PRs. Use when reviewing pull requests, checking code quality, or assessing whether a PR is ready to merge.
Lean Bisect
Bisect Lean toolchain versions to find where behavior changes. Use when trying to identify which Lean 4 commit caused a regression or behavior change.