MCP server: "Cannot read LSP message: Stream was closed" on every request; CLI path works (v0.2.0-beta)

[spitters]

MCP server: "Cannot read LSP message: Stream was closed" on every request; CLI path works

• server: lean-beam-mcp 0.2.0-beta (commit 0bc94e6d9af2), MCP protocol 2026-07-28
• project toolchain: leanprover/lean4:v4.30.0 (exact-validated), bundle ready
• file to: https://github.com/ejgallego/lean-beam/issues

Summary

The lean-beam-mcp server fails on the first workspace-bound request for any file with
internalError "Cannot read LSP message: Stream was closed". The identical operation via the
lean-beam CLI on the same workspace/file succeeds. So the daemon, plugin, and v4.30.0 bundle
are functional; only the MCP-server code path cannot hold its Lean LSP connection.

Root cause signal (from beam_feedback_report collected stats)

stats.byBackend.lean: requestCount: 5, errorCount: 5, successCount: 0, sessionStarts: 0, sessionRestarts: 0, workerExitedCount: 0; openFiles.sessions.lean.active: false.

The Lean backend session never starts (sessionStarts: 0, no worker ever exits) — so every
workspace-bound request hits an absent/closed stream. The MCP broker's session-start path is
broken, whereas the CLI daemon does start a Lean session. .beam/beam-daemon-startup.log is empty
(no spawn diagnostic captured).

Reproduction

1. install-beam.sh --dont-ask --toolchain leanprover/lean4:v4.30.0 --claude --claude-mcp.
2. lean-beam doctor: bundle ready: true, daemon starts live, incidents none.
3. CLI works: lean-beam ensure then lean-beam update <file> → {"ok":true,"result":{"version":1,"changed":true}}.
4. MCP fails: lean_update {path:<file>, workspace:{root:<project>}} → internalError "Cannot read LSP message: Stream was closed".
5. Reproduced with no MCP client via the wrapper: lean-beam-mcp --self-check <file> → same error (its internal lean_sync).

Ruled out as causes: file weight (fails on a trivial 3-line no-import file and on a large
import-closure file alike); root/daemon contention (fails with the CLI daemon shut down, root clean);
environment (fails under the MCP client env and under a login shell with elan/lean on PATH); daemon
liveness (fails whether or not lean-beam ensure ran first). beam_version/beam_stats succeed
(no workspace binding), so the MCP transport is up; only workspace-bound requests that must drive the
Lean LSP fail.

Expected

lean_update / lean_sync return a document version (as the CLI lean-beam update does).

Impact

The MCP surface — the agent/tool-facing half — is unusable; only the CLI works. Agents drive Lean
through the MCP tools, so Beam cannot be adopted for the intended agent workflow until this is fixed.

Workaround

Use the lean-beam CLI (update/goals/hover), which starts and holds the Lean session; the MCP
path does not.

[GZGavinZhao]

Finally manage to extract the output from beam_feedback:

Details

MCP lean worker crashes: spawned without LD_LIBRARY_PATH, beam plugin cannot load libLake_shared.so

Summary

Every workspace-bound MCP tool fails with internalError: Cannot read LSP message: Stream was closed. Root cause (confirmed at syscall level): lean-beam-mcp spawns Lean worker as lean --server --plugin=<beam bundle>/libbeam_Beam_LSP.so -Dexperimental.module=true without LD_LIBRARY_PATH, so dlopen of plugin fails on NEEDED libLake_shared.so and lean exits 1. beam-daemon builds and sets LD_LIBRARY_PATH for workers, MCP broker does not. Not caused by project .envrc (only LEAN_CC/LEAN_AR). With LD_LIBRARY_PATH exported, crash disappears but sync still ends in syncBarrierIncomplete.

• Kind: bug
• Severity: high
• Tags: mcp, worker-spawn, ld-library-path

Beam Runtime

• generated at: 2026-08-24T22:38:18Z
• server: lean-beam-mcp 0.2.0-beta
• MCP protocol: 2025-11-25
• active root: ~/CS/Lean/veir
• runtime active: false
• runtime current: true
• source: commit a5fc58482700
• daemon registry pid: not alive
• daemon endpoint: tcp://127.0.0.1:37730

Collection warnings:

• Beam daemon registry pid is not alive while a registry endpoint is recorded; stats/open-files may come from a live endpoint with stale registry metadata. Run lean-beam shutdown, then lean-beam ensure from the project root to refresh daemon registry state.
• no active MCP Lean runtime was available for stats/open-files

Reproduction

1. cd ~/CS/Lean/veir (leanprover/lean4:v4.32.2)
2. Call any workspace-bound MCP tool e.g. lean_sync on Veir/Printer.lean -> internalError Stream was closed
3. Shell repro: echo '...' | lean --server --plugin=$BEAM_BUNDLE/libbeam_Beam_LSP.so -Dexperimental.module=true fails with 'error loading library, libLake_shared.so' unless LD_LIBRARY_PATH includes toolchain lib/lean
4. Built-in repro: lean-beam-mcp --self-check Veir/Printer.lean fails same way
5. With LD_LIBRARY_PATH exported, self-check progresses past crash but reports syncBarrierIncomplete
   Confirm: daemon lean worker has LD_LIBRARY_PATH set, MCP worker does not (checked /proc/*/environ and strace execve).

Expected Behavior

MCP-spawned Lean worker should set LD_LIBRARY_PATH like beam-daemon does (lean toolchain lib/lean + lib plus project .lake/build/lib dirs) before exec, or launch via beam-daemon. lean_sync should then complete diagnostics barrier (saveReady true).

Actual Behavior

MCP spawns lean directly as child (zombie [lean] children of lean-beam-mcp, strace execve with 134 vars, zero LD_LIBRARY_PATH). libbeam_Beam_LSP.so has no RUNPATH, NEEDED libLake_shared.so in /lib/lean not on default loader path, lean exits 1. Every MCP tool fails Stream was closed. With LD_LIBRARY_PATH, worker starts but sync ends syncBarrierIncomplete (fileProgress done=false rangeEndLine 468, no blocking diagnostics); strace shows worker publishDiagnostics write gets EPIPE after broker closure.

Beam Debug Context

{
  "daemon": {
    "recentDaemonIncidents": [],
    "registry": {
      "bundleId": "12976783265816896148",
      "clientBin": "~/.local/share/beam/state/install-bundles/linux-x86_64/12976783265816896148/workspace/.lake/build/bin/beam-client",
      "configHash": "9028405053784680601",
      "daemonBin": "~/.local/share/beam/state/install-bundles/linux-x86_64/12976783265816896148/workspace/.lake/build/bin/beam-daemon",
      "daemonId": "902840505378-260470",
      "leanCmd": "~/.elan/toolchains/leanprover--lean4---v4.32.2/bin/lean",
      "pid": 260470,
      "pidNamespace": "pid:[4026531836]",
      "plugin": "~/.local/share/beam/state/install-bundles/linux-x86_64/12976783265816896148/workspace/.lake/build/lib/libbeam_Beam_LSP.so",
      "port": 37730,
      "root": "~/CS/Lean/veir",
      "startedAt": "2026-08-20T15:15:25Z",
      "toolchain": "leanprover/lean4:v4.32.2"
    },
    "registryEndpoint": "tcp://127.0.0.1:37730",
    "registryPath": "~/CS/Lean/veir/.beam/beam-daemon.json",
    "registryPidStatus": "not alive"
  },
  "identity": {
    "version": "0.2.0-beta",
    "active_root": "~/CS/Lean/veir",
    "beam_cli": "~/.local/share/beam/versions/0a99cf01b161b6f4a3294debdbd39e789ab0b149347bf11b4de8c3b13d70f72e/libexec/beam-cli",
    "beam_home": "~/.local/share/beam/versions/0a99cf01b161b6f4a3294debdbd39e789ab0b149347bf11b4de8c3b13d70f72e",
    "manifest": "~/.local/share/beam/versions/0a99cf01b161b6f4a3294debdbd39e789ab0b149347bf11b4de8c3b13d70f72e/manifest.json",
    "mcp_protocol": "2025-11-25",
    "name": "lean-beam-mcp",
    "runtime_active": false,
    "runtime_current": true,
    "runtime_payload": "0a99cf01b161b6f4a3294debdbd39e789ab0b149347bf11b4de8c3b13d70f72e",
    "server_binary": "~/.local/share/beam/versions/0a99cf01b161b6f4a3294debdbd39e789ab0b149347bf11b4de8c3b13d70f72e/libexec/lean-beam-mcp",
    "source_commit": "a5fc58482700615e94eedfcc8aa4198688658623",
    "wrapper": "~/.local/share/beam/versions/0a99cf01b161b6f4a3294debdbd39e789ab0b149347bf11b4de8c3b13d70f72e/bin/lean-beam-mcp"
  },
  "openFiles": null,
  "stats": null
}

Collection warnings:

• Beam daemon registry pid is not alive while a registry endpoint is recorded; stats/open-files may come from a live endpoint with stale registry metadata. Run lean-beam shutdown, then lean-beam ensure from the project root to refresh daemon registry state.
• no active MCP Lean runtime was available for stats/open-files

The project that I'm working on is opencompl/veir though this is likely not a project-specific issue as @spitters is also hitting it.