From b782acb530e27c991d3cb544276ba58b7fa64248 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 22 Mar 2026 02:23:14 +0100 Subject: [PATCH 1/2] Harden wrapper text and handle inputs --- Beam/Cli.lean | 367 +++++++++++++----- README.md | 24 ++ scripts/install-beam-notes.txt | 3 + scripts/lean-beam | 13 +- skills/lean-beam/SKILL.md | 13 + .../references/lean-run-at-semantics.md | 8 +- skills/lean-beam/references/mcts-search.md | 25 +- .../lean-beam/references/workflow-details.md | 7 +- tests/test-beam-wrapper.sh | 223 ++++++++++- 9 files changed, 578 insertions(+), 105 deletions(-) diff --git a/Beam/Cli.lean b/Beam/Cli.lean index e32b2423..6d4279a5 100644 --- a/Beam/Cli.lean +++ b/Beam/Cli.lean @@ -7,6 +7,7 @@ Author: Emilio J. Gallego Arias import Lean import Beam.Broker.Client import Beam.Broker.Transport +import RunAt.Protocol import Std.Internal.UV.Signal open Lean @@ -73,6 +74,10 @@ private structure CliOptions where requestedSocket? : Option System.FilePath := none args : List String := [] +private structure ParsedTextArg where + text? : Option String := none + source : String := "argv" + private def parseNatArg (name value : String) : IO Nat := do let some n := value.toNat? | throw <| IO.userError s!"invalid {name} '{value}'" @@ -81,6 +86,35 @@ private def parseNatArg (name value : String) : IO Nat := do private def joinTextArgs (args : List String) : Option String := if args.isEmpty then none else some <| String.intercalate " " args +private def hasSubstring (text needle : String) : Bool := + match text.splitOn needle with + | [_] => false + | _ => true + +private def textArgUsage (cmdHead : String) : String := + s!"usage: beam [--root PATH] [--socket PATH | --port N] {cmdHead} [--stdin | --text-file | -- | ]" + +private def textArgReadsStdin (args : List String) : Bool := + match args with + | ["--stdin"] => true + | _ => false + +private def parseTextArg (cmdHead : String) (args : List String) : IO ParsedTextArg := do + match args with + | [] => pure {} + | ["--stdin"] => + pure { text? := some (← (← IO.getStdin).readToEnd), source := "stdin" } + | ["--text-file", path] => + pure { text? := some (← IO.FS.readFile (System.FilePath.mk path)), source := s!"text-file:{path}" } + | "--" :: rest => + pure { text? := joinTextArgs rest, source := "argv" } + | "--stdin" :: _ => + throw <| IO.userError (textArgUsage cmdHead) + | "--text-file" :: _ => + throw <| IO.userError (textArgUsage cmdHead) + | _ => + pure { text? := joinTextArgs args, source := "argv" } + private def parseJsonText (label text : String) : IO Json := do match Json.parse text with | .ok json => pure json @@ -94,6 +128,14 @@ private def parseJsonArg (label arg : String) : IO Json := do pure arg parseJsonText label raw +private def handleArgUsage (cmdHead : String) : String := + s!"usage: beam [--root PATH] [--socket PATH | --port N] {cmdHead} >" + +private def handleArgReadsStdin (args : List String) : Bool := + match args with + | "-" :: _ => true + | _ => false + private def extractHandleJson (json : Json) : Json := match json.getObjVal? "handle" with | .ok handle => handle @@ -105,17 +147,31 @@ private def extractHandleJson (json : Json) : Json := | .error _ => json | .error _ => json +private def parseHandleText (raw : String) : IO Handle := do + let json ← parseJsonText "handle json" raw + match fromJson? (extractHandleJson json) with + | .ok handle => pure handle + | .error err => + throw <| IO.userError s!"invalid handle payload: {err}" + private def parseHandleArg (arg : String) : IO Handle := do let raw ← if arg == "-" then (← IO.getStdin).readToEnd else pure arg - let json ← parseJsonText "handle json" raw - match fromJson? (extractHandleJson json) with - | .ok handle => pure handle - | .error err => - throw <| IO.userError s!"invalid handle payload: {err}" + parseHandleText raw + +private def parseHandleInput (cmdHead : String) (args : List String) : IO (Handle × List String) := do + match args with + | [] => + throw <| IO.userError (handleArgUsage cmdHead) + | "--handle-file" :: path :: rest => + pure ((← parseHandleText (← IO.FS.readFile (System.FilePath.mk path))), rest) + | "--handle-file" :: _ => + throw <| IO.userError (handleArgUsage cmdHead) + | arg :: rest => + pure ((← parseHandleArg arg), rest) private def parseLeanSyncArgs (args : List String) : IO Bool := do match args with @@ -282,6 +338,32 @@ private def ensureSupportedLeanToolchain (home : System.FilePath) (toolchain : S private def boolText (value : Bool) : String := if value then "true" else "false" +private def parseEnvFlag (raw : String) : Bool := + let normalized := raw.trimAscii.toString.toLower + !(normalized.isEmpty || normalized == "0" || normalized == "false" || normalized == "no") + +private def envFlag? (name : String) : IO (Option Bool) := do + match ← IO.getEnv name with + | some raw => pure <| some (parseEnvFlag raw) + | none => pure none + +private def hexDigit (n : Nat) : Char := + if n < 10 then + Char.ofNat (48 + n) + else + Char.ofNat (87 + n) + +private def hexByte (byte : UInt8) : String := + let n := byte.toNat + String.singleton (hexDigit (n / 16)) ++ String.singleton (hexDigit (n % 16)) + +private def utf8Hex (bytes : ByteArray) : String := + String.intercalate " " <| Id.run do + let mut parts : Array String := #[] + for byte in bytes do + parts := parts.push (hexByte byte) + return parts.toList + private def bundleWorkspaceFor (bundleDir : System.FilePath) : System.FilePath := bundleDir / "workspace" @@ -1019,6 +1101,62 @@ private def annotateRunatMessage (clientRequestId? : Option String) (msg : Strin | none => msg +private def debugTextEnabled : IO Bool := do + pure <| (← envFlag? "BEAM_DEBUG_TEXT").getD false + +private def maybeEmitTextDebug (clientRequestId? : Option String) (action source : String) (text? : Option String) : IO Unit := do + if !(← debugTextEnabled) then + pure () + else + match text? with + | none => pure () + | some text => + let bytes := text.toUTF8 + let containsLiteralBackslashN := hasSubstring text "\\n" + IO.eprintln <| annotateRunatMessage clientRequestId? + s!"beam: debug text for {action}: source={source} utf8Bytes={bytes.size} containsNewline={boolText (text.contains '\n')} containsLiteralBackslashN={boolText containsLiteralBackslashN}" + IO.eprintln <| annotateRunatMessage clientRequestId? + s!"beam: debug text escaped={(Json.str text).compress}" + IO.eprintln <| annotateRunatMessage clientRequestId? + s!"beam: debug text utf8Hex={utf8Hex bytes}" + +private def decodeRunAtResult? (resp : Response) : Option RunAt.Result := + match resp.result? with + | none => none + | some result => + match fromJson? result with + | .ok payload => some payload + | .error _ => none + +private def responseErrorSummary? (action failureBoundary : String) (resp : Response) : Option String := + resp.error?.map fun err => + s!"beam: {action} request failed {failureBoundary} ({err.code}): {err.message}" + +private def runAtPayloadSummary? (action noun : String) (resp : Response) : Option String := + match decodeRunAtResult? resp with + | some result => + if result.success then + none + else + some s!"beam: {action} {noun} failed inside Lean; the request completed and returned result.success=false" + | none => + none + +private def maybeEmitLiteralBackslashNewlineHint (req : Request) (resp : Response) : IO Unit := do + match req.op with + | .runAt | .runWith => + match req.text?, decodeRunAtResult? resp with + | some text, some result => + if !result.success && hasSubstring text "\\n" && !text.contains '\n' then + IO.eprintln <| annotateRunatMessage req.clientRequestId? + "beam: hint: the probe text contains the literal characters '\\n'; if you meant a real newline, use --stdin or --text-file." + else + pure () + | _, _ => + pure () + | _ => + pure () + private def withBrokerErrorContext {α} (root : System.FilePath) (action : IO α) : IO α := do try action @@ -1057,20 +1195,22 @@ private def syncFileProgressSuffix (progress? : Option SyncFileProgress) : Strin s!", fp updates={progress.updates}{doneSuffix}" private structure BrokerWaitSpec where + action : String startMsg : String progressMsg : SyncFileProgress → String stillWaitingMsg : Nat → String completeMsg : Response → String + failureBoundary : String := "before the request completed" + responseNote? : Response → Option String := fun _ => none private structure InterruptWatcher where signal : Std.Internal.UV.Signal task : Task (Except IO.Error Unit) private def progressEnabled : IO Bool := do - match ← IO.getEnv "BEAM_PROGRESS" with - | some raw => - let normalized := raw.trimAscii.toString.toLower - pure <| !(normalized.isEmpty || normalized == "0" || normalized == "false" || normalized == "no") + match ← envFlag? "BEAM_PROGRESS" with + | some enabled => + pure enabled | none => (← IO.getStderr).isTty @@ -1130,6 +1270,7 @@ private def awaitBrokerResponse private def syncWaitSpec (path : String) : BrokerWaitSpec := { + action := "lean-sync" startMsg := s!"beam: syncing {path} and waiting for Lean diagnostics" progressMsg := fun progress => s!"beam: sync progress for {path}{syncFileProgressSuffix (some progress)}" stillWaitingMsg := fun seconds => s!"beam: still syncing {path} ({seconds}s)" @@ -1142,15 +1283,17 @@ private def syncWaitSpec (path : String) : BrokerWaitSpec := "" else s!", saveReady=false ({result.saveReadyReason}, " ++ - s!"stateErrorCount={result.stateErrorCount}, " ++ + s!"stateErrorCount={result.stateErrorCount}, " ++ s!"stateCommandErrorCount={result.stateCommandErrorCount})" s!"beam: sync complete for {path} (version {result.version}{suffix}{readinessSuffix})" | none => - s!"beam: sync complete for {path}" + s!"beam: sync complete for {path}" + failureBoundary := "before a complete diagnostics barrier was available" } private def refreshWaitSpec (path : String) : BrokerWaitSpec := { + action := "lean-refresh" startMsg := s!"beam: refreshing {path} by closing and resyncing" progressMsg := fun progress => s!"beam: refresh progress for {path}{syncFileProgressSuffix (some progress)}" stillWaitingMsg := fun seconds => s!"beam: still refreshing {path} ({seconds}s)" @@ -1163,33 +1306,39 @@ private def refreshWaitSpec (path : String) : BrokerWaitSpec := "" else s!", saveReady=false ({result.saveReadyReason}, " ++ - s!"stateErrorCount={result.stateErrorCount}, " ++ + s!"stateErrorCount={result.stateErrorCount}, " ++ s!"stateCommandErrorCount={result.stateCommandErrorCount})" s!"beam: refresh complete for {path} (version {result.version}{suffix}{readinessSuffix})" | none => - s!"beam: refresh complete for {path}" + s!"beam: refresh complete for {path}" + failureBoundary := "before a complete diagnostics barrier was available" } -private def leanRunAtWaitSpec (path : String) (line character : Nat) : BrokerWaitSpec := +private def leanRunAtWaitSpec (action path : String) (line character : Nat) : BrokerWaitSpec := let pos := s!"{path}:{line}:{character}" { - startMsg := s!"beam: running lean-run-at on {pos} and waiting for a ready Lean snapshot" + action := action + startMsg := s!"beam: running {action} on {pos} and waiting for a ready Lean snapshot" progressMsg := fun progress => s!"beam: snapshot progress for {pos}{syncFileProgressSuffix (some progress)}" stillWaitingMsg := fun seconds => - s!"beam: still waiting for a ready Lean snapshot for {pos} ({seconds}s)" + s!"beam: still waiting for a ready Lean snapshot for {action} on {pos} ({seconds}s)" completeMsg := fun resp => - s!"beam: lean-run-at complete for {pos}{syncFileProgressSuffix (responseFileProgress? resp)}" + s!"beam: {action} complete for {pos}{syncFileProgressSuffix (responseFileProgress? resp)}" + failureBoundary := "before probe execution" + responseNote? := runAtPayloadSummary? action "probe" } private def leanHoverWaitSpec (path : String) (line character : Nat) : BrokerWaitSpec := let pos := s!"{path}:{line}:{character}" { + action := "lean-hover" startMsg := s!"beam: running lean-hover on {pos} and waiting for a ready Lean snapshot" progressMsg := fun progress => s!"beam: hover progress for {pos}{syncFileProgressSuffix (some progress)}" stillWaitingMsg := fun seconds => s!"beam: still waiting for lean-hover on {pos} ({seconds}s)" completeMsg := fun resp => s!"beam: lean-hover complete for {pos}{syncFileProgressSuffix (responseFileProgress? resp)}" + failureBoundary := "before hover data was available" } private def leanGoalsWaitSpec (path : String) (line character : Nat) (mode : GoalMode) : BrokerWaitSpec := @@ -1199,44 +1348,53 @@ private def leanGoalsWaitSpec (path : String) (line character : Nat) (mode : Goa | .after => "lean-goals-after" | .prev => "lean-goals-prev" { + action := action startMsg := s!"beam: running {action} on {pos} and waiting for a ready Lean snapshot" progressMsg := fun progress => s!"beam: goals progress for {pos}{syncFileProgressSuffix (some progress)}" stillWaitingMsg := fun seconds => s!"beam: still waiting for {action} on {pos} ({seconds}s)" completeMsg := fun resp => s!"beam: {action} complete for {pos}{syncFileProgressSuffix (responseFileProgress? resp)}" + failureBoundary := "before goal inspection completed" } private def leanRequestAtWaitSpec (path : String) (line character : Nat) (method : String) : BrokerWaitSpec := let pos := s!"{path}:{line}:{character}" { + action := s!"lean-request-at {method}" startMsg := s!"beam: forwarding experimental {method} at {pos} and waiting for a ready Lean snapshot" progressMsg := fun progress => s!"beam: request-at progress for {pos}{syncFileProgressSuffix (some progress)}" stillWaitingMsg := fun seconds => s!"beam: still waiting for experimental {method} at {pos} ({seconds}s)" completeMsg := fun resp => s!"beam: experimental {method} complete for {pos}{syncFileProgressSuffix (responseFileProgress? resp)}" + failureBoundary := s!"before experimental {method} completed" } private def leanRunWithWaitSpec (path : String) (linear : Bool := false) : BrokerWaitSpec := let action := if linear then "lean-run-with-linear" else "lean-run-with" { + action := action startMsg := s!"beam: running {action} on {path} and waiting for a ready Lean snapshot" progressMsg := fun progress => s!"beam: {action} progress for {path}{syncFileProgressSuffix (some progress)}" stillWaitingMsg := fun seconds => s!"beam: still waiting for {action} on {path} ({seconds}s)" completeMsg := fun resp => s!"beam: {action} complete for {path}{syncFileProgressSuffix (responseFileProgress? resp)}" + failureBoundary := "before speculative continuation completed" + responseNote? := runAtPayloadSummary? action "continuation" } private def leanSaveWaitSpec (path : String) (closeAfter : Bool := false) : BrokerWaitSpec := let action := if closeAfter then "lean-close-save" else "lean-save" let verb := if closeAfter then "closing and saving" else "saving" { + action := action startMsg := s!"beam: {verb} {path} and waiting for Lean diagnostics/artifacts" progressMsg := fun progress => s!"beam: {action} progress for {path}{syncFileProgressSuffix (some progress)}" stillWaitingMsg := fun seconds => s!"beam: still waiting for {action} on {path} ({seconds}s)" completeMsg := fun resp => s!"beam: {action} complete for {path}{syncFileProgressSuffix (responseFileProgress? resp)}" + failureBoundary := "before save artifacts were finalized" } private def callBrokerWithProgress @@ -1260,6 +1418,17 @@ private def callBrokerWithProgress awaitBrokerResponse task endpoint req spec else sendRequestWithCallbacks endpoint req callbacks + match responseErrorSummary? spec.action spec.failureBoundary resp with + | some note => + IO.eprintln <| annotateRunatMessage req.clientRequestId? note + | none => + pure () + match spec.responseNote? resp with + | some note => + IO.eprintln <| annotateRunatMessage req.clientRequestId? note + | none => + pure () + maybeEmitLiteralBackslashNewlineHint req resp printResponse resp failOnError resp @@ -1268,14 +1437,14 @@ private def usage : String := "usage:", " beam [--root PATH] [--socket PATH | --port N] ensure lean|rocq", " beam [--root PATH] cancel ", - " beam [--root PATH] [--socket PATH | --port N] lean-run-at ", - " beam [--root PATH] [--socket PATH | --port N] lean-run-at-handle ", + " beam [--root PATH] [--socket PATH | --port N] lean-run-at [--stdin | --text-file | -- | ]", + " beam [--root PATH] [--socket PATH | --port N] lean-run-at-handle [--stdin | --text-file | -- | ]", " beam [--root PATH] [--socket PATH | --port N] lean-hover ", " beam [--root PATH] [--socket PATH | --port N] lean-goals-after ", " beam [--root PATH] [--socket PATH | --port N] lean-goals-prev ", - " beam [--root PATH] [--socket PATH | --port N] lean-run-with ", - " beam [--root PATH] [--socket PATH | --port N] lean-run-with-linear ", - " beam [--root PATH] [--socket PATH | --port N] lean-release ", + " beam [--root PATH] [--socket PATH | --port N] lean-run-with > [--stdin | --text-file | -- | ]", + " beam [--root PATH] [--socket PATH | --port N] lean-run-with-linear > [--stdin | --text-file | -- | ]", + " beam [--root PATH] [--socket PATH | --port N] lean-release >", " beam [--root PATH] [--socket PATH | --port N] lean-deps ", " beam [--root PATH] [--socket PATH | --port N] lean-sync [+full]", " beam [--root PATH] [--socket PATH | --port N] lean-refresh [+full]", @@ -1300,10 +1469,15 @@ private def usage : String := "Separate lean-run-at calls are independent probes on the current saved file snapshot.", "For exact speculative chaining, use lean-run-at-handle and then lean-run-with /", "lean-run-with-linear.", + "For multiline text-carrying Lean probes, prefer --stdin or --text-file ; use -- before", + "text that itself starts with --.", + "For handle-based commands, use --handle-file when you do not want to inline handle json.", "For lean-sync / lean-refresh / lean-save / lean-close-save, diagnostics always stream for the", "current request;", "default is errors only, and +full widens the stream to warnings, info, and hints.", "Wrapper diagnostics and progress are human-facing on stderr.", + "Set BEAM_DEBUG_TEXT=1 to print the exact escaped text and UTF-8 bytes sent for text-carrying", + "Lean probe requests.", "For machine-readable streaming diagnostics/progress, use beam-client request-stream.", "", "Expert-only experimental commands are documented in docs/experimental.md.", @@ -1316,6 +1490,81 @@ private def printExperimentalInfo (home : System.FilePath) : IO Unit := do IO.println "This is an unstable broker escape hatch, not part of the stable runAt contract." IO.println "Current experimental entry point: lean-request-at" +private def runLeanRunAt + (home : System.FilePath) + (opts : CliOptions) + (action path lineText characterText : String) + (textArgs : List String) + (storeHandle : Bool := false) : IO Unit := do + let root ← projectRoot opts .lean + let (endpoint, _) ← ensureProjectDaemon home root .lean opts + let line ← parseNatArg "line" lineText + let character ← parseNatArg "character" characterText + let parsedText ← parseTextArg s!"{action} " textArgs + let req ← withEnvClientRequestId { + op := .runAt + backend := .lean + root? := some root.toString + path? := some path + line? := some line + character? := some character + text? := parsedText.text? + storeHandle? := if storeHandle then some true else none + } + maybeEmitTextDebug req.clientRequestId? action parsedText.source parsedText.text? + callBrokerWithProgress root endpoint req (leanRunAtWaitSpec action path line character) + +private def runLeanRunWith + (home : System.FilePath) + (opts : CliOptions) + (action path : String) + (args : List String) + (linear : Bool := false) : IO Unit := do + let textArgs := + match args with + | [] => [] + | "--handle-file" :: _ :: rest => rest + | _ :: rest => rest + if handleArgReadsStdin args && textArgReadsStdin textArgs then + throw <| IO.userError <| String.intercalate "\n" [ + textArgUsage s!"{action} >", + "cannot read both handle json and continuation text from stdin; pass the handle inline, use --handle-file, or use --text-file for the text" + ] + let root ← projectRoot opts .lean + let (endpoint, _) ← ensureProjectDaemon home root .lean opts + let (handle, textArgs) ← parseHandleInput s!"{action} " args + let parsedText ← parseTextArg s!"{action} >" textArgs + let req ← withEnvClientRequestId { + op := .runWith + backend := .lean + root? := some root.toString + path? := some path + handle? := some handle + text? := parsedText.text? + storeHandle? := some true + linear? := some linear + } + maybeEmitTextDebug req.clientRequestId? action parsedText.source parsedText.text? + callBrokerWithProgress root endpoint req (leanRunWithWaitSpec path (linear := linear)) + +private def runLeanRelease + (home : System.FilePath) + (opts : CliOptions) + (path : String) + (args : List String) : IO Unit := do + let root ← projectRoot opts .lean + let (endpoint, _) ← ensureProjectDaemon home root .lean opts + let (handle, extra) ← parseHandleInput "lean-release " args + unless extra.isEmpty do + throw <| IO.userError (handleArgUsage "lean-release ") + callBroker root endpoint { + op := .release + backend := .lean + root? := some root.toString + path? := some path + handle? := some handle + } + private partial def parseCliOptions (opts : CliOptions) : List String → IO CliOptions | [] => pure opts | "--root" :: root :: rest => do @@ -1470,34 +1719,9 @@ private def runCommand (home : System.FilePath) (opts : CliOptions) : IO Unit := let (endpoint, _) ← ensureProjectDaemon home root backend opts callBroker root endpoint { op := .ensure, backend := backend, root? := some root.toString } | "lean-run-at" :: path :: line :: character :: text => - let root ← projectRoot opts .lean - let (endpoint, _) ← ensureProjectDaemon home root .lean opts - let line ← parseNatArg "line" line - let character ← parseNatArg "character" character - callBrokerWithProgress root endpoint { - op := .runAt - backend := .lean - root? := some root.toString - path? := some path - line? := some line - character? := some character - text? := joinTextArgs text - } (leanRunAtWaitSpec path line character) + runLeanRunAt home opts "lean-run-at" path line character text | "lean-run-at-handle" :: path :: line :: character :: text => - let root ← projectRoot opts .lean - let (endpoint, _) ← ensureProjectDaemon home root .lean opts - let line ← parseNatArg "line" line - let character ← parseNatArg "character" character - callBrokerWithProgress root endpoint { - op := .runAt - backend := .lean - root? := some root.toString - path? := some path - line? := some line - character? := some character - text? := joinTextArgs text - storeHandle? := some true - } (leanRunAtWaitSpec path line character) + runLeanRunAt home opts "lean-run-at-handle" path line character text (storeHandle := true) | "lean-hover" :: path :: line :: character :: [] => let root ← projectRoot opts .lean let (endpoint, _) ← ensureProjectDaemon home root .lean opts @@ -1560,45 +1784,12 @@ private def runCommand (home : System.FilePath) (opts : CliOptions) : IO Unit := method? := some method params? := params? } (leanRequestAtWaitSpec path line character method) - | "lean-run-with" :: path :: handleArg :: text => - let root ← projectRoot opts .lean - let (endpoint, _) ← ensureProjectDaemon home root .lean opts - let handle ← parseHandleArg handleArg - callBrokerWithProgress root endpoint { - op := .runWith - backend := .lean - root? := some root.toString - path? := some path - handle? := some handle - text? := joinTextArgs text - storeHandle? := some true - linear? := some false - } (leanRunWithWaitSpec path) - | "lean-run-with-linear" :: path :: handleArg :: text => - let root ← projectRoot opts .lean - let (endpoint, _) ← ensureProjectDaemon home root .lean opts - let handle ← parseHandleArg handleArg - callBrokerWithProgress root endpoint { - op := .runWith - backend := .lean - root? := some root.toString - path? := some path - handle? := some handle - text? := joinTextArgs text - storeHandle? := some true - linear? := some true - } (leanRunWithWaitSpec path (linear := true)) - | "lean-release" :: path :: handleArg :: [] => - let root ← projectRoot opts .lean - let (endpoint, _) ← ensureProjectDaemon home root .lean opts - let handle ← parseHandleArg handleArg - callBroker root endpoint { - op := .release - backend := .lean - root? := some root.toString - path? := some path - handle? := some handle - } + | "lean-run-with" :: path :: args => + runLeanRunWith home opts "lean-run-with" path args + | "lean-run-with-linear" :: path :: args => + runLeanRunWith home opts "lean-run-with-linear" path args (linear := true) + | "lean-release" :: path :: args => + runLeanRelease home opts path args | "lean-deps" :: path :: [] => let root ← projectRoot opts .lean let (endpoint, _) ← ensureProjectDaemon home root .lean opts diff --git a/README.md b/README.md index cc0a3717..1f585db4 100644 --- a/README.md +++ b/README.md @@ -80,6 +80,7 @@ lean-beam ensure lean-beam hover "Foo.lean" 10 2 lean-beam goals-prev "Foo.lean" 10 2 lean-beam run-at "Foo.lean" 10 2 "exact trivial" +printf 'example : True := by\n trivial\n' | lean-beam run-at "Foo.lean" 10 2 --stdin lean-beam sync "MyPkg/Sub/Module.lean" lean-beam refresh "MyPkg/Sub/Module.lean" lean-beam save "MyPkg/Sub/Module.lean" @@ -92,6 +93,29 @@ Read those commands like this: - `lean-beam refresh` is `lean-beam close` plus `lean-beam sync` - `lean-beam save` checkpoints one synced workspace module; it does not validate downstream importers +Multiline and handle-oriented wrapper ergonomics: + +```bash +# avoid shell-escape mistakes for multiline probe text +printf 'example : True := by\n trivial\n' | lean-beam run-at "Foo.lean" 10 2 --stdin +lean-beam run-at "Foo.lean" 10 2 --text-file probe.lean + +# continuation from an explicit stored handle +lean-beam run-at-handle "Foo.lean" 10 2 "constructor" +lean-beam run-with "Foo.lean" --handle-file handle.json "exact trivial" + +# when quoting is suspect, inspect exactly what the wrapper is sending +BEAM_DEBUG_TEXT=1 lean-beam run-at "Foo.lean" 10 2 "exact trivial" +``` + +Read those flags like this: + +- `--stdin` and `--text-file ` avoid shell quoting fragility for text-carrying Lean probes +- `--` forces the remaining arguments to be treated as text, even if they start with `--` +- `--handle-file ` avoids inlining handle JSON for `lean-beam run-with`, `lean-beam run-with-linear`, and `lean-beam release` +- `BEAM_DEBUG_TEXT=1` prints escaped probe text and UTF-8 bytes to wrapper stderr for human debugging +- if `lean-beam run-with` or `lean-beam run-with-linear` takes the handle as `-`, stdin is already used for the handle JSON, so prefer `--handle-file ` or `--text-file ` for the continuation text + When `lean-beam sync` fails with `syncBarrierIncomplete`, the JSON error may include `error.data.staleDirectDeps`, `error.data.saveDeps`, and `error.data.recoveryPlan` to suggest a cheap direct-import recovery path before falling back to `lake build`. diff --git a/scripts/install-beam-notes.txt b/scripts/install-beam-notes.txt index 51a3965b..479384e5 100644 --- a/scripts/install-beam-notes.txt +++ b/scripts/install-beam-notes.txt @@ -2,6 +2,8 @@ Quick Start lean-beam ensure lean-beam run-at "Foo.lean" 10 2 "exact trivial" + printf 'example : True := by\n trivial\n' | lean-beam run-at "Foo.lean" 10 2 --stdin + BEAM_DEBUG_TEXT=1 lean-beam run-at "Foo.lean" 10 2 "exact trivial" After Saving A Real Edit lean-beam sync "Foo.lean" @@ -11,6 +13,7 @@ Exact Continuation Separate lean-beam run-at calls do not chain. For exact continuation from one speculative state: lean-beam run-at-handle "Foo.lean" 10 2 "constructor" + lean-beam run-with "Foo.lean" --handle-file handle.json "exact trivial" Diagnostics lean-beam sync / lean-beam save / lean-beam close-save stream errors by default diff --git a/scripts/lean-beam b/scripts/lean-beam index 4a4e63de..90ea13ad 100755 --- a/scripts/lean-beam +++ b/scripts/lean-beam @@ -10,14 +10,14 @@ usage() { cat <<'EOF' >&2 usage: lean-beam [--root PATH] [--socket PATH | --port N] ensure [lean|rocq] - lean-beam [--root PATH] [--socket PATH | --port N] run-at - lean-beam [--root PATH] [--socket PATH | --port N] run-at-handle + lean-beam [--root PATH] [--socket PATH | --port N] run-at [--stdin | --text-file | -- | ] + lean-beam [--root PATH] [--socket PATH | --port N] run-at-handle [--stdin | --text-file | -- | ] lean-beam [--root PATH] [--socket PATH | --port N] hover lean-beam [--root PATH] [--socket PATH | --port N] goals-after lean-beam [--root PATH] [--socket PATH | --port N] goals-prev - lean-beam [--root PATH] [--socket PATH | --port N] run-with - lean-beam [--root PATH] [--socket PATH | --port N] run-with-linear - lean-beam [--root PATH] [--socket PATH | --port N] release + lean-beam [--root PATH] [--socket PATH | --port N] run-with > [--stdin | --text-file | -- | ] + lean-beam [--root PATH] [--socket PATH | --port N] run-with-linear > [--stdin | --text-file | -- | ] + lean-beam [--root PATH] [--socket PATH | --port N] release > lean-beam [--root PATH] [--socket PATH | --port N] deps lean-beam [--root PATH] [--socket PATH | --port N] sync [+full] lean-beam [--root PATH] [--socket PATH | --port N] refresh [+full] @@ -37,6 +37,9 @@ usage: notes: - lean-beam keeps the Lean wrapper surface primary, but also exposes Rocq goal probes and backend selection commands - common Rocq entry points are `lean-beam ensure rocq`, `lean-beam doctor rocq`, `lean-beam rocq-goals-after`, and `lean-beam rocq-goals-prev` + - for multiline text-carrying Lean probes, prefer `--stdin` or `--text-file `; use `--` before text that starts with `--` + - for handle-based commands, use `--handle-file ` when you do not want to inline handle json + - set `BEAM_DEBUG_TEXT=1` to print the exact escaped text and UTF-8 bytes sent for text-carrying Lean probes EOF } diff --git a/skills/lean-beam/SKILL.md b/skills/lean-beam/SKILL.md index 47de089a..ed05de10 100644 --- a/skills/lean-beam/SKILL.md +++ b/skills/lean-beam/SKILL.md @@ -85,6 +85,12 @@ Prefer the smallest command that matches the actual task: truly empty line only character `0` is valid - use `lean-beam run-at-handle` and then `lean-beam run-with` or `lean-beam run-with-linear` only when exact speculative continuation matters +- for multiline text-carrying Lean probes (`lean-beam run-at`, `lean-beam run-at-handle`, + `lean-beam run-with`, `lean-beam run-with-linear`), prefer `--stdin` or `--text-file `; + use `--` before text that itself starts with `--` +- when `lean-beam run-with` or `lean-beam run-with-linear` takes the handle as `-`, stdin is already + consumed by the handle json, so prefer `--handle-file ` or use `--text-file` for the + continuation text - do not expect one `lean-beam run-at` call to become the basis of the next one automatically - use `lean-beam sync` right after every real saved edit before the next speculative probe - use `lean-beam save` or `lean-beam close-save` only for a synced workspace module path such as @@ -127,8 +133,11 @@ Use the right tool for each goal: - if you made a real edit and want fresh file diagnostics: save the file, then use `lean-beam sync` - if you want exact continuation from speculative state: mint a handle with `lean-beam run-at-handle`, then continue with `lean-beam run-with` or `lean-beam run-with-linear` +- for handle-based commands, `--handle-file ` is the easiest way to avoid inlining handle json - if surface syntax depends on indentation or layout: pass the exact text you want Lean to parse, or make a real edit in the file instead of expecting the wrapper to fill whitespace for you +- if shell quoting is suspect, set `BEAM_DEBUG_TEXT=1` to print the exact escaped text and UTF-8 + bytes the wrapper is sending for text-carrying Lean probes Open [references/lean-run-at-semantics.md](references/lean-run-at-semantics.md) when the task needs concrete examples for: @@ -200,6 +209,7 @@ lean-beam goals-prev "Foo.lean" 10 2 # try speculative Lean text without editing the file lean-beam run-at "Foo.lean" 10 2 "exact trivial" +printf 'example : True := by\n trivial\n' | lean-beam run-at "Foo.lean" 10 2 --stdin # after every real edit saved to disk, on that same workspace module path lean-beam sync "MyPkg/Sub/Module.lean" @@ -237,6 +247,9 @@ Diagnostic defaults on that path: Surface rule: - wrapper `stderr` is the human-facing diagnostic surface +- wrapper `stderr` may distinguish request-level failures from a completed request whose payload + failed inside Lean; use stdout JSON for machine decisions +- `BEAM_DEBUG_TEXT=1` adds escaped text and UTF-8 byte dumps for text-carrying Lean probes on stderr - `beam-client request-stream ...` is the machine-facing streamed surface - do not parse wrapper `stderr` in tooling diff --git a/skills/lean-beam/references/lean-run-at-semantics.md b/skills/lean-beam/references/lean-run-at-semantics.md index e7cd1725..e14deed3 100644 --- a/skills/lean-beam/references/lean-run-at-semantics.md +++ b/skills/lean-beam/references/lean-run-at-semantics.md @@ -98,7 +98,13 @@ If the speculative text is the version you want to keep, open For multi-line probes, include the actual newline characters you want Lean to parse. For example: ```bash -# using ANSI-C shell quoting so `\n` becomes a real newline +# piping the exact text through stdin avoids shell-escape mistakes +printf ' first | exact h1\n | exact h2\n' | lean-beam run-at "Foo.lean" 18 0 --stdin + +# or read the probe from a file +lean-beam run-at "Foo.lean" 18 0 --text-file probe.lean + +# ANSI-C shell quoting also works when you do want to keep everything on one command line lean-beam run-at "Foo.lean" 18 0 $' first | exact h1\n | exact h2' ``` diff --git a/skills/lean-beam/references/mcts-search.md b/skills/lean-beam/references/mcts-search.md index 2b654698..70432774 100644 --- a/skills/lean-beam/references/mcts-search.md +++ b/skills/lean-beam/references/mcts-search.md @@ -39,8 +39,14 @@ Rules: lean-beam ensure root="$(lean-beam run-at-handle "Proofs.lean" 42 6 "constructor")" -left="$(printf '%s\n' "$root" | lean-beam run-with "Proofs.lean" - "constructor")" -right="$(printf '%s\n' "$root" | lean-beam run-with "Proofs.lean" - "aesop")" +# writing handles to files avoids stdin conflicts in larger shell scripts +printf '%s\n' "$root" > root.handle.json +left="$(lean-beam run-with "Proofs.lean" --handle-file root.handle.json "constructor")" +right="$(lean-beam run-with "Proofs.lean" --handle-file root.handle.json "aesop")" + +# stdin handle flow remains supported too +left_pipe="$(printf '%s\n' "$root" | lean-beam run-with "Proofs.lean" - "constructor")" +right_pipe="$(printf '%s\n' "$root" | lean-beam run-with "Proofs.lean" - "aesop")" printf '%s\n' "$left" | lean-beam release "Proofs.lean" - printf '%s\n' "$right" | lean-beam release "Proofs.lean" - @@ -53,9 +59,18 @@ Use this when you want to explore multiple children from the same preserved basi ```bash lean-beam ensure root="$(lean-beam run-at-handle "Proofs.lean" 42 6 "constructor")" -step1="$(printf '%s\n' "$root" | lean-beam run-with-linear "Proofs.lean" - "constructor")" -step2="$(printf '%s\n' "$step1" | lean-beam run-with-linear "Proofs.lean" - "exact trivial")" -printf '%s\n' "$step2" | lean-beam run-with-linear "Proofs.lean" - "exact trivial" +# file-backed handles are often easier in longer shell loops +printf '%s\n' "$root" > root.handle.json +step1="$(lean-beam run-with-linear "Proofs.lean" --handle-file root.handle.json "constructor")" +printf '%s\n' "$step1" > step1.handle.json +step2="$(lean-beam run-with-linear "Proofs.lean" --handle-file step1.handle.json "exact trivial")" +printf '%s\n' "$step2" > step2.handle.json +lean-beam run-with-linear "Proofs.lean" --handle-file step2.handle.json "exact trivial" + +# stdin handle flow remains supported when you prefer pipes +step1_pipe="$(printf '%s\n' "$root" | lean-beam run-with-linear "Proofs.lean" - "constructor")" +step2_pipe="$(printf '%s\n' "$step1_pipe" | lean-beam run-with-linear "Proofs.lean" - "exact trivial")" +printf '%s\n' "$step2_pipe" | lean-beam run-with-linear "Proofs.lean" - "exact trivial" ``` Use this when you want one evolving playout path instead of a preserved branch point. diff --git a/skills/lean-beam/references/workflow-details.md b/skills/lean-beam/references/workflow-details.md index 217a9e9c..915f31d4 100644 --- a/skills/lean-beam/references/workflow-details.md +++ b/skills/lean-beam/references/workflow-details.md @@ -31,6 +31,12 @@ Use this reference when the task needs more than the default loop in `SKILL.md`. Continue from a stored handle: ```bash +# `--handle-file` avoids inlining handle json and frees stdin for continuation text +lean-beam run-with "Foo.lean" --handle-file handle.json "exact trivial" +lean-beam run-with-linear "Foo.lean" --handle-file handle.json "exact trivial" +lean-beam release "Foo.lean" --handle-file handle.json + +# stdin handle flow remains supported when it fits your shell loop better printf '%s\n' "$HANDLE_JSON" | lean-beam run-with "Foo.lean" - "exact trivial" printf '%s\n' "$HANDLE_JSON" | lean-beam run-with-linear "Foo.lean" - "exact trivial" printf '%s\n' "$HANDLE_JSON" | lean-beam release "Foo.lean" - @@ -135,7 +141,6 @@ What is not a valid checkpoint target: `contentModified` or handle invalidation instead of hidden reuse - `lean-beam save` / `lean-beam close-save` checkpoint the current synced Lake module only; they do not rebuild reverse dependencies or make downstream files fresh by themselves - ## Diagnostics, Progress, And Request IDs - `lean-beam sync`, `lean-beam save`, and `lean-beam close-save` always stream fresh diagnostics for the current diff --git a/tests/test-beam-wrapper.sh b/tests/test-beam-wrapper.sh index 99cbf92f..e9d84a51 100755 --- a/tests/test-beam-wrapper.sh +++ b/tests/test-beam-wrapper.sh @@ -274,6 +274,120 @@ fi exit 1 fi rm -f "$cmd_err" + multiline_stdin_out="$(printf 'def stdinProbe : Nat :=\n 42' | "$beam_script" lean-run-at PositionEmptyLine.lean 1 0 --stdin)" + if [ "$(RUNAT_JSON_PAYLOAD="$multiline_stdin_out" read_json_text_field ok)" != "true" ]; then + echo "expected wrapper lean-run-at --stdin probe to succeed" >&2 + printf '%s\n' "$multiline_stdin_out" >&2 + exit 1 + fi + if [ "$(RUNAT_JSON_PAYLOAD="$multiline_stdin_out" read_json_text_field result.success)" != "true" ]; then + echo "expected wrapper lean-run-at --stdin payload success" >&2 + printf '%s\n' "$multiline_stdin_out" >&2 + exit 1 + fi + if [ "$(RUNAT_JSON_PAYLOAD="$multiline_stdin_out" read_json_array_len result.messages)" != "0" ]; then + echo "expected wrapper lean-run-at --stdin multiline declaration to produce no messages" >&2 + printf '%s\n' "$multiline_stdin_out" >&2 + exit 1 + fi + probe_text_file="multiline-probe.lean" + printf 'def fileProbe : Nat :=\n 42' > "$probe_text_file" + multiline_file_out="$("$beam_script" lean-run-at PositionEmptyLine.lean 1 0 --text-file "$probe_text_file")" + if [ "$(RUNAT_JSON_PAYLOAD="$multiline_file_out" read_json_text_field ok)" != "true" ]; then + echo "expected wrapper lean-run-at --text-file probe to succeed" >&2 + printf '%s\n' "$multiline_file_out" >&2 + exit 1 + fi + if [ "$(RUNAT_JSON_PAYLOAD="$multiline_file_out" read_json_text_field result.success)" != "true" ]; then + echo "expected wrapper lean-run-at --text-file payload success" >&2 + printf '%s\n' "$multiline_file_out" >&2 + exit 1 + fi + if [ "$(RUNAT_JSON_PAYLOAD="$multiline_file_out" read_json_array_len result.messages)" != "0" ]; then + echo "expected wrapper lean-run-at --text-file multiline declaration to produce no messages" >&2 + printf '%s\n' "$multiline_file_out" >&2 + exit 1 + fi + delimiter_out="$("$beam_script" lean-run-at PositionEmptyLine.lean 1 0 -- $'--stdin\n#check answer')" + if [ "$(RUNAT_JSON_PAYLOAD="$delimiter_out" read_json_text_field ok)" != "true" ]; then + echo "expected wrapper lean-run-at -- delimiter path to treat leading --stdin as text" >&2 + printf '%s\n' "$delimiter_out" >&2 + exit 1 + fi + if ! printf '%s\n' "$delimiter_out" | grep -q 'answer : Nat'; then + echo "expected wrapper lean-run-at -- delimiter path to keep the leading --stdin text as a comment" >&2 + printf '%s\n' "$delimiter_out" >&2 + exit 1 + fi + debug_text_err="$(mktemp /tmp/beam-wrapper-debug-text-XXXXXX)" + debug_text_out="$(printf 'def debugProbe : Nat :=\n 42' | BEAM_DEBUG_TEXT=1 "$beam_script" lean-run-at PositionEmptyLine.lean 1 0 --stdin 2>"$debug_text_err")" + if [ "$(RUNAT_JSON_PAYLOAD="$debug_text_out" read_json_text_field ok)" != "true" ]; then + echo "expected wrapper debug-text probe to succeed" >&2 + printf '%s\n' "$debug_text_out" >&2 + cat "$debug_text_err" >&2 + rm -f "$debug_text_err" + exit 1 + fi + if ! grep -q 'debug text for lean-run-at: source=stdin' "$debug_text_err"; then + echo "expected wrapper debug-text mode to report stdin as the text source" >&2 + cat "$debug_text_err" >&2 + rm -f "$debug_text_err" + exit 1 + fi + if ! grep -q 'containsNewline=true' "$debug_text_err"; then + echo "expected wrapper debug-text mode to report a real newline" >&2 + cat "$debug_text_err" >&2 + rm -f "$debug_text_err" + exit 1 + fi + if ! grep -q 'containsLiteralBackslashN=false' "$debug_text_err"; then + echo "expected wrapper debug-text mode to distinguish literal backslash-n from a real newline" >&2 + cat "$debug_text_err" >&2 + rm -f "$debug_text_err" + exit 1 + fi + if ! grep -q 'escaped="def debugProbe : Nat :=\\n 42"' "$debug_text_err"; then + echo "expected wrapper debug-text mode to print the escaped probe text" >&2 + cat "$debug_text_err" >&2 + rm -f "$debug_text_err" + exit 1 + fi + if ! grep -q 'utf8Hex=' "$debug_text_err" || ! grep -q '0a' "$debug_text_err"; then + echo "expected wrapper debug-text mode to print UTF-8 bytes including the newline byte" >&2 + cat "$debug_text_err" >&2 + rm -f "$debug_text_err" + exit 1 + fi + rm -f "$debug_text_err" + literal_newline_err="$(mktemp /tmp/beam-wrapper-literal-newline-XXXXXX)" + literal_newline_out="$("$beam_script" lean-run-at PositionEmptyLine.lean 1 0 'def _probe_tmp : Nat := 0\n' 2>"$literal_newline_err")" + if [ "$(RUNAT_JSON_PAYLOAD="$literal_newline_out" read_json_text_field ok)" != "true" ]; then + echo "expected wrapper literal-\\n probe to stay a payload failure, not a transport error" >&2 + printf '%s\n' "$literal_newline_out" >&2 + cat "$literal_newline_err" >&2 + rm -f "$literal_newline_err" + exit 1 + fi + if [ "$(RUNAT_JSON_PAYLOAD="$literal_newline_out" read_json_text_field result.success)" != "false" ]; then + echo "expected wrapper literal-\\n probe to fail in the run-at payload" >&2 + printf '%s\n' "$literal_newline_out" >&2 + cat "$literal_newline_err" >&2 + rm -f "$literal_newline_err" + exit 1 + fi + if ! grep -q "literal characters '\\\\n'" "$literal_newline_err"; then + echo "expected wrapper literal-\\n probe to print a newline hint" >&2 + cat "$literal_newline_err" >&2 + rm -f "$literal_newline_err" + exit 1 + fi + if ! grep -q 'probe failed inside Lean; the request completed and returned result.success=false' "$literal_newline_err"; then + echo "expected wrapper literal-\\n probe to distinguish a probe failure from a request failure" >&2 + cat "$literal_newline_err" >&2 + rm -f "$literal_newline_err" + exit 1 + fi + rm -f "$literal_newline_err" blank_ok_out="$("$beam_script" lean-run-at PositionEmptyLine.lean 1 0 "#check answer")" if [ "$(RUNAT_JSON_PAYLOAD="$blank_ok_out" read_json_text_field ok)" != "true" ]; then echo "expected wrapper blank-line probe at character 0 to succeed" >&2 @@ -298,6 +412,12 @@ fi rm -f "$blank_err" exit 1 fi + if ! grep -q 'lean-run-at request failed before probe execution (invalidParams)' "$blank_err"; then + echo "expected wrapper blank-line invalid position path to distinguish request failure from probe failure" >&2 + cat "$blank_err" >&2 + rm -f "$blank_err" + exit 1 + fi rm -f "$blank_err" utf16_ok_out="$("$beam_script" lean-run-at PositionUtf16.lean 1 5 "#check Nat")" if [ "$(RUNAT_JSON_PAYLOAD="$utf16_ok_out" read_json_text_field ok)" != "true" ]; then @@ -924,6 +1044,34 @@ EOF example : True ∧ True := by EOF + mint_handle_stdin="$(printf 'constructor' | "$beam_script" lean-run-at-handle HandleSmoke.lean 0 27 --stdin)" + if [ "$(RUNAT_JSON_PAYLOAD="$mint_handle_stdin" read_json_text_field ok)" != "true" ]; then + echo "expected wrapper handle mint via --stdin to succeed" >&2 + printf '%s\n' "$mint_handle_stdin" >&2 + exit 1 + fi + if [ "$(RUNAT_JSON_PAYLOAD="$mint_handle_stdin" read_json_text_field result.handle.backend)" != "lean" ]; then + echo "expected wrapper handle mint via --stdin to return a lean handle" >&2 + printf '%s\n' "$mint_handle_stdin" >&2 + exit 1 + fi + + handle_mint_file="handle-mint.txt" + printf 'constructor' > "$handle_mint_file" + mint_handle_file="$("$beam_script" lean-run-at-handle HandleSmoke.lean 0 27 --text-file "$handle_mint_file")" + if [ "$(RUNAT_JSON_PAYLOAD="$mint_handle_file" read_json_text_field ok)" != "true" ]; then + echo "expected wrapper handle mint via --text-file to succeed" >&2 + printf '%s\n' "$mint_handle_file" >&2 + exit 1 + fi + if [ "$(RUNAT_JSON_PAYLOAD="$mint_handle_file" read_json_text_field result.handle.backend)" != "lean" ]; then + echo "expected wrapper handle mint via --text-file to return a lean handle" >&2 + printf '%s\n' "$mint_handle_file" >&2 + exit 1 + fi + branch_handle_file="branch-handle.json" + printf '%s\n' "$mint_handle_file" > "$branch_handle_file" + mint_handle="$("$beam_script" lean-run-at-handle HandleSmoke.lean 0 27 "constructor")" if [ "$(RUNAT_JSON_PAYLOAD="$mint_handle" read_json_text_field ok)" != "true" ]; then echo "expected wrapper handle mint to succeed" >&2 @@ -936,6 +1084,57 @@ EOF exit 1 fi + branch_step_stdin_err="$(mktemp /tmp/beam-wrapper-run-with-stdin-XXXXXX)" + branch_step_stdin="$(printf 'exact trivial' | BEAM_DEBUG_TEXT=1 "$beam_script" lean-run-with HandleSmoke.lean "$mint_handle_stdin" --stdin 2>"$branch_step_stdin_err")" + if [ "$(RUNAT_JSON_PAYLOAD="$branch_step_stdin" read_json_text_field ok)" != "true" ]; then + echo "expected wrapper non-linear handle continuation via --stdin to succeed" >&2 + printf '%s\n' "$branch_step_stdin" >&2 + cat "$branch_step_stdin_err" >&2 + rm -f "$branch_step_stdin_err" + exit 1 + fi + if [ "$(RUNAT_JSON_PAYLOAD="$branch_step_stdin" read_json_text_field result.handle.backend)" != "lean" ]; then + echo "expected wrapper non-linear handle continuation via --stdin to return a successor handle" >&2 + printf '%s\n' "$branch_step_stdin" >&2 + cat "$branch_step_stdin_err" >&2 + rm -f "$branch_step_stdin_err" + exit 1 + fi + if ! grep -q 'debug text for lean-run-with: source=stdin' "$branch_step_stdin_err"; then + echo "expected wrapper run-with debug-text mode to report stdin as the continuation text source" >&2 + cat "$branch_step_stdin_err" >&2 + rm -f "$branch_step_stdin_err" + exit 1 + fi + rm -f "$branch_step_stdin_err" + + branch_step_file="$(printf 'exact trivial' | "$beam_script" lean-run-with HandleSmoke.lean --handle-file "$branch_handle_file" --stdin)" + if [ "$(RUNAT_JSON_PAYLOAD="$branch_step_file" read_json_text_field ok)" != "true" ]; then + echo "expected wrapper non-linear handle continuation via --handle-file to succeed" >&2 + printf '%s\n' "$branch_step_file" >&2 + exit 1 + fi + if [ "$(RUNAT_JSON_PAYLOAD="$branch_step_file" read_json_text_field result.handle.backend)" != "lean" ]; then + echo "expected wrapper non-linear handle continuation via --handle-file to return a successor handle" >&2 + printf '%s\n' "$branch_step_file" >&2 + exit 1 + fi + + stdin_conflict_err="$(mktemp /tmp/beam-wrapper-run-with-stdin-conflict-XXXXXX)" + if printf '%s\n' "$mint_handle" | "$beam_script" lean-run-with HandleSmoke.lean - --stdin >"$stdin_conflict_err" 2>&1; then + echo "expected wrapper run-with to reject reading both handle json and text from stdin" >&2 + cat "$stdin_conflict_err" >&2 + rm -f "$stdin_conflict_err" + exit 1 + fi + if ! grep -q 'cannot read both handle json and continuation text from stdin' "$stdin_conflict_err"; then + echo "expected wrapper run-with stdin conflict to explain the single-stdin limitation" >&2 + cat "$stdin_conflict_err" >&2 + rm -f "$stdin_conflict_err" + exit 1 + fi + rm -f "$stdin_conflict_err" + branch_step="$(printf '%s\n' "$mint_handle" | "$beam_script" lean-run-with HandleSmoke.lean - "exact trivial")" if [ "$(RUNAT_JSON_PAYLOAD="$branch_step" read_json_text_field ok)" != "true" ]; then echo "expected wrapper non-linear handle continuation to succeed" >&2 @@ -967,14 +1166,18 @@ EOF exit 1 fi - linear_step="$(printf '%s\n' "$mint_linear" | "$beam_script" lean-run-with-linear HandleSmoke.lean - "exact trivial")" + linear_text_file="linear-continuation.txt" + printf 'exact trivial' > "$linear_text_file" + linear_handle_file="linear-handle.json" + printf '%s\n' "$mint_linear" > "$linear_handle_file" + linear_step="$("$beam_script" lean-run-with-linear HandleSmoke.lean --handle-file "$linear_handle_file" --text-file "$linear_text_file")" if [ "$(RUNAT_JSON_PAYLOAD="$linear_step" read_json_text_field ok)" != "true" ]; then - echo "expected wrapper linear handle continuation to succeed" >&2 + echo "expected wrapper linear handle continuation via --handle-file and --text-file to succeed" >&2 printf '%s\n' "$linear_step" >&2 exit 1 fi if [ "$(RUNAT_JSON_PAYLOAD="$linear_step" read_json_text_field result.handle.backend)" != "lean" ]; then - echo "expected wrapper linear handle continuation to return a successor handle" >&2 + echo "expected wrapper linear handle continuation via --handle-file and --text-file to return a successor handle" >&2 printf '%s\n' "$linear_step" >&2 exit 1 fi @@ -994,9 +1197,11 @@ EOF fi rm -f "$linear_reuse_err" - release_out="$(printf '%s\n' "$linear_step" | "$beam_script" lean-release HandleSmoke.lean -)" + release_handle_file="release-handle.json" + printf '%s\n' "$linear_step" > "$release_handle_file" + release_out="$("$beam_script" lean-release HandleSmoke.lean --handle-file "$release_handle_file")" if [ "$(RUNAT_JSON_PAYLOAD="$release_out" read_json_text_field ok)" != "true" ]; then - echo "expected wrapper handle release to succeed" >&2 + echo "expected wrapper handle release via --handle-file to succeed" >&2 printf '%s\n' "$release_out" >&2 exit 1 fi @@ -1576,6 +1781,14 @@ fi rm -f "$stale_sync_err" exit 1 fi + if ! grep -q 'lean-sync request failed before a complete diagnostics barrier was available (syncBarrierIncomplete)' "$stale_sync_err"; then + echo "expected stale-import lean-sync failure to distinguish request failure from ordinary sync diagnostics" >&2 + cat "$stale_sync_json" >&2 + cat "$stale_sync_err" >&2 + rm -f "$stale_sync_json" + rm -f "$stale_sync_err" + exit 1 + fi if [ "$(RUNAT_JSON_PAYLOAD="$(cat "$stale_sync_json")" read_json_text_field error.code)" != "syncBarrierIncomplete" ]; then echo "expected stale-import lean-sync failure to expose syncBarrierIncomplete" >&2 cat "$stale_sync_json" >&2 From 0b6e15a4beec9ebe176a849683f51c202beb4149 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 22 Mar 2026 10:50:24 +0100 Subject: [PATCH 2/2] test: run shell lint in slow broker suite --- tests/test-beam-wrapper.sh | 8 ++++---- tests/test-broker-slow.sh | 3 +++ 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/tests/test-beam-wrapper.sh b/tests/test-beam-wrapper.sh index e9d84a51..6144379a 100755 --- a/tests/test-beam-wrapper.sh +++ b/tests/test-beam-wrapper.sh @@ -362,27 +362,27 @@ fi literal_newline_err="$(mktemp /tmp/beam-wrapper-literal-newline-XXXXXX)" literal_newline_out="$("$beam_script" lean-run-at PositionEmptyLine.lean 1 0 'def _probe_tmp : Nat := 0\n' 2>"$literal_newline_err")" if [ "$(RUNAT_JSON_PAYLOAD="$literal_newline_out" read_json_text_field ok)" != "true" ]; then - echo "expected wrapper literal-\\n probe to stay a payload failure, not a transport error" >&2 + printf '%s\n' "expected wrapper literal-\\n probe to stay a payload failure, not a transport error" >&2 printf '%s\n' "$literal_newline_out" >&2 cat "$literal_newline_err" >&2 rm -f "$literal_newline_err" exit 1 fi if [ "$(RUNAT_JSON_PAYLOAD="$literal_newline_out" read_json_text_field result.success)" != "false" ]; then - echo "expected wrapper literal-\\n probe to fail in the run-at payload" >&2 + printf '%s\n' "expected wrapper literal-\\n probe to fail in the run-at payload" >&2 printf '%s\n' "$literal_newline_out" >&2 cat "$literal_newline_err" >&2 rm -f "$literal_newline_err" exit 1 fi if ! grep -q "literal characters '\\\\n'" "$literal_newline_err"; then - echo "expected wrapper literal-\\n probe to print a newline hint" >&2 + printf '%s\n' "expected wrapper literal-\\n probe to print a newline hint" >&2 cat "$literal_newline_err" >&2 rm -f "$literal_newline_err" exit 1 fi if ! grep -q 'probe failed inside Lean; the request completed and returned result.success=false' "$literal_newline_err"; then - echo "expected wrapper literal-\\n probe to distinguish a probe failure from a request failure" >&2 + printf '%s\n' "expected wrapper literal-\\n probe to distinguish a probe failure from a request failure" >&2 cat "$literal_newline_err" >&2 rm -f "$literal_newline_err" exit 1 diff --git a/tests/test-broker-slow.sh b/tests/test-broker-slow.sh index 3bd8b27c..bf7230e9 100644 --- a/tests/test-broker-slow.sh +++ b/tests/test-broker-slow.sh @@ -38,6 +38,9 @@ mkdir -p "$tmp_env_root/home" "$tmp_env_root/codex" "$tmp_env_root/claude" toolchain="$(awk 'NR==1 {print $1}' lean-toolchain)" +echo "[broker-slow] shell lint" +bash scripts/lint-shell.sh > /dev/null + echo "[broker-slow] build" lake build \ RunAt:shared \