lean_build
Build the Lean project and restart LSP server; required after adding new imports or making structural changes.
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 |