# Lean Build

> Build, test, and debug Lean 4 projects using Lake. Use when building the ComputationalPaths project, checking for errors, running tests, cleaning artifacts, or debugging Lean 4 compilation issues. Use when this capability is needed.

- Skill: `tomevault-io/lean-build` (Agent Skill, multi-file: 2 files)
- Install (CLI): `npx skillmds@latest add tomevault-io/lean-build`
- Raw SKILL.md: https://api.skillmd.com/api/skills/tomevault-io/lean-build/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Coding & Dev Tools
- Author: tomevault-io (https://skillmd.com/u/tomevault-io)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/tomevault-io/lean-build

---


# Lean 4 Build & Debug

Build the ComputationalPaths Lean 4 project using Lake.

## Essential Commands

```bash
# Build entire project
lake build

# Build specific module
lake build ComputationalPaths.Path.CompPath.CircleCompPath

# Clean and rebuild
lake clean && lake build

# Run executable
lake exe computational_paths
```

## Common Build Errors

| Error | Solution |
|-------|----------|
| `unknown identifier` | Check imports, use fully qualified name |
| `type mismatch` | Add type annotations or use `@` for explicit args |
| `must be marked as 'noncomputable'` | Add `noncomputable` keyword |
| `universe level mismatch` | Ensure consistent universe variables (typically `Type u`) |

## Debugging

```lean
#check myTerm             -- show type
#print axioms myTheorem   -- show axioms used
#reduce myTerm            -- fully normalize
```

## Toolchain

- Current: `leanprover/lean4:v4.24.0` (see `lean-toolchain`)
- Update: edit `lean-toolchain`, then `lake clean && lake build`

---
> Converted and distributed by [TomeVault](https://tomevault.io/claim/arthur742ramos) — claim your Tome and manage your conversions.
<!-- tomevault:4.0:skill_md:2026-04-15 -->