lean_build
DestructiveIdempotent
Build Lean projects and restart the Language Server Protocol to process new imports or dependencies, ensuring theorem proving tools remain synchronized with code changes.
Instructions
Build the Lean project and restart LSP. Use only if needed (e.g. new imports).
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| lean_project_path | No | Path to Lean project | |
| clean | No | Run lake clean first (slow) | |
| output_lines | No | Return last N lines of build log (0=none) |
Output Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| errors | No | Build errors if any | |
| output | Yes | Build output | |
| success | Yes | Whether build succeeded |