doc: improve README first-reader flow

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<br/>request routing<br/>session ownership"]
+  subgraph runtime["Beam broker"]
+    broker["request routing<br/>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).
 

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

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