From e14ecec0e3a08e2090d8703fef6576de5b51b543 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 24 Aug 2026 15:48:12 +0200 Subject: [PATCH] fix: improve startup and feedback diagnostics --- Beam/Broker/Server.lean | 114 ++++++++++++++++-- Beam/Cli/Commands.lean | 2 + Beam/Cli/DaemonManager.lean | 3 +- Beam/Cli/Info.lean | 20 ++- Beam/Feedback.lean | 6 +- Beam/Mcp/Projection.lean | 3 +- CHANGELOG.md | 4 + README.md | 6 +- docs/FEEDBACK.md | 11 +- docs/SETUP.md | 19 +-- docs/STATUS.md | 3 + docs/TESTING.md | 3 +- scripts/install-beam.sh | 27 +++++ tests/lean/BeamTest/Broker/FeedbackTest.lean | 6 +- tests/lean/BeamTest/Broker/ProtocolTest.lean | 2 + tests/lean/BeamTest/Broker/SmokeTest.lean | 6 + .../BeamTest/Broker/StartupHandshakeTest.lean | 69 +++++++++-- .../lean/BeamTest/Broker/StreamDedupTest.lean | 4 + tests/test-beam-install.sh | 49 ++++++++ 19 files changed, 305 insertions(+), 52 deletions(-) diff --git a/Beam/Broker/Server.lean b/Beam/Broker/Server.lean index 2c24a692..3f59fe08 100644 --- a/Beam/Broker/Server.lean +++ b/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 "" + +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 "" 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 diff --git a/Beam/Cli/Commands.lean b/Beam/Cli/Commands.lean index 3b19a600..b2b241cd 100644 --- a/Beam/Cli/Commands.lean +++ b/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" :: [] => diff --git a/Beam/Cli/DaemonManager.lean b/Beam/Cli/DaemonManager.lean index 46786433..82d7c1b2 100644 --- a/Beam/Cli/DaemonManager.lean +++ b/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 diff --git a/Beam/Cli/Info.lean b/Beam/Cli/Info.lean index 3398fbc1..47d52f9a 100644 --- a/Beam/Cli/Info.lean +++ b/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 " - 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 diff --git a/Beam/Feedback.lean b/Beam/Feedback.lean index 7c4b483c..7d4bcc1c 100644 --- a/Beam/Feedback.lean +++ b/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 diff --git a/Beam/Mcp/Projection.lean b/Beam/Mcp/Projection.lean index 3b0bb63e..fb04b1d4 100644 --- a/Beam/Mcp/Projection.lean +++ b/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) diff --git a/CHANGELOG.md b/CHANGELOG.md index 37bcf431..a66c81af 100644 --- a/CHANGELOG.md +++ b/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. diff --git a/README.md b/README.md index da81088f..7cd70e73 100644 --- a/README.md +++ b/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 diff --git a/docs/FEEDBACK.md b/docs/FEEDBACK.md index 52af3d21..010cf173 100644 --- a/docs/FEEDBACK.md +++ b/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 diff --git a/docs/SETUP.md b/docs/SETUP.md index d6d6a99a..d1c96478 100644 --- a/docs/SETUP.md +++ b/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 diff --git a/docs/STATUS.md b/docs/STATUS.md index 4a4f6685..0dcb24ef 100644 --- a/docs/STATUS.md +++ b/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 diff --git a/docs/TESTING.md b/docs/TESTING.md index 2ae57fff..a731d414 100644 --- a/docs/TESTING.md +++ b/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 diff --git a/scripts/install-beam.sh b/scripts/install-beam.sh index 3b36726b..7419a3e5 100755 --- a/scripts/install-beam.sh +++ b/scripts/install-beam.sh @@ -1275,6 +1275,30 @@ write_install_manifest() { "$beam_cli" install-manifest "$payload_id" "$source_commit_arg" "$@" >"$dest" } +refresh_reused_install_manifest() { + local staging_root="$1" + local version_root="$2" + local source_commit="$3" + local staged_manifest="$staging_root/manifest.json" + local installed_manifest="$version_root/manifest.json" + local source_commit_arg="-" + require_owned_staging_dir "$staging_root" + require_path_within "$version_root" "$versions_root" "installed runtime version" + if [ -L "$staged_manifest" ] || [ ! -f "$staged_manifest" ]; then + die "staged runtime manifest must be a regular non-symlinked file: $staged_manifest" + fi + if [ -L "$installed_manifest" ] || [ ! -f "$installed_manifest" ]; then + die "installed runtime manifest must be a regular non-symlinked file: $installed_manifest" + fi + if [ -n "$source_commit" ]; then + source_commit_arg="$source_commit" + fi + "$beam_cli" install-manifest-with-source-commit \ + "$installed_manifest" "$source_commit_arg" >"$staged_manifest" + confirm_path_edit "refresh reused runtime provenance" "$installed_manifest" + mv "$staged_manifest" "$installed_manifest" +} + prebuild_bundle() { local runtime_home="$1" local toolchain="$2" @@ -1403,6 +1427,9 @@ prepare_install_version() { ${prepared_selected_toolchains[@]+"${prepared_selected_toolchains[@]}"} if [ -d "$prepared_version_root" ]; then validate_runtime_version_for_reuse "$prepared_version_root" "$prepared_payload_id" + refresh_reused_install_manifest \ + "$staging_root" "$prepared_version_root" "$prepared_source_commit" + validate_runtime_version_for_reuse "$prepared_version_root" "$prepared_payload_id" remove_owned_staging_dir "$staging_root" return 0 fi diff --git a/tests/lean/BeamTest/Broker/FeedbackTest.lean b/tests/lean/BeamTest/Broker/FeedbackTest.lean index 8f919200..618c53d2 100644 --- a/tests/lean/BeamTest/Broker/FeedbackTest.lean +++ b/tests/lean/BeamTest/Broker/FeedbackTest.lean @@ -104,6 +104,7 @@ private def sampleCollection (home : String) : Beam.Feedback.Collection := { ("source_commit", toJson "0123456789abcdef"), ("source_branch", toJson "feedback"), ("source_dirty", toJson true), + ("runtime_payload", toJson "sha256-abcdef0123456789"), ("runtime_active", toJson true), ("runtime_current", toJson false), ("runtime_error", toJson "invalid install manifest") @@ -145,7 +146,10 @@ private def checkRenderAndRedaction : IO Unit := do (result.markdown.contains "- runtime current: `false`") require "report card runtime section includes installed runtime error" (result.markdown.contains "- runtime error: `invalid install manifest`") - require "report card runtime section includes source" (result.markdown.contains "commit 0123456789ab") + require "report card runtime section includes exact source commit" + (result.markdown.contains "commit 0123456789abcdef") + require "report card runtime section includes payload identity" + (result.markdown.contains "- runtime payload: `sha256-abcdef0123456789`") require "report card debug context section" (result.markdown.contains "## Beam Debug Context") require "report card should render each collection warning once" (result.markdown.contains "Collection warnings:" && diff --git a/tests/lean/BeamTest/Broker/ProtocolTest.lean b/tests/lean/BeamTest/Broker/ProtocolTest.lean index 1b08bdf5..a5cad3fe 100644 --- a/tests/lean/BeamTest/Broker/ProtocolTest.lean +++ b/tests/lean/BeamTest/Broker/ProtocolTest.lean @@ -978,6 +978,7 @@ private def stubbornSession ] } let pending ← Std.Mutex.new ({} : Std.TreeMap Lean.JsonRpc.RequestID PendingRequest) + let stderrCapture ← startBackendStderrCapture proc.stderr pure { workspaceId backend := .lean @@ -987,6 +988,7 @@ private def stubbornSession proc stdin := IO.FS.Stream.ofHandle proc.stdin stdout := IO.FS.Stream.ofHandle proc.stdout + stderrCapture pending } diff --git a/tests/lean/BeamTest/Broker/SmokeTest.lean b/tests/lean/BeamTest/Broker/SmokeTest.lean index 4163e579..b81c9dd5 100644 --- a/tests/lean/BeamTest/Broker/SmokeTest.lean +++ b/tests/lean/BeamTest/Broker/SmokeTest.lean @@ -722,6 +722,12 @@ private def runWorkerExitSmoke killLeanServerForEndpoint endpoint root let (slowResp, slowEvents) ← awaitTask "worker-exit slow run_at" slowTask expectErrCode slowResp "workerExited" + let some workerExitError := slowResp.error? + | throw <| IO.userError s!"expected worker-exit error, got {(toJson slowResp).compress}" + unless workerExitError.message.contains "Lean backend failed after startup" do + throw <| IO.userError s!"expected worker-exit phase diagnostic, got {(toJson slowResp).compress}" + unless workerExitError.message.contains "backend stderr tail (last 16384 bytes):" do + throw <| IO.userError s!"expected worker-exit stderr diagnostic, got {(toJson slowResp).compress}" expectProgressIds "worker-exit run_at progress" slowEvents workerExitRequestId let commandPath := "tests/scenario/docs/CommandA.lean" diff --git a/tests/lean/BeamTest/Broker/StartupHandshakeTest.lean b/tests/lean/BeamTest/Broker/StartupHandshakeTest.lean index f459d8f2..7cb3252f 100644 --- a/tests/lean/BeamTest/Broker/StartupHandshakeTest.lean +++ b/tests/lean/BeamTest/Broker/StartupHandshakeTest.lean @@ -13,8 +13,8 @@ namespace BeamTest.Broker.StartupHandshakeTest open BeamTest.Broker.TestUtil -private def writeFakeServer (root : System.FilePath) : IO System.FilePath := do - let script := root / "fake-lean-startup.sh" +private def writeResponseErrorServer (root : System.FilePath) : IO System.FilePath := do + let script := root / "fake-lean-startup-response-error.sh" let body := String.intercalate "\n" [ "#!/usr/bin/env bash", "set -euo pipefail", @@ -51,12 +51,31 @@ private partial def waitForProcessGone (pid : Nat) (tries : Nat := 80) : IO Unit IO.sleep 25 waitForProcessGone pid (tries - 1) -def main : IO Unit := do +private def writeAbruptExitServer (root : System.FilePath) : IO System.FilePath := do + let script := root / "fake-lean-startup-abrupt-exit.sh" + let body := String.intercalate "\n" [ + "#!/usr/bin/env bash", + "set -euo pipefail", + "python3 -c 'import sys; sys.stderr.buffer.write(b\"stderr-prefix-start\\n\" + bytes([0xc3, 0xa9]) * 10000 + b\"\\nAstderr-tail-marker\\n\")'", + "exit 23" + ] ++ "\n" + IO.FS.writeFile script body + let out ← IO.Process.output { + cmd := "chmod" + args := #["+x", script.toString] + } + if out.exitCode != 0 then + throw <| IO.userError s!"failed to chmod abrupt-exit startup server\n{out.stderr}" + pure script + +private def checkStartupFailure + (root fakeServer plugin : System.FilePath) + (expected : String) + (checkPidGone := false) + (forbidden? : Option String := none) + (maxMessageLength? : Option Nat := none) : IO Unit := do let endpoint ← freshTcpEndpoint - let root ← mkTempProjectRoot "beam-daemon-startup" - IO.FS.createDirAll root - let fakeServer ← writeFakeServer root - let broker ← spawnLeanBrokerWithPlugin endpoint root (← BeamTest.TestHarness.pluginPath) fakeServer.toString + let broker ← spawnLeanBrokerWithPlugin endpoint root plugin fakeServer.toString try waitForBrokerReadyForRoot endpoint root let resp ← runClient endpoint { op := .ensure, root? := some root.toString } @@ -66,18 +85,42 @@ def main : IO Unit := do | throw <| IO.userError s!"expected startup handshake error payload, got {(toJson resp).compress}" if err.code != "internalError" then throw <| IO.userError s!"expected internalError for startup failure, got {(toJson resp).compress}" - unless err.message.contains "initialize failed" do - throw <| IO.userError s!"expected startup failure to mention initialize failure, got {(toJson resp).compress}" - let pidText ← IO.FS.readFile (root / "fake-lean.pid") - let some pid := pidText.trimAscii.toString.toNat? - | throw <| IO.userError s!"invalid fake backend pid '{pidText}'" - waitForProcessGone pid + unless err.message.contains "Lean backend failed during startup" do + throw <| IO.userError s!"expected startup failure phase, got {(toJson resp).compress}" + unless err.message.contains "backend stderr tail (last 16384 bytes):" do + throw <| IO.userError s!"expected bounded stderr label, got {(toJson resp).compress}" + unless err.message.contains expected do + throw <| IO.userError s!"expected startup failure to mention '{expected}', got {(toJson resp).compress}" + if let some forbidden := forbidden? then + if err.message.contains forbidden then + throw <| IO.userError s!"expected bounded startup failure to omit '{forbidden}', got {(toJson resp).compress}" + if let some maxMessageLength := maxMessageLength? then + if err.message.length > maxMessageLength then + throw <| IO.userError + s!"expected startup failure at most {maxMessageLength} characters, got {err.message.length}" + if checkPidGone then + let pidText ← IO.FS.readFile (root / "fake-lean.pid") + let some pid := pidText.trimAscii.toString.toNat? + | throw <| IO.userError s!"invalid fake backend pid '{pidText}'" + waitForProcessGone pid finally try broker.kill catch _ => pure () discard <| broker.tryWait + +def main : IO Unit := do + let root ← mkTempProjectRoot "beam-daemon-startup" + IO.FS.createDirAll root + let plugin ← BeamTest.TestHarness.pluginPath + try + let responseErrorServer ← writeResponseErrorServer root + checkStartupFailure root responseErrorServer plugin "initialize failed" (checkPidGone := true) + let abruptExitServer ← writeAbruptExitServer root + checkStartupFailure root abruptExitServer plugin "stderr-tail-marker" + (forbidden? := some "stderr-prefix-start") (maxMessageLength? := some 17000) + finally try IO.FS.removeDirAll root catch _ => diff --git a/tests/lean/BeamTest/Broker/StreamDedupTest.lean b/tests/lean/BeamTest/Broker/StreamDedupTest.lean index 1724da81..fdcb404d 100644 --- a/tests/lean/BeamTest/Broker/StreamDedupTest.lean +++ b/tests/lean/BeamTest/Broker/StreamDedupTest.lean @@ -97,6 +97,7 @@ private def fakeTrackedSession (root transcript : System.FilePath) : IO Beam.Bro cwd := root.toString } let pending ← Std.Mutex.new ({} : Std.TreeMap Lean.JsonRpc.RequestID Beam.Broker.PendingRequest) + let stderrCapture ← Beam.Broker.startBackendStderrCapture proc.stderr let session : Beam.Broker.Session := { workspaceId := fixtureWorkspaceId backend := .lean @@ -106,6 +107,7 @@ private def fakeTrackedSession (root transcript : System.FilePath) : IO Beam.Bro proc stdin := IO.FS.Stream.ofHandle proc.stdin stdout := IO.FS.Stream.ofHandle proc.stdout + stderrCapture pending } let _ ← IO.asTask (prio := Task.Priority.dedicated) <| Beam.Broker.sessionReaderLoop session @@ -125,6 +127,7 @@ private def fakeSessionWithSyncedDoc (version : Nat := 1) : IO Beam.Broker.Session := do let proc ← fakeOneRequestProcess root transcript let pending ← Std.Mutex.new ({} : Std.TreeMap Lean.JsonRpc.RequestID Beam.Broker.PendingRequest) + let stderrCapture ← Beam.Broker.startBackendStderrCapture proc.stderr let text ← IO.FS.readFile path let textMTime ← Lake.getFileMTime path let uri := Beam.Broker.sessionUri path @@ -144,6 +147,7 @@ private def fakeSessionWithSyncedDoc proc stdin := IO.FS.Stream.ofHandle proc.stdin stdout := IO.FS.Stream.ofHandle proc.stdout + stderrCapture pending docs } diff --git a/tests/test-beam-install.sh b/tests/test-beam-install.sh index 49237070..905371a0 100644 --- a/tests/test-beam-install.sh +++ b/tests/test-beam-install.sh @@ -799,6 +799,55 @@ if [ -n "$expected_source_commit" ]; then assert_output_contains "installed lean-beam-mcp --version" "$installed_mcp_version" "source commit: $expected_source_commit" fi +git -C "$source_checkout" init -q +git -C "$source_checkout" config user.name "Beam Install Test" +git -C "$source_checkout" config user.email "beam-install-test@example.invalid" +git -C "$source_checkout" commit --allow-empty --no-gpg-sign -q -m "test source provenance refresh" +expected_source_commit="$(git -C "$source_checkout" rev-parse HEAD)" +stale_source_commit="0000000000000000000000000000000000000000" +python3 - "$installed_version_root/manifest.json" "$stale_source_commit" <<'PY' +import json +import sys + +path, stale_source_commit = sys.argv[1:] +with open(path, encoding="utf-8") as stream: + manifest = json.load(stream) +manifest["sourceCommit"] = stale_source_commit +with open(path, "w", encoding="utf-8") as stream: + json.dump(manifest, stream) + stream.write("\n") +PY +run_step "refresh reused runtime provenance" run_install_from_source --toolchain "$toolchain" +assert_symlink_target "$installed_runtime_root" "$installed_version_root" +assert_version_count "$BEAM_INSTALL_ROOT/versions" 1 +BEAM_INSTALL_LAYOUT_JSON="$install_layout_json" assert_manifest_metadata \ + "$installed_runtime_root/manifest.json" "$installed_payload_id" "$expected_source_commit" "$toolchain" +refreshed_mcp_version="$("$installed_mcp" --version)" +if [ -n "$expected_source_commit" ]; then + assert_output_contains "refreshed lean-beam-mcp --version" "$refreshed_mcp_version" \ + "source commit: $expected_source_commit" +fi +assert_output_not_contains "refreshed lean-beam-mcp --version" "$refreshed_mcp_version" \ + "source commit: $stale_source_commit" + +cleared_source_manifest="$tmp_root/runtime-reuse-cleared-source-manifest.json" +"$installed_version_root/libexec/beam-cli" install-manifest-with-source-commit \ + "$installed_version_root/manifest.json" - >"$cleared_source_manifest" +python3 - "$installed_version_root/manifest.json" "$cleared_source_manifest" <<'PY' +import json +import sys + +installed_path, cleared_path = sys.argv[1:] +with open(installed_path, encoding="utf-8") as stream: + expected = json.load(stream) +with open(cleared_path, encoding="utf-8") as stream: + actual = json.load(stream) +expected["sourceCommit"] = None +if actual != expected: + raise SystemExit(f"clearing sourceCommit changed other manifest data: {actual}") +PY +remove_tmp_file "$cleared_source_manifest" + reuse_guard_backup="$tmp_root/runtime-reuse-Beam.lean" reuse_guard_err="$tmp_root/runtime-reuse.err" cp "$installed_version_root/Beam.lean" "$reuse_guard_backup"