diff --git a/README.md b/README.md index d1354af2..81a7fca6 100644 --- a/README.md +++ b/README.md @@ -6,18 +6,38 @@ The extensions provide Lean-specific capabilities, and the broker exposes them t [`lean-beam` CLI](docs/SETUP.md#use-beam-from-a-lean-project) and an [MCP server](docs/SETUP.md#mcp-setup) for agent- and tool-facing workflows. +Its central operation is speculative execution: a client sends +[`runAt`](docs/STATUS.md#core-lean-surface) for a position in a saved file and a Lean command or +tactic, and Beam checks whether that text would work there without changing the file. + +`runAt` is exposed by the CLI as +[`lean-beam run-at`](docs/SETUP.md#use-beam-from-a-lean-project) and through MCP as +[`lean_run_at`](docs/MCP.md#public-tools). Because these probes can be issued concurrently, agents +and tools can cheaply explore several "would this work here?" possibilities in the real module +context. + +Together, the LSP extensions, CLI, and MCP interface make this loop cheaper and more structured than +repeatedly creating scratch files or using full `lake build` runs as the inner loop. Beam is +implemented in Lean, which lets it integrate directly with Lean server state, saved snapshots, and +synchronization where that matters. + +## Architecture At A Glance + +Most clients only need the CLI or MCP surface, but the split below explains where request routing +and Lean state live. + ```mermaid flowchart TB - subgraph level1["Level 1: agents and tools"] + subgraph clients["Clients and agents"] cli["CLI / shell / agent"] mcp["MCP client / agent"] end - subgraph level2["Level 2: Beam broker"] - broker["Beam broker
request routing
session ownership"] + subgraph runtime["Beam broker"] + broker["request routing
session ownership"] end - subgraph level3["Level 3: Lean instances"] + subgraph sessions["Lean LSP sessions"] subgraph lsp1["Lean LSP server"] lean1["Lean"] plugin1["Beam LSP plugin"] @@ -42,32 +62,12 @@ flowchart TB leanN --- pluginN ``` -Beam keeps the agent-facing surface small: clients talk to the broker, and the broker owns request -routing plus one or more Lean LSP sessions with the Beam plugin loaded. - -Beam lets a client try Lean commands or tactics at specific positions in saved files without -changing those files. The central Beam extension is speculative execution through -[`runAt`](docs/STATUS.md#core-lean-surface), exposed by the CLI as -[`lean-beam run-at`](docs/SETUP.md#use-beam-from-a-lean-project) and through MCP as -[`lean_run_at`](docs/MCP.md#public-tools). Because these probes can be issued -concurrently, agents and tools can cheaply explore several "would this work here?" possibilities in -the real module context. - -Together, the LSP extensions, CLI, and MCP interface are intended to make that loop cheaper and more -structured than repeatedly creating scratch files or using full `lake build` runs as the inner loop. - -Beam is implemented in Lean, which lets it integrate more directly with Lean server state, saved -snapshots, and synchronization where that matters. +Clients talk to the broker, and the broker owns request routing plus one or more Lean LSP sessions +with the Beam plugin loaded. We have found Beam useful for proof repair, proof search experiments, proof translation and porting, autoformalization experiments, and regular AI-assisted Lean editing. -Feedback is welcome through GitHub issues or Lean Zulip. For structured bug reports from a local -checkout, `lean-beam feedback-report --stdin` can produce a pasteable report card; see -[docs/FEEDBACK.md](docs/FEEDBACK.md). Review non-confidential cards before posting them publicly; -set `"confidential": true` in the feedback input JSON for a non-public workspace and never post that -report publicly. Beam does not upload or submit the report. - Lean Beam is currently available as a preview. We are working to stabilize it into dependable agent tooling for everyday Lean use and prepare it for distribution with Lean. Until that work lands, Beam is installed separately, its interfaces may change, and its current scope and limitations are @@ -77,40 +77,6 @@ Most readers should start with [Install](#install), then use [docs/SETUP.md](doc toolchains, first CLI commands, agent-skill setup, and MCP registration. Release-facing changes are tracked in [CHANGELOG.md](CHANGELOG.md). -## Current Beta Surface - -The current development line includes support for: - -- speculative Lean execution with [`runAt`](docs/STATUS.md#core-lean-surface) -- incremental synchronization of Lean's view of a file after edits with - [`sync`](docs/SYNC_AND_DIAGNOSTICS.md#command-model) -- actionable file information with [`todo`](docs/STATUS.md#core-lean-surface), including sorries, - holes, diagnostics, code actions, and incomplete proofs -- creating development `.olean` checkpoints from an interactive session with - [`save`](docs/SYNC_AND_DIAGNOSTICS.md#command-model) -- selected Lean/LSP features through the same - [CLI](docs/SETUP.md#use-beam-from-a-lean-project) and - [MCP](docs/MCP.md#public-tools) interfaces, including hover, signature help, - definitions, references, document/workspace symbols, and proof-state inspection -- feedback report cards for bug reports and project feedback through - [`lean-beam feedback-report`](docs/FEEDBACK.md) and MCP - [`beam_feedback_report`](docs/FEEDBACK.md#mcp) - -See [docs/STATUS.md](docs/STATUS.md) for the current supported surface, known limitations, and -release direction. - -Beam checkpoints accelerate the development loop by writing the Lean server's accepted state, -including structured Lake options, dynamic libraries, and plugins already applied by the file -worker. 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. A -running Lean server is not guaranteed to pick up Lake workspace configuration changes; after such a -change, run `lean-beam shutdown` before the next command that uses the Lean server. A successful -checkpoint is normally sufficient while working; do not add an expensive clean build to every Beam -loop. Final project validation should come from CI running `lake build` from clean Lake artifacts. -If no successful clean CI result is available, or server-sensitive elaboration is suspected, use the -one-time local batch check described in the -[sync and diagnostics contract](docs/SYNC_AND_DIAGNOSTICS.md#development-checkpoints-and-batch-validation). - ## Install Install or update Beam from a Lean Beam checkout: @@ -134,6 +100,28 @@ variants from [`compatible-lean-release-lines`](compatible-lean-release-lines). [docs/SETUP.md](docs/SETUP.md#validated-and-compatible-toolchains) for bundle setup and [docs/CUSTOM_TOOLCHAINS.md](docs/CUSTOM_TOOLCHAINS.md) for explicitly accepted local Lean builds. +## Current Preview Surface + +The current development line includes support for: + +- speculative Lean execution with [`runAt`](docs/STATUS.md#core-lean-surface) +- incremental synchronization of Lean's view of a file after edits with + [`sync`](docs/SYNC_AND_DIAGNOSTICS.md#command-model) +- actionable file information with [`todo`](docs/STATUS.md#core-lean-surface), including sorries, + holes, diagnostics, code actions, and incomplete proofs +- creating development `.olean` checkpoints from an interactive session with + [`save`](docs/SYNC_AND_DIAGNOSTICS.md#command-model) +- selected Lean/LSP features through the same + [CLI](docs/SETUP.md#use-beam-from-a-lean-project) and + [MCP](docs/MCP.md#public-tools) interfaces, including hover, signature help, + definitions, references, document/workspace symbols, and proof-state inspection +- feedback report cards for bug reports and project feedback through + [`lean-beam feedback-report`](docs/FEEDBACK.md) and MCP + [`beam_feedback_report`](docs/FEEDBACK.md#mcp) + +See [docs/STATUS.md](docs/STATUS.md) for the current supported surface, known limitations, and +release direction. + ## Documentation Map For users: @@ -164,11 +152,16 @@ For contributors and maintainers: ## Contributing And Help -The main goal of the beta development cycle is to gather feedback from Lean users and tool authors. +The main goal of the preview development cycle is to gather feedback from Lean users and tool +authors. Bug reports, design feedback, and documentation improvements are welcome through [GitHub issues](https://github.com/leanprover/lean-beam/issues). Discussion is also welcome on the [Lean Zulip](https://leanprover.zulipchat.com). +For structured bug reports from a local checkout, `lean-beam feedback-report --stdin` produces a +pasteable report card; see [docs/FEEDBACK.md](docs/FEEDBACK.md) for the command and confidentiality +guidance. Beam does not upload or submit the report. + Before contributing code or docs, read [CONTRIBUTING.md](CONTRIBUTING.md). Maintainer workflow notes live in [docs/DEVELOPMENT.md](docs/DEVELOPMENT.md). diff --git a/docs/DEVELOPMENT.md b/docs/DEVELOPMENT.md index ca91ef1e..864640c9 100644 --- a/docs/DEVELOPMENT.md +++ b/docs/DEVELOPMENT.md @@ -10,11 +10,12 @@ contributors. Current maintainer priorities are: -- keep README human-facing and release-ready +- keep README human-facing and current - keep maintainer and agent workflow guidance out of README +- keep status, setup, compatibility, MCP, and sync/diagnostic contracts at distinct levels of detail - make the harness work well for both humans and AI agents without turning it into public product surface -- prefer small targeted fixes over broad refactors unless a release-facing doc or workflow problem +- prefer small targeted fixes over broad refactors unless a public doc or workflow problem demands the larger change ## Entry Points diff --git a/docs/ROCQ.md b/docs/ROCQ.md index c09bb7e8..8f08cc2c 100644 --- a/docs/ROCQ.md +++ b/docs/ROCQ.md @@ -10,33 +10,19 @@ Rocq Beam is not a second full execution layer. It exposes saved-file goal probe ## Install -The default agent skill install is Lean-only: - -```bash -./scripts/install-beam.sh --codex -./scripts/install-beam.sh --claude -./scripts/install-beam.sh --pi -./scripts/install-beam.sh --opencode -./scripts/install-beam.sh --vibe -./scripts/install-beam.sh --all-skills -``` - -Install the optional Rocq skill by adding `--rocq-skill` to a selected agent target: +Install Beam through the main [setup guide](SETUP.md). The default agent skill install is +Lean-only; add `--rocq-skill` to a selected agent target when you also want the optional Rocq skill: ```bash ./scripts/install-beam.sh --codex --rocq-skill -./scripts/install-beam.sh --claude --rocq-skill -./scripts/install-beam.sh --pi --rocq-skill -./scripts/install-beam.sh --opencode --rocq-skill -./scripts/install-beam.sh --vibe --rocq-skill ./scripts/install-beam.sh --all-skills --rocq-skill ``` `--rocq-skill` is only a modifier. It must be paired with `--codex`, `--claude`, `--pi`, `--opencode`, `--vibe`, `--all-skills`, or an interactive skill target. -General installer locations, MCP registration, and toolchain options are documented in -[SETUP.md](SETUP.md). +The full installer target matrix, locations, MCP registration, and toolchain options are documented +in [SETUP.md](SETUP.md). ## Rocq Setup diff --git a/docs/STATUS.md b/docs/STATUS.md index 1d669ce7..4ca386ce 100644 --- a/docs/STATUS.md +++ b/docs/STATUS.md @@ -1,307 +1,207 @@ # Status -Lean Beam is experimental beta software. The repository is public for collaboration, early use, -and feedback, but interfaces and installation details may still change before a stable release. +Lean Beam is preview beta software. The repository is public for collaboration, early use, and +feedback, but interfaces and installation details may still change before a stable release. -The main product idea is a small, type-safe, isolated execution surface for Lean. Beam is the shared -thin layer on top of Lean LSP plus Beam-specific extensions: the Lean plugin provides low-level -facts, and the local Beam layer turns those facts into practical CLI, broker, MCP, and skill -workflows. +This page summarizes what users can rely on today. Exact setup instructions live in +[SETUP.md](SETUP.md), exact MCP behavior lives in [MCP.md](MCP.md), and exact sync, save, progress, +and diagnostic behavior lives in [SYNC_AND_DIAGNOSTICS.md](SYNC_AND_DIAGNOSTICS.md). The pre-stable +compatibility policy lives in [COMPATIBILITY.md](COMPATIBILITY.md). -Pre-stable compatibility policy lives in [Compatibility Policy](COMPATIBILITY.md). +The main product idea remains small: run speculative Lean text at a saved-file position without +mutating the user's real document state. The conceptual request is: + +```text +runAt(pos, "lean text") +``` + +Beam adds a thin local layer around Lean LSP plus Beam-specific Lean extensions. The Lean plugin +provides low-level facts; the local Beam layer exposes them through the `lean-beam` CLI, broker +runtime, MCP server, and installed agent skills. ## Current Scope ### Core Lean Surface -- standalone Lean plugin for `$/lean/runAt` -- internal proof-first, command-fallback basis selection -- typed response payload with messages, traces, optional proof state, and optional follow-up handle -- optional follow-up execution through `$/lean/runWith` and `$/lean/releaseHandle` -- agent-oriented `$/lean/todo` range inspection for actionable items such as sorries, holes, - diagnostics, code actions, and incomplete proofs, exposed through the broker, `lean-beam todo`, - and MCP `lean_todo` -- versioned broker/MCP code-action resolution for raw Lean code actions returned by `lean_todo`; - clients still apply returned LSP workspace edits themselves and then update or sync the file -- small Lean semantic navigation wrappers for hover, signature help, definition, references, - document symbols, workspace symbols, and mode-based goal inspection, exposed through the broker, - `lean-beam`, and MCP -- explicit Lean `lean-beam sync` barrier with diagnostics wait and compact `fileProgress` reporting -- zero-build `lean-beam save` development checkpoint for one synced workspace module, including - structured Lake setup already applied by the Lean file worker -- typed sync summaries with current diagnostic/readiness counts for the synced document version - -### Local Beam Layer - -- local Beam daemon/client pair for Lean and Rocq workflows -- optional Rocq Beam goal probes through `coq-lsp`, documented separately in - [docs/ROCQ.md](ROCQ.md) -- experimental Lean wrapper commands for follow-up handle continuation and release -- installed `lean-beam-search` helper for shorter shell branching/playout workflows -- explicit broker `ok` / `error` response envelopes for machine-readable local protocol consumers -- `lean-beam open-files` daemon introspection for tracked documents, including `diskStatus`, - the daemon-recorded `checkpointed` marker, and the last compact `fileProgress` -- local broker workspaces keyed by explicit workspace ids, each owning its own LSP session, document - mirror, handles, sync/save history, and metrics -- compact `fileProgress` reporting on slow Lean wrapper calls when matching LSP progress - notifications were observed while the request was pending -- explicit support for installed custom elan-linked Lean toolchains through - `--custom-toolchain `, recorded in the runtime's `custom-lean-toolchains` registry -- conservative installed-state maintenance through `lean-beam prune`, with a dry run by default, - ownership and manifest validation, and optional stale installed bundle-cache cleanup +Currently supported: + +- speculative Lean execution through `$/lean/runAt`, exposed as `lean-beam run-at` and MCP + `lean_run_at` +- internal proof-first, command-fallback basis selection with no public mode flag +- typed responses containing messages, traces, optional proof state, and optional follow-up handles +- follow-up execution through `$/lean/runWith`, `$/lean/releaseHandle`, wrapper commands, and + matching MCP tools +- actionable file inspection through `$/lean/todo`, `lean-beam todo`, and MCP `lean_todo`, including + versioned code-action resolution +- selected Lean/LSP-style navigation through the same wrapper and MCP projections: hover, signature + help, definitions, references, document and workspace symbols, and goal inspection +- saved-file update, synchronization, and development checkpoints through `lean-beam update`, + `lean-beam sync`, `lean-beam refresh`, `lean-beam save`, and `lean-beam close-save` + +The base `runAt` path is the main API story. Follow-up handles and search helpers are useful +pre-stable extensions, but they are not the center of the product contract. + +### CLI, Broker, And Runtime + +The normal human and agent entry point is the installed `lean-beam` wrapper. It resolves the current +project root, talks to a local Beam daemon, and reports structured JSON on stdout. The broker owns +isolated workspaces, their Lean sessions, document mirrors, handles, sync and save history, and +metrics. + +The wrapper currently supports: + +- saved-file update, sync, run-at, todo, navigation, and checkpoint commands +- daemon inspection through `lean-beam open-files`, `lean-beam stats`, and `lean-beam doctor` +- runtime identity through `lean-beam --version` +- conservative installed-state maintenance through `lean-beam prune` +- structured report cards through `lean-beam feedback-report` + +Programmatic local consumers should prefer the broker JSON stream exposed by +`beam-client request-stream`. Wrapper stderr is human-facing and may change as diagnostic text +improves. ### MCP And Agent Integration -- installed experimental `lean-beam-mcp` stdio server exposing the curated Lean Beam tool set - through stateless MCP `2026-07-28`; initialization-based MCP `2025-11-25` remains available during - the transition -- MCP implementation backed directly by the broker runtime rather than by a second daemon/client - connection -- bug-report identity surfaces: `lean-beam --version`, `lean-beam-mcp --version`, and MCP - `beam_version` for the running server process, including manifest commit or source checkout - commit/branch/dirty data, installed `runtime_current` status, and structural `runtime_error` - reporting for invalid owned markers or manifests -- feedback report-card surfaces: `lean-beam feedback-report` and MCP `beam_feedback_report` return - structured JSON containing pasteable Markdown, metadata, collection warnings, and optional - evidence bundle paths without uploading or submitting feedback; CLI output and MCP - `include_collected: true` include collected version/stats/open-file context, daemon registry - context, and recent daemon incident paths; `confidential: true` instead omits automatically - collected project debug context, request/response payloads, and evidence, forces HOME-path - redaction, and marks the report as unsuitable for public posting -- `lean-beam-mcp --self-check ` verification from a Lean project through a real - descriptor-bound `lean_sync` call -- request-stateless local MCP workspaces: every workspace-bound call carries - `{"workspace":{"root":"/absolute/project"}}`; runtimes are cached lazily by canonical root, - `lean_drop_workspace` evicts one cache, and there is no default workspace, setup tool, startup - `--root`, or Roots discovery -- projected MCP tools for versioned Lean file operations, semantic navigation, todo/code-action - workflows, follow-up handles, save/sync operations, version/stats, and feedback report cards; the - generated tool list and client semantics are documented in [MCP.md](MCP.md) -- MCP progress notifications for requests that pass `_meta.progressToken` -- MCP diagnostic log notifications for incremental Lean diagnostics during `lean_sync`, - `lean_refresh`, `lean_save`, and `lean_close_save`, with protocol-era opt-in documented in - [MCP.md](MCP.md#progress-and-diagnostic-logs) -- MCP `lean_sync` and `lean_refresh` `diagnostics_in_result` option for clients that need selected - current diagnostics replayed in the final structured result instead of collecting only - interleaved log notifications -- bundled Lean skills for supported agent clients, plus optional Rocq skills when installed with +The installed `lean-beam-mcp` server is an experimental stdio MCP projection over the same Beam +operation layer. It is not a raw Lean LSP proxy and does not expose arbitrary LSP methods. + +Currently supported: + +- stateless MCP `2026-07-28`, with initialization-based MCP `2025-11-25` available during the + transition +- explicit local workspace descriptors on every workspace-bound call, with lazy runtime caching + and explicit eviction through `lean_drop_workspace` +- projected Lean tools for update, sync, refresh, run-at, handles, navigation, todo and code-action + resolution, save, close, and workspace symbols +- utility tools such as `beam_version`, `beam_stats`, and `beam_feedback_report` +- concurrent independent tool calls, exact request-ID routing, and cooperative cancellation of + active broker work +- ordered progress notifications for calls with `_meta.progressToken` and incremental Lean + diagnostic log notifications for sync-style calls +- `lean-beam-mcp --self-check ` for installed-path verification +- bundled Lean skills for supported agent clients, with optional Rocq skills when installed with `--rocq-skill` +The generated MCP tool list and exact client semantics are documented in [MCP.md](MCP.md). + +### Rocq Surface + +Rocq support is intentionally narrow. Beam exposes optional goal probes through `coq-lsp`, mainly +for Rocq-to-Lean porting workflows. It is not a Rocq analogue of the Lean speculative execution +layer. Rocq setup and workflow details live in [ROCQ.md](ROCQ.md). + ### Coverage -- repo-local regression coverage around isolation, stale state, cancellation, and handle invalidation -- broker, wrapper, install, MCP, and CI coverage described in [docs/TESTING.md](TESTING.md) -## Operational Notes +The repository includes regression coverage for isolation, stale state, cancellation, handle +invalidation, broker and wrapper behavior, installation, MCP conformance, and supported toolchains. +The suite map and exact commands live in [TESTING.md](TESTING.md). + +## Current Contracts -The base request remains intentionally small: +### Request Isolation -- one document -- one position -- one Lean command or tactic-block payload -- no required command/tactic mode flag +Each speculative Lean request behaves like an isolated sandbox: -Request-level failures stay at the transport layer. Semantic Lean outcomes stay in the normal typed -response payload. +- it does not mutate the document's real elaboration state +- it does not rely on side effects from previous speculative requests +- it does not leak hidden mutable state through the base API +- continuation state is retained only when the caller explicitly asks for a follow-up handle -Follow-up handles exist, but they should be treated as pre-stable support APIs rather than as a frozen -long-term contract. They are opaque, workspace- and document-bound, invalidated by same-document -edits, document close, worker or daemon restart, and reset/drop of their owning workspace. Exact -continuation requires an explicit handle path; separate `lean-beam run-at` calls do not chain +Handles are workspace- and document-bound. Same-document edits, document close, worker or daemon +restart, and workspace eviction invalidate them. Separate `lean-beam run-at` calls do not chain through hidden state. -The `lean-beam update`, `lean-beam sync`, `lean-beam save`, and `lean-beam close-save` commands are -a progression: - -- `lean-beam update` opens or updates the broker's LSP mirror and returns the current document - version without waiting for diagnostics -- `lean-beam sync` establishes the diagnostics-complete saved file snapshot for the current document - version -- `lean-beam save` creates a development checkpoint from that server snapshot for one module -- `lean-beam close-save` creates the same checkpoint and then closes the tracked file - -Position/range/document operations are version-bound across the broker, MCP, and wrapper surfaces. -Clients first update or sync a saved file, then pass the returned document version to later probes. -Workspace symbol queries are workspace-scoped and do not take a file version. The canonical -field-level contract for update, sync, save, progress, diagnostics, stale-version failures, -readiness, and recovery hints lives in [SYNC_AND_DIAGNOSTICS.md](SYNC_AND_DIAGNOSTICS.md). - -If a speculative probe looks right and should become real source, the current contract is still: -make the real edit in the file, save it, then run `lean-beam sync`. After the client has written and -saved accepted text, the intended future direction is for `lean-beam update` or `lean-beam sync` to -reuse matching speculative execution rather than replaying it from scratch. Beam would still not -apply the source edit. - -For programmatic local consumers, the preferred machine-readable surface is the JSON stream exposed -by `beam-client request-stream`; wrapper stderr should be treated as human-facing. Broker responses -require an explicit top-level `ok` boolean, giving projection layers an unambiguous success/error -discriminator. A successful response always includes `result`; response and stream envelopes reject -undeclared fields, and typed save/close-save results reject incomplete or extended artifact shapes. -All raw stream variants use the same `kind`, `payload`, and optional outer `clientRequestId` fields; -the terminal response payload does not duplicate transport correlation. Exact event ordering and -examples live in [SYNC_AND_DIAGNOSTICS.md](SYNC_AND_DIAGNOSTICS.md#raw-broker-stream). - -`lean-beam-mcp` is the experimental stdio MCP entry point. User setup lives in -[SETUP.md](SETUP.md#mcp-setup); implementation, protocol, tool-list, and conformance notes live in -[MCP.md](MCP.md). +### Saved Files And Versions + +Beam operates on saved files, not unsaved editor buffers. Position and range operations are +version-bound: callers update or sync a file, then pass the returned document version to later +probes. If Beam reports `contentModified`, update or sync again and retry with the accepted current +version. + +`lean-beam sync` is the diagnostics and readiness barrier after a real saved edit. `lean-beam save` +adds a zero-build development checkpoint for one synced Lake module. `lean-beam close-save` +checkpoints and then closes the tracked file. The exact fields, readiness rules, and failure shapes +live in [SYNC_AND_DIAGNOSTICS.md](SYNC_AND_DIAGNOSTICS.md). + +### Compatibility + +During beta, compatibility is intentionally narrow. Exact validated Lean toolchains, compatible +release lines, runtime and install metadata, advertised MCP revisions, and explicitly documented +client requirements are the named compatibility targets. CLI and MCP surfaces remain discoverable +through help text, installed skill text, and MCP `tools/list`. See +[COMPATIBILITY.md](COMPATIBILITY.md). ## Known Limitations -### Toolchains And Bundles +### Toolchains And Distribution - Lean plugin loading currently depends on `-Dexperimental.module=true`. -- Lean plugin loading is toolchain-keyed, not toolchain-agnostic. +- Lean plugin loading and runtime bundles are toolchain-keyed, not toolchain-agnostic. - Exact CI-validated Lean toolchains are listed in [validated-lean-toolchains](../validated-lean-toolchains). Canonical RC and patch variants from - [compatible-lean-release-lines](../compatible-lean-release-lines) are admitted separately and - must build and pass a local plugin load/elaboration probe for their exact fingerprint. -- The supported fast path is the Lean toolchain pinned by this repository's `lean-toolchain`, because - the plugin uses internal Lean APIs. -- The installer prebuilds the pinned validated toolchain by default and can prebuild additional - validated, release-line-compatible, or explicitly custom toolchains; setup flags and offline notes live in - [SETUP.md](SETUP.md). -- Runtime requests first try that installed bundle cache, then fall back to a project-local - runtime bundle under `.beam/bundles/` for validated, release-line-compatible, or explicitly custom - toolchains. -- Toolchains outside the validated exact list and compatible canonical release lines that are not - explicitly custom fail early instead of attempting an opportunistic build. -- Bundle rebuild keys intentionally exclude the full `.lake/packages` checkout tree and instead use - the resolved toolchain fingerprint, the runtime source tree, `lean-toolchain`, - `lake-manifest.json`, `validated-lean-toolchains`, `compatible-lean-release-lines`, and - `custom-lean-toolchains`. See - [CUSTOM_TOOLCHAINS.md](CUSTOM_TOOLCHAINS.md) for the custom toolchain and runtime-bundle model. -- The first use of an accepted but not-yet-prebuilt toolchain must still build and qualify a matching - local fallback bundle. -- On a cold machine, that local fallback build may need network access to fetch dependencies. + [compatible-lean-release-lines](../compatible-lean-release-lines) are admitted separately, and + explicitly custom elan-linked toolchains require installer registration. +- First use of an accepted but not-yet-prebuilt toolchain may need to build and qualify a local + fallback bundle. On a cold machine, that build may require network access. +- Beam is installed separately today; it is not yet distributed with Lean. ### Runtime And Sandbox Behavior -- In sandboxed agent environments, Beam daemon startup itself may require elevated permissions even - when the installed bundle and project-local `.beam` paths resolve correctly. -- A startup failure that reports `operation not permitted` through `.beam/beam-daemon-startup.log` is +- In sandboxed agent environments, daemon startup can require elevated permissions even when the + installed bundle and project-local paths resolve correctly. +- A startup failure reporting `operation not permitted` through `.beam/beam-daemon-startup.log` is usually an environment restriction, not a bundle-resolution mismatch. -- Beam daemon disappearance errors include registry/log context and write a JSON incident record under - `.beam/daemon-failures/` or the per-root subdirectory of `BEAM_CONTROL_DIR`. Beam keeps the latest - 50 incident records and `lean-beam doctor` lists recent incident paths. -- A standalone Beam daemon watches its canonical project root. If a git worktree or project - directory is removed while the daemon is active, it shuts down its backend sessions and exits - instead of remaining undiscoverable after its project-local registry disappears. A later wrapper - request for that path fails root validation with a direct `workspace root does not resolve` - error; it does not start a replacement daemon for a missing directory. +- Daemon disappearance errors include registry and log context and write a bounded set of incident + records under `.beam/daemon-failures/` or the per-root `BEAM_CONTROL_DIR` directory. +- A standalone daemon exits if its canonical project root disappears; later requests fail root + validation instead of starting a replacement daemon for the missing path. - Cancellation is cooperative; prompt stopping depends on inner elaboration polling interruption. -- The Beam daemon can manage multiple local workspaces, with one active session per backend per - workspace. Remote workspaces and same-source multi-toolchain mirrors are not implemented yet. +- Beam workspaces are local. Remote workspaces and same-source multi-toolchain mirrors are not + implemented. ### MCP -- `lean-beam-mcp` prefers MCP `2026-07-28` and implements `server/discover`, required per-request - protocol metadata, modern result envelopes, cache hints, and request-scoped diagnostic logging. - It also supports the initialization-based `2025-11-25` lifecycle as an explicit transition - target; older revisions are not advertised or tested. -- `beam_feedback_report`, `lean_drop_workspace`, and all Lean operation tools require an explicit - local workspace descriptor. Dropping a workspace invalidates its proof handles; a later request - with the same descriptor recreates its runtime lazily. -- `lean-beam-mcp` can execute ordinary tool calls concurrently in one process. Responses may arrive - out of request order and are routed by exact JSON-RPC ID, with string and numeric IDs kept distinct. -- The observational tools enumerated in the [MCP tool documentation](MCP.md#public-tools) advertise - `annotations.readOnlyHint = true`. Codex MCP registration also sets - `supports_parallel_tool_calls = true`, allowing Codex to schedule independent probes - concurrently. The annotation describes Beam-managed state and artifacts; it is not an OS sandbox - for arbitrary Lean metaprogramming. -- Additive retained-handle tools advertise `annotations.destructiveHint = false`, while idempotent - workspace-drop and document-close tools advertise `annotations.idempotentHint = true`. These - remain non-read-only operations; the hints describe Beam-managed effects rather than client - approval or scheduling policy. -- Tool calls that include `_meta.progressToken` receive concise live MCP progress notifications. - Updates for one request remain strictly ordered before its final response, while different - requests may interleave; clients should use distinct tokens for concurrently active requests. - Without a token, fast broker-backed Lean operations, feedback collection, and workspace drops stay - quiet; if one enters Lake setup or remains pending for two seconds, it emits at most one structured - `beam.status` log with the request id and a progress-token discovery hint when the active legacy or - per-request modern log policy admits `notice`. Other local MCP tools do not receive this watchdog. -- MCP `notifications/cancelled` cooperatively cancels active broker work. Lazy runtime creation and - workspace eviction remain serialized. Once admitted, `lean_drop_workspace` ignores client - cancellation and returns its terminal result because partial eviction cannot be rolled back - safely. Previously admitted calls drain first; later calls wait for eviction to finish and may - recreate the same descriptor. -- MCP JSON-RPC envelopes, `tools/call` parameters, and broker operation fields are closed at their - current protocol boundaries; undeclared or operation-irrelevant fields are rejected rather than - ignored. MCP `_meta` remains open for protocol-defined metadata. -- Incremental Lean diagnostics are forwarded as `lean.diagnostic` MCP log notifications. Recognized - Lake setup/build observations use `beam.status` or tokened progress instead. +- MCP `2026-07-28` is the preferred protocol. Initialization-based `2025-11-25` remains an explicit + transition target; older revisions are not advertised or tested. +- Workspace-bound calls require an explicit local descriptor. Dropping a workspace invalidates its + proof handles; a later request recreates the runtime lazily. +- Lazy runtime creation and workspace eviction remain serialized even though ordinary tool calls + can run concurrently. - The Streamable HTTP bridge is test-only; the product entry point remains stdio. -- Exact protocol behavior and conformance notes live in [MCP.md](MCP.md). +- Exact concurrency, cancellation, progress, logging, annotation, and closed-schema behavior lives + in [MCP.md](MCP.md). ### Sync, Save, And Staleness -- Zero-build `lean-beam save` helps checkpoint one module, but it is not a whole-workspace freshness - solution. Structured Lake options, dynamic libraries, and plugins are supported when the Lean file - worker has already applied them; batch-only `moreLeanArgs` fail with `saveUnsupportedSetup`. +- A zero-build checkpoint covers one module; it is not whole-workspace freshness evidence. +- Structured Lake options, dynamic libraries, and plugins are supported when the Lean file worker + has already applied them. Batch-only `moreLeanArgs` fail with `saveUnsupportedSetup`. - Beam does not detect Lake workspace configuration changes during a running Lean session. After - editing a lakefile, manifest, package override, `lean-toolchain`, Lean options, plugins, or dynamic - libraries, run `lean-beam shutdown` before the next command that uses the Lean server; - `lean-beam refresh` does not restart the server. -- A Beam checkpoint contains the Lean server's accepted environment. Elaborators can - distinguish server execution from batch execution, so exceptional custom elaboration can produce - an artifact that differs from a fresh `lake build` artifact. Successful checkpoints are normally - sufficient during local development. Final batch evidence should come from a clean CI `lake build`; - if no successful clean CI result is available, run the one-time local batch-validation sequence in + changing a lakefile, manifest, package override, toolchain, Lean options, plugins, or dynamic + libraries, run `lean-beam shutdown` before the next server command. +- A checkpoint captures the Lean server's accepted environment. Final batch evidence should come + from a clean CI `lake build`, or from the one-time local batch-validation sequence documented in [SYNC_AND_DIAGNOSTICS.md](SYNC_AND_DIAGNOSTICS.md#development-checkpoints-and-batch-validation). -- If you edit a dependency of the target file, downstream speculative results should be treated as - stale until rebuild or checkpoint. -- For open files in Lake workspaces, Beam uses Lean's native stale-dependency diagnostic when a synced - source change makes an importer need refresh. Beam does not yet implement Lean's dynamic watched-file - registration, so external source changes that never pass through `sync` remain outside the current - watcher surface. -- `error.data.staleDirectDeps` recovery hints are still broker-derived metadata. Beam currently - uses direct imports returned by Beam's diagnostics barrier request from Lean's accepted header - snapshot and combines those imports with broker sync/save history to infer stale direct - dependencies and `needsSave`. The planned Lean-side backlog item is to expose structured - stale-dependency metadata from Lean's watchdog/file-worker - path, so Beam can derive these hints from Lean instead of duplicating that state in the broker. - -### Distribution And Rocq - -- Agent-skill distribution currently relies on a local checkout and local install script; it is not - yet published through a registry or marketplace flow. -- Rocq support is currently limited to goal inspection through `coq-lsp`; it is not yet a full - stateful execution layer. +- Editing a dependency can make downstream speculative results stale until rebuild or checkpoint. + Beam does not yet implement Lean's dynamic watched-file registration for source changes that never + pass through Beam synchronization. +- Some stale-dependency recovery hints remain broker-derived rather than coming directly from + Lean's native watchdog and file-worker state. + +### Rocq + +- Rocq support is limited to goal inspection through `coq-lsp`. +- Rocq does not expose a corresponding sync, save, or speculative execution layer through Beam. ## Direction -Near-term work is mostly about hardening and simplifying: - -- keep the base `runAt` request small -- preserve strict per-request isolation -- reduce packaging and workspace rough edges -- publish a smoother distribution path, likely GitHub-backed install for Codex and plugin - marketplace packaging for Claude -- improve stale-dependency handling, especially by moving structured stale-dependency metadata into - Lean's native stale-dependency signal instead of broker-side reconstruction -- upstream structured JSON-RPC error data for Lean request failures, so plugin-level - `contentModified` errors can carry machine-readable recovery fields such as - `documentVersionMismatch` without requiring broker-side preflight rejection -- replace broker-side diagnostics/fileProgress barrier inference with a stronger backend-facing - readiness primitive, so `lean-beam sync` / `lean-beam save` can trust one authoritative completion - signal instead of reconstructing barrier completeness from multiple LSP channels -- track an upstream Lean API improvement for a pure frontend readiness/reporting helper, close to - `SnapshotTree.runAndReport` but returning the build-blocking decision and message counts without - printing -- add richer MCP progress percentages or bounded work-unit totals if Lean exposes them; keep - structured MCP log messages for incremental diagnostics rather than overloading progress - notifications or the final tool result -- keep the `sync`, `refresh`, `save`, and `close-save` projections aligned as the canonical - sync-result schema evolves -- keep Beam-daemon-side conveniences useful without turning them into a large public surface too early -- add a short comparison against Pantograph in the docs, to clarify where `runAt` fits among nearby Lean tooling -- keep cross-surface utility code such as root resolution and workspace-relative path derivation in - shared Beam modules, not copied across CLI, broker, MCP, and test helpers - -## First Alpha Release Focus - -The first public Lean release should stay conservative: - -- keep the current `runAt`, `lean-beam`, and MCP surfaces small and documented +The current focus is to stabilize the small public surface into dependable agent tooling for daily +Lean work and prepare it for distribution with Lean: + +- keep the base `runAt` request small, typed, and isolated - keep CLI and MCP as thin projections over shared typed operation adapters -- keep supported Lean-toolchain and install behavior covered in CI -- take stability fixes when they materially improve release confidence -- defer broader dependency/readiness redesigns until Lean or Lake expose stronger primitives +- reduce packaging, installation, and workspace rough edges +- improve dependency freshness and readiness using stronger Lean- or Lake-owned signals when they + become available +- keep daemon conveniences useful without expanding the public API prematurely +- continue exercising Beam in real agent workflows and harden the failures those workflows expose