refactor: remove the embedded MCP self-check

Beam/Mcp/Application.lean

@@ -6,7 +6,6 @@ Author: Emilio J. Gallego Arias
 
 import Beam.Mcp.Options
 import Beam.Mcp.StdioServer
-import Beam.Mcp.SelfCheck
 import Beam.Installation.Lookup
 
 namespace Beam.Mcp.Application
@@ -45,8 +44,6 @@ def main (args : List String) : IO Unit := do
   if opts.showVersion then
     IO.println (← readIdentity installation).text
     return
-  match opts.selfCheckPath? with
-  | some path => SelfCheck.run path
-  | none => Server.runStdio (serverOptions installation)
+  Server.runStdio (serverOptions installation)
 
 end Beam.Mcp.Application

Beam/Mcp/Options.lean

@@ -7,29 +7,22 @@ Author: Emilio J. Gallego Arias
 namespace Beam.Mcp
 
 structure Options where
-  selfCheckPath? : Option String := none
   showVersion : Bool := false
 
 def usage : String :=
   String.intercalate "\n" [
     "usage: lean-beam-mcp",
-    "       lean-beam-mcp --self-check <lean-file>",
     "       lean-beam-mcp --version",
     "",
     "Runs the experimental Lean Beam MCP server over newline-delimited JSON-RPC on stdio.",
     "Every workspace-bound tool call carries {\"workspace\":{\"root\":\"/absolute/project\"}}.",
-    "--self-check starts a child MCP server and calls lean_sync for the current Lean project.",
-    "Self-check uses one best-effort probe timeout of 120000 ms; override with LEAN_BEAM_MCP_SELF_CHECK_TIMEOUT_MS.",
-    "This setting does not bound total command duration; blocking I/O and cleanup may outlast it.",
     "--version prints the MCP server version, protocol revision, and available resolved identity paths.",
     "Runtime components come exclusively from this installation's recorded target set.",
     "Only curated Lean tools are exposed; raw LSP and broker escape hatches are intentionally absent."
   ]
 
 partial def parseOptions (opts : Options) : List String → Except String Options
   | [] => pure opts
-  | "--self-check" :: path :: rest =>
-      parseOptions { opts with selfCheckPath? := some path } rest
   | "--version" :: rest =>
       parseOptions { opts with showVersion := true } rest
   | "-h" :: _ | "--help" :: _ =>

CHANGELOG.md

@@ -37,6 +37,8 @@ This project keeps a lightweight, reverse-chronological changelog. Dates use `YY
 
 ### Removed
 
+- Remove `lean-beam-mcp --self-check`. Verify the configured MCP client with a normal `lean_sync`
+  call; installed and native stdio smoke tests run through the external test harness.
 - Move Rocq goal probes, agent skill, and `coq-lsp` setup to the independent `rocq-beam` project.
   Lean Beam no longer accepts Rocq broker requests, `serve rocq`, or `--rocq-skill`.
 - Remove the redundant backend selector from broker requests and continuation handles. CLI commands

docs/DEVELOPMENT.md

@@ -242,13 +242,16 @@ The executable path is split into importable modules:
 - [Beam/Mcp/Protocol.lean](../Beam/Mcp/Protocol.lean): current MCP JSON-RPC helpers
 - [Beam/Mcp/Options.lean](../Beam/Mcp/Options.lean): executable options and usage
 - [Beam/Mcp/Application.lean](../Beam/Mcp/Application.lean): installation-owned runtime admission
-- [Beam/Mcp/SelfCheck.lean](../Beam/Mcp/SelfCheck.lean): installed-wrapper self-check
 - [Beam/Mcp/Server.lean](../Beam/Mcp/Server.lean): descriptor resolution, lazy runtime dispatch, and
   the synchronous protocol-test seam
 - [Beam/Mcp/StdioServer.lean](../Beam/Mcp/StdioServer.lean): permanent stdin reader, concurrent
   coordination, cancellation, cache-control barriers, and serialized output
 - [Beam/Mcp/ServerMain.lean](../Beam/Mcp/ServerMain.lean): executable entry point
 
+Installed and relocated native executable checks use the external `McpClient` in
+`tests/test-mcp-stdio.py`, via `tests/lib/installed-mcp-smoke.py`. Keep client conversation and
+integration-test process supervision outside the server executable.
+
 Keep these stdio invariants explicit:
 
 - only `runStdio` reads stdin
@@ -835,6 +838,13 @@ keep artifact caches local to each build workspace. The save/checkpoint regressi
 suite uses separate fixture packages and disables their artifact caches so a Lake replay cannot
 masquerade as a Beam-written artifact.
 
+Lake may hard-link executables to its artifact cache. On macOS, dyld can identify that inode by its
+cache path, so a raw cached frontend may fail to find its sibling `lib/lean` libraries. Construction
+and native packaging copy executables into independent files before running them. The application
+startup regression uses that boundary; its cache-linked input simulates the hardlink layout rather
+than running Lake's cache save/restore cycle. See [the application test coverage](TESTING.md#beam-surface)
+for its discovery checks. Do not modify a cache-linked build output in place.
+
 CI restores the artifact cache for every Lean job. In combined macOS mode, `beam-fast` writes the
 Linux cache and `macos-platform` writes the macOS cache. With `BEAM_FULL_MACOS_CI=true`, the
 `beam-fast` matrix writes both.

docs/MCP.md

@@ -208,13 +208,16 @@ request dispatcher and runtime teardown boundary.
   runtime description on reuse. It uses the installation adapter directly.
 - [Beam/Version.lean](../Beam/Version.lean) holds pure identity data and rendering; installation
   discovery belongs to the application adapters.
-- [Beam/Mcp/SelfCheck.lean](../Beam/Mcp/SelfCheck.lean) owns the installed-wrapper self-check.
 - [Beam/Mcp/Server.lean](../Beam/Mcp/Server.lean) owns descriptor resolution, lazy broker-runtime
   access, the typed protocol-family state machine, and the synchronous protocol-test seam. Runtime
   resolution and process identity are supplied as explicit application effects. The broker runtime
   is authoritative for workspace state.
 - [Beam/Mcp/StdioServer.lean](../Beam/Mcp/StdioServer.lean) owns the permanent stdin reader,
   concurrent coordination, cancellation, cache-control barriers, and serialized output.
+- [tests/lib/installed-mcp-smoke.py](../tests/lib/installed-mcp-smoke.py) verifies installed and
+  native executables through the shared external stdio client in
+  [tests/test-mcp-stdio.py](../tests/test-mcp-stdio.py). Process supervision for this integration
+  check belongs to the test harness.
 
 ## Public Tools
 

docs/SETUP.md

@@ -381,27 +381,20 @@ opencode mcp add
 
 ### Verify The MCP Server
 
-To verify the installed MCP path without writing JSON-RPC by hand, change to the Lean project.
-Use the same absolute MCP command you registered above:
+After registering the server, use your client's MCP tools to call `lean_sync` for an existing
+Lean file. Supply the absolute project root in `workspace` and the file path relative to that root,
+as shown below. The project's Lean target must already belong to the installed component set.
+A successful call verifies the configured client, stdio transport, runtime selection, and Lean
+request path together. The returned `document_progress` describes elaboration progress; success
+does not require `done: true`, a file without Lean diagnostics, or readiness to save artifacts.
+
+For executable and installation identity, run:
 
 ```bash
-cd /path/to/lean/project
-"/absolute/path/to/lean-beam-mcp" --self-check MyPkg/Sub/Module.lean
+"/absolute/path/to/lean-beam-mcp" --version
 ```
 
-The self-check starts a child MCP server, calls `lean_sync` with an explicit descriptor for the
-current project, and shuts the child server down. The project target must already be a member of
-the installed component set; the self-check does not construct missing runtimes. Success requires valid discovery and sync
-responses and a zero server exit status. It verifies that sync can run, without requiring completed
-elaboration, a file without Lean diagnostics, or readiness to save artifacts. Server stderr is
-diagnostic: logging does not fail an otherwise successful check, and failures include the final
-64 KiB of captured stderr when available.
-The smoke test uses one best-effort timeout for discovery, sync, and shutdown, including stderr
-draining; notifications do not restart it. Process creation and failure cleanup are outside that
-budget, and blocked I/O tasks can delay process exit. If a very slow machine needs a longer wait,
-set `LEAN_BEAM_MCP_SELF_CHECK_TIMEOUT_MS` to a positive timeout in milliseconds (default 120000).
-CI supervises the command with a separate process watchdog. Maintainer details
-for MCP live in the [MCP maintainer notes](MCP.md).
+This reports identity and runtime paths without starting Lean or sending a tool request.
 
 ### Workspaces And Server Identity
 

docs/STATUS.md

@@ -67,8 +67,6 @@ Pre-stable compatibility policy lives in [Compatibility Policy](COMPATIBILITY.md
   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 <lean-file>` 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