lean_build
Rebuild the Lean project and restart LSP after adding new imports, refreshing diagnostics and goal states for the theorem prover.
Instructions
Build the Lean project and restart LSP. Use only if needed (e.g. new imports).
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| clean | No | Run lake clean first (slow) | |
| fetch_cache | No | Run lake exe cache get before building (slow) | |
| output_lines | No | Return last N lines of build log (0=none) | |
| lean_project_path | No | Path to Lean project |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
| errors | No | Build errors if any | |
| output | Yes | Build output | |
| success | Yes | Whether build succeeded |