mathlib-build
Building Mathlib
Datos de origen
- Repositorio
- leanprover/skills
- Última actividad en el origen
- 20 de febrero de 2026 a las 12:34
- Idioma detectado de SKILL.md
- inglés
- Estrellas
- 72
- Forks
- 2
Opciones de instalación
De forma predeterminada está seleccionado el prompt que primero revisa el origen. Puedes cambiar a un comando directo o descargar una copia local.
Revisa los archivos de origen
Lee SKILL.md y los archivos complementarios que muestra SkillsMP antes de decidir si quieres instalarlo.
Mostrando SKILL.md
SKILL.md
Instrucciones de origen · Vista previa de solo lectura- name
- mathlib-build
- description
- Building Mathlib
# 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`.
Ver en GitHub