lean-beam

# Lean Beam Use this skill for Lean projects when you want the AI to replace repeated inner-loop `lake build` runs with cheap speculative Lean probes, optional follow-up handle execution, and targeted file checkpoints. A successful checkpoint is normally enough for local development. CI should run a clean `lake build`; do not force an expensive clean local rebuild after every checkpoint. Before calling work batch-validated, require a successful clean CI build, or run one clean local build when no such CI result is available or server-sensitive elaboration is suspected. This is the Lean-only skill. It should stay focused on Lean and should not require Rocq setup or Rocq concepts. Do not factor shared Lean/Rocq skill instructions into a common helper; duplicate short guidance if both skills need it. ## Setup From the `lean-beam` repo root: ```bash ./scripts/install-beam.sh --codex ``` Use `--claude`, `--pi`, `--opencode`, or `--vibe` instead when installing for Claude Code, Pi Agent, OpenCode, or Mistral Vibe. Use `--all-skills` when you want every supported agent skill target. The installer puts `lean-beam`, `lean-beam-search`, and `lean-beam-mcp` in `~/.local/bin`, stages the self-contained runtime under `BEAM_INSTALL_ROOT` (default `~/.local/share/beam`), requires `elan` on `PATH`, prebuilds the pinned `lean-toolchain` bundle by default, and installs the bundled Lean skill only for the agent flags you request. Use the setup docs for additional supported or custom toolchain prebuilds. Use `lean-beam --version` for CLI bug reports and installed runtime identity checks. Use `lean-beam-mcp --version` to verify which installed MCP server wrapper, server binary, runtime payload hash, manifest, and source commit a client command resolves. Source checkout runs also report git commit/branch/dirty state when available. From a live MCP session, call `beam_version` to report the running server process identity as structured content. Installed identities include `runtime_current`; if a live session reports `false` after reinstalling, restart the agent or MCP client so it launches the current runtime. If a newly resolved installed wrapper still reports `false`, the install root's `current` link is missing or broken; stop normal Beam work and reinstall. If an installed identity reports `runtime_error`, do not treat it as a source checkout or try to clean it with `lean-beam prune`. After stopping active Beam agents and MCP clients, move an invalid manifest runtime out of `BEAM_INSTALL_ROOT/versions`, preserve it for inspection, and rerun the installer. For an invalid install-root marker, preserve and rename the exact `BEAM_INSTALL_ROOT` as a unit before reinstalling; do not recreate its ownership marker in place or delete the preserved state. MCP workspace-bound tools carry an explicit local workspace descriptor on every call. Dropping that workspace only evicts its cached runtime and retained handles; it does not prove the MCP server binary itself was refreshed. Retain the canonical descriptor when a Lean operation, non-confidential feedback result, or drop result echoes it so a cached runtime can still be dropped if the project path or its Lean/Lake markers become unavailable. Restart active agent or MCP client sessions after installation. For the authoritative install and bundle-resolution order, see the repo [docs/SETUP.md](../../docs/SETUP.md) and [Validated And Compatible Toolchains](../../docs/SETUP.md#validated-and-compatible-toolchains) sections. ## Skill Surface This skill documents the current Lean-facing `lean-beam` workflow surface. Use the smallest command family that fits the task. Agents may access Beam through the `lean-beam` wrapper or through a registered `lean-beam-mcp` server. This skill names wrapper commands because they are always available after installation. When your client exposes the matching MCP tools, use them with the same saved-file, version, update, sync, and isolation rules; do not treat MCP as a raw Lean LSP proxy. Supported command families: - start and own a wrapper session: `lean-beam serve` - inspect the selected session state: `lean-beam status` - inspect existing code, navigation data, or proof state: `lean-beam hover`, `lean-beam signature-help`, `lean-beam definition`, `lean-beam references`, `lean-beam document-symbols`, `lean-beam workspace-symbols`, `lean-beam goals before`, `lean-beam goals after` - inspect actionable Lean items in a range: `lean-beam todo` - inspect file or daemon state: `lean-beam open-files`, `lean-beam doctor`, `lean-beam stats` - produce a local, pasteable bug report card from JSON input: `lean-beam feedback-report` - try one isolated speculative Lean snippet: `lean-beam run-at` - continue from one exact speculative state: `lean-beam run-at-handle`, `lean-beam run-with`, `lean-beam run-with-linear`, `lean-beam release` - refresh or checkpoint one tracked workspace module: `lean-beam sync`, `lean-beam refresh`, `lean-beam save`, `lean-beam close-save` - run shell-oriented search loops over the same handle APIs: `lean-beam-search` What to treat as the normal agent workflow surface: - default workflow commands: `lean-beam hover`, `lean-beam signature-help`, `lean-beam definition`, `lean-beam references`, `lean-beam document-symbols`, `lean-beam workspace-symbols`, `lean-beam goals`, `lean-beam todo`, `lean-beam run-at`, `lean-beam sync`, `lean-beam refresh` - operational commands: `lean-beam open-files`, `lean-beam doctor`, `lean-beam stats`, `lean-beam feedback-report`, `lean-beam save`, `lean-beam close-save` - pre-stable support APIs: `lean-beam run-at-handle`, `lean-beam run-with`, `lean-beam run-with-linear`, `lean-beam release`, `lean-beam-search` Core workflow contract: - use `lean-beam`, not raw JSON and not raw LSP - Beam never applies source edits to `.lean` files on disk; the client applies source edits - `lean-beam` only sees the on-disk file, not unsaved editor buffers - before using wrapper workflow commands, start one foreground `lean-beam serve` process and keep it running across shell invocations; interrupt it or run `lean-beam --root ROOT stop` when finished - MCP owns its stdio runtime session automatically; do not start a separate wrapper holder solely for MCP tool calls - after every real Lean source edit: save the file normally, then run `lean-beam update` before the next version-bound probe; run `lean-beam sync` when you need diagnostics/readiness - use `lean-beam save` only for a synced workspace module path in the current Lake workspace package graph, for example `MyPkg/Sub/Module.lean` - `lean-beam save` checks readiness and checkpoints only the module snapshot you save; it does not validate importers of that module - `lean-beam save` writes the accepted Lean server environment, including structured Lake options, dynamic libraries, and plugins already applied by the file worker; an elaborator can behave differently in server and batch mode, so treat the result as a development checkpoint rather than final build evidence - modules with batch-only `moreLeanArgs` fail with `saveUnsupportedSetup`; move shared `-D` settings to `leanOptions`, or use `lake build` when the arguments are intentionally batch-only - after changing a lakefile or related Lake workspace configuration, run `lean-beam --root ROOT stop` before the next command that uses the Lean server; `lean-beam refresh` does not restart it - check wrapper exit status before parsing output; completed broker operations use final stdout JSON, while selector, setup, or transport failures may have human-facing stderr and no JSON - use MCP when a client requires structured live progress or diagnostic notifications - `lean-beam feedback-report` and `beam_feedback_report` return a report to the caller; Beam does not upload or submit it; before posting non-confidential output, review caller-authored narrative, request/response payloads, local paths, Beam stats, open-file data, daemon logs/incidents, and bundle evidence - `lean-beam feedback-report` does not accept free-form notes; pass a JSON object with required string fields `title`, `summary`, `reproduction`, `expected`, and `actual` - use optional feedback triage fields `kind` (`bug`, `ux`, `perf`, `docs`, `question`) and `severity` (`low`, `medium`, `high`, `critical`) when they help route the report - set feedback `confidential` to `true` for a non-public workspace; this forces HOME-path redaction and omits automatically collected project debug context, request/response payloads, evidence, and the echoed MCP workspace descriptor; requested bundles still return operational paths locally - confidential feedback retains other caller-authored narrative without scanning it for arbitrary secrets; review those fields before sharing through an authorized private channel, and never post the report publicly - do not assume hidden mutable session state carries across unrelated requests ## Agent Cost Model Prefer Beam probes over detached scratch Lean files for project-local questions. A standalone scratch file has a high fixed cost: it starts from a detached module, reloads imports and environment, and encourages simplified contexts that may not match the real source position. A `lean-beam run-at` probe has low marginal cost once the per-project daemon and module context are warm: it asks one speculative question against an explicit broker document version and the real module environment. This changes the right agent behavior: - prefer many small `run-at` probes at the source position over one large scratch experiment - use `goals before`, `goals after`, `hover`, `signature-help`, `definition`, `references`, and symbol queries instead of reconstructing semantic state elsewhere - issue independent `run-at` probes or handle-rooted search sequences in parallel when you have many candidates to check; use distinct request IDs if you need per-request cancellation or tracing - do not batch unrelated questions just to amortize Lean startup; future batch APIs may reduce per-call overhead, but high-bandwidth clients can already get most of the throughput benefit by keeping independent probe sequences in flight - after a real source edit, run `lean-beam update <file>` before later probes; run `lean-beam sync <file>` when you need diagnostics/readiness - use `lake build` for dependency-cone validation and in clean CI; use a local `lean-beam --root ROOT stop` / `lake clean` / `lake build` sequence once when no successful clean CI result is available or server-sensitive elaboration is suspected - use scratch files only for context-free Lean syntax checks or Beam incident isolation ## Prompting Contract Prefer the smallest command that matches the actual task: - use `lean-beam hover` when you want semantic information about existing code at one position - use `lean-beam signature-help` when you want callable-argument signature information at one position - use `lean-beam definition` or `lean-beam references` when you want navigation targets for an existing symbol - use `lean-beam document-symbols` for file-local symbol outlines and `lean-beam workspace-symbols` for workspace-wide symbol search - use `lean-beam goals before` or `lean-beam goals after` when you want existing proof state at one tactic position - use `lean-beam todo` when you want actionable items in a saved file range, such as sorries, holes, diagnostics, code actions, or incomplete proofs - use `lean-beam run-at` when you want to try one speculative Lean snippet without editing the file - for a tactic replacement, probe at its first character after indentation to use its before-state; positions inside a simple tactic can use its after-state - before `lean-beam run-at`, `lean-beam run-at-handle`, `lean-beam hover`, `lean-beam signature-help`, `lean-beam definition`, `lean-beam references`, `lean-beam document-symbols`, `lean-beam goals`, or `lean-beam todo`, call `lean-beam update <file>` and pass the returned `version`; `lean-beam workspace-symbols` takes only a query - if a versioned request fails with `contentModified` and `error.data.reason = "documentVersionMismatch"`, use `error.data.acceptedVersion` for the next retry or run `lean-beam update` / `lean-beam sync` again; do not guess a version - for `lean-beam run-at`, `lean-beam hover`, `lean-beam signature-help`, `lean-beam definition`, `lean-beam references`, `lean-beam goals`, and `lean-beam todo`, treat line and character arguments as Lean/LSP coordinates: line `0` is the first line, character `0` is the first UTF-16 code unit, and on a truly empty line only character `0` is valid - use `lean-beam run-at-handle` and then `lean-beam run-with` or `lean-beam run-with-linear` only when exact speculative continuation matters - for multiline speculative text, prefer `--stdin` as the normal path; use `--text-file <path>` when the text already lives in a file - for handle-based continuation, prefer `--handle-file <path>` as the normal path; deeper shell-loop variants such as stdin handle piping live in the reference docs - do not expect one `lean-beam run-at` call to become the basis of the next one automatically - parallel probes are fine when they are independent; do not concurrently reuse a linear handle or assume ordered side effects between separate speculative sequences - use `lean-beam update` right after every real saved edit before the next speculative probe - use `lean-beam sync` when you need diagnostics/readiness before saving or checkpointing - use `lean-beam save` or `lean-beam close-save` only for a synced workspace module path such as `MyPkg/Sub/Module.lean` Stop probing and change tactics when: - the speculative result now needs to become real source: edit the file, save it, then `lean-beam sync` - repeated `lean-beam run-at` probes are no longer clarifying the problem - you edited a dependency and now need trustworthy downstream results; `lean-beam save` only checkpoints the module you save, not downstream importers - stale-state, `contentModified`, or rebuild trouble keeps appearing; inspect with `lean-beam open-files` and `lean-beam doctor` - no successful clean CI result is available, or the task may depend on server-sensitive elaboration; stop Beam and perform the clean batch build once - if `lean-beam sync` fails with `syncBarrierIncomplete`: inspect `error.data.staleDirectDeps`, `error.data.saveDeps`, and `error.data.recoveryPlan`; save only the listed direct deps that still need checkpointing, then `lean-beam refresh "Target.lean"` if the plan says to; if this repeats across multiple dependency hops, escalate to `lake build` When those conditions hold, prefer a real edit plus `lean-beam sync`, or escalate to `lake build` when the task has become dependency freshness across importers or explicitly requires the optional batch-equivalence check rather than one-file probing. ## Lean-Run-At Semantics `lean-beam run-at` is a speculative execution request against one explicit broker document version. Read it as "try this Lean text here", not as "edit the file here". What `lean-beam run-at` does not do: - it does not edit the source file or create a new on-disk baseline for the next request - it does not make the speculative text become the basis of the next `lean-beam run-at` call - it does not wait for or return the full diagnostics barrier for the rest of the file - it does not replay full-file diagnostics in its final JSON payload - it does not auto-indent or synthesize leading spaces when you probe at an indented empty line - it does not reinterpret blank-line coordinates; if the line is truly empty then character `1` is already out of range - in command mode, one `run-at` request accepts one Lean command, not a complete top-level command sequence; use `run-at-handle` plus `run-with` for explicit sequencing, or make a real edit and `sync` Use the right tool for each goal: - if you made a real edit and want fresh file diagnostics: save the file, then use `lean-beam sync` - if you want exact continuation from speculative state: mint a handle with `lean-beam run-at-handle`, then continue with `lean-beam run-with` or `lean-beam run-with-linear` - if you want to test several top-level commands together: write them to the file and sync, or split the experiment into explicit handle continuations - for handle-based commands, `--handle-file <path>` is the easiest way to avoid inlining handle json - if surface syntax depends on indentation or layout: pass the exact text you want Lean to parse, or make a real edit in the file instead of expecting the wrapper to fill whitespace for you Open [references/lean-run-at-semantics.md](references/lean-run-at-semantics.md) when the task needs concrete examples for: - full-file diagnostics after a speculative probe - chaining speculative state across multiple calls - indentation-sensitive or newline-sensitive probes on blank or layout-sensitive lines Open [references/workflow-details.md](references/workflow-details.md) for position semantics, text/handle input variants, and wrapper debugging. Open [references/commit-speculative.md](references/commit-speculative.md) when the task needs the current workflow for turning a good speculative probe into a real saved edit. Open [references/anti-patterns.md](references/anti-patterns.md) when you want a short checklist of what Lean agents should not assume about `lean-beam run-at`, `lean-beam sync`, handles, or dependency edits. ## Lean Wrapper Use `lean-beam`, not raw JSON and not raw LSP. `lean-beam` for Lean: - infers the target project root from the current directory or `--root` - keeps one owner per resolved workspace and session-directory selector; the default descriptor is `<root>/.beam/beam-daemon.json` - in sandboxed or read-only project trees, set `BEAM_SESSION_ROOT` to a writable directory; `lean-beam` uses a per-root subdirectory there - for an exact stable alternate session location, pass the same absolute path with `--session-dir DIR` to the owner and every attaching command; Beam does not search alternate session directories - resolves a toolchain-keyed Lean bundle, preferring the installed beam bundle cache and falling back to a project-local runtime bundle under `<root>/.beam/bundles` or `BEAM_BUNDLE_DIR` - fully validates exact Lean toolchains listed in `validated-lean-toolchains`, locally qualifies canonical RC/patch variants from `compatible-lean-release-lines`, and accepts exact custom names recorded by the installer in `custom-lean-toolchains` - gives daemon startup authority only to `lean-beam serve`; ordinary wrapper commands attach to its registry generation and never start a daemon implicitly - owns stopping and descriptor handling - resolves Lean with `elan which lean` - builds and plugin-qualifies a local fallback bundle only when no matching installed bundle exists for the exact accepted toolchain fingerprint - fails early on toolchains that are neither validated, canonical members of a compatible release line, nor explicitly custom; use `lean-beam validated-toolchains`, `lean-beam compatible-release-lines`, and `lean-beam doctor` to inspect the decision - after effective Lean startup configuration changes, requires shutting down the old session and starting a new `lean-beam serve` owner - after abnormal owner/broker exit, preserves the session fence until explicit `recover --generation ID`; recovery quarantines metadata and never signals its persisted PIDs - `lean-beam --root ROOT stop` requires an explicit root; `lean-beam status` and `lean-beam stats` may infer a unique root - `lean-beam prune` previews old installed runtimes; restart active agents and MCP clients before any `--apply`, and add `--bundles` when stale installed bundle caches should also be removed - wrapper commands talk to the per-project Beam daemon over localhost TCP; they are not direct in-process Lean calls - `lean-beam serve` prints a running-session JSON response after backend readiness and keeps the wrapper process alive as the session owner; an inherited pipe ties daemon lifetime to that process without heartbeat files or lease expiry - the OS assigns the internal loopback endpoint and the daemon reports it through a private typed readiness handshake; callers select sessions by root and optional session directory rather than by transport details - interrupting an ordinary wrapper call closes its one-request connection so the daemon cancels that exact admission; `lean-beam cancel <id>` remains available for cross-process cancellation - interrupting the holder or using `lean-beam --root ROOT stop` performs bounded owner cleanup; killing the holder closes the owner pipe and requests cooperative daemon shutdown, while the session fence remains for explicit recovery `lean-beam` is more than a one-shot probe: - the common path is still a single isolated `lean-beam run-at` request, which wraps the standalone Lean method `$/lean/runAt` - the underlying Lean side can also retain follow-up state through opaque handles for continuation and branching when one-shot probing is not enough, through follow-up methods `$/lean/runWith` and `$/lean/releaseHandle` - treat handles as pre-stable support APIs: useful, real, and powerful, but more fragile than the base request - handles are document-bound and are invalidated by same-document edits, close, worker restart, or Beam daemon restart - do not present handles as the main story unless the task actually needs continuation from the exact speculative state Default rules: - use `lean-beam`, not raw JSON and not raw LSP - start and keep one `lean-beam serve` owner before issuing wrapper workflow commands - start with `lean-beam run-at` - after every real source edit: save the file to disk normally, then `lean-beam update` before the next version-bound probe; use `lean-beam sync` for diagnostics/readiness - if exact continuation matters: mint a handle - if search branches: use `lean-beam run-with`, `lean-beam run-with-linear`, and `lean-beam release` - if you want shorter shell commands for search loops: use `lean-beam-search` - if bundle resolution or startup looks wrong: check `lean-beam doctor` before guessing ## Fast Path If you only remember one workflow, use this one: ```bash # terminal or long-lived agent process 1: keep this running lean-beam serve # terminal or agent process 2: inspect existing code or proof state update_out="$(lean-beam update "Foo.lean")" printf '%s\n' "$update_out" version="$(printf '%s\n' "$update_out" | python3 -c 'import json,sys; print(json.load(sys.stdin)["result"]["version"])')" lean-beam hover "Foo.lean" "$version" 10 2 lean-beam signature-help "Foo.lean" "$version" 10 2 lean-beam definition "Foo.lean" "$version" 10 2 lean-beam references "Foo.lean" "$version" 10 2