fix: improve startup and feedback diagnostics

Beam/Broker/Server.lean

@@ -38,9 +38,55 @@ namespace Beam.Broker
 abbrev brokerStdio : IO.Process.StdioConfig where
   stdin := .piped
   stdout := .piped
-  -- Keep backend stderr away from MCP stdio. Inheriting it can corrupt
-  -- client framing; piping and draining it caused macOS save_olean hangs.
-  stderr := .null
+  -- Keep backend stderr away from MCP stdio while retaining a bounded tail for
+  -- startup and worker-exit diagnostics. The blocking drain runs on a dedicated
+  -- task so it cannot starve regular Lean tasks.
+  stderr := .piped
+
+private def backendStderrTailLimit : Nat :=
+  16 * 1024
+
+private def backendStderrReadSize : USize :=
+  4096
+
+private def isUtf8ContinuationByte (byte : UInt8) : Bool :=
+  decide (128 ≤ byte.toNat ∧ byte.toNat < 192)
+
+private def utf8BoundaryAtOrAfter (bytes : ByteArray) (offset : Nat) : Nat :=
+  let rec loop (offset : Nat) : Nat → Nat
+    | 0 => offset
+    | fuel + 1 =>
+        if h : offset < bytes.size then
+          if isUtf8ContinuationByte bytes[offset] then
+            loop (offset + 1) fuel
+          else
+            offset
+        else
+          offset
+  loop offset 3
+
+structure BackendStderrCapture where
+  tail : Std.Mutex ByteArray
+  drainTask : Task (Except IO.Error Unit)
+
+private partial def drainBackendStderr
+    (stderr : IO.FS.Handle)
+    (tail : Std.Mutex ByteArray) : IO Unit := do
+  let chunk ← stderr.read backendStderrReadSize
+  unless chunk.isEmpty do
+    tail.atomically do
+      let combined := (← get) ++ chunk
+      if combined.size > backendStderrTailLimit then
+        let start := utf8BoundaryAtOrAfter combined (combined.size - backendStderrTailLimit)
+        set <| combined.extract start combined.size
+      else
+        set combined
+    drainBackendStderr stderr tail
+
+def startBackendStderrCapture (stderr : IO.FS.Handle) : IO BackendStderrCapture := do
+  let tail ← Std.Mutex.new ByteArray.empty
+  let drainTask ← IO.asTask (prio := Task.Priority.dedicated) <| drainBackendStderr stderr tail
+  pure { tail, drainTask }
 
 structure Session where
   workspaceId : WorkspaceId
@@ -51,6 +97,7 @@ structure Session where
   proc : IO.Process.Child brokerStdio
   stdin : IO.FS.Stream
   stdout : IO.FS.Stream
+  stderrCapture : BackendStderrCapture
   pending : PendingRequestStore
   nextId : Nat := 1
   nextEventSeq : Nat := 1
@@ -155,6 +202,31 @@ private partial def waitForTaskWithTimeout
     loop (remainingMs - min pollMs remainingMs)
   loop timeoutMs
 
+private def backendName : Backend → String
+  | .lean => "Lean"
+  | .rocq => "Rocq"
+
+private def BackendStderrCapture.snapshot (capture : BackendStderrCapture) : IO String := do
+  let bytes ← capture.tail.atomically get
+  pure <| (String.fromUTF8? bytes).getD "<backend stderr tail is not valid UTF-8>"
+
+private def BackendStderrCapture.awaitDrain
+    (capture : BackendStderrCapture)
+    (timeoutMs : Nat := 500) : IO Unit := do
+  discard <| waitForTaskWithTimeout capture.drainTask timeoutMs
+
+private def backendFailureMessage
+    (backend : Backend)
+    (phase cause : String)
+    (capture : BackendStderrCapture) : IO String := do
+  let stderr := (← capture.snapshot).trimAscii.toString
+  let stderr := if stderr.isEmpty then "<empty>" else stderr
+  pure <| String.intercalate "\n" [
+    s!"{backendName backend} backend failed {phase}: {cause}",
+    s!"backend stderr tail (last {backendStderrTailLimit} bytes):",
+    stderr
+  ]
+
 private def sessionShutdownReplyTimeoutMs : Nat :=
   1000
 
@@ -209,6 +281,25 @@ private def terminateBackendProcess (proc : IO.Process.Child brokerStdio) : IO U
   catch _ =>
     pure ()
 
+private def startBackendStderrCaptureOrTerminate
+    (backend : Backend)
+    (proc : IO.Process.Child brokerStdio) : IO BackendStderrCapture := do
+  try
+    startBackendStderrCapture proc.stderr
+  catch err =>
+    terminateBackendProcess proc
+    throw <| IO.userError <|
+      s!"{backendName backend} backend failed during startup before stderr capture: {err}"
+
+private def terminateBackendFailure
+    (backend : Backend)
+    (phase cause : String)
+    (proc : IO.Process.Child brokerStdio)
+    (capture : BackendStderrCapture) : IO String := do
+  terminateBackendProcess proc
+  capture.awaitDrain
+  backendFailureMessage backend phase cause capture
+
 private def sessionExited (session : Session) : IO Bool := do
   try
     pure (← session.proc.tryWait).isSome
@@ -453,11 +544,13 @@ partial def sessionReaderLoop (session : Session) : IO Unit := do
         pure ()
     sessionReaderLoop session
   catch e =>
+    let message ←
+      terminateBackendFailure session.backend "after startup" e.toString
+        session.proc session.stderrCapture
     PendingRequestStore.failAll session.pending <| BrokerFailure.toResponseFailure {
       code := .workerExited
-      message := e.toString
+      message
     }
-    terminateBackendProcess session.proc
 
 private def startRequestJsonTrackedDetailed
     (session : Session)
@@ -589,6 +682,7 @@ private def acquireBackendSession
     env := env
     cwd := root.toString
   }
+  let stderrCapture ← startBackendStderrCaptureOrTerminate backend proc
   let (session, initializeTask) ←
     try
       let stdin := IO.FS.Stream.ofHandle proc.stdin
@@ -604,6 +698,7 @@ private def acquireBackendSession
         proc
         stdin
         stdout
+        stderrCapture
         pending
       }
       writeLspRequest stdin
@@ -613,8 +708,8 @@ private def acquireBackendSession
         awaitInitializeResponse stdout
       pure (session, initializeTask)
     catch err =>
-      terminateBackendProcess proc
-      throw err
+      throw <| IO.userError <| ←
+        terminateBackendFailure backend "during startup" err.toString proc stderrCapture
   try
     match ← waitForTaskWithTimeout initializeTask backendInitializeTimeoutMs with
     | some (.ok ()) => pure ()
@@ -632,9 +727,10 @@ private def acquireBackendSession
     pure session
   catch err =>
     IO.cancel initializeTask
-    terminateBackendProcess proc
+    let message ←
+      terminateBackendFailure backend "during startup" err.toString proc stderrCapture
     discard <| waitForTaskWithTimeout initializeTask sessionShutdownReplyTimeoutMs
-    throw err
+    throw <| IO.userError message
 
 private def requireWorkspace (workspaceId : WorkspaceId) : M WorkspaceState := do
   let state ← get

Beam/Cli/Commands.lean

@@ -310,6 +310,8 @@ def runCommand (home : System.FilePath) (opts : CliOptions) : IO Unit := do
       printInstallLayout
   | "install-manifest" :: payloadHash :: sourceCommitArg :: createdWithToolchains =>
       printInstallManifest payloadHash sourceCommitArg createdWithToolchains
+  | "install-manifest-with-source-commit" :: manifestPath :: sourceCommitArg :: [] =>
+      printInstallManifestWithSourceCommit (System.FilePath.mk manifestPath) sourceCommitArg
   | "install-runtime-validate" :: path :: [] =>
       validateInstalledRuntimeForReuse (System.FilePath.mk path)
   | "mcp-config" :: [] =>

Beam/Cli/DaemonManager.lean

@@ -1205,9 +1205,10 @@ def withProjectDaemonOwner
   -- `.beam` state for a previously unseen toolchain.
   preparePrivateControlDir controlDir
   let desired ← desiredConfig home root backend
+  -- Allocate all fallible owner bookkeeping before the child and registry generation exist.
+  let exitCodeRef ← IO.mkRef (none : Option UInt32)
   let owned ← withProjectControl root (explicitControlDir? := some controlDir) fun control =>
     startOwnedProjectDaemon control desired backend opts
-  let exitCodeRef ← IO.mkRef (none : Option UInt32)
   try
     act {
         client := owned.client

Beam/Cli/Info.lean

@@ -217,17 +217,25 @@ def printCompatibleReleaseLines (home : System.FilePath) : IO Unit := do
 def printInstallLayout : IO Unit := do
   printJsonLine (toJson installLayout)
 
+private def sourceCommitArg? (sourceCommitArg : String) : Option String :=
+  if sourceCommitArg == "-" then none else some sourceCommitArg
+
 def printInstallManifest (payloadHash : String) (sourceCommitArg : String)
     (createdWithToolchains : List String) : IO Unit := do
   if createdWithToolchains.isEmpty then
     throw <| IO.userError
       "usage: beam install-manifest <payload-hash> <source-commit|-> <creation-toolchain...>"
-  let sourceCommit? :=
-    if sourceCommitArg == "-" then
-      none
-    else
-      some sourceCommitArg
-  printJsonLine (installManifestJson payloadHash sourceCommit? createdWithToolchains)
+  printJsonLine (installManifestJson payloadHash (sourceCommitArg? sourceCommitArg)
+    createdWithToolchains)
+
+def printInstallManifestWithSourceCommit
+    (manifestPath : System.FilePath)
+    (sourceCommitArg : String) : IO Unit := do
+  let manifest ← readInstallManifest manifestPath
+  unless manifest.schemaVersion == installManifestSchemaVersion do
+    throw <| IO.userError
+      s!"cannot refresh source commit in install manifest schemaVersion {manifest.schemaVersion}"
+  printJsonLine <| toJson { manifest with sourceCommit := sourceCommitArg? sourceCommitArg }
 
 def printMcpConfig (home : System.FilePath) (opts : CliOptions) : IO Unit := do
   let root ← projectRoot opts .lean

Beam/Feedback.lean

@@ -391,9 +391,6 @@ private def optionalLine (label : String) (value? : Option String) : List String
 private def boolText (value : Bool) : String :=
   if value then "true" else "false"
 
-private def shortCommit (commit : String) : String :=
-  String.ofList <| commit.toList.take 12
-
 private def jsonField? (json : Json) (field : String) : Option Json :=
   match json.getObjVal? field with
   | .ok value => some value
@@ -440,7 +437,7 @@ private def runtimeSummarySection (collection : Collection) : String :=
     | branch?, commit?, dirty? =>
         let parts :=
           (branch?.map (fun branch => s!"branch {branch}")).toList ++
-          (commit?.map (fun commit => s!"commit {shortCommit commit}")).toList ++
+          (commit?.map (fun commit => s!"commit {commit}")).toList ++
           (dirty?.map (fun dirty => s!"dirty {boolText dirty}")).toList
         some <| String.intercalate ", " parts
   let activeRoot? :=
@@ -460,6 +457,7 @@ private def runtimeSummarySection (collection : Collection) : String :=
     optionalLine "runtime active" ((jsonBoolField? identity "runtime_active").map boolText) ++
     optionalLine "runtime current" ((jsonBoolField? identity "runtime_current").map boolText) ++
     optionalLine "runtime error" (jsonStringField? identity "runtime_error") ++
+    optionalLine "runtime payload" (jsonStringField? identity "runtime_payload") ++
     optionalLine "source" source? ++
     optionalLine "daemon endpoint" (jsonStringField? daemon "registryEndpoint") ++
     warningLines

Beam/Mcp/Projection.lean

@@ -179,7 +179,8 @@ private def evidenceInputSchema : Json :=
     ("properties", Json.mkObj [
       ("name", Beam.JsonSchema.string "Simple evidence filename, without path separators."),
       ("content", anyJsonSchema "Inline JSON or text evidence to write into the bundle."),
-      ("path", Beam.JsonSchema.string "Path to a local evidence file under the known root or Beam control directory.")
+      ("path", Beam.JsonSchema.string
+        "Path to a local evidence file under the known root or selected Beam session directory.")
     ]),
     ("required", toJson (#[("name" : String)] : Array String)),
     ("additionalProperties", toJson false)

CHANGELOG.md

@@ -90,6 +90,10 @@ This project keeps a lightweight, reverse-chronological changelog. Dates use `YY
 
 ### Fixed
 
+- Backend handshake and worker-exit failures now include a bounded stderr tail. Feedback report
+  cards show the complete source commit and runtime payload, and reusing an installed runtime
+  refreshes its source commit so reports identify the checkout that performed the install
+  ([#242](https://github.com/leanprover/lean-beam/pull/242), @ejgallego).
 - MCP `lean_run_at` and `lean_todo` again advertise the read-only hint used by approval- and
   concurrency-aware clients. Codex MCP registration also enables parallel tool calls so independent
   probes need not be serialized by the client.

README.md

@@ -125,9 +125,9 @@ Setup details, validated and compatible toolchains, agent-skill installation, MC
 direct CLI examples, installer locations, overrides, and offline advice live in
 [docs/SETUP.md](docs/SETUP.md).
 
-Beam retains prior immutable runtimes so updates remain atomic. Use `lean-beam prune` to preview
-old installed state and follow the [prune guide](docs/SETUP.md#prune-old-installed-state) before
-applying cleanup.
+Beam retains prior immutable runtime payloads so updates remain atomic. Use `lean-beam prune` to
+preview old installed state and follow the [prune guide](docs/SETUP.md#prune-old-installed-state)
+before applying cleanup.
 
 Lean Beam fully validates exact toolchains listed in
 [`validated-lean-toolchains`](validated-lean-toolchains) and locally qualifies canonical RC/patch

docs/FEEDBACK.md

@@ -105,11 +105,12 @@ descriptor. Beam validates that local target even when confidential mode omits p
 MCP returns compact report-card JSON in
 `structuredContent`: `markdown`, `metadata`, `collection_warnings`, and any bundle paths. The
 default Markdown includes a short Beam runtime summary instead of the full collected debug JSON,
-including stale-runtime or invalid-install identity when available. Pass `include_collected: true`
-to include the full collected Beam debug context inline and render the full debug-context section in
-Markdown. Non-confidential results echo the resolved `workspace` descriptor. Confidential results
-omit that descriptor; `include_collected: true` returns only the restricted runtime identity and
-cannot restore omitted project context.
+including the full source commit, runtime payload, and stale-runtime or invalid-install identity
+when available. Pass `include_collected: true` to include the full collected Beam debug context
+inline and render the full debug-context section in Markdown. Non-confidential results echo the
+resolved `workspace` descriptor. Confidential results omit that descriptor;
+`include_collected: true` returns only the restricted runtime identity and cannot restore omitted
+project context.
 
 MCP does not start a Lean runtime just to collect feedback. In non-confidential mode it includes
 daemon registry and recent daemon incident context for the described workspace. When a runtime is

docs/SETUP.md

@@ -38,13 +38,14 @@ install/config paths and does not allow replacing unrelated user files.
 These forms install:
 
 - `lean-beam`, `lean-beam-search`, and `lean-beam-mcp` into `~/.local/bin`
-- an immutable runtime under `BEAM_INSTALL_ROOT`, default `~/.local/share/beam`
+- an immutable runtime payload under `BEAM_INSTALL_ROOT`, default `~/.local/share/beam`
 - a bundle cache under `~/.local/share/beam/state/install-bundles`
 - a prebuilt bundle for the repo-pinned validated Lean toolchain
 
 Each install rebuilds the runtime binaries from the current source checkout before staging the
-immutable runtime. After reinstalling, restart active MCP client sessions so they launch the new
-runtime instead of continuing to use an already-running server process.
+immutable runtime payload and its provenance manifest. After reinstalling, restart active MCP client
+sessions so they launch the new runtime instead of continuing to use an already-running server
+process.
 
 The agent flags install the bundled Lean skill into the corresponding agent home. Rocq support is a
 separate optional skill; add `--rocq-skill` to a selected agent target when you also want the Rocq
@@ -126,14 +127,16 @@ lean-beam doctor
 
 ## Prune Old Installed State
 
-The installer publishes each distinct content payload as an immutable runtime under
+The installer publishes each distinct content payload as an immutable runtime payload under
 `BEAM_INSTALL_ROOT/versions`. Reinstalling an identical payload reuses its existing runtime only
 after validating its ownership marker, manifest, required files, executable commands, and payload
 contents. The schema-3 manifest field `createdWithToolchains` records the toolchain selection that
-first created that immutable payload; later prebuilds add mutable bundle-cache entries without
-rewriting that provenance. Beam keeps prior distinct runtimes so publishing `current` stays atomic,
-but those snapshots are not removed automatically. Schema-2 manifests are readable only for
-identity and cleanup; reinstalling never republishes a schema-2 runtime. Preview old state with:
+first created that immutable payload. On reuse, the installer refreshes only the manifest's
+`sourceCommit` to the current source checkout commit, or clears it when no commit is available;
+`createdWithToolchains` remains unchanged. Later prebuilds add mutable bundle-cache entries without
+changing the runtime payload. Beam keeps prior distinct runtimes so publishing `current` stays
+atomic, but those snapshots are not removed automatically. Schema-2 manifests are readable only
+for identity and cleanup; reinstalling never republishes a schema-2 runtime. Preview old state with:
 
 ```bash
 lean-beam prune

docs/STATUS.md

@@ -248,6 +248,9 @@ Exact event ordering and examples live in
   service. Unix-domain/per-user native IPC remains a possible later transport improvement.
 - A startup failure that reports `operation not permitted` through `.beam/beam-daemon-startup.log` is
   usually an environment restriction, not a bundle-resolution mismatch.
+- Once the Beam daemon is running, a Lean or Rocq backend handshake failure is returned with the
+  bounded tail of that backend's stderr. This backend diagnostic is separate from the selected
+  session directory's daemon startup log, which covers startup of the Beam daemon process itself.
 - Typed broker transport, invalid-response, and response-timeout failures include registry/log
   context and write a JSON incident record below the selected session directory. Incident kinds are `brokerTransportFailure`,
   `invalidBrokerResponse`, and `brokerResponseTimeout`; callback/display failures do not create

docs/TESTING.md

@@ -143,7 +143,8 @@ Current Beam coverage includes:
   [tests/test-beam-save-olean.sh](../tests/test-beam-save-olean.sh)
 - install flow, installed runtime layout, manifest metadata, exact/compatible toolchain selection,
   shell/Lean owned-root marker parity, required artifact and executable-mode validation,
-  content-addressed runtime reuse, schema-2 reuse rejection and cleanup compatibility,
+  content-addressed runtime reuse, reused-runtime source-commit refresh and clearing, schema-2 reuse
+  rejection and cleanup compatibility,
   `validated-toolchains`,
   `compatible-release-lines`, `doctor`, installed-state pruning, and installed MCP wrapper coverage
   in [tests/test-beam-install.sh](../tests/test-beam-install.sh), with focused prune safety and