lean_build
Build the Lean project and restart the LSP server to apply changes such as new imports or modified dependencies.
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) | |
| 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 |