From d35aaebe8714d1950bb0c845f5db6402a749e6e0 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 2 Sep 2026 22:29:00 +0200 Subject: [PATCH] docs: add architecture message-path diagrams --- README.md | 6 +- docs/ARCHITECTURE.md | 53 ++++++ docs/DEVELOPMENT.md | 2 + docs/architecture/configuration-flow.dot | 61 ++++++ docs/architecture/configuration-flow.svg | 177 ++++++++++++++++++ docs/architecture/message-paths.dot | 90 +++++++++ docs/architecture/message-paths.svg | 227 +++++++++++++++++++++++ 7 files changed, 612 insertions(+), 4 deletions(-) create mode 100644 docs/ARCHITECTURE.md create mode 100644 docs/architecture/configuration-flow.dot create mode 100644 docs/architecture/configuration-flow.svg create mode 100644 docs/architecture/message-paths.dot create mode 100644 docs/architecture/message-paths.svg diff --git a/README.md b/README.md index 71347925..b4953626 100644 --- a/README.md +++ b/README.md @@ -22,7 +22,6 @@ flowchart TB cliRuntime["ServerRuntime
single workspace"] cliAdapter --> cliRuntime end - shared["shared typed operations
admission + dispatch"] subgraph mcpOwner["MCP lifetime"] direction TB mcpAdapter["lean-beam-mcp
multiplexed stdio"] @@ -37,15 +36,14 @@ flowchart TB cli --> cliAdapter mcp --> mcpAdapter - cliRuntime -. uses .-> shared - mcpRuntime -. uses .-> shared cliRuntime -- Beam requests --> backends mcpRuntime -- Beam requests --> backends ``` Beam keeps the agent-facing surface small. The CLI and MCP paths share typed operations and broker runtime code, but each owns its transport and runtime lifetime. Those runtime instances own request -routing plus one or more Lean LSP sessions with the Beam plugin loaded. +routing plus one or more Lean LSP sessions with the Beam plugin loaded. See the +[architecture message paths](docs/ARCHITECTURE.md) for the complete component and lifetime flows. 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 diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md new file mode 100644 index 00000000..d404471d --- /dev/null +++ b/docs/ARCHITECTURE.md @@ -0,0 +1,53 @@ +# Beam Architecture + +Beam has two user-facing paths into the same typed Lean operations, but it does not share their +transport or lifetime coordination. The CLI owns a project session through a foreground +`lean-beam serve` process and a private daemon. The MCP server owns its broker runtime directly and +multiplexes calls over JSON-RPC on standard input and output. + +The diagrams in this document are generated from the adjacent Graphviz sources. Update and render +both forms together when a component or message path changes. From the repository root, run: + +```bash +dot -Tsvg docs/architecture/message-paths.dot -o docs/architecture/message-paths.svg +dot -Tsvg docs/architecture/configuration-flow.dot -o docs/architecture/configuration-flow.svg +``` + +## Message Paths + +[Open the rendered message-path diagram](architecture/message-paths.svg), or inspect its +[Graphviz source](architecture/message-paths.dot). + +![Beam message paths](architecture/message-paths.svg) + +The CLI session descriptor selects one generation and contains its TCP endpoint and capability. +An ordinary CLI operation reads that descriptor, verifies the daemon generation from the +same-connection greeting, and only then sends its capability-bound request. The foreground owner +alone creates the session and supervises normal shutdown. `status`, `stop`, and `recover` are +explicit lifecycle paths rather than Lean operations. + +The MCP process does not attach to the CLI daemon. It owns an in-process `ServerRuntime`, resolves +workspace descriptors from MCP tool arguments, and lazily owns the corresponding backend sessions. +CLI and MCP reuse operation and runtime implementation, but each arrow in the diagram belongs to a +separate runtime instance. + +## Backend Configuration Flow + +[Open the rendered configuration-flow diagram](architecture/configuration-flow.svg), or inspect +its [Graphviz source](architecture/configuration-flow.dot). + +![Beam backend configuration flow](architecture/configuration-flow.svg) + +`DesiredConfig` is the internal wrapper-session configuration. Every configured Lean backend owns +its command, plugin, toolchain, and bundle identity together. Temporary Rocq support is represented +as either an optional companion to Lean or the sole backend; an empty backend set and partial Lean +configuration cannot be constructed. + +The session configuration hash is a pure projection of `DesiredConfig`, not separately stored +derived state. The established field order remains stable while the value cannot disagree with the +root, backend set, or daemon binary from which it was computed. + +The option-heavy `WorkspaceBinding` remains a private descriptor and daemon-startup wire format. +It is produced only by lowering a complete `BackendSet`. This keeps protocol compatibility at the +edge without spreading independently optional Lean fields through configuration resolution, +hashing, daemon startup, and MCP setup output. diff --git a/docs/DEVELOPMENT.md b/docs/DEVELOPMENT.md index 543b9655..ba74dfa4 100644 --- a/docs/DEVELOPMENT.md +++ b/docs/DEVELOPMENT.md @@ -29,6 +29,8 @@ If the question is "how do I work on the repo safely and efficiently?", start he ## Code Organization +- [Architecture](ARCHITECTURE.md): rendered component message paths, runtime lifetimes, and wrapper + backend-configuration flow. - `Beam.LSP`: Lean LSP server plugin code, including the `$/lean/runAt` request for speculative execution at saved document positions. - `Beam`: shared broker, CLI, and MCP layer over Lean LSP plus Beam-specific extensions. diff --git a/docs/architecture/configuration-flow.dot b/docs/architecture/configuration-flow.dot new file mode 100644 index 00000000..9512950a --- /dev/null +++ b/docs/architecture/configuration-flow.dot @@ -0,0 +1,61 @@ +digraph BeamConfigurationFlow { + graph [ + rankdir=LR, + bgcolor="#ffffff", + fontname="sans-serif", + fontsize=18, + label="Wrapper backend configuration flow", + labelloc=t, + nodesep=0.45, + ranksep=0.75, + pad=0.2 + ]; + node [ + shape=box, + style="rounded,filled", + fillcolor="#f7f8fa", + color="#52606d", + fontname="sans-serif", + fontsize=11, + margin="0.16,0.10" + ]; + edge [color="#52606d", fontname="sans-serif", fontsize=9]; + + root [label="canonical project root"]; + required [label="required backend"]; + resolver [label="desiredConfig", fillcolor="#e8f1fb"]; + lean_resolve [label="resolve Lean bundle"]; + rocq_resolve [label="resolve temporary Rocq command"]; + lean_config [ + label="LeanBackendConfig\ncommand + plugin\ntoolchain + bundleId", + fillcolor="#e8f5eb" + ]; + rocq_config [label="RocqBackendConfig\ncommand", fillcolor="#e8f5eb"]; + backend_set [ + label="BackendSet\nnonempty and complete", + shape=hexagon, + fillcolor="#fff6db" + ]; + desired [ + label="DesiredConfig\nroot + backends + daemonBin", + fillcolor="#e8f1fb" + ]; + hash [label="derived configuration hash\nstable ordered fields"]; + args [label="daemon arguments"]; + binding [label="WorkspaceBinding\nprivate wire shape"]; + mcp_config [label="mcp-config output"]; + + root -> resolver; + required -> resolver; + resolver -> lean_resolve; + resolver -> rocq_resolve; + lean_resolve -> lean_config; + rocq_resolve -> rocq_config; + lean_config -> backend_set; + rocq_config -> backend_set; + backend_set -> desired; + desired -> hash; + desired -> args; + desired -> binding; + desired -> mcp_config; +} diff --git a/docs/architecture/configuration-flow.svg b/docs/architecture/configuration-flow.svg new file mode 100644 index 00000000..e543edfb --- /dev/null +++ b/docs/architecture/configuration-flow.svg @@ -0,0 +1,177 @@ + + + + + + +BeamConfigurationFlow + +Wrapper backend configuration flow + + +root + +canonical project root + + + +resolver + +desiredConfig + + + +root->resolver + + + + + +required + +required backend + + + +required->resolver + + + + + +lean_resolve + +resolve Lean bundle + + + +resolver->lean_resolve + + + + + +rocq_resolve + +resolve temporary Rocq command + + + +resolver->rocq_resolve + + + + + +lean_config + +LeanBackendConfig +command + plugin +toolchain + bundleId + + + +lean_resolve->lean_config + + + + + +rocq_config + +RocqBackendConfig +command + + + +rocq_resolve->rocq_config + + + + + +backend_set + +BackendSet +nonempty and complete + + + +lean_config->backend_set + + + + + +rocq_config->backend_set + + + + + +desired + +DesiredConfig +root + backends + daemonBin + + + +backend_set->desired + + + + + +hash + +derived configuration hash +stable ordered fields + + + +desired->hash + + + + + +args + +daemon arguments + + + +desired->args + + + + + +binding + +WorkspaceBinding +private wire shape + + + +desired->binding + + + + + +mcp_config + +mcp-config output + + + +desired->mcp_config + + + + + diff --git a/docs/architecture/message-paths.dot b/docs/architecture/message-paths.dot new file mode 100644 index 00000000..0d807f8b --- /dev/null +++ b/docs/architecture/message-paths.dot @@ -0,0 +1,90 @@ +digraph BeamMessagePaths { + graph [ + rankdir=LR, + bgcolor="#ffffff", + fontname="sans-serif", + fontsize=18, + label="Beam message paths", + labelloc=t, + nodesep=0.55, + ranksep=0.75, + pad=0.2 + ]; + node [ + shape=box, + style="rounded,filled", + fillcolor="#f7f8fa", + color="#52606d", + fontname="sans-serif", + fontsize=11, + margin="0.16,0.10" + ]; + edge [color="#52606d", fontname="sans-serif", fontsize=9]; + + subgraph cluster_callers { + label="Callers"; + color="#9fb3c8"; + style="rounded,dashed"; + human [label="Human or agent shell"]; + mcp_client [label="MCP client / agent"]; + { rank=same; human; mcp_client; } + } + + subgraph cluster_cli { + label="CLI-owned project session"; + color="#3e7cb1"; + style="rounded"; + wrapper [label="scripts/lean-beam\nruntime discovery", fillcolor="#e8f1fb"]; + cli [label="beam-cli\ncommands and foreground owner", fillcolor="#e8f1fb"]; + descriptor [ + label="private session descriptor\ngeneration + endpoint + capability", + shape=cylinder, + style="filled", + fillcolor="#fff6db" + ]; + daemon [label="beam-daemon\nTCP transport", fillcolor="#e8f1fb"]; + cli_runtime [label="ServerRuntime\nfrozen project workspace", fillcolor="#e8f1fb"]; + + wrapper -> cli [label="exec"]; + cli -> daemon [ + label="serve: spawn + owner pipe\nconnect + capability-bound operation\nauthenticated stop\ninterrupt: close connection" + ]; + daemon -> cli [ + label="typed ready message\nServerHello: generation identity\nprogress, diagnostics, response" + ]; + cli -> descriptor [ + label="publish / read lifecycle state\nordinary call: select session", + dir=both + ]; + daemon -> cli_runtime; + } + + subgraph cluster_mcp { + label="MCP-owned multi-workspace session"; + color="#7a5195"; + style="rounded"; + mcp [label="lean-beam-mcp\nJSON-RPC stdio transport", fillcolor="#f1eafa"]; + projection [label="MCP tool projection\nworkspace selection", fillcolor="#f1eafa"]; + mcp_runtime [label="ServerRuntime\nlazy workspace cache", fillcolor="#f1eafa"]; + + mcp -> projection [label="tool call / result", dir=both]; + projection -> mcp_runtime [label="typed operation / result", dir=both]; + mcp -> mcp_runtime [label="cancel notification", style=dashed]; + } + + subgraph cluster_backends { + label="Workspace backends"; + color="#4c956c"; + style="rounded"; + lean [label="Lean language server\nBeam LSP plugin", fillcolor="#e8f5eb"]; + rocq [label="coq-lsp\ntemporary Rocq path", fillcolor="#e8f5eb"]; + { rank=same; lean; rocq; } + } + + human -> wrapper; + mcp_client -> mcp [label="JSON-RPC stdio", dir=both]; + cli_runtime -> lean [label="LSP requests and notifications", dir=both]; + cli_runtime -> rocq [label="goal probes", dir=both]; + mcp_runtime -> lean [label="LSP requests and notifications", dir=both]; + mcp_runtime -> rocq [label="goal probes", dir=both]; +} diff --git a/docs/architecture/message-paths.svg b/docs/architecture/message-paths.svg new file mode 100644 index 00000000..8a66b2b6 --- /dev/null +++ b/docs/architecture/message-paths.svg @@ -0,0 +1,227 @@ + + + + + + +BeamMessagePaths + +Beam message paths + +cluster_callers + +Callers + + +cluster_cli + +CLI-owned project session + + +cluster_mcp + +MCP-owned multi-workspace session + + +cluster_backends + +Workspace backends + + + +human + +Human or agent shell + + + +wrapper + +scripts/lean-beam +runtime discovery + + + +human->wrapper + + + + + +mcp_client + +MCP client / agent + + + +mcp + +lean-beam-mcp +JSON-RPC stdio transport + + + +mcp_client->mcp + + + +JSON-RPC stdio + + + +cli + +beam-cli +commands and foreground owner + + + +wrapper->cli + + +exec + + + +descriptor + + +private session descriptor +generation + endpoint + capability + + + +cli->descriptor + + + +publish / read lifecycle state +ordinary call: select session + + + +daemon + +beam-daemon +TCP transport + + + +cli->daemon + + +serve: spawn + owner pipe +connect + capability-bound operation +authenticated stop +interrupt: close connection + + + +daemon->cli + + +typed ready message +ServerHello: generation identity +progress, diagnostics, response + + + +cli_runtime + +ServerRuntime +frozen project workspace + + + +daemon->cli_runtime + + + + + +lean + +Lean language server +Beam LSP plugin + + + +cli_runtime->lean + + + +LSP requests and notifications + + + +rocq + +coq-lsp +temporary Rocq path + + + +cli_runtime->rocq + + + +goal probes + + + +projection + +MCP tool projection +workspace selection + + + +mcp->projection + + + +tool call / result + + + +mcp_runtime + +ServerRuntime +lazy workspace cache + + + +mcp->mcp_runtime + + +cancel notification + + + +projection->mcp_runtime + + + +typed operation / result + + + +mcp_runtime->lean + + + +LSP requests and notifications + + + +mcp_runtime->rocq + + + +goal probes + + +