lean_build
Build Lean projects and restart the Language Server Protocol when new imports or dependencies require compilation updates.
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) |