diff --git a/Beam/Broker/Protocol.lean b/Beam/Broker/Protocol.lean index e83a8974..a1c407f2 100644 --- a/Beam/Broker/Protocol.lean +++ b/Beam/Broker/Protocol.lean @@ -446,16 +446,15 @@ The generic `Request` remains the internal broker protocol used by maintenance t -/ structure ProjectRequest where private request : Request - private requestId : String private def projectRequestForbiddenFields : Array String := #["workspaceId", "workspaceMode", "daemonCapability", "root", "leanCmd", "leanPlugin", "rocqCmd"] private def ProjectRequest.supportedOp : Op → Bool - | .ensure | .openDocs | .cancel | .updateFile | .syncFile | .refreshFile | .close | .runAt + | .openDocs | .cancel | .updateFile | .syncFile | .refreshFile | .close | .runAt | .hover | .signatureHelp | .definition | .references | .documentSymbols | .workspaceSymbols | .codeActionResolve | .saveOlean | .goals | .todo | .runWith | .release | .stats => true - | .initWorkspace | .listWorkspaces | .dropWorkspace | .resetStats | .shutdown => false + | .ensure | .initWorkspace | .listWorkspaces | .dropWorkspace | .resetStats | .shutdown => false def ProjectRequest.ofRequest (request : Request) : Except String ProjectRequest := do unless ProjectRequest.supportedOp request.op do @@ -469,7 +468,7 @@ def ProjectRequest.ofRequest (request : Request) : Except String ProjectRequest if clientRequestId.isEmpty then throw "project requests require a non-empty clientRequestId" request.validateFields - pure { request, requestId := clientRequestId } + pure { request } instance : FromJson ProjectRequest where fromJson? json := do @@ -484,9 +483,6 @@ instance : FromJson ProjectRequest where def ProjectRequest.op (request : ProjectRequest) : Op := request.request.op -def ProjectRequest.clientRequestId (request : ProjectRequest) : String := - request.requestId - /-- Attach one semantic request to a selected, authenticated workspace session. -/ def ProjectRequest.attach (request : ProjectRequest) diff --git a/Beam/BrokerClient.lean b/Beam/BrokerClient.lean index c8a74911..7f7ac1d0 100644 --- a/Beam/BrokerClient.lean +++ b/Beam/BrokerClient.lean @@ -23,7 +23,7 @@ private def usage : String := "usage: beam-client [--port N] request | request-stream ", "", "beam-client is raw port-oriented maintainer/debug tooling.", - "For wrapper sessions, use: lean-beam --root PATH [--control-dir DIR] request-stream ", + "For wrapper sessions, use: lean-beam --root PATH [--session-dir DIR] request-stream ", "That supported machine interface selects the session descriptor and injects routing/authentication.", "", "request prints the final response on stdout and formats streamed diagnostics for humans on stderr.", diff --git a/Beam/Cli/Args.lean b/Beam/Cli/Args.lean index 47a30cd1..09e2be8a 100644 --- a/Beam/Cli/Args.lean +++ b/Beam/Cli/Args.lean @@ -22,7 +22,7 @@ structure CliOptions where args : List String := [] structure ParsedTextArg where - text? : Option String := none + text : String source : String := "argv" def parseNatArg (name value : String) : IO Nat := do @@ -39,7 +39,7 @@ def hasSubstring (text needle : String) : Bool := | _ => true def textArgUsage (cmdHead : String) : String := - s!"usage: beam [--root PATH] {cmdHead} [--stdin | --text-file | -- | ]" + s!"usage: beam [--root PATH] {cmdHead} (--stdin | --text-file | -- | )" def textArgReadsStdin (args : List String) : Bool := match args with @@ -48,19 +48,23 @@ def textArgReadsStdin (args : List String) : Bool := def parseTextArg (cmdHead : String) (args : List String) : IO ParsedTextArg := do match args with - | [] => pure {} + | [] => throw <| IO.userError (textArgUsage cmdHead) | ["--stdin"] => - pure { text? := some (← (← IO.getStdin).readToEnd), source := "stdin" } + pure { text := ← (← 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" } + pure { text := ← IO.FS.readFile (System.FilePath.mk path), source := s!"text-file:{path}" } + | "--" :: rest => do + let some text := joinTextArgs rest + | throw <| IO.userError (textArgUsage cmdHead) + pure { text, source := "argv" } | "--stdin" :: _ => throw <| IO.userError (textArgUsage cmdHead) | "--text-file" :: _ => throw <| IO.userError (textArgUsage cmdHead) - | _ => - pure { text? := joinTextArgs args, source := "argv" } + | _ => do + let some text := joinTextArgs args + | throw <| IO.userError (textArgUsage cmdHead) + pure { text, source := "argv" } def parseJsonText (label text : String) : IO Json := do match Json.parse text with @@ -194,6 +198,29 @@ def parseLeanTodoArgs (args : List String) : def shellQuote (text : String) : String := "'" ++ text.replace "'" "'\\''" ++ "'" +inductive WrapperSessionCommand where + | serve (backend : Backend) + | status + | stop + | recoverGeneration (generation : String) + | recoverForce + +private def WrapperSessionCommand.text : WrapperSessionCommand → String + | .serve .lean => "serve" + | .serve .rocq => "serve rocq" + | .status => "status" + | .stop => "stop" + | .recoverGeneration generation => + s!"recover --generation {shellQuote generation}" + | .recoverForce => "recover --force" + +/-- Render one exact public wrapper-session command selector. -/ +def wrapperSessionCommand + (root sessionDir : System.FilePath) + (command : WrapperSessionCommand) : String := + s!"lean-beam --root {shellQuote root.toString} " ++ + s!"--session-dir {shellQuote sessionDir.toString} {command.text}" + def parseEnvFlag (raw : String) : Bool := let normalized := raw.trimAscii.toString.toLower !(normalized.isEmpty || normalized == "0" || normalized == "false" || normalized == "no") @@ -209,22 +236,29 @@ private def resolveExplicitRootArg (root : String) : IO System.FilePath := do catch err => throw <| IO.userError s!"workspace root does not resolve: {err.toString}" -private def resolveControlDirArg (dir : String) : IO System.FilePath := do +private def resolveSessionDirArg (dir : String) : IO System.FilePath := do let path := System.FilePath.mk dir - if ← path.pathExists then - Beam.resolveExistingPath path - else - let cwd ← IO.currentDir - let absolute := if path.isAbsolute then path else cwd / path - pure absolute.normalize + unless path.isAbsolute do + throw <| IO.userError s!"--session-dir requires an absolute path, got '{path}'" + try + let metadata ← path.symlinkMetadata + match metadata.type with + | .symlink => + throw <| IO.userError <| + s!"--session-dir does not accept a symbolic-link leaf: '{path}'" + | .dir | .file | .other => + Beam.resolveExistingPath path + catch + | .noFileOrDirectory .. => Beam.resolvePathForCreation path + | err => throw err partial def parseCliOptions (opts : CliOptions) : List String → IO CliOptions | [] => pure opts | "--root" :: root :: rest => do let root ← resolveExplicitRootArg root parseCliOptions { opts with explicitRoot? := some root } rest - | "--control-dir" :: dir :: rest => do - let dir ← resolveControlDirArg dir + | "--session-dir" :: dir :: rest => do + let dir ← resolveSessionDirArg dir parseCliOptions { opts with explicitControlDir? := some dir } rest | "--port" :: port :: rest => do let port ← IO.ofExcept <| parsePortText "port" port diff --git a/Beam/Cli/Commands.lean b/Beam/Cli/Commands.lean index 8e637307..3b19a600 100644 --- a/Beam/Cli/Commands.lean +++ b/Beam/Cli/Commands.lean @@ -22,6 +22,58 @@ namespace Beam.Cli open Beam.Broker +private inductive SessionState where + | absent + | running + | stopping + | recoveryRequired + deriving BEq, Repr + +private instance : ToJson SessionState where + toJson + | .absent => "absent" + | .running => "running" + | .stopping => "stopping" + | .recoveryRequired => "recoveryRequired" + +private structure SessionStatus where + state : SessionState + workspace : String + sessionDir : String + generation? : Option String := none + detail? : Option String := none + deriving ToJson + +private structure SessionTransitionWarning where + code : String + message : String + deriving ToJson + +private structure SessionTransitionResult where + state : SessionState + changed : Bool + warning? : Option SessionTransitionWarning := none + deriving ToJson + +private structure SessionRecoveryResult where + state : SessionState + changed : Bool + generation? : Option String := none + quarantinedPath? : Option String := none + reason? : Option String := none + deriving ToJson + +private def mkSessionStatus + (state : SessionState) + (workspace sessionDir : System.FilePath) + (generation? detail? : Option String := none) : SessionStatus := { + state + workspace := workspace.toString + sessionDir := sessionDir.toString + generation? + detail? +} + private def wrapperDisplayAction (fallback : String) : IO String := do match ← IO.getEnv "BEAM_WRAPPER_COMMAND" with | some action => pure action @@ -48,15 +100,15 @@ private def runLeanRunAt (action path versionText lineText characterText : String) (textArgs : List String) (storeHandle : Bool := false) : IO Unit := do - let root ← projectRoot opts .lean let version ← parseNatArg "version" versionText let line ← parseNatArg "line" lineText let character ← parseNatArg "character" characterText let parsedText ← parseTextArg s!"{action} " textArgs + let root ← projectRoot opts .lean withProjectDaemon root .lean (explicitControlDir? := opts.explicitControlDir?) fun client => do let req ← withEnvClientRequestId <| - leanRunAtRequest root path version line character parsedText.text? (storeHandle := storeHandle) - maybeEmitTextDebug req.clientRequestId? action parsedText.source parsedText.text? + leanRunAtRequest root path version line character parsedText.text (storeHandle := storeHandle) + maybeEmitTextDebug req.clientRequestId? action parsedText.source parsedText.text callBrokerWithProgress root client req (leanRunAtWaitSpec action path line character) private def runLeanRunWith @@ -74,12 +126,12 @@ private def runLeanRunWith 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 (handle, textArgs) ← parseHandleInput s!"{action} " args let parsedText ← parseTextArg s!"{action} >" textArgs + let root ← projectRoot opts .lean let req ← withEnvClientRequestId <| - leanRunWithRequest root path handle parsedText.text? (linear := linear) - maybeEmitTextDebug req.clientRequestId? action parsedText.source parsedText.text? + leanRunWithRequest root path handle parsedText.text (linear := linear) + maybeEmitTextDebug req.clientRequestId? action parsedText.source parsedText.text withProjectDaemon root .lean (explicitControlDir? := opts.explicitControlDir?) fun client => callBrokerWithProgress root client req (leanRunWithWaitSpec path (linear := linear)) @@ -95,28 +147,54 @@ private def runLeanRelease withProjectDaemon root .lean (explicitControlDir? := opts.explicitControlDir?) fun client => callBroker root client <| leanReleaseRequest root path handle -private def shutdownProjectDaemon (opts : CliOptions) : IO Unit := do - let root ← projectRootAny opts +private def stopProjectSession (opts : CliOptions) : IO Unit := do + let root ← explicitProjectRoot opts "stop" match ← shutdownRegisteredProjectDaemon root opts.explicitControlDir? with - | .ok (some resp) => printResponse resp - | .ok none => - printJsonLine <| Json.mkObj [ - ("result", Json.mkObj [("shutdown", toJson false), ("reason", toJson ("notFound" : String))]) - ] - | .error failure => - throw <| IO.userError (← daemonFailureMessage root failure opts.explicitControlDir?) + | .absent => + printResponse <| Response.success <| + toJson ({ state := .absent, changed := false } : SessionTransitionResult) + | .alreadyStopping => + printResponse <| Response.success <| toJson ({ + state := .stopping + changed := false + } : SessionTransitionResult) + | .stopping delivery => + let warning? ← + match delivery with + | .acknowledged => pure none + | .rejected failure => + pure <| some ({ + code := "shutdownRejected" + message := failure.error.message + } : SessionTransitionWarning) + | .failed failure => + pure <| some ({ + code := "shutdownDeliveryFailed" + message := ← daemonFailureMessage root failure opts.explicitControlDir? + } : SessionTransitionWarning) + printResponse <| Response.success <| toJson ({ + state := .stopping + changed := true + warning? + } : SessionTransitionResult) private def recoverProjectSession (opts : CliOptions) (args : List String) : IO Unit := do - let root ← projectRootAny opts + let root ← explicitProjectRoot opts "recover" let (generation?, forceOpaque) ← match args with | ["--generation", generation] => pure (some generation, false) | ["--force"] => pure (none, true) | _ => throw <| IO.userError - "usage: beam [--root PATH] [--control-dir DIR] recover --generation ID | --force" + "usage: beam --root PATH [--session-dir DIR] recover --generation ID | --force" let result ← recoverProjectDaemon root generation? forceOpaque opts.explicitControlDir? - printJsonLine (toJson result) + printResponse <| Response.success <| toJson ({ + state := .absent + changed := result.recovered + generation? := result.generation? + quarantinedPath? := result.quarantinedPath? + reason? := result.reason? + } : SessionRecoveryResult) private def parseProjectRequestArg (raw : String) : IO ProjectRequest := do let text ← if raw == "-" then (← IO.getStdin).readToEnd else pure raw @@ -143,13 +221,13 @@ private def parseBackendName (name : String) : IO Backend := do | .error err => throw <| IO.userError err private def commandMaySelectPort : List String → Bool - | ["ensure", "--hold"] => true - | ["ensure", _, "--hold"] => true + | ["serve"] => true + | ["serve", _] => true | _ => false private def validateRequestedPortScope (opts : CliOptions) : IO Unit := do if opts.requestedPort?.isSome && !commandMaySelectPort opts.args then - throw <| IO.userError "--port is only valid when starting an owner with 'ensure [lean|rocq] --hold'" + throw <| IO.userError "--port is only valid when starting an owner with 'serve [lean|rocq]'" private def runThenHoldUntilInterrupted (owner : ProjectDaemonOwner) @@ -165,23 +243,46 @@ private def runThenHoldUntilInterrupted unless exitCode == 0 do throw <| IO.userError s!"owned Beam daemon exited with status {exitCode}" -private def ensureBackend +private def serveBackend (home : System.FilePath) (opts : CliOptions) - (backend : Backend) - (hold : Bool := false) : IO Unit := do + (backend : Backend) : IO Unit := do let root ← projectRoot opts backend - if hold then - withProjectDaemonOwner home root backend opts fun owner => - runThenHoldUntilInterrupted owner do - callBroker root owner.client { - op := .ensure, backend := backend, root? := some root.toString - } - (← IO.getStdout).flush - IO.eprintln "beam: owning Beam session; interrupt this wrapper process when finished" - else - withProjectDaemon root backend (explicitControlDir? := opts.explicitControlDir?) fun client => - callBroker root client { op := .ensure, backend := backend, root? := some root.toString } + withProjectDaemonOwner home root backend opts fun owner => + runThenHoldUntilInterrupted owner do + callBrokerQuiet root owner.client { + op := .ensure, backend := backend, root? := some root.toString + } + printResponse <| Response.success <| toJson <| + mkSessionStatus .running root owner.client.controlDir (some owner.generation) + (← IO.getStdout).flush + IO.eprintln <| + "beam: serving Beam session; interrupt this process or run when finished:\n" ++ + wrapperSessionCommand root owner.client.controlDir .stop + +private def sessionStatus (opts : CliOptions) : IO Unit := do + let root ← projectRootAny opts + let sessionDir ← Beam.Daemon.controlDirFor root opts.explicitControlDir? + let result : SessionStatus ← + match ← observeProjectRegistry root opts.explicitControlDir? with + | .absent => pure <| mkSessionStatus .absent root sessionDir + | .live entry => pure <| mkSessionStatus .running root sessionDir (some entry.daemonId) + | .draining entry => pure <| mkSessionStatus .stopping root sessionDir (some entry.daemonId) + | .legacy => + pure <| mkSessionStatus .recoveryRequired root sessionDir none + (some "legacy session descriptor") + | .unsupported schemaVersion => + pure <| mkSessionStatus .recoveryRequired root sessionDir none + (some s!"unsupported session descriptor schema {schemaVersion}") + | .malformed detail => + pure <| mkSessionStatus .recoveryRequired root sessionDir none (some detail) + | .selectorMismatch entry => + throw <| IO.userError <| + sessionSelectorMismatchMessage root sessionDir entry + | .unusable entry reason => + pure <| mkSessionStatus .recoveryRequired root sessionDir + (some entry.daemonId) (some reason.message) + printResponse <| Response.success (toJson result) def runCommand (home : System.FilePath) (opts : CliOptions) : IO Unit := do validateRequestedPortScope opts @@ -215,14 +316,10 @@ def runCommand (home : System.FilePath) (opts : CliOptions) : IO Unit := do printMcpConfig home opts | "feedback-report" :: args => Beam.Cli.Feedback.run home opts args - | "ensure" :: [] => - ensureBackend home opts .lean - | "ensure" :: "--hold" :: [] => - ensureBackend home opts .lean (hold := true) - | "ensure" :: backend :: [] => - ensureBackend home opts (← parseBackendName backend) - | "ensure" :: backend :: "--hold" :: [] => - ensureBackend home opts (← parseBackendName backend) (hold := true) + | "serve" :: [] => + serveBackend home opts .lean + | "serve" :: backend :: [] => + serveBackend home opts (← parseBackendName backend) | "lean-run-at" :: path :: version :: line :: character :: text => runLeanRunAt opts (← wrapperDisplayAction "lean-run-at") path version line character text | "lean-run-at-handle" :: path :: version :: line :: character :: text => @@ -417,8 +514,10 @@ def runCommand (home : System.FilePath) (opts : CliOptions) : IO Unit := do let root ← projectRootAny opts withExistingProjectDaemon root (explicitControlDir? := opts.explicitControlDir?) fun client => callBroker root client { op := .resetStats } - | "shutdown" :: [] => - shutdownProjectDaemon opts + | "status" :: [] => + sessionStatus opts + | "stop" :: [] => + stopProjectSession opts | "recover" :: args => recoverProjectSession opts args | "request-stream" :: raw :: [] => diff --git a/Beam/Cli/DaemonManager.lean b/Beam/Cli/DaemonManager.lean index fbff39e0..46786433 100644 --- a/Beam/Cli/DaemonManager.lean +++ b/Beam/Cli/DaemonManager.lean @@ -49,7 +49,6 @@ live but stuck wrapper process. Longer bundle build locks intentionally use the unbounded lock helper. -/ private structure ProjectControl where - root : System.FilePath dir : System.FilePath registry : System.FilePath @@ -57,98 +56,35 @@ private def projectControl (root : System.FilePath) (explicitControlDir? : Option System.FilePath := none) : IO ProjectControl := do let dir ← controlDirFor root explicitControlDir? - pure { root, dir, registry := dir / "beam-daemon.json" } - -private def privateControlDirRights : IO.FileRight := { - user := { read := true, write := true, execution := true } -} - -private def privateControlDirMode : UInt32 := - privateControlDirRights.flags - -private def invalidControlDirMessage (dir detail : String) : String := - s!"unsafe Beam control directory {dir}: {detail}. Select a dedicated directory that is a real " ++ - "directory with mode 0700; Beam does not change permissions on existing paths" - -private def permissionModeText (mode : UInt32) : String := - let value := mode.toNat - s!"0{value / 64}{(value / 8) % 8}{value % 8}" - -private inductive ControlDirObservation where - | absent - | privateDir - | symlink - | nonPrivate (mode : UInt32) - | notDirectory - -/-- Inspect the exact control leaf without following a final symbolic link. -/ -private def observeControlDir (dir : System.FilePath) : IO ControlDirObservation := do - try - let metadata ← dir.symlinkMetadata - match metadata.type with - | .dir => - let mode ← Beam.fileModeNoFollow dir - if mode == privateControlDirMode then - pure .privateDir - else - pure <| .nonPrivate mode - | .symlink => pure .symlink - | .file | .other => pure .notDirectory - catch - | .noFileOrDirectory .. => pure .absent - | err => throw err + pure { dir, registry := dir / "beam-daemon.json" } private def rejectControlDirObservation - (dir : System.FilePath) : ControlDirObservation → IO Unit - | .symlink => - throw <| IO.userError <| - invalidControlDirMessage dir.toString "symbolic links are not accepted" - | .nonPrivate mode => - throw <| IO.userError <| - invalidControlDirMessage dir.toString - s!"existing mode is {permissionModeText mode}, expected 0700" - | .notDirectory => - throw <| IO.userError <| - invalidControlDirMessage dir.toString "the path is not a directory" - | .absent => - throw <| IO.userError <| - invalidControlDirMessage dir.toString "the path disappeared during control preparation" - | .privateDir => pure () + (dir : System.FilePath) + (observation : Beam.PrivateDirObservation) : IO Unit := do + Beam.requirePrivateDir "Beam session directory" dir observation + +/-- Validate an existing session selection without creating it; absence remains observable. -/ +private def validateControlDirForObservation (dir : System.FilePath) : IO Unit := do + match ← Beam.observePrivateDir dir with + | .absent | .privateDir => pure () + | observation => rejectControlDirObservation dir observation -/-- Accept an existing control path only when it is a real, account-private directory. -/ -private def validatePrivateControlDir (dir : System.FilePath) : IO Unit := do - rejectControlDirObservation dir (← observeControlDir dir) +/-- Recognize absence without creating a session directory or accepting an unsafe existing leaf. -/ +private def sessionDescriptorAbsent (control : ProjectControl) : IO Bool := do + match ← Beam.observePrivateDir control.dir with + | .absent => pure true + | .privateDir => + match ← readRegistryAt control.registry with + | .absent => pure true + | .legacy | .unsupported _ | .malformed _ | .current _ => pure false + | .symlink | .nonPrivate _ | .notDirectory => pure false /-- Create a missing dedicated control leaf as private, or validate an existing path without mutating it. The directory is ready before Beam creates its lock or any capability-bearing descriptor. -/ private def preparePrivateControlDir (dir : System.FilePath) : IO Unit := do - match ← observeControlDir dir with - | .privateDir => return - | .absent => pure () - | observation => rejectControlDirObservation dir observation - if let some parent := dir.parent then - IO.FS.createDirAll parent - try - IO.FS.createDir dir - catch - | .alreadyExists .. => - -- A concurrent owner may have created the leaf after our absent observation. Never adopt it - -- implicitly: apply the same read-only validation as any other existing path. - validatePrivateControlDir dir - return - | err => throw err - try - -- This chmod is restricted to the leaf created successfully by this invocation. - IO.setAccessRights dir privateControlDirRights - validatePrivateControlDir dir - catch err => - try - IO.FS.removeDir dir - catch _ => - pure () - throw err + Beam.ensurePrivateDir "Beam session directory" dir /-- Supply project registry mutation only for the dynamic extent of the project control lock. -/ private def withProjectControl @@ -169,8 +105,9 @@ private def withExistingProjectControl (act : ProjectControl → IO Unit) (explicitControlDir? : Option System.FilePath := none) : IO Unit := do let control ← projectControl root explicitControlDir? - unless ← control.dir.isDir do - return + match ← Beam.observePrivateDir control.dir with + | .privateDir => pure () + | .absent | .symlink | .nonPrivate _ | .notDirectory => return try withExistingLockTimeout (control.dir / "lock") (← projectControlLockTimeoutMs) do act control @@ -271,7 +208,6 @@ def requestDaemonShutdown inductive RegistryUnsafeReason where | invalidIdentity - | wrongRegistryRoot (recordedRoot : String) | invalidEndpoint | endpointUnavailable | endpointUnrecognized (detail : String) @@ -286,16 +222,17 @@ inductive RegistryObservation where | malformed (detail : String) | live (entry : SessionDescriptor) | draining (entry : SessionDescriptor) + | selectorMismatch (entry : SessionDescriptor) | unusable (entry : SessionDescriptor) (reason : RegistryUnsafeReason) /-- Select the unique descriptor binding for a canonical or filesystem-equivalent project root. -/ def sessionWorkspaceForRoot? (entry : SessionDescriptor) (root : System.FilePath) : IO (Option WorkspaceBinding) := do - for workspace in entry.workspaces do - if ← Beam.sameFilePath (System.FilePath.mk workspace.root) root then - return some workspace - pure none + if ← Beam.sameFilePath (System.FilePath.mk entry.workspace.root) root then + pure (some entry.workspace) + else + pure none private def observeProjectRegistryAt (root registry : System.FilePath) : IO RegistryObservation := do @@ -308,7 +245,7 @@ private def observeProjectRegistryAt if entry.daemonId.isEmpty || entry.capability.isEmpty then return .unusable entry .invalidIdentity let some workspace ← sessionWorkspaceForRoot? entry root - | return .unusable entry (.wrongRegistryRoot entry.rootSummary) + | return .selectorMismatch entry if entry.lifecycle == .draining then return .draining entry let some endpoint := registryEndpoint? entry @@ -324,10 +261,16 @@ private def observeProjectRegistryAt | .wrongGeneration daemonRoot => pure <| .unusable entry (.wrongGeneration daemonRoot) +private def observeProjectControl + (root : System.FilePath) + (control : ProjectControl) : IO RegistryObservation := do + validateControlDirForObservation control.dir + observeProjectRegistryAt root control.registry + def observeProjectRegistry (root : System.FilePath) (explicitControlDir? : Option System.FilePath := none) : IO RegistryObservation := do - observeProjectRegistryAt root (← registryPathFor root explicitControlDir?) + observeProjectControl root (← projectControl root explicitControlDir?) private def requestedPortNat? (opts : CliOptions) : Option Nat := opts.requestedPort?.map (·.toNat) @@ -665,16 +608,15 @@ private def registryEntryFor pid ownerPid := ownerPid.toNat port? - workspaces := #[{ + workspace := { workspaceId := projectDaemonWorkspaceId root := desired.root.toString - configHash := desired.configHash leanCmd? := desired.leanCmd? plugin? := desired.plugin?.map (·.toString) rocqCmd? := desired.rocqCmd? toolchain? := desired.toolchain? bundleId? := some desired.bundleId - }] + } configHash := desired.configHash clientBin? := some desired.clientBin.toString daemonBin? := some desired.daemonBin.toString @@ -811,7 +753,6 @@ structure SelectedProjectDaemon where def RegistryUnsafeReason.message : RegistryUnsafeReason → String | .invalidIdentity => "registry identity or capability is empty" - | .wrongRegistryRoot recordedRoot => s!"registry records another root: {recordedRoot}" | .invalidEndpoint => "registry endpoint is invalid" | .endpointUnavailable => "the recorded daemon endpoint is unavailable" | .endpointUnrecognized detail => s!"the recorded endpoint is not a recognized Beam generation: {detail}" @@ -819,87 +760,143 @@ def RegistryUnsafeReason.message : RegistryUnsafeReason → String | .wrongGeneration daemonRoot => s!"the recorded endpoint serves another Beam generation for {daemonRoot}" -private def activeOwnerMessage (root : System.FilePath) (entry : SessionDescriptor) : String := - s!"Beam session for {root} is already owned by wrapper pid {entry.ownerPid}; " ++ - "interrupt that 'lean-beam ensure --hold' process before starting another owner" +private def activeOwnerMessage (root : System.FilePath) : String := + s!"Beam session for {root} is already owned by a foreground process; " ++ + "interrupt that 'lean-beam serve' process before starting another owner" private def configMismatchMessage (root : System.FilePath) + (sessionDir : System.FilePath) (entry : SessionDescriptor) - (expectedHash : String) : String := + (expectedHash : String) + (backend : Backend) : String := s!"the live Beam session for {root} uses configuration {entry.configHash}, " ++ s!"but this command requires {expectedHash}; the current owner was preserved. " ++ - "Interrupt its 'lean-beam ensure --hold' process, then start a new owner with the desired configuration" + "Interrupt its foreground owner, then start a new one with the desired configuration:\n" ++ + wrapperSessionCommand root sessionDir (.serve backend) private def drainingOwnerMessage (root : System.FilePath) (entry : SessionDescriptor) : String := s!"Beam session {entry.daemonId} for {root} is draining; " ++ "wait for its foreground owner to exit before starting or attaching to another session" -private def registryRecoveryMessage (root : System.FilePath) (detail : String) : String := +def sessionSelectorMismatchMessage + (root sessionDir : System.FilePath) + (entry : SessionDescriptor) : String := + let recordedRoot := entry.workspace.root + s!"sessionSelectorMismatch: selected workspace {root}, but Beam session {entry.daemonId} " ++ + s!"in {sessionDir} belongs to workspace {recordedRoot}. Use the recorded exact selector:\n" ++ + wrapperSessionCommand (System.FilePath.mk recordedRoot) sessionDir .status + +private def registryRecoveryMessage + (root : System.FilePath) + (detail : String) : String := s!"Beam cannot safely use or replace the daemon registry for {root}: {detail}. " ++ "The session remains fenced; preserve its descriptor and use explicit recovery with the same " ++ - "--root and --control-dir selection after stopping the matching owner or daemon" + "--root and --session-dir selection after stopping the matching owner or daemon" private def generationRecoveryMessage (root : System.FilePath) + (sessionDir : System.FilePath) (entry : SessionDescriptor) (reason : RegistryUnsafeReason) : String := let message := registryRecoveryMessage root reason.message - match reason with - | .wrongRegistryRoot recordedRoots => - message ++ "; recovery must select one of the descriptor's recorded workspace roots " ++ - s!"({recordedRoots}) with the same --control-dir; the selected root {root} cannot recover " ++ - s!"session {entry.daemonId}" - | _ => - message ++ "; run " ++ - s!"'lean-beam --root {root} recover --generation {entry.daemonId}' when recovery is safe" + let recovery := wrapperSessionCommand root sessionDir + (.recoverGeneration entry.daemonId) + message ++ s!"; when recovery is safe, run:\n{recovery}" private def registryReadRecoveryMessage (root : System.FilePath) + (sessionDir : System.FilePath) (registryRead : RegistryRead) : String := registryRecoveryMessage root - (registryRead.detail?.getD s!"unexpected registry state '{registryRead.status}'") ++ - "; opaque state can be quarantined explicitly with " ++ - "'lean-beam --root ROOT recover --force'" + (registryRead.detail?.getD s!"unexpected registry state '{registryRead.status}'") ++ + "; opaque state can be quarantined explicitly with:\n" ++ + wrapperSessionCommand root sessionDir .recoverForce + +private inductive RegistryDrainTransition where + | committed + | alreadyDraining + | changedUnderfoot -private def markRegistryDraining (control : ProjectControl) (entry : SessionDescriptor) : IO Unit := do +private def markRegistryDraining + (control : ProjectControl) + (entry : SessionDescriptor) : IO RegistryDrainTransition := do match ← readRegistryAt control.registry with | .current current => - if sameRegistryGeneration current entry && current.lifecycle == .live then + if !sameRegistryGeneration current entry then + pure .changedUnderfoot + else if current.lifecycle == .draining then + pure .alreadyDraining + else writeExistingRegistry control { current with lifecycle := .draining } - | .absent | .legacy | .unsupported _ | .malformed _ => pure () + pure .committed + | .absent | .legacy | .unsupported _ | .malformed _ => pure .changedUnderfoot private inductive ShutdownPlan where | none - | request (entry : SessionDescriptor) + | alreadyStopping + | committed (entry : SessionDescriptor) + +/-- Delivery of the authenticated shutdown request after the draining fence was committed. -/ +inductive ProjectDaemonStopDelivery where + | acknowledged + | rejected (failure : ResponseFailure) + | failed (failure : BrokerClientFailure) + +/-- Authoritative state committed by an explicit wrapper-session stop operation. -/ +inductive ProjectDaemonStopResult where + | absent + | alreadyStopping + | stopping (delivery : ProjectDaemonStopDelivery) /-- Fence and request shutdown of the exact wrapper-owned generation without PID signalling. -/ def shutdownRegisteredProjectDaemon (root : System.FilePath) (explicitControlDir? : Option System.FilePath := none) : - IO (Except BrokerClientFailure (Option Response)) := do + IO ProjectDaemonStopResult := do + let selected ← projectControl root explicitControlDir? + if ← sessionDescriptorAbsent selected then + return .absent let plan : ShutdownPlan ← withProjectControl root (explicitControlDir? := explicitControlDir?) fun control => do match ← observeProjectRegistryAt root control.registry with | .absent => pure ShutdownPlan.none | .live entry => - markRegistryDraining control entry - pure <| ShutdownPlan.request entry - | .draining entry => pure <| ShutdownPlan.request entry + match ← markRegistryDraining control entry with + | .committed => pure <| ShutdownPlan.committed entry + | .alreadyDraining => pure ShutdownPlan.alreadyStopping + | .changedUnderfoot => + throw <| IO.userError <| + "Beam session descriptor changed while committing its draining fence; " ++ + "the shutdown request was not sent" + | .draining _ => pure ShutdownPlan.alreadyStopping | .legacy => - throw <| IO.userError <| registryReadRecoveryMessage root .legacy + throw <| IO.userError <| registryReadRecoveryMessage root control.dir .legacy | .unsupported schemaVersion => - throw <| IO.userError <| registryReadRecoveryMessage root (.unsupported schemaVersion) + throw <| IO.userError <| + registryReadRecoveryMessage root control.dir (.unsupported schemaVersion) | .malformed detail => - throw <| IO.userError <| registryReadRecoveryMessage root (.malformed detail) + throw <| IO.userError <| registryReadRecoveryMessage root control.dir (.malformed detail) + | .selectorMismatch entry => + throw <| IO.userError <| + sessionSelectorMismatchMessage root control.dir entry | .unusable entry reason => - throw <| IO.userError <| generationRecoveryMessage root entry reason + throw <| IO.userError <| generationRecoveryMessage root control.dir entry reason match plan with - | ShutdownPlan.none => pure <| .ok none - | ShutdownPlan.request entry => - let some endpoint := registryEndpoint? entry - | return .error <| .invalidResponse "draining Beam registry has no valid endpoint" - pure <| (← requestDaemonShutdown endpoint entry.capability).map some + | .none => pure .absent + | .alreadyStopping => pure .alreadyStopping + | .committed entry => + let delivery ← + match registryEndpoint? entry with + | none => + pure <| ProjectDaemonStopDelivery.failed <| + .invalidResponse "draining Beam session descriptor has no valid endpoint" + | some endpoint => + match ← requestDaemonShutdown endpoint entry.capability with + | .ok (.successResult ..) => pure .acknowledged + | .ok (.errorResult failure) => pure <| .rejected failure + | .error failure => pure <| .failed failure + pure <| .stopping delivery structure RecoveryResult where recovered : Bool @@ -933,6 +930,9 @@ def recoverProjectDaemon (generation? : Option String) (forceOpaque : Bool) (explicitControlDir? : Option System.FilePath := none) : IO RecoveryResult := do + let selected ← projectControl root explicitControlDir? + if ← sessionDescriptorAbsent selected then + return { recovered := false, reason? := some "absent" } withProjectControl root (explicitControlDir? := explicitControlDir?) fun control => do match ← readRegistryAt control.registry with | .absent => @@ -947,7 +947,7 @@ def recoverProjectDaemon let some workspace ← sessionWorkspaceForRoot? entry root | throw <| IO.userError <| s!"selected root {root} is not a workspace in session {entry.daemonId}; " ++ - s!"recorded workspace roots: {entry.rootSummary}" + s!"recorded workspace root: {entry.workspace.root}" if ← registeredGenerationResponds root workspace entry then throw <| IO.userError <| s!"Beam session {entry.daemonId} still responds; stop its foreground owner or use authenticated shutdown" @@ -995,6 +995,9 @@ def ProjectDaemonOwner.exitCode? (owner : ProjectDaemonOwner) : IO (Option UInt3 owner.exitCodeRef.set (some exitCode) pure exitCode? +def ProjectDaemonOwner.generation (owner : ProjectDaemonOwner) : String := + owner.daemonId + /-- Whether this owner generation is still the one published for its project. -/ def ProjectDaemonOwner.registered (owner : ProjectDaemonOwner) : IO Bool := do match ← readRegistryAt (owner.controlDir / "beam-daemon.json") with @@ -1003,35 +1006,45 @@ def ProjectDaemonOwner.registered (owner : ProjectDaemonOwner) : IO Bool := do current.capability == owner.client.capability && current.lifecycle == .live) | .absent | .legacy | .unsupported _ | .malformed _ => pure false -private def missingOwnerCommand : Option Backend → String - | some .rocq => "lean-beam ensure rocq --hold" - | some .lean | none => "lean-beam ensure --hold" +private def missingOwnerCommand : Option Backend → WrapperSessionCommand + | some .rocq => .serve .rocq + | some .lean | none => .serve .lean -private def missingOwnerMessage (root : System.FilePath) (backend? : Option Backend) : String := +private def missingOwnerMessage + (root sessionDir : System.FilePath) + (backend? : Option Backend) : String := + let command := wrapperSessionCommand root sessionDir (missingOwnerCommand backend?) s!"no live Beam session owner is registered for {root}; " ++ - s!"start '{missingOwnerCommand backend?}' for this project and keep it running while using wrapper commands" + s!"start this foreground owner and keep it running while using wrapper commands:\n{command}" private def startOwnedProjectDaemon (control : ProjectControl) (desired : DesiredConfig) + (backend : Backend) (opts : CliOptions) : IO OwnedProjectDaemon := do match ← observeProjectRegistryAt desired.root control.registry with | .absent => pure () | .live entry => if entry.configHash == desired.configHash then - throw <| IO.userError (activeOwnerMessage desired.root entry) + throw <| IO.userError (activeOwnerMessage desired.root) else - throw <| IO.userError (configMismatchMessage desired.root entry desired.configHash) + throw <| IO.userError + (configMismatchMessage desired.root control.dir entry desired.configHash backend) | .draining entry => throw <| IO.userError (drainingOwnerMessage desired.root entry) | .legacy => - throw <| IO.userError <| registryReadRecoveryMessage desired.root .legacy + throw <| IO.userError <| registryReadRecoveryMessage desired.root control.dir .legacy | .unsupported schemaVersion => throw <| IO.userError <| - registryReadRecoveryMessage desired.root (.unsupported schemaVersion) + registryReadRecoveryMessage desired.root control.dir (.unsupported schemaVersion) | .malformed detail => - throw <| IO.userError <| registryReadRecoveryMessage desired.root (.malformed detail) + throw <| IO.userError <| + registryReadRecoveryMessage desired.root control.dir (.malformed detail) + | .selectorMismatch entry => + throw <| IO.userError <| + sessionSelectorMismatchMessage desired.root control.dir entry | .unusable entry reason => - throw <| IO.userError <| generationRecoveryMessage desired.root entry reason + throw <| IO.userError <| + generationRecoveryMessage desired.root control.dir entry reason let (endpoint, entry, child) ← startDaemonEntry desired opts control.dir try writeRegistry control entry @@ -1083,28 +1096,69 @@ private def attemptCleanup (act : IO Unit) : IO Unit := do catch _ => pure () +private inductive OwnedDaemonFinish where + | exitedCleanly + | forcedReaped + | exitedAbnormally (exitCode : UInt32) + | unreaped + +private def classifyOwnedDaemonExit (exitCode : UInt32) : OwnedDaemonFinish := + if exitCode == 0 then .exitedCleanly else .exitedAbnormally exitCode + +private def forceOwnedDaemonChild + {cfg : IO.Process.StdioConfig} + (child : IO.Process.Child cfg) + (exitCodeRef : IO.Ref (Option UInt32)) : IO OwnedDaemonFinish := do + let killSent ← + try + child.kill + pure true + catch _ => + pure false + attemptCleanup <| waitForOwnedDaemonExit child exitCodeRef 20 + match ← exitCodeRef.get with + | some exitCode => + if killSent then pure .forcedReaped else pure <| classifyOwnedDaemonExit exitCode + | none => pure .unreaped + private def finishOwnedDaemonChild (owned : OwnedProjectDaemon) - (exitCodeRef : IO.Ref (Option UInt32)) : IO Bool := do + (exitCodeRef : IO.Ref (Option UInt32)) : IO OwnedDaemonFinish := do + if let some exitCode ← exitCodeRef.get then + return classifyOwnedDaemonExit exitCode try let child ← closeDaemonOwnerPipe owned.child attemptCleanup <| waitForOwnedDaemonExit child exitCodeRef 100 - if (← exitCodeRef.get).isNone then - -- `startDaemon` uses `setsid`; Lean's retained child handle therefore kills the complete - -- daemon process group rather than only the broker PID. - attemptCleanup child.kill - attemptCleanup <| waitForOwnedDaemonExit child exitCodeRef 20 + match ← exitCodeRef.get with + | some exitCode => pure <| classifyOwnedDaemonExit exitCode + | none => + -- `startDaemon` uses `setsid`; Lean's retained child handle therefore kills the complete + -- daemon process group rather than only the broker PID. + forceOwnedDaemonChild child exitCodeRef catch _ => - attemptCleanup owned.child.kill - attemptCleanup <| waitForOwnedDaemonExit owned.child exitCodeRef 20 - pure (← exitCodeRef.get).isSome + forceOwnedDaemonChild owned.child exitCodeRef private def markOwnedRegistryDraining (root controlDir : System.FilePath) (entry : SessionDescriptor) : IO Unit := do try withExistingProjectControl root (explicitControlDir? := some controlDir) fun control => - markRegistryDraining control entry + discard <| markRegistryDraining control entry + catch _ => + pure () + +private def restoreOwnedRegistryRecoveryFence + (root controlDir : System.FilePath) + (entry : SessionDescriptor) : IO Unit := do + try + withExistingProjectControl root (explicitControlDir? := some controlDir) fun control => do + match ← readRegistryAt control.registry with + | .current current => + if sameRegistryGeneration current entry && current.lifecycle == .draining then + -- A current `live` descriptor whose endpoint no longer responds projects to the public + -- `recoveryRequired` state. Restore that conservative fence after a failed drain. + writeExistingRegistry control { current with lifecycle := .live } + | .absent | .legacy | .unsupported _ | .malformed _ => pure () catch _ => pure () @@ -1127,13 +1181,19 @@ private def finishOwnedProjectDaemon | .current current => pure (sameRegistryGeneration current owned.entry && current.lifecycle == .draining) | .absent | .legacy | .unsupported _ | .malformed _ => pure false - markOwnedRegistryDraining root controlDir owned.entry if exitedBeforeOwnerCleanup && !registryWasDraining then -- An unexpected daemon exit is not evidence that its complete process tree disappeared. Keep - -- the exact generation fenced for explicit, non-signalling recovery. + -- the exact live generation fenced so observation projects it to recovery-required state. pure () - else if ← finishOwnedDaemonChild owned exitCodeRef then - removeOwnedRegistry root controlDir owned.entry + else + markOwnedRegistryDraining root controlDir owned.entry + match ← finishOwnedDaemonChild owned exitCodeRef with + | .exitedCleanly | .forcedReaped => + removeOwnedRegistry root controlDir owned.entry + | .exitedAbnormally _ => + restoreOwnedRegistryRecoveryFence root controlDir owned.entry + | .unreaped => + pure () def withProjectDaemonOwner (home root : System.FilePath) @@ -1146,7 +1206,7 @@ def withProjectDaemonOwner preparePrivateControlDir controlDir let desired ← desiredConfig home root backend let owned ← withProjectControl root (explicitControlDir? := some controlDir) fun control => - startOwnedProjectDaemon control desired opts + startOwnedProjectDaemon control desired backend opts let exitCodeRef ← IO.mkRef (none : Option UInt32) try act { @@ -1165,21 +1225,25 @@ private def lookupProjectDaemon (backend? : Option Backend := none) (explicitControlDir? : Option System.FilePath := none) : IO SelectedProjectDaemon := do let control ← projectControl root explicitControlDir? - match ← observeProjectRegistryAt root control.registry with + match ← observeProjectControl root control with | .live entry => let workspace ← selectWorkspaceBackend root entry backend? pure { client := ← projectDaemonClient entry workspace control.dir, workspace } | .absent => - throw <| IO.userError (missingOwnerMessage root backend?) + throw <| IO.userError (missingOwnerMessage root control.dir backend?) | .draining entry => throw <| IO.userError (drainingOwnerMessage root entry) | .legacy => - throw <| IO.userError <| registryReadRecoveryMessage root .legacy + throw <| IO.userError <| registryReadRecoveryMessage root control.dir .legacy | .unsupported schemaVersion => - throw <| IO.userError <| registryReadRecoveryMessage root (.unsupported schemaVersion) + throw <| IO.userError <| + registryReadRecoveryMessage root control.dir (.unsupported schemaVersion) | .malformed detail => - throw <| IO.userError <| registryReadRecoveryMessage root (.malformed detail) + throw <| IO.userError <| registryReadRecoveryMessage root control.dir (.malformed detail) + | .selectorMismatch entry => + throw <| IO.userError <| + sessionSelectorMismatchMessage root control.dir entry | .unusable entry reason => - throw <| IO.userError <| generationRecoveryMessage root entry reason + throw <| IO.userError <| generationRecoveryMessage root control.dir entry reason def withProjectDaemon (root : System.FilePath) diff --git a/Beam/Cli/Feedback.lean b/Beam/Cli/Feedback.lean index f668570e..c6a3d8e8 100644 --- a/Beam/Cli/Feedback.lean +++ b/Beam/Cli/Feedback.lean @@ -134,6 +134,10 @@ private def collectDaemonPayload pure (Json.null, Json.null, warnings.push "the Beam daemon registry schema is unsupported") | .malformed detail => pure (Json.null, Json.null, warnings.push s!"the Beam daemon registry is malformed: {detail}") + | .selectorMismatch entry => + let controlDir ← Beam.Daemon.controlDirFor root explicitControlDir? + pure (Json.null, Json.null, warnings.push <| + sessionSelectorMismatchMessage root controlDir entry) | .unusable _ reason => pure (Json.null, Json.null, warnings.push s!"the Beam daemon registry is unsafe: {reason.message}") diff --git a/Beam/Cli/Info.lean b/Beam/Cli/Info.lean index 7faa7ee3..3398fbc1 100644 --- a/Beam/Cli/Info.lean +++ b/Beam/Cli/Info.lean @@ -191,6 +191,10 @@ def doctor (home : System.FilePath) (opts : CliOptions) (backend : Backend) : IO | .malformed detail => IO.println "daemon status: malformed registry" IO.println s!"registry error: {detail}" + | .selectorMismatch entry => + IO.println "daemon status: session selector mismatch" + IO.println <| sessionSelectorMismatchMessage root + (← Beam.Daemon.controlDirFor root opts.explicitControlDir?) entry | .unusable _ reason => IO.println "daemon status: unsafe" IO.println s!"daemon safety error: {reason.message}" diff --git a/Beam/Cli/LeanOperation.lean b/Beam/Cli/LeanOperation.lean index 099931d1..ef40e158 100644 --- a/Beam/Cli/LeanOperation.lean +++ b/Beam/Cli/LeanOperation.lean @@ -15,52 +15,24 @@ open Beam.Broker private def rootText (root : System.FilePath) : String := root.toString -private def storeHandleFlag (storeHandle : Bool) : Option Bool := - if storeHandle then some true else none - def leanRunAtRequest (root : System.FilePath) (path : String) (version : Nat) (line character : Nat) - (text? : Option String) + (text : String) (storeHandle : Bool := false) : Request := - match text? with - | some text => - ({ path, version, line, character, text } : Beam.Lean.RunAtInput).toBrokerRequest - (rootText root) (storeHandle := storeHandle) - | none => - { - op := .runAt - backend := .lean - root? := some (rootText root) - path? := some path - version? := some version - line? := some line - character? := some character - storeHandle? := storeHandleFlag storeHandle - } + ({ path, version, line, character, text } : Beam.Lean.RunAtInput).toBrokerRequest + (rootText root) (storeHandle := storeHandle) def leanRunWithRequest (root : System.FilePath) (path : String) (handle : Handle) - (text? : Option String) + (text : String) (linear : Bool := false) : Request := - match text? with - | some text => - ({ path, handle, text } : Beam.Lean.RunWithInput).toBrokerRequest - (rootText root) (linear := linear) - | none => - { - op := .runWith - backend := .lean - root? := some (rootText root) - path? := some path - handle? := some handle - storeHandle? := some true - linear? := some linear - } + ({ path, handle, text } : Beam.Lean.RunWithInput).toBrokerRequest + (rootText root) (linear := linear) def leanReleaseRequest (root : System.FilePath) (path : String) (handle : Handle) : Request := ({ path, handle } : Beam.Lean.ReleaseInput).toBrokerRequest (rootText root) diff --git a/Beam/Cli/Output.lean b/Beam/Cli/Output.lean index f575a77f..1ef32948 100644 --- a/Beam/Cli/Output.lean +++ b/Beam/Cli/Output.lean @@ -44,21 +44,20 @@ def annotateRunatMessage (clientRequestId? : Option String) (msg : String) : Str private def debugTextEnabled : IO Bool := do pure <| (← envFlag? "BEAM_DEBUG_TEXT").getD false -def maybeEmitTextDebug (clientRequestId? : Option String) (action source : String) (text? : Option String) : IO Unit := do +def maybeEmitTextDebug + (clientRequestId? : Option String) + (action source text : 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}" + 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}" def decodeRunAtResult? (resp : Response) : Option Beam.LSP.RunAt.Result := match resp.result? with diff --git a/Beam/Cli/Project.lean b/Beam/Cli/Project.lean index 4a496c2f..b64352ad 100644 --- a/Beam/Cli/Project.lean +++ b/Beam/Cli/Project.lean @@ -72,16 +72,32 @@ def projectRoot (opts : CliOptions) (backend : Backend) : IO System.FilePath := let backendName := match backend with | .lean => "lean" | .rocq => "rocq" throw <| IO.userError s!"could not infer {backendName} project root; use --root PATH" +def inferProjectRootAny (start : System.FilePath) : IO System.FilePath := do + let leanRoot? ← findRootUpwards start .lean + let rocqRoot? ← findRootUpwards start .rocq + match leanRoot?, rocqRoot? with + | none, none => + throw <| IO.userError "could not infer project root; use --root PATH" + | some root, none | none, some root => + pure root + | some leanRoot, some rocqRoot => + if ← Beam.sameFilePath leanRoot rocqRoot then + pure leanRoot + else + throw <| IO.userError <| + "project root is ambiguous; found both " ++ + s!"Lean root {leanRoot} and Rocq root {rocqRoot}; use --root PATH" + def projectRootAny (opts : CliOptions) : IO System.FilePath := do + match opts.explicitRoot? with + | some root => pure root + | none => inferProjectRootAny (System.FilePath.mk ".") + +def explicitProjectRoot (opts : CliOptions) (action : String) : IO System.FilePath := do match opts.explicitRoot? with | some root => pure root | none => - if let some root ← findRootUpwards (System.FilePath.mk ".") .lean then - pure root - else if let some root ← findRootUpwards (System.FilePath.mk ".") .rocq then - pure root - else - throw <| IO.userError "could not infer project root; use --root PATH" + throw <| IO.userError s!"{action} requires an explicit --root PATH" def leanToolchain (root : System.FilePath) : IO String := do let path := root / "lean-toolchain" diff --git a/Beam/Cli/RuntimeBundle/Paths.lean b/Beam/Cli/RuntimeBundle/Paths.lean index 22e89efc..f8cc7def 100644 --- a/Beam/Cli/RuntimeBundle/Paths.lean +++ b/Beam/Cli/RuntimeBundle/Paths.lean @@ -6,6 +6,7 @@ Author: Emilio J. Gallego Arias import Lean import Beam.LSP.Lib.NativeLib +import Beam.System open Lean @@ -103,35 +104,16 @@ def runtimeBundleCacheRoot (root : System.FilePath) : IO System.FilePath := do | some path => pure (System.FilePath.mk path) | none => pure (beamStateDir root / runtimeBundlesDirName) -private def privateBeamStateDirRights : IO.FileRight := { - user := { read := true, write := true, execution := true } -} - /-- Create the project-local Beam state leaf privately when runtime bundle construction is the first -Beam operation for a project. Existing state directories are never chmodded: wrapper ownership -applies its stricter control-directory validation separately. +Beam operation for a project. Existing state directories are validated but never chmodded. -/ def runtimeBundleCacheRootForWrite (root : System.FilePath) : IO System.FilePath := do match ← IO.getEnv "BEAM_BUNDLE_DIR" with | some path => pure (System.FilePath.mk path) | none => let stateDir := beamStateDir root - unless ← stateDir.pathExists do - try - IO.FS.createDir stateDir - catch - | .alreadyExists .. => - return stateDir / runtimeBundlesDirName - | err => throw err - try - IO.setAccessRights stateDir privateBeamStateDirRights - catch err => - try - IO.FS.removeDir stateDir - catch _ => - pure () - throw err + Beam.ensurePrivateDir "Beam project state directory" stateDir pure (stateDir / runtimeBundlesDirName) def validatedLeanToolchainsPath (home : System.FilePath) : System.FilePath := diff --git a/Beam/Cli/Usage.lean b/Beam/Cli/Usage.lean index dd434bf8..baf8309f 100644 --- a/Beam/Cli/Usage.lean +++ b/Beam/Cli/Usage.lean @@ -13,10 +13,9 @@ def usage : String := "usage:", " beam --version", " beam version", - " beam [--root PATH] ensure [lean|rocq]", - " beam [--root PATH] [--port N] ensure [lean|rocq] --hold", - " beam [--root PATH] lean-run-at [--stdin | --text-file | -- | ]", - " beam [--root PATH] lean-run-at-handle [--stdin | --text-file | -- | ]", + " beam [--root PATH] [--session-dir DIR] [--port N] serve [lean|rocq]", + " beam [--root PATH] lean-run-at (--stdin | --text-file | -- | )", + " beam [--root PATH] lean-run-at-handle (--stdin | --text-file | -- | )", " beam [--root PATH] lean-hover ", " beam [--root PATH] lean-signature-help ", " beam [--root PATH] lean-definition ", @@ -25,8 +24,8 @@ def usage : String := " beam [--root PATH] lean-workspace-symbols ", " beam [--root PATH] lean-goals before|after ", " beam [--root PATH] lean-todo [--kind ...] [--suggest none|basic]", - " beam [--root PATH] lean-run-with > [--stdin | --text-file | -- | ]", - " beam [--root PATH] lean-run-with-linear > [--stdin | --text-file | -- | ]", + " beam [--root PATH] lean-run-with > (--stdin | --text-file | -- | )", + " beam [--root PATH] lean-run-with-linear > (--stdin | --text-file | -- | )", " beam [--root PATH] lean-release >", " beam [--root PATH] lean-update ", " beam [--root PATH] lean-sync [+all-diagnostics]", @@ -46,12 +45,13 @@ def usage : String := " beam [--root PATH] cancel ", " beam [--root PATH] stats", " beam [--root PATH] reset-stats", - " beam [--root PATH] shutdown", - " beam [--root PATH] [--control-dir DIR] recover --generation ID | --force", - " beam --root PATH [--control-dir DIR] request-stream ", + " beam [--root PATH] [--session-dir DIR] status", + " beam --root PATH [--session-dir DIR] stop", + " beam --root PATH [--session-dir DIR] recover --generation ID | --force", + " beam --root PATH [--session-dir DIR] request-stream ", "", - "Project-session commands accept --control-dir DIR as an exact alternate control selection.", - "Use the same --root and --control-dir for owner, attachment, diagnostics, shutdown, and recovery.", + "Project-session commands accept an absolute --session-dir DIR as an exact alternate session selection.", + "Use the same --root and --session-dir for serving, attachment, diagnostics, stopping, and recovery.", "Beam never applies source edits to `.lean` files on disk; the client applies source edits.", "Lean edit loop: save the file, then run lean-update for a broker document version.", "Run lean-sync when you need the diagnostics/readiness barrier. lean-save is lean-sync plus a", @@ -64,9 +64,8 @@ def usage : String := "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.", - "Wrapper commands require one live session owner. Start ensure --hold in a foreground process", - "and keep it running across wrapper invocations; interrupt it or run shutdown when finished.", - "Plain ensure checks and warms that owned session but never starts one implicitly.", + "Wrapper commands require one live session owner. Start serve in a foreground process", + "and keep it running across wrapper invocations; interrupt it or run stop when finished.", "Abnormal session state remains fenced until recover --generation ID quarantines that record.", "Beam does not upload or submit feedback. Use feedback-report to print a pasteable report", "with cheap version, stats, open-files, daemon registry, and daemon incident context.", diff --git a/Beam/Daemon/Debug.lean b/Beam/Daemon/Debug.lean index 80eabc5a..cb16885f 100644 --- a/Beam/Daemon/Debug.lean +++ b/Beam/Daemon/Debug.lean @@ -108,14 +108,13 @@ def daemonRegistryContext? | .malformed detail => pure <| some s!"Beam daemon registry ({path}):\n status: malformed\n detail: {detail}" | .current entry => - let workspaceLines := entry.workspaces.toList.flatMap fun workspace => - ([ - s!" workspace: {workspace.workspaceId}", - s!" root: {workspace.root}", - s!" configHash: {workspace.configHash}" - ] ++ - (optionLine " toolchain" workspace.toolchain?).toList ++ - (optionLine " bundleId" workspace.bundleId?).toList) + let workspace := entry.workspace + let workspaceLines := [ + s!" workspace: {workspace.workspaceId}", + s!" root: {workspace.root}" + ] ++ + (optionLine " toolchain" workspace.toolchain?).toList ++ + (optionLine " bundleId" workspace.bundleId?).toList let lines := ([ s!"Beam daemon registry ({path}):", s!" schemaVersion: {entry.schemaVersion}", diff --git a/Beam/Daemon/Paths.lean b/Beam/Daemon/Paths.lean index 3bd0c1d7..5f3e96fe 100644 --- a/Beam/Daemon/Paths.lean +++ b/Beam/Daemon/Paths.lean @@ -5,13 +5,14 @@ Author: Emilio J. Gallego Arias -/ import Lean +import Beam.Path namespace Beam.Daemon private def beamStateDir (root : System.FilePath) : System.FilePath := root / ".beam" -/-- Stable FNV-1a tag used only for deterministic `BEAM_CONTROL_ROOT` discovery. -/ +/-- Stable FNV-1a tag used only for deterministic `BEAM_SESSION_ROOT` discovery. -/ private def controlRootTag (root : System.FilePath) : String := let hash := root.toString.toUTF8.foldl (fun acc byte => (acc ^^^ byte.toUInt64) * 1099511628211) @@ -24,12 +25,13 @@ def controlDirFor match explicitControlDir? with | some dir => pure dir | none => - match ← IO.getEnv "BEAM_CONTROL_ROOT" with + match ← IO.getEnv "BEAM_SESSION_ROOT" with | some base => let base := System.FilePath.mk base unless base.isAbsolute do throw <| IO.userError - s!"BEAM_CONTROL_ROOT must be an absolute path, got '{base}'" + s!"BEAM_SESSION_ROOT must be an absolute path, got '{base}'" + let base ← Beam.resolvePathForCreation base pure (base / controlRootTag root) | none => pure (beamStateDir root) diff --git a/Beam/Daemon/Protocol.lean b/Beam/Daemon/Protocol.lean index 50dc0ea6..cf8ee5cc 100644 --- a/Beam/Daemon/Protocol.lean +++ b/Beam/Daemon/Protocol.lean @@ -16,7 +16,7 @@ namespace Beam.Daemon open Beam.Broker def registrySchemaVersion : Nat := - 2 + 3 inductive RegistryLifecycle where | live @@ -38,7 +38,6 @@ instance : FromJson RegistryLifecycle where structure WorkspaceBinding where workspaceId : WorkspaceId root : String - configHash : String leanCmd? : Option String := none plugin? : Option String := none rocqCmd? : Option String := none @@ -49,9 +48,8 @@ structure WorkspaceBinding where /-- The private descriptor for one wrapper-owned CLI session. -The descriptor is deliberately shaped as a session with a nonempty workspace collection even -while the public owner command creates one workspace. This keeps session identity separate from -workspace routing and leaves static multi-workspace ownership as an additive CLI feature. +Wrapper sessions deliberately own exactly one workspace. Standalone broker and MCP runtimes retain +their independent multi-workspace models. -/ structure SessionDescriptor where schemaVersion : Nat @@ -61,7 +59,7 @@ structure SessionDescriptor where pid : Nat ownerPid : Nat port? : Option Nat := none - workspaces : Array WorkspaceBinding + workspace : WorkspaceBinding /-- Hash of the complete frozen session configuration. -/ configHash : String clientBin? : Option String := none @@ -70,9 +68,6 @@ structure SessionDescriptor where requestedPort? : Option Nat := none deriving FromJson, ToJson -def SessionDescriptor.rootSummary (entry : SessionDescriptor) : String := - String.intercalate ", " <| entry.workspaces.toList.map (·.root) - def SessionDescriptor.identity (entry : SessionDescriptor) : DaemonIdentity := { daemonId := entry.daemonId configHash := entry.configHash @@ -104,7 +99,7 @@ def endpointFromEntry (entry : SessionDescriptor) : IO Transport.Endpoint := do | some endpoint => pure endpoint | none => let message := - s!"invalid Beam daemon transport data for session {entry.daemonId} ({entry.rootSummary})" + s!"invalid Beam daemon transport data for session {entry.daemonId} ({entry.workspace.root})" throw (IO.userError message) def endpointSummary (endpoint : Transport.Endpoint) : String := diff --git a/Beam/Daemon/Registry.lean b/Beam/Daemon/Registry.lean index 3c6eb9d7..1ab751c4 100644 --- a/Beam/Daemon/Registry.lean +++ b/Beam/Daemon/Registry.lean @@ -37,29 +37,14 @@ def RegistryRead.detail? : RegistryRead → Option String | .malformed detail => some detail | .absent | .current _ => none -private def validateWorkspaceBindings (workspaces : Array WorkspaceBinding) : Except String Unit := do - if workspaces.isEmpty then - throw "session descriptor must contain at least one workspace" - let mut ids : Std.TreeSet String compare := {} - let mut roots : Std.TreeSet String compare := {} - for workspace in workspaces do - if workspace.workspaceId.isEmpty then - throw "session workspace id must not be empty" - if workspace.root.isEmpty then - throw s!"session workspace '{workspace.workspaceId}' has an empty root" - let rootPath := System.FilePath.mk workspace.root - unless rootPath.isAbsolute do - throw s!"session workspace '{workspace.workspaceId}' root is not absolute" - if workspace.configHash.isEmpty then - throw s!"session workspace '{workspace.workspaceId}' has an empty configuration hash" - if ids.contains workspace.workspaceId then - throw s!"duplicate session workspace id '{workspace.workspaceId}'" - let normalizedRoot := rootPath.normalize.toString - if roots.contains normalizedRoot then - throw s!"duplicate session workspace root '{workspace.root}'" - ids := ids.insert workspace.workspaceId - roots := roots.insert normalizedRoot - +private def validateWorkspaceBinding (workspace : WorkspaceBinding) : Except String Unit := do + if workspace.workspaceId.isEmpty then + throw "session workspace id must not be empty" + if workspace.root.isEmpty then + throw s!"session workspace '{workspace.workspaceId}' has an empty root" + let rootPath := System.FilePath.mk workspace.root + unless rootPath.isAbsolute do + throw s!"session workspace '{workspace.workspaceId}' root is not absolute" private def validateSessionDescriptor (entry : SessionDescriptor) : Except String Unit := do if entry.daemonId.isEmpty then throw "session descriptor daemonId must not be empty" @@ -67,7 +52,7 @@ private def validateSessionDescriptor (entry : SessionDescriptor) : Except Strin throw "session descriptor capability must not be empty" if entry.configHash.isEmpty then throw "session descriptor configuration hash must not be empty" - validateWorkspaceBindings entry.workspaces + validateWorkspaceBinding entry.workspace def readRegistryAt (path : System.FilePath) : IO RegistryRead := do unless ← path.pathExists do diff --git a/Beam/Feedback.lean b/Beam/Feedback.lean index 45ed8f71..7c4b483c 100644 --- a/Beam/Feedback.lean +++ b/Beam/Feedback.lean @@ -7,6 +7,7 @@ Author: Emilio J. Gallego Arias import Lean import Beam.JsonPretty import Beam.Path +import Beam.System open Lean @@ -796,6 +797,9 @@ private def writePreparedBundle if input.bundle == .none then pure result else + if opts.outputDir?.isNone then + if let some root := opts.root? then + Beam.ensurePrivateDir "Beam project state directory" (root / ".beam") let bundleDir ← resolveBundleDir input collection opts IO.FS.createDirAll bundleDir let home? ← if input.redact then IO.getEnv "HOME" else pure none diff --git a/Beam/Lean/Operation.lean b/Beam/Lean/Operation.lean index 7f021183..86fe28cf 100644 --- a/Beam/Lean/Operation.lean +++ b/Beam/Lean/Operation.lean @@ -111,7 +111,7 @@ private def operationDescription : Operation → String | .closeSave => "Read and synchronize the current on-disk Lean source, write the same Lean/Lake build artifacts when possible, and close the tracked LSP document." | .close => "Close the tracked LSP document." -private def sourceFileInvariant : String := +def sourceFileInvariant : String := "Beam never applies source edits to `.lean` files on disk; the client applies source edits." private def executesSuppliedLeanText : Operation → Bool @@ -121,14 +121,13 @@ private def executesSuppliedLeanText : Operation → Bool private def speculativeIoCaveat : String := "Speculative execution isolates Beam's source and document state, but it is not an OS sandbox; Lean commands and project metaprogramming may perform IO." -private def progressDiscovery : String := - "For detailed live updates, clients can pass `tools/call` `_meta.progressToken`; without one, Beam emits one status log when setup or a long-running request is detected and the request's logging policy admits notice-level events." - -def Operation.description (operation : Operation) : String := +def Operation.behaviorDescription (operation : Operation) : String := String.intercalate " " <| [operationDescription operation] ++ - (if executesSuppliedLeanText operation then [speculativeIoCaveat] else []) ++ - [progressDiscovery, sourceFileInvariant] + (if executesSuppliedLeanText operation then [speculativeIoCaveat] else []) + +def Operation.description (operation : Operation) : String := + String.intercalate " " [operation.behaviorDescription, sourceFileInvariant] private def pathField : String × Json := ("path", Beam.JsonSchema.string "Lean file path, relative to the server root unless absolute.") diff --git a/Beam/Mcp/Projection.lean b/Beam/Mcp/Projection.lean index 05ad69e9..3b0bb63e 100644 --- a/Beam/Mcp/Projection.lean +++ b/Beam/Mcp/Projection.lean @@ -141,6 +141,11 @@ def beamVersionDescription : String := def beamStatsDescription : String := "Return process-wide debug Beam broker runtime statistics for lazily cached workspaces." +private def progressDiscovery (delayedActivity : String) : String := + "For detailed live updates, clients can pass `tools/call` `_meta.progressToken`; without one, " ++ + s!"Beam emits one status log when {delayedActivity} and the request's logging policy admits " ++ + "notice-level events." + def beamFeedbackReportDescription : String := String.intercalate " " [ "Beam does not upload or submit feedback. This tool creates and returns a pasteable feedback report for one explicit workspace.", @@ -148,8 +153,7 @@ def beamFeedbackReportDescription : String := "Set confidential for non-public workspaces; confidential results retain caller-authored narrative", "except for HOME-path redaction and do not scan it for other secrets; never post them publicly.", "A local evidence bundle is optional.", - "For detailed live updates, clients can pass `tools/call` `_meta.progressToken`; without one,", - "Beam emits one status log when collection is delayed and the request's logging policy admits notice-level events." + progressDiscovery "collection is delayed" ] open Beam.JsonSchema in @@ -217,7 +221,11 @@ def feedbackReportInputSchema : Json := ] (Beam.Feedback.requiredInputFields.push "workspace") def dropWorkspaceDescription : String := - "Evict one local Lean workspace cache and invalidate its retained proof handles. A later request recreates it lazily. For detailed live updates, clients can pass `tools/call` `_meta.progressToken`; without one, Beam emits one status log when eviction is delayed and the request's logging policy admits notice-level events." + String.intercalate " " [ + "Evict one local Lean workspace cache and invalidate its retained proof handles.", + "A later request recreates it lazily.", + progressDiscovery "eviction is delayed" + ] open Beam.JsonSchema in def dropWorkspaceInputSchema : Json := @@ -246,7 +254,12 @@ def ToolName.descriptor (tool : ToolName) : ToolDescriptor := | .beamVersion => (beamVersionDescription, emptyInputSchema) | .beamStats => (beamStatsDescription, emptyInputSchema) | .beamFeedbackReport => (beamFeedbackReportDescription, feedbackReportInputSchema) - | .leanOperation op => (op.description, schemaWithWorkspace op.inputSchema) + | .leanOperation op => + (String.intercalate " " [ + op.behaviorDescription, + progressDiscovery "setup or a long-running request is detected", + Beam.Lean.sourceFileInvariant + ], schemaWithWorkspace op.inputSchema) | .leanDropWorkspace => (dropWorkspaceDescription, dropWorkspaceInputSchema) { name := tool, description, inputSchema, annotations := tool.annotations } diff --git a/Beam/Path.lean b/Beam/Path.lean index 63c62d31..fd052b0a 100644 --- a/Beam/Path.lean +++ b/Beam/Path.lean @@ -20,6 +20,27 @@ def regularNonSymlinkFile (path : System.FilePath) : IO Bool := do def resolveExistingPath (path : System.FilePath) : IO System.FilePath := IO.FS.realPath path +/-- +Resolve the existing prefix of `path`, then append its missing suffix. + +This gives a path selected before creation the same canonical spelling it will have afterward. In +particular, aliases in an existing ancestor such as macOS `/tmp` are resolved even when the selected +leaf does not exist yet. +-/ +partial def resolvePathForCreation (path : System.FilePath) : IO System.FilePath := do + try + resolveExistingPath path + catch + | .noFileOrDirectory .. => + let some parent := path.parent + | throw <| IO.userError s!"cannot resolve a creation parent for '{path}'" + let some name := path.fileName + | throw <| IO.userError s!"cannot resolve a creation leaf for '{path}'" + -- Resolve before normalizing: lexical normalization would give the wrong meaning to `..` + -- after an existing symbolic-link ancestor. Normalize only the rebuilt canonical path. + pure <| ((← resolvePathForCreation parent) / name).normalize + | err => throw err + /-- Resolve `path`, interpreting relative paths under an already-resolved `root`. -/ def resolvePathAgainstRoot (root path : System.FilePath) : IO System.FilePath := resolveExistingPath <| if path.isAbsolute then path else root / path diff --git a/Beam/System.lean b/Beam/System.lean index fb13a9d9..f6e05e35 100644 --- a/Beam/System.lean +++ b/Beam/System.lean @@ -17,6 +17,100 @@ private opaque lstatMode (path : @& String) : IO UInt32 def fileModeNoFollow (path : System.FilePath) : IO UInt32 := lstatMode path.toString +def privateDirRights : IO.FileRight := { + user := { read := true, write := true, execution := true } +} + +def privateDirMode : UInt32 := + privateDirRights.flags + +/-- Classification of one exact directory leaf without following a final symbolic link. -/ +inductive PrivateDirObservation where + | absent + | privateDir + | symlink + | nonPrivate (mode : UInt32) + | notDirectory + deriving BEq, Repr + +def permissionModeText (mode : UInt32) : String := + let value := mode.toNat + s!"0{value / 64}{(value / 8) % 8}{value % 8}" + +def PrivateDirObservation.problem : PrivateDirObservation → Option String + | .privateDir => none + | .absent => some "the path disappeared during private-directory preparation" + | .symlink => some "symbolic links are not accepted" + | .nonPrivate mode => + some s!"existing mode is {permissionModeText mode}, expected 0700" + | .notDirectory => some "the path is not a directory" + +/-- Inspect an exact directory leaf without following its final symbolic link. -/ +def observePrivateDir (dir : System.FilePath) : IO PrivateDirObservation := do + try + let metadata ← dir.symlinkMetadata + match metadata.type with + | .dir => + let mode ← fileModeNoFollow dir + if mode == privateDirMode then + pure .privateDir + else + pure <| .nonPrivate mode + | .symlink => pure .symlink + | .file | .other => pure .notDirectory + catch + | .noFileOrDirectory .. => pure .absent + | err => throw err + +/-- +Create a missing private directory leaf, or observe an existing leaf without changing it. + +Only the leaf successfully created by this call is changed to mode `0700`. A concurrent or +pre-existing path is returned as observed so the caller can reject it without hidden mutation. +-/ +def preparePrivateDir (dir : System.FilePath) : IO PrivateDirObservation := do + match ← observePrivateDir dir with + | .privateDir => return .privateDir + | .absent => pure () + | observation => return observation + if let some parent := dir.parent then + IO.FS.createDirAll parent + try + IO.FS.createDir dir + catch + | .alreadyExists .. => return ← observePrivateDir dir + | err => throw err + try + IO.setAccessRights dir privateDirRights + let observation ← observePrivateDir dir + unless observation == .privateDir do + try + IO.FS.removeDir dir + catch _ => + pure () + pure observation + catch err => + try + IO.FS.removeDir dir + catch _ => + pure () + throw err + +def requirePrivateDir + (label : String) + (dir : System.FilePath) + (observation : PrivateDirObservation) : IO Unit := do + match observation.problem with + | none => pure () + | some problem => + throw <| IO.userError <| + s!"unsafe {label} {dir}: {problem}. Select a dedicated directory that is a real " ++ + "directory with mode 0700; Beam does not change permissions on existing paths" + +/-- Create a missing private leaf or validate an existing one without adopting it. -/ +def ensurePrivateDir (label : String) (dir : System.FilePath) : IO Unit := do + requirePrivateDir label dir (← preparePrivateDir dir) + def trimLine (text : String) : String := text.trimAscii.toString diff --git a/CHANGELOG.md b/CHANGELOG.md index ad268338..37bcf431 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -33,10 +33,21 @@ This project keeps a lightweight, reverse-chronological changelog. Dates use `YY ### Changed -- Wrapper daemons now have explicit session ownership: only `lean-beam ensure --hold` starts a - generation, ordinary wrapper commands attach to it, `--port` is accepted only by that owner-start - command, and holder exit cancels admitted requests before closing the daemon through an inherited - pipe without heartbeat leases or time-based retirement +- Wrapper lifecycle commands now use the explicit `serve`, `status`, and `stop` vocabulary; + `stop` and `recover` require `--root`, alternate selectors use `--session-dir`, and wrapper + descriptors contain exactly one frozen workspace. Successful lifecycle commands use typed + `ok`/`result` envelopes, diagnostics preserve the complete session selector, and every wrapper + observation revalidates the selected directory without following a symbolic-link leaf. Project + state writers share private-directory preparation, and Lean execution commands require text at + the typed CLI boundary instead of constructing incomplete broker requests. Missing session paths + canonicalize their existing ancestor before creation, abnormal daemon exits project to + `recoveryRequired`, selector mismatches stay separate from lifecycle state, and repeated `stop` + reports `changed: false` + ([#243](https://github.com/leanprover/lean-beam/pull/243), @ejgallego). +- Wrapper daemons now have explicit session ownership: only the foreground owner command starts a + generation, ordinary wrapper commands attach to it, `--port` is owner-only, and holder exit + cancels admitted requests before closing the daemon through an inherited pipe without heartbeat + leases or time-based retirement ([#241](https://github.com/leanprover/lean-beam/pull/241), @ejgallego). - Long-running Lean operations now separate liveness status, request progress, and diagnostics. Sync and refresh use the discoverable `diagnostic_scope: "errors" | "all"` and @@ -97,7 +108,7 @@ This project keeps a lightweight, reverse-chronological changelog. Dates use `YY instead of accepting any existing filesystem entry at an artifact path. - Install and prune control-file reads now reject non-regular or symlinked paths, and a failed lock owner-PID write removes the lock directory acquired by that process. -- `lean-beam ensure --hold` now exits cleanly and promptly after `SIGINT`. +- `lean-beam serve` now exits cleanly and promptly after `SIGINT`. - `lean-save` and `lean-close-save` now stage and commit complete artifact sets, preserving prior outputs on reported failure or cancellation and preventing same-worker saves from mixing files ([#217](https://github.com/leanprover/lean-beam/pull/217), @ejgallego). diff --git a/README.md b/README.md index 61839176..da81088f 100644 --- a/README.md +++ b/README.md @@ -104,7 +104,7 @@ including structured Lake options, dynamic libraries, and plugins already applie worker. Modules with batch-only `moreLeanArgs` fail with `saveUnsupportedSetup`: move shared `-D` settings to `leanOptions`, or use `lake build` when the arguments are intentionally batch-only. A running Lean server is not guaranteed to pick up Lake workspace configuration changes; after such a -change, run `lean-beam shutdown`, then start a new foreground `lean-beam ensure --hold` wrapper +change, run `lean-beam --root ROOT stop`, then start a new foreground `lean-beam serve` wrapper session before the next wrapper command that uses the Lean server. A successful checkpoint is normally sufficient while working; do not add an expensive clean build to every Beam loop. Final project validation should come from CI running `lake build` from clean Lake artifacts. diff --git a/docs/COMPATIBILITY.md b/docs/COMPATIBILITY.md index 29ff8bb6..09bb602e 100644 --- a/docs/COMPATIBILITY.md +++ b/docs/COMPATIBILITY.md @@ -20,9 +20,10 @@ A Lean release line is the canonical `major.minor` family recorded in - Runtime bundle metadata schema 2 and install manifest schema 3. Install manifest schema 2 is cleanup-only compatibility during the 0.2 release line: identity and `lean-beam prune` may read it, but the installer does not reuse it. Remove the schema-2 decoder when 0.3 development opens. -- CLI session descriptor schema 2. It freezes a nonempty array of workspace bindings plus one - generation identity, lifecycle, endpoint, and capability. Schema-less, schema-1, and unknown - records are reported and remain fenced; normal startup does not decode, delete, or migrate them. +- CLI session descriptor schema 3. It freezes one workspace binding plus one + generation identity, lifecycle, endpoint, and capability. Schema-less, schema-1, the superseded + schema-2 multi-binding shape, and unknown records are reported and remain fenced; + normal startup does not decode, delete, or migrate them. After independently stopping the generation that wrote an opaque record, an operator may quarantine it with `lean-beam --root ROOT recover --force`. Current descriptors instead require their exact generation ID. Persisted PIDs are never recovery signal capabilities. diff --git a/docs/CUSTOM_TOOLCHAINS.md b/docs/CUSTOM_TOOLCHAINS.md index 946d0187..3240f1ae 100644 --- a/docs/CUSTOM_TOOLCHAINS.md +++ b/docs/CUSTOM_TOOLCHAINS.md @@ -93,4 +93,4 @@ BEAM_STAGE0_TOOLCHAIN=lean4-dev bash tests/test-stage0-toolchain.sh The smoke skips when the requested elan toolchain is unavailable. When it runs, it installs Beam with `--custom-toolchain`, checks that `doctor` resolves the installed bundle and reports a -fingerprint, then starts and closes an explicit `ensure --hold` wrapper session. +fingerprint, then starts and closes an explicit `serve` wrapper session. diff --git a/docs/DEVELOPMENT.md b/docs/DEVELOPMENT.md index 67d4108f..4fab4f28 100644 --- a/docs/DEVELOPMENT.md +++ b/docs/DEVELOPMENT.md @@ -62,7 +62,7 @@ Preferred maintainer entrypoints: - new Codex task: `./scripts/codex-harness.sh session start ` - risky wrapper/install validation: `bash scripts/validate-defensive.sh` - public workflow checks: `lean-beam` and the skill docs -- sandboxed repeated wrapper probes: `lean-beam ensure --hold`, then interrupt that foreground +- sandboxed repeated wrapper probes: `lean-beam serve`, then interrupt that foreground process when the probe loop is finished - contributor process questions: [CONTRIBUTING.md](../CONTRIBUTING.md) @@ -250,8 +250,8 @@ Broker requests remain a shared record for the CLI, MCP projection, and daemon t ownership is operation-specific. Update `Op.optionalRequestFields` with every new broker field and keep `Request.validateFields` at both the JSON decoder and direct dispatch boundary. Do not let an operation silently ignore a field owned by another operation. The broker protocol's `.cancel` -operation is process-wide and is identified only by `cancelRequestId`; it does not carry a workspace -or root selector. +operation is workspace-scoped and is identified by that workspace plus `cancelRequestId`; the +supported wrapper machine surface injects its fixed workspace and does not let callers select one. Broker `Response` and `StreamMessage` values are tagged unions internally. Their explicit JSON codecs retain the public `ok` and `kind` discriminants while preventing mismatched payloads from @@ -400,11 +400,9 @@ broker-derived decision. This wrapper path is easy to break accidentally, so keep the mental model simple. -A CLI session descriptor is the schema-versioned `beam-daemon.json` selected by the control -directory. It contains one generation identity, capability, lifecycle, endpoint, and a nonempty -array of frozen workspace bindings. The public owner command currently creates one binding; the -shape permits a future explicitly configured static multi-workspace session without changing -request routing. Exactly one foreground `lean-beam ensure --hold` process owns the generation. It +A CLI session descriptor is the schema-versioned `beam-daemon.json` selected by the session +directory. It contains one generation identity, capability, lifecycle, endpoint, and one frozen +workspace binding. Exactly one foreground `lean-beam serve` process owns the generation. It starts the daemon in a dedicated process session, passes the identity, effective configuration hash, and random capability through piped stdin, and retains the pipe's write end. Before creating the lock or descriptor, Beam creates a missing control leaf with mode `0700`, or validates that an @@ -427,42 +425,51 @@ by an attaching command. Persisted PIDs are display-only diagnostics, never prob used as automatic stale-reclamation proof. Only the foreground owner may force termination, through its retained child handle and process group. -The owner watches its exact descriptor generation and daemon child. `lean-beam shutdown` changes +The owner watches its exact descriptor generation and daemon child. `lean-beam --root ROOT stop` changes that generation from `live` to `draining` under the control lock before sending authenticated -shutdown. Normal holder exit likewise publishes `draining`, closes its pipe, waits for graceful +shutdown. A repeated stop observes the committed drain and does not deliver another request; a +post-commit delivery failure is presentation detail rather than a rollback of the fence. Normal +holder exit likewise publishes `draining`, closes its pipe, waits for graceful teardown, and, after the deadline, terminates the owned process group. It removes only the exact -generation after owned cleanup completes. An unexpected daemon or owner exit deliberately leaves -the descriptor fenced: startup does not infer complete process-tree exit from persisted PIDs. Once +generation after owned cleanup completes. A nonzero daemon exit during graceful drain restores the +exact conservative fence instead of clearing it; a controlled process-group kill that reaps the +leader completes normal owner cleanup. An unexpected daemon exit preserves its exact live +descriptor so endpoint observation reports recovery-required state. An unexpected owner exit also +deliberately leaves the descriptor fenced: startup does not infer complete process-tree exit from +persisted PIDs. Once the operator establishes that the old session is no longer authoritative, `lean-beam --root ROOT recover --generation ID` quarantines that exact descriptor without signalling any recorded process. Opaque legacy, unsupported, or malformed state requires `recover --force`. A paused holder keeps its pipe open and remains valid without expiry. If the project root disappears, cleanup uses the already resolved control path without recreating the project. -Human commands may infer the nearest project root. The supported machine stream requires explicit +Human commands may infer a project root only when the Lean and Rocq candidates agree or exactly one +exists; otherwise they report every candidate and require `--root`. The supported machine stream requires explicit `--root` and a nonempty `clientRequestId`; its semantic JSON cannot supply `root`, `workspaceId`, capability, dynamic workspace operations, or process-wide control operations such as `shutdown` and `resetStats`. The wrapper selects the descriptor binding and injects session metadata. Lifecycle -shutdown remains the dedicated `lean-beam shutdown` command so it can publish `draining` first. Raw +shutdown remains the dedicated `lean-beam --root ROOT stop` command so it can publish `draining` first. Raw port-oriented `beam-client` requests are maintainer/debug tooling. A wrapper-owned daemon rejects `initWorkspace`, `listWorkspaces`, and `dropWorkspace`; a separately launched broker retains the generic multi-workspace surface and has its own explicit owner. Broker runtime ownership is a typed `ServerMode`: wrapper identity and capability cannot be constructed independently. -The default control directory is `/.beam`, discoverable to project-scoped agents. -`--control-dir DIR` is an exact, stateless selection that every participant must repeat. -`BEAM_CONTROL_ROOT` must be absolute and hashes each canonical root below a writable base for +The default session directory is `/.beam`, discoverable to project-scoped agents. +An absolute `--session-dir DIR` is an exact, stateless selection that every participant must repeat. +`BEAM_SESSION_ROOT` must be absolute, resolves the base through its longest existing ancestor, and +hashes each canonical root below that writable base for sandboxed/read-only roots. The selected directory is private to one local account; coordination is supported between that account's processes, not across a group-shared control directory. Existing directories must be prepared explicitly as mode `0700`; validation rejects symlinks, other file types, and broader permissions without mutating them. -Do not hide policy inside automatic fallback between these locations. A future multi-root CLI owner -should require a stable explicit control directory and freeze all bindings before publication. +Do not hide policy inside automatic fallback between these locations. Wrapper descriptors stay +single-workspace until a concrete multi-workspace CLI design defines explicit configuration and +workspace selection. Keep these invariants covered: -- only `ensure --hold` may create and publish a wrapper daemon generation +- only `serve` may create and publish a wrapper daemon generation - a second owner is rejected while the current endpoint/root/generation identity is live - ordinary wrapper commands are read-only with respect to registry and process lifecycle, including in ambiguous or unsafe state; they attach to frozen owner configuration rather than recomputing it diff --git a/docs/MCP.md b/docs/MCP.md index 4e7e3749..12f6e3a9 100644 --- a/docs/MCP.md +++ b/docs/MCP.md @@ -133,7 +133,7 @@ inside the old Lean process is not sufficient to reload workspace configuration. ## Transport Lifetime The `lean-beam-mcp` stdio process owns its optional in-process broker runtime. MCP clients do not -start or attach to a wrapper daemon and do not need a separate `lean-beam ensure --hold` owner. The +start or attach to a wrapper daemon and do not need a separate `lean-beam serve` owner. The first Lean operation that needs broker execution creates the runtime lazily; later descriptors share that runtime while the broker remains authoritative for workspace membership. Feedback and cache eviction can inspect or update an absent runtime without creating one. `lean_drop_workspace` evicts @@ -339,7 +339,7 @@ scope ends, so a late cancellation cannot affect a later request even if a broke is reused. EOF is the transport shutdown in both supported revisions. `lean-beam-mcp` defines no private -shutdown request. This is separate from `lean-beam shutdown`, which sends the typed shutdown +shutdown request. This is separate from `lean-beam --root ROOT stop`, which sends the typed shutdown operation directly to a Beam broker daemon. ## Progress And Diagnostic Logs diff --git a/docs/ROCQ.md b/docs/ROCQ.md index eb7b18f6..4204d9fc 100644 --- a/docs/ROCQ.md +++ b/docs/ROCQ.md @@ -56,7 +56,7 @@ Rocq commands are available through the same installed `lean-beam` wrapper: ```bash # keep this foreground owner running in one terminal/session -lean-beam ensure rocq --hold +lean-beam serve rocq # issue probes from another terminal/session lean-beam doctor rocq @@ -66,7 +66,7 @@ lean-beam rocq-goals-prev "Demo.v" 2 8 "intro x." ``` The holder is the explicit owner of the wrapper daemon and its `coq-lsp` backend. Interrupt it, or -run `lean-beam shutdown`, when the session is finished. Ordinary wrapper commands attach to that +run `lean-beam --root ROOT stop`, when the session is finished. Ordinary wrapper commands attach to that session and do not start a daemon implicitly. Use `rocq-goals-after` to inspect goals after an existing sentence. Use `rocq-goals-prev` to diff --git a/docs/SETUP.md b/docs/SETUP.md index 793fb542..d6d6a99a 100644 --- a/docs/SETUP.md +++ b/docs/SETUP.md @@ -208,7 +208,7 @@ process, ask questions against saved Lean files in that project: ```bash # terminal/session 1 -lean-beam ensure --hold +lean-beam serve # terminal/session 2 update_json="$(lean-beam update "Foo.lean")" @@ -220,45 +220,74 @@ lean-beam goals before "Foo.lean" "$version" 10 2 lean-beam run-at "Foo.lean" "$version" 10 2 "exact trivial" ``` -`lean-beam ensure --hold` is the only wrapper command that starts the per-project daemon. Its +`lean-beam serve` is the only wrapper command that starts a project session. Its inherited ownership pipe defines the session lifetime: interrupt the holder, or run -`lean-beam shutdown`, to close the daemon and its backend processes. Plain `lean-beam ensure` and -all other wrapper commands attach to an existing owner and fail with a recovery command when none +`lean-beam --root ROOT stop`, to close the daemon and its backend processes. All other wrapper +commands attach to an existing owner and fail with a recovery command when none is live. Attaching commands use the owner's frozen configuration and do not rebuild a competing desired configuration. A second owner does resolve its proposed configuration and reports any -mismatch while preserving the old owner. During shutdown the registry reports `draining` and a -replacement owner is refused until the old process tree has exited. MCP clients do not need a -separate holder; the stdio MCP process owns its runtime session. +mismatch while preserving the old owner. During stopping the descriptor reports `draining` and a +replacement owner is refused until owned cleanup completes after graceful or process-group +teardown and daemon-leader reaping. MCP clients do not need a separate holder; the stdio MCP +process owns its runtime session. + +`lean-beam status` reports the public session state as `absent`, `running`, `stopping`, or +`recoveryRequired`, together with the resolved workspace and session directory. Human-facing +commands may infer a root only when the result is unique. If Lean and Rocq markers identify +different candidate roots, Beam lists the ambiguity and requires `--root`. Machine requests, +`stop`, and `recover` always require an explicit root. + +Successful `serve`, `status`, `stop`, and `recover` commands emit the same top-level +`{"ok": true, "result": ...}` shape. `serve` reports the public running session rather than its +private backend warm-up request. `stop` reports whether it committed the transition to `stopping`; +repeating it while already stopping returns `changed: false`. If the transition commits but its +immediate authenticated shutdown delivery fails, the successful stopping result includes a typed +warning. Recovery reports `state: "absent"` and whether it changed the selected session fence. The default session descriptor and lock live in `/.beam`. This is intentional for project-scoped agent sandboxes: clients that can access the same workspace can discover the same -session. Before creating a lock or capability-bearing descriptor, Beam makes the selected control +session. Before creating a lock or capability-bearing descriptor, Beam makes the selected session directory account-private (`0700`) when the leaf does not exist; the published descriptor is `0600`. An existing selection must already be a real, non-symlinked directory with mode `0700`, or Beam refuses it without changing its permissions. This permits coordination between sandboxes and -agents running as the same local account, but a group-shared or traversable control directory is +agents running as the same local account, but a group-shared or traversable session directory is not a supported authentication boundary. Use an exact alternate directory when the project is read-only or several same-account clients need another stable control plane: ```bash -lean-beam --root /workspace/a --control-dir /workspace/control ensure --hold -lean-beam --root /workspace/a --control-dir /workspace/control stats +lean-beam --root /workspace/a --session-dir /workspace/control serve +lean-beam --root /workspace/a --session-dir /workspace/control stats ``` -Every participant must supply the same `--root` and `--control-dir`; Beam does not search alternate -control directories. If the exact directory already exists, prepare its `0700` mode explicitly; -Beam will not adopt it by silently changing permissions. `BEAM_CONTROL_ROOT=/writable/base` is the -sandbox convenience form and must be absolute: Beam derives a separate hashed directory for each -canonical root below that base. An -explicit control directory is also the intended future location for a statically configured -multi-workspace CLI session. The current public owner command still publishes one frozen workspace, -and wrapper mode does not allow runtime `init_workspace`, `list_workspaces`, or `drop_workspace` requests. The +The session selector is the canonical workspace root plus the resolved session directory. Beam +admits at most one owner for that selector; choosing another session directory deliberately chooses +another namespace. A shared `BEAM_SESSION_ROOT` can coordinate several workspaces without sharing +their broker processes: each canonical root receives its own derived session directory and owner. + +Every participant must supply the same `--root` and an absolute `--session-dir`; Beam does not +search alternate session directories. If the exact directory already exists, prepare its `0700` mode explicitly; +Beam will not adopt it by silently changing permissions. `BEAM_SESSION_ROOT=/writable/base` is the +sandbox convenience form and must be absolute: Beam canonicalizes the base, then derives a separate +hashed directory for each canonical root below it. + +For a missing explicit session directory, Beam canonicalizes its longest existing ancestor before +retaining the missing suffix. The selector therefore has the same spelling before and after Beam +creates it, including through platform aliases such as macOS `/tmp`. + +Beam rejects an explicit symbolic-link leaf before canonicalizing `--session-dir` and revalidates +the selected leaf without following links before every status or attachment operation. Permission +drift therefore fails closed instead of silently weakening an already published session boundary. + +Each wrapper session publishes exactly one frozen workspace. Wrapper mode does not allow runtime +`init_workspace`, `list_workspaces`, or `drop_workspace` requests. The supported semantic `request-stream` also excludes process-wide `shutdown` and `reset_stats`; use -the dedicated `lean-beam shutdown` command for lifecycle control. -Use a stable external control directory when ownership must remain fenced while the project path is +the dedicated `lean-beam --root ROOT stop` command for lifecycle control. + +Use a stable external session directory when ownership must remain fenced while the project path is deleted and recreated; deleting a project-local `.beam` necessarily deletes its default fence. -An abnormal owner or broker exit leaves the descriptor as a safety fence. After independently +An abnormal owner or broker exit, including a nonzero broker exit after stopping begins, leaves the +descriptor as a safety fence. After independently establishing that the recorded generation is no longer authoritative, quarantine that exact record without signalling its recorded PIDs: @@ -266,12 +295,13 @@ without signalling its recorded PIDs: lean-beam --root /workspace/a recover --generation GENERATION_ID ``` -Use the same `--control-dir` selection when applicable. `recover --force` is reserved for opaque +Use the same `--session-dir` selection when applicable. `recover --force` is reserved for opaque legacy, unsupported, or malformed descriptors. Recovery preserves the old file under a `beam-daemon.recovered-*.json` name for diagnosis. -For a current descriptor, the selected `--root` must be one of its recorded workspace bindings; -using the same control directory with an unrelated root cannot quarantine the session. +For a current descriptor, the selected `--root` must match its recorded workspace; +using the same session directory with an unrelated root cannot quarantine the session. `status` +reports this as `sessionSelectorMismatch`, not as a lifecycle state or recovery requirement. Machine clients should avoid root auto-detection and raw port/session fields: @@ -334,8 +364,8 @@ checks. The running Lean server and existing file workers are not guaranteed to pick up Lake workspace configuration changes. After editing a lakefile, manifest, package override, `lean-toolchain`, Lean -options, plugins, or dynamic libraries, run `lean-beam shutdown`, then start a new -`lean-beam ensure --hold` owner before the next wrapper command that uses the Lean server. +options, plugins, or dynamic libraries, run `lean-beam --root ROOT stop`, then start a new +`lean-beam serve` owner before the next wrapper command that uses the Lean server. `lean-beam refresh` reopens a file within the current server and is not sufficient for this case. ### Final Batch Validation @@ -353,7 +383,7 @@ If no successful clean CI result is available, or when investigating code that m mode, validate the project once from clean local Lake artifacts: ```bash -lean-beam shutdown +lean-beam --root ROOT stop lake clean lake build ``` diff --git a/docs/STATUS.md b/docs/STATUS.md index 72abc6f3..4a4f6685 100644 --- a/docs/STATUS.md +++ b/docs/STATUS.md @@ -132,13 +132,13 @@ reuse matching speculative execution rather than replaying it from scratch. Beam apply the source edit. For programmatic local consumers of a wrapper session, the supported machine-readable surface is -`lean-beam --root ROOT [--control-dir DIR] request-stream `. The request JSON contains the +`lean-beam --root ROOT [--session-dir DIR] request-stream `. The request JSON contains the operation, its arguments, and a nonempty `clientRequestId`; it cannot select a workspace, root, or capability, and it cannot issue workspace-administration or process-wide control operations. The wrapper canonicalizes the explicit root, selects its static workspace binding from the session descriptor, and injects routing and authentication. Wrapper stderr is human-facing. The port-oriented `beam-client request-stream` remains maintainer/debug tooling for separately -managed brokers. A wrapper daemon exists only while its foreground `lean-beam ensure --hold` owner +managed brokers. A wrapper daemon exists only while its foreground `lean-beam serve` owner is alive. Attaching requests do not acquire daemon ownership. A separately launched standalone daemon has its own explicit process owner. Broker responses require an explicit top-level `ok` boolean, giving projection layers an unambiguous @@ -186,55 +186,70 @@ Exact event ordering and examples live in - In sandboxed agent environments, Beam daemon startup itself may require elevated permissions even when the installed bundle and project-local `.beam` paths resolve correctly. -- Wrapper sessions use explicit ownership. `lean-beam ensure --hold` is the only wrapper command that +- Wrapper sessions use explicit ownership. `lean-beam serve` is the only wrapper command that starts a project daemon; it passes the daemon an inherited pipe and remains alive as the owner. - Ordinary wrapper calls, including plain `lean-beam ensure`, only attach to that generation and + Ordinary wrapper calls only attach to that generation and fail with the exact owner-start command when none is live. The optional `--port` override belongs - only to `ensure --hold`; attaching commands reject it. Owner EOF shuts down request admission, + only to `serve`; attaching commands reject it. Owner EOF shuts down request admission, marks admitted requests for cancellation, and closes backend sessions and the daemon after those requests drain; a backend success that completed before cancellation remains successful. This happens without heartbeat timeouts or filesystem leases and works across PID namespaces because authority does not depend on observing persisted PIDs. Endpoint, root, and generation-identity validation are authoritative. Each wrapper request carries a random per-generation capability - from a mode-`0600` registry inside a mode-`0700` control directory. A paused owner retains the + from a mode-`0600` descriptor inside a mode-`0700` session directory. A paused owner retains the session; a killed owner closes the pipe; explicit - `lean-beam shutdown` changes the descriptor to `draining`, and that fence remains until normal - owner cleanup has reaped the daemon leader after graceful or process-group teardown. + `lean-beam --root ROOT stop` changes the descriptor to `draining`, and that fence remains until normal + owner cleanup has reaped the daemon leader after graceful or process-group teardown. If the daemon + instead exits abnormally during that drain, Beam restores the exact conservative fence so status + reports `recoveryRequired` rather than treating leader exit as successful cleanup. Ordinary lookups take no mutation lock, create no control files, use the frozen workspace configuration, and preserve unsafe session state. A competing owner computes its proposed configuration but cannot replace a mismatched live owner. +- `lean-beam status` projects internal descriptor observations onto four public states: `absent`, + `running`, `stopping`, and `recoveryRequired`. Backend-neutral root inference accepts a unique + Lean/Rocq candidate and rejects different candidates as ambiguous. Machine requests, `stop`, and + `recover` require an explicit canonical `--root`. Successful lifecycle commands use one + top-level `ok`/`result` envelope; `serve` projects its private backend warm-up onto the public + running-session result instead of exposing broker workspace or epoch fields. `stop` distinguishes + a newly committed transition from an already-stopping session and retains committed state in its + result when immediate shutdown delivery produces a typed warning. - Abnormal or ambiguous state is never reclaimed automatically. The descriptor remains as a fence - after an unexpected broker/owner exit. Once the operator has established that the matching - session is no longer authoritative, `lean-beam --root ROOT recover --generation ID` quarantines + after an unexpected broker/owner exit; an unexpected broker exit preserves the live descriptor, + whose unavailable endpoint projects to `recoveryRequired`. Once the operator has established that + the matching session is no longer authoritative, `lean-beam --root ROOT recover --generation ID` quarantines that exact descriptor without signalling persisted PIDs. Legacy, unsupported, or malformed descriptor state requires the deliberately broader `recover --force` form. Current-descriptor recovery additionally requires a root recorded in that descriptor, so a wrong-root caller using - the same control directory cannot quarantine the session. + the same session directory cannot quarantine the session. Such a wrong-root selection is reported + as `sessionSelectorMismatch`, outside the public lifecycle states. - The default authoritative descriptor is `/.beam/beam-daemon.json`, which keeps discovery - available inside project-scoped agent sandboxes. `--control-dir DIR` selects one exact alternate - control directory; callers must repeat the same selection for every owner, request, diagnostic, - shutdown, and recovery command. `BEAM_CONTROL_ROOT` is the sandbox convenience that derives a - per-root subdirectory below an absolute writable base. Beam requires every selected control + available inside project-scoped agent sandboxes. An absolute `--session-dir DIR` selects one exact + alternate + session directory; callers must repeat the same selection for every owner, request, diagnostic, + stop, and recovery command. `BEAM_SESSION_ROOT` is the sandbox convenience that derives a + per-root subdirectory below an absolute writable base. Uniqueness is per canonical root plus + resolved session directory, not globally per root. Beam requires every selected session directory to be account-private (`0700`) before creating its lock or capability descriptor: it creates and privatizes a missing leaf, but accepts an existing path only when it is a real, non-symlinked mode-`0700` directory. It rejects broader existing permissions without changing - them. A stable - explicit control directory is also the intended future boundary for a statically configured - multi-workspace CLI session; dynamic - workspace mutation remains unavailable in wrapper mode. + them. Explicit symbolic-link leaves are rejected before canonicalization, and read-only status or + attachment operations revalidate the exact leaf and its permissions without mutating it. + Wrapper sessions contain exactly one frozen workspace; dynamic workspace mutation remains + unavailable in wrapper mode. Standalone broker and MCP runtimes retain their independent + multi-workspace behavior. - Deleting the project tree also deletes its default project-local fence. Workflows that may remove and immediately recreate the same canonical path, and need exclusion to survive that operation, - should select a stable external `--control-dir`; this tradeoff keeps the default usable from + should select a stable external `--session-dir`; this tradeoff keeps the default usable from project-scoped agent sandboxes without assuming access to a host-global runtime directory. - Wrapper-owned brokers currently use authenticated loopback TCP. The supported trust boundary is - one local OS account with a private control directory and registry-file permissions; another user who can only discover + one local OS account with a private session directory and descriptor-file permissions; another user who can only discover the port cannot issue requests without the generation capability. A manually launched standalone `beam-daemon` has no wrapper registry capability and is maintainer tooling, not a shared-host 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. - Typed broker transport, invalid-response, and response-timeout failures include registry/log - context and write a JSON incident record below the selected control directory. Incident kinds are `brokerTransportFailure`, + 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 daemon incidents. Beam keeps the latest 50 incident records, and `lean-beam doctor` lists recent incident paths. @@ -244,8 +259,9 @@ Exact event ordering and examples live in request for that path fails root validation with a direct `workspace root does not resolve` error; it does not start a replacement daemon for a missing directory. - Cancellation is cooperative; prompt stopping depends on inner elaboration polling interruption. -- The Beam daemon can manage multiple local workspaces, with one active session per backend per - workspace. Remote workspaces and same-source multi-toolchain mirrors are not implemented yet. +- Standalone Beam brokers and MCP runtimes can manage multiple local workspaces, with one active + session per backend per workspace. Wrapper sessions deliberately publish one frozen workspace. + Remote workspaces and same-source multi-toolchain mirrors are not implemented yet. ### MCP @@ -294,7 +310,7 @@ Exact event ordering and examples live in worker has already applied them; batch-only `moreLeanArgs` fail with `saveUnsupportedSetup`. - Beam does not detect Lake workspace configuration changes during a running Lean session. After editing a lakefile, manifest, package override, `lean-toolchain`, Lean options, plugins, or dynamic - libraries, run `lean-beam shutdown`, then start a new `lean-beam ensure --hold` owner before the + libraries, run `lean-beam --root ROOT stop`, then start a new `lean-beam serve` owner before the next wrapper command that uses the Lean server; `lean-beam refresh` does not restart the server. - A Beam checkpoint contains the Lean server's accepted environment. Elaborators can distinguish server execution from batch execution, so exceptional custom elaboration can produce diff --git a/docs/SYNC_AND_DIAGNOSTICS.md b/docs/SYNC_AND_DIAGNOSTICS.md index 56540b82..5dcd1f4f 100644 --- a/docs/SYNC_AND_DIAGNOSTICS.md +++ b/docs/SYNC_AND_DIAGNOSTICS.md @@ -69,7 +69,7 @@ configuration from `lakefile.lean` text and never batch-builds as part of `save` Beam assumes Lake workspace configuration remains unchanged for the lifetime of the running Lean server. The server and existing file workers are not guaranteed to pick up edits to a lakefile, manifest, package override, `lean-toolchain`, Lean options, plugins, or dynamic libraries. After any -such change, run `lean-beam shutdown` before the next command that uses the Lean server; +such change, run `lean-beam --root ROOT stop` before the next command that uses the Lean server; `lean-beam refresh` only reopens the file within the current server and is not sufficient. Beam does not detect this configuration drift, so reusing a running session after such an edit is unsupported. @@ -95,7 +95,7 @@ If no successful clean CI result is available, or if server-sensitive elaboratio discard the development checkpoints and perform one clean local batch build: ```bash -lean-beam shutdown +lean-beam --root ROOT stop lake clean lake build ``` @@ -118,7 +118,7 @@ Their transport types differ by surface. | Current result | Stable synced-state verdict for one document version. | Final broker/CLI `diagnostics`, `readiness`, and `fileProgress` fields; MCP spells the progress field `document_progress`. | Wrapper stderr is the human-facing surface. Machine consumers of an owned wrapper session should -use final stdout JSON or `lean-beam --root ROOT [--control-dir DIR] request-stream `. +use final stdout JSON or `lean-beam --root ROOT [--session-dir DIR] request-stream `. ### Machine Broker Stream @@ -126,11 +126,11 @@ use final stdout JSON or `lean-beam --root ROOT [--control-dir DIR] request-stre broker observed it. Its input is a semantic project request with a required nonempty `clientRequestId`; callers cannot supply `root`, `workspaceId`, `daemonCapability`, executable configuration, workspace administration operations, or process-wide `shutdown` / `reset_stats`. -Use the dedicated `lean-beam shutdown` command for lifecycle control. A request may produce any +Use the dedicated `lean-beam --root ROOT stop` command for lifecycle control. A request may produce any number of `fileProgress` and `diagnostic` messages, followed by exactly one terminal `response`; the response is last and no later message belongs to that request. -Keep the session's `lean-beam ensure --hold` owner active for the request lifetime. Only the holder +Keep the session's `lean-beam serve` owner active for the request lifetime. Only the holder starts the daemon; the root-aware machine client reads the mode-`0600` descriptor, selects its frozen workspace binding, and injects routing and the per-generation capability. Requests participate in typed request admission and workspace-scoped cancellation but do not own the daemon. diff --git a/docs/TESTING.md b/docs/TESTING.md index 0371585d..2ae57fff 100644 --- a/docs/TESTING.md +++ b/docs/TESTING.md @@ -115,23 +115,27 @@ Current Beam coverage includes: - focused daemon lifecycle coverage in [tests/test-beam-wrapper-daemon.sh](../tests/test-beam-wrapper-daemon.sh), including the no-implicit-start contract, duplicate-owner rejection, Beam and non-Beam endpoint collision safety without cross-project disclosure, authenticated generation probes, mode-`0700` - control-directory and mode-`0600` registry publication, rejection of symlinked or non-private - existing control paths without mutating their targets, wrong-root recovery rejection with + session-directory and mode-`0600` descriptor publication, rejection of symlinked or non-private + existing session paths without mutating their targets, stable missing-path canonicalization, + wrong-root status classification and recovery rejection with byte-for-byte descriptor preservation, unauthorized-shutdown rejection without listener teardown, oversized-frame and first-message limits, a bounded identity probe against a silent non-Beam listener, cross-root unsafe-registry preservation that does not affect the daemon serving the other root, configuration-drift preservation of the owner and active request, - explicit shutdown, cancellation of requests active during shutdown or owner loss, - exact-generation cleanup that preserves a replacement registry, a published draining fence while + explicit stop, committed-state reporting after shutdown delivery failure, cancellation of requests + active during shutdown or owner loss, exact-generation cleanup that preserves a replacement + registry, idempotent repeated stop, a published draining fence while a daemon is paused, rejection of attachment or replacement while that generation remains published, forced process-group cleanup of the daemon and its backend, - holder reporting after an unexpected daemon crash, abrupt owner death through inherited-pipe EOF, - read-only crash-fence lookup, exact-generation non-signalling recovery, explicit control-directory + holder reporting and recovery-required projection after an unexpected daemon crash, abrupt owner + death through inherited-pipe EOF, + read-only crash-fence lookup, four-state status projection, ambiguity-safe human root inference, + explicit-root lifecycle commands, exact-generation non-signalling recovery, exact session-directory selection, root-aware machine request routing, and self-termination after the project worktree disappears without recreating it - Linux-only PID-isolated sandbox wrapper coverage in [tests/test-beam-wrapper-sandbox.sh](../tests/test-beam-wrapper-sandbox.sh), including cross-namespace endpoint attachment, duplicate-owner rejection, a paused owner without - time-based expiry, explicit shutdown, killed-owner EOF cleanup, fail-closed preservation of an + time-based expiry, explicit stop, killed-owner EOF cleanup, fail-closed preservation of an unavailable foreign-domain descriptor before explicit recovery, distinct generation identity, and the absence of legacy lease/retirement artifacts - zero-build save replay, structured-setup support, batch-only-argument rejection, and stale-save diff --git a/scripts/broker-eval.sh b/scripts/broker-eval.sh index 680ce761..41969db9 100755 --- a/scripts/broker-eval.sh +++ b/scripts/broker-eval.sh @@ -21,7 +21,7 @@ usage: scripts/broker-eval.sh case-a scripts/broker-eval.sh report scripts/broker-eval.sh reset - scripts/broker-eval.sh shutdown + scripts/broker-eval.sh stop EOF } @@ -41,11 +41,11 @@ case "${1:-}" in exit 1 fi lean_root="$(ensure_abs_dir "$2")" - "$beam" --root "$lean_root" ensure lean > /dev/null + "$beam" --root "$lean_root" stats > /dev/null "$beam" --root "$lean_root" reset-stats > /dev/null cat <&2 exit 1 fi root="$(ensure_abs_dir "$2")" - "$beam" --root "$root" shutdown + "$beam" --root "$root" stop ;; *) usage >&2 diff --git a/scripts/lean-beam b/scripts/lean-beam index fdc5cd34..66861da4 100755 --- a/scripts/lean-beam +++ b/scripts/lean-beam @@ -11,10 +11,9 @@ usage() { usage: lean-beam --version lean-beam version - lean-beam [--root PATH] ensure [lean|rocq] - lean-beam [--root PATH] [--port N] ensure [lean|rocq] --hold - lean-beam [--root PATH] run-at [--stdin | --text-file | -- | ] - lean-beam [--root PATH] run-at-handle [--stdin | --text-file | -- | ] + lean-beam [--root PATH] [--session-dir DIR] [--port N] serve [lean|rocq] + lean-beam [--root PATH] run-at (--stdin | --text-file | -- | ) + lean-beam [--root PATH] run-at-handle (--stdin | --text-file | -- | ) lean-beam [--root PATH] hover lean-beam [--root PATH] signature-help lean-beam [--root PATH] definition @@ -23,8 +22,8 @@ usage: lean-beam [--root PATH] workspace-symbols lean-beam [--root PATH] goals before|after lean-beam [--root PATH] todo [--kind ...] [--suggest none|basic] - lean-beam [--root PATH] run-with > [--stdin | --text-file | -- | ] - lean-beam [--root PATH] run-with-linear > [--stdin | --text-file | -- | ] + lean-beam [--root PATH] run-with > (--stdin | --text-file | -- | ) + lean-beam [--root PATH] run-with-linear > (--stdin | --text-file | -- | ) lean-beam [--root PATH] release > lean-beam [--root PATH] update lean-beam [--root PATH] sync [+all-diagnostics] @@ -42,22 +41,22 @@ usage: lean-beam [--root PATH] open-files lean-beam [--root PATH] stats lean-beam [--root PATH] reset-stats - lean-beam [--root PATH] shutdown - lean-beam [--root PATH] [--control-dir DIR] recover --generation ID | --force - lean-beam --root PATH [--control-dir DIR] request-stream + lean-beam [--root PATH] [--session-dir DIR] status + lean-beam --root PATH [--session-dir DIR] stop + lean-beam --root PATH [--session-dir DIR] recover --generation ID | --force + lean-beam --root PATH [--session-dir DIR] request-stream lean-beam [--root PATH] cancel notes: - - pass --control-dir DIR before the command to select one exact alternate session control directory; repeat it for every participant + - pass an absolute --session-dir DIR before the command to select one exact alternate session directory; repeat it for every participant - lean-beam keeps the Lean wrapper surface primary; optional Rocq goal probes are documented in docs/ROCQ.md - - start a Rocq session with `lean-beam ensure rocq --hold`; plain `ensure rocq` only checks and warms that owned session + - start a Rocq session with `lean-beam serve rocq` - other common Rocq entry points are `lean-beam doctor rocq`, `lean-beam rocq-goals-after`, and `lean-beam rocq-goals-prev` - run `lean-beam update ` first, then pass its returned `version` to Lean position/range probes - run `lean-beam sync ` when you also need the diagnostics/readiness barrier - 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 - - wrapper commands require one live session owner; start `ensure --hold` in a foreground process and keep it running - - plain `ensure` checks and warms that owned session but never starts one implicitly + - wrapper commands require one live session owner; start `serve` in a foreground process and keep it running - abnormal session state remains fenced; after verifying the old generation is gone, use `recover --generation ID` - set `BEAM_DEBUG_TEXT=1` to print the exact escaped text and UTF-8 bytes sent for text-carrying Lean probes - use `lean-beam --version` for bug reports and installed runtime identity checks @@ -134,7 +133,7 @@ prefix=() cmd="" while [ "$#" -gt 0 ]; do case "$1" in - --root|--control-dir|--port) + --root|--session-dir|--port) [ "$#" -ge 2 ] || break prefix+=("$1" "$2") shift 2 @@ -240,12 +239,12 @@ case "$cmd" in prune) mapped=("install-prune") ;; - ensure) + serve) if [ "${#rest[@]}" -eq 0 ]; then - mapped=("ensure" "lean") + mapped=("serve" "lean") rest=() else - mapped=("ensure") + mapped=("serve") fi ;; doctor) diff --git a/skills/lean-beam/SKILL.md b/skills/lean-beam/SKILL.md index ccd33d98..b9bc9e8f 100644 --- a/skills/lean-beam/SKILL.md +++ b/skills/lean-beam/SKILL.md @@ -73,8 +73,8 @@ and isolation rules; do not treat MCP as a raw Lean LSP proxy. Supported command families: -- start and own a wrapper session: `lean-beam ensure --hold` -- check and warm an already-owned Lean session: `lean-beam ensure` +- start and own a wrapper session: `lean-beam serve` +- inspect the selected session state: `lean-beam status` - inspect existing code, navigation data, or proof state: `lean-beam hover`, `lean-beam signature-help`, `lean-beam definition`, `lean-beam references`, `lean-beam document-symbols`, `lean-beam workspace-symbols`, `lean-beam goals before`, @@ -108,8 +108,9 @@ Core workflow contract: - use `lean-beam`, not raw JSON and not raw LSP - Beam never applies source edits to `.lean` files on disk; the client applies source edits - `lean-beam` only sees the on-disk file, not unsaved editor buffers -- before using wrapper workflow commands, start one foreground `lean-beam ensure --hold` process - and keep it running across shell invocations; interrupt it or run `lean-beam shutdown` when finished +- before using wrapper workflow commands, start one foreground `lean-beam serve` process + and keep it running across shell invocations; interrupt it or run + `lean-beam --root ROOT stop` when finished - MCP owns its stdio runtime session automatically; do not start a separate wrapper holder solely for MCP tool calls - after every real Lean source edit: save the file normally, then run `lean-beam update` before the @@ -124,12 +125,12 @@ Core workflow contract: final build evidence - modules with batch-only `moreLeanArgs` fail with `saveUnsupportedSetup`; move shared `-D` settings to `leanOptions`, or use `lake build` when the arguments are intentionally batch-only -- after changing a lakefile or related Lake workspace configuration, run `lean-beam shutdown` +- after changing a lakefile or related Lake workspace configuration, run `lean-beam --root ROOT stop` before the next command that uses the Lean server; `lean-beam refresh` does not restart it - treat wrapper `stderr` as human-facing only; use stdout JSON or `lean-beam --root ROOT request-stream` for machine-readable automation -- for a machine-readable wrapper stream, keep `lean-beam ensure --hold` active and use +- for a machine-readable wrapper stream, keep `lean-beam serve` active and use `lean-beam --root ROOT request-stream`; raw `beam-client --port` requests are maintainer tooling for separately managed brokers - `lean-beam feedback-report` and `beam_feedback_report` return a report to the caller; Beam does not @@ -171,9 +172,9 @@ This changes the right agent behavior: keeping independent probe sequences in flight - after a real source edit, run `lean-beam update ` before later probes; run `lean-beam sync ` when you need diagnostics/readiness -- use `lake build` for dependency-cone validation and in clean CI; use a local `shutdown` / `lake - clean` / `lake build` sequence once when no successful clean CI result is available or - server-sensitive elaboration is suspected +- use `lake build` for dependency-cone validation and in clean CI; use a local + `lean-beam --root ROOT stop` / `lake clean` / `lake build` sequence once when no successful + clean CI result is available or server-sensitive elaboration is suspected - use scratch files only for context-free Lean syntax checks or Beam incident isolation ## Prompting Contract @@ -293,19 +294,21 @@ Use `lean-beam`, not raw JSON and not raw LSP. `lean-beam` for Lean: - infers the target project root from the current directory or `--root` -- keeps one Beam daemon per project root and records it in `/.beam/beam-daemon.json` - - in sandboxed or read-only project trees, set `BEAM_CONTROL_ROOT` to a writable directory; +- keeps one owner per resolved workspace and session-directory selector; the default descriptor is + `/.beam/beam-daemon.json` + - in sandboxed or read-only project trees, set `BEAM_SESSION_ROOT` to a writable directory; `lean-beam` uses a per-root subdirectory there - - for an exact stable alternate session location, pass the same `--control-dir DIR` to the owner - and every attaching command; Beam does not search alternate control directories + - for an exact stable alternate session location, pass the same absolute path with + `--session-dir DIR` to the owner and every attaching command; Beam does not search alternate + session directories - resolves a toolchain-keyed Lean bundle, preferring the installed beam bundle cache and falling back to a project-local runtime bundle under `/.beam/bundles` or `BEAM_BUNDLE_DIR` - fully validates exact Lean toolchains listed in `validated-lean-toolchains`, locally qualifies canonical RC/patch variants from `compatible-lean-release-lines`, and accepts exact custom names recorded by the installer in `custom-lean-toolchains` -- gives daemon startup authority only to `lean-beam ensure --hold`; ordinary wrapper commands attach +- gives daemon startup authority only to `lean-beam serve`; ordinary wrapper commands attach to its registry generation and never start a daemon implicitly -- owns shutdown and registry handling +- owns stopping and descriptor handling - resolves Lean with `elan which lean` - builds and plugin-qualifies a local fallback bundle only when no matching installed bundle exists for the exact accepted toolchain fingerprint @@ -313,22 +316,21 @@ Use `lean-beam`, not raw JSON and not raw LSP. line, nor explicitly custom; use `lean-beam validated-toolchains`, `lean-beam compatible-release-lines`, and `lean-beam doctor` to inspect the decision - after effective Lean startup configuration changes, requires shutting down the old session and - starting a new `lean-beam ensure --hold` owner + starting a new `lean-beam serve` owner - after abnormal owner/broker exit, preserves the session fence until explicit `recover --generation ID`; recovery quarantines metadata and never signals its persisted PIDs -- `lean-beam shutdown`, `lean-beam stats`, and `lean-beam reset-stats` apply to the current project only +- `lean-beam --root ROOT stop` requires an explicit root; `lean-beam status`, `lean-beam stats`, and + `lean-beam reset-stats` may infer a unique root - `lean-beam prune` previews old installed runtimes; restart active agents and MCP clients before any `--apply`, and add `--bundles` when stale installed bundle caches should also be removed - wrapper commands talk to the per-project Beam daemon over localhost TCP; they are not direct in-process Lean calls -- `lean-beam ensure --hold` prints the usual JSON ensure response on stdout and keeps the wrapper +- `lean-beam serve` prints a backend-readiness JSON response on stdout and keeps the wrapper process alive as the session owner; an inherited pipe ties daemon lifetime to that process without heartbeat files or lease expiry -- `--port` is an optional owner-start override for `lean-beam ensure --hold`; attaching commands +- `--port` is an optional owner-start override for `lean-beam serve`; attaching commands reject it instead of silently ignoring it - interrupting or killing the holder closes the owner pipe and shuts down the daemon; explicit - `lean-beam shutdown` releases the holder cleanly -- plain `lean-beam ensure` checks and warms a live owned session; if there is no owner, follow its - error and start `lean-beam ensure --hold` + `lean-beam --root ROOT stop` releases the holder cleanly `lean-beam` is more than a one-shot probe: @@ -347,7 +349,7 @@ Use `lean-beam`, not raw JSON and not raw LSP. Default rules: - use `lean-beam`, not raw JSON and not raw LSP -- start and keep one `lean-beam ensure --hold` owner before issuing wrapper workflow commands +- start and keep one `lean-beam serve` owner before issuing wrapper workflow commands - start with `lean-beam run-at` - after every real source edit: save the file to disk normally, then `lean-beam update` before the next version-bound probe; use `lean-beam sync` for diagnostics/readiness @@ -362,7 +364,7 @@ If you only remember one workflow, use this one: ```bash # terminal or long-lived agent process 1: keep this running -lean-beam ensure --hold +lean-beam serve # terminal or agent process 2: inspect existing code or proof state update_out="$(lean-beam update "Foo.lean")" @@ -398,7 +400,7 @@ clean CI result is available, or server-sensitive elaboration is suspected, run outside the inner loop: ```bash -lean-beam shutdown +lean-beam --root ROOT stop lake clean lake build ``` @@ -414,11 +416,12 @@ Read the save path as a progression, not as three unrelated commands: by the Lean file worker - modules with batch-only `moreLeanArgs` fail with `saveUnsupportedSetup`; move shared `-D` settings to `leanOptions`, or use `lake build` when the arguments are intentionally batch-only -- after changing a lakefile or related Lake workspace configuration, run `lean-beam shutdown` +- after changing a lakefile or related Lake workspace configuration, run + `lean-beam --root ROOT stop` before the next command that uses the Lean server; `lean-beam refresh` is not sufficient - `lean-beam close-save` is `lean-beam save` plus closing the tracked file afterward - a Beam save checkpoints the accepted Lean server environment; it does not rerun batch elaboration -- the one-time `shutdown` / `lake clean` / `lake build` sequence discards development checkpoints +- the one-time `stop` / `lake clean` / `lake build` sequence discards development checkpoints and supplies final batch evidence when no successful clean CI result is available; routine local Beam work does not require it after every checkpoint @@ -501,7 +504,7 @@ Open these only when the task needs the detail: - prefer `lean-beam save` / `lean-beam close-save` over a full `lake build` when only one file needs checkpointing - treat `lean-beam save` as a single-module checkpoint, not as dependency-cone validation - use `lake build` for initial failure discovery, coarse dependency checkpoints, and clean CI; after - Beam saves, use `lean-beam shutdown`, `lake clean`, and `lake build` locally once only when no + Beam saves, use `lean-beam --root ROOT stop`, `lake clean`, and `lake build` locally once only when no successful clean CI result is available or server-sensitive elaboration is suspected - if you edit a dependency of the target file, `lean-beam save` is not enough for downstream trust; rebuild before trusting importers diff --git a/skills/lean-beam/agents/openai.yaml b/skills/lean-beam/agents/openai.yaml index 9d4c3f6b..910b184f 100644 --- a/skills/lean-beam/agents/openai.yaml +++ b/skills/lean-beam/agents/openai.yaml @@ -5,7 +5,7 @@ interface: display_name: "Lean Beam" short_description: "Lean probes, sync, and exact chaining" - default_prompt: "Use $lean-beam on an external Lean project for isolated on-disk Lean probes through beam; start lean-beam ensure --hold and keep it running while using wrapper commands, use lean-beam sync after real edits, do not assume separate lean-beam run-at calls chain, and use pre-stable handle workflows only when exact speculative continuation matters." + default_prompt: "Use $lean-beam on an external Lean project for isolated on-disk Lean probes through beam; start lean-beam serve and keep it running while using wrapper commands, use lean-beam sync after real edits, do not assume separate lean-beam run-at calls chain, and use pre-stable handle workflows only when exact speculative continuation matters." policy: allow_implicit_invocation: true diff --git a/skills/lean-beam/references/anti-patterns.md b/skills/lean-beam/references/anti-patterns.md index dbbfcda5..8772b2dd 100644 --- a/skills/lean-beam/references/anti-patterns.md +++ b/skills/lean-beam/references/anti-patterns.md @@ -32,5 +32,5 @@ Use this reference as a short checklist of what not to assume in Lean `beam` wor - use `lean-beam --root ROOT request-stream` for machine-readable streaming diagnostics or progress - use `lake build` when the task has become dependency freshness - rely on successful Beam checkpoints for ordinary local development, ensure CI runs `lake build` - from clean artifacts, and use local `lean-beam shutdown`, `lake clean`, and `lake build` once only + from clean artifacts, and use local `lean-beam --root ROOT stop`, `lake clean`, and `lake build` once only when no successful clean CI result is available or server-sensitive elaboration is suspected diff --git a/skills/lean-beam/references/mcts-search.md b/skills/lean-beam/references/mcts-search.md index eded285f..94969826 100644 --- a/skills/lean-beam/references/mcts-search.md +++ b/skills/lean-beam/references/mcts-search.md @@ -36,7 +36,7 @@ Rules: ## Minimal branching example ```bash -# with `lean-beam ensure --hold` running in another process +# with `lean-beam serve` running in another process root="$(lean-beam run-at-handle "Proofs.lean" 42 6 "constructor")" # writing handles to files avoids stdin conflicts in larger shell scripts @@ -57,7 +57,7 @@ Use this when you want to explore multiple children from the same preserved basi ## Minimal linear playout example ```bash -# with `lean-beam ensure --hold` running in another process +# with `lean-beam serve` running in another process root="$(lean-beam run-at-handle "Proofs.lean" 42 6 "constructor")" # file-backed handles are often easier in longer shell loops printf '%s\n' "$root" > root.handle.json @@ -87,7 +87,7 @@ Use this when you want one evolving playout path instead of a preserved branch p Concrete shell sketch: ```bash -# with `lean-beam ensure --hold` running in another process +# with `lean-beam serve` running in another process root="$(lean-beam run-at-handle "Proofs.lean" 42 6 "constructor")" child_a="$(printf '%s\n' "$root" | lean-beam run-with "Proofs.lean" - "constructor")" @@ -102,7 +102,7 @@ printf '%s\n' "$child_b" | lean-beam release "Proofs.lean" - The same sketch with the helper: ```bash -# with `lean-beam ensure --hold` running in another process +# with `lean-beam serve` running in another process root="$(lean-beam-search mint "Proofs.lean" 42 6 "constructor")" child_a="$(printf '%s\n' "$root" | lean-beam-search branch "Proofs.lean" "constructor")" child_b="$(printf '%s\n' "$root" | lean-beam-search branch "Proofs.lean" "aesop")" diff --git a/skills/lean-beam/references/workflow-details.md b/skills/lean-beam/references/workflow-details.md index 7d6cf42c..550c01a3 100644 --- a/skills/lean-beam/references/workflow-details.md +++ b/skills/lean-beam/references/workflow-details.md @@ -98,7 +98,7 @@ batch-only. Beam assumes Lake workspace configuration remains unchanged while the Lean server is running. After editing a lakefile, manifest, package override, `lean-toolchain`, Lean options, plugins, or dynamic -libraries, run `lean-beam shutdown` before the next command that uses the Lean server. +libraries, run `lean-beam --root ROOT stop` before the next command that uses the Lean server. `lean-beam refresh` only reopens a file within the current server and is not sufficient. Beam does not detect this configuration drift. @@ -210,7 +210,7 @@ What is not a valid checkpoint target: Treat `fileProgress` as observability, not as proof that every call is a full barrier. ```bash -# with `lean-beam ensure --hold` running in another process +# with `lean-beam serve` running in another process sync_out="$(lean-beam sync "Foo.lean")" printf '%s\n' "$sync_out" version="$(printf '%s\n' "$sync_out" | python3 -c 'import json,sys; print(json.load(sys.stdin)["result"]["version"])')" @@ -308,7 +308,7 @@ If you edit `A.lean` and `B.lean` imports `A.lean`, a successful probe in `B.lea itself to prove the dependency cone is fresh. ```bash -# with `lean-beam ensure --hold` running in another process +# with `lean-beam serve` running in another process # make a real edit in A.lean and save the source file to disk lean-beam sync "A.lean" b_update="$(lean-beam update "B.lean")" @@ -334,7 +334,7 @@ Use `lake build` when: For the one-time local completion fallback, discard Beam checkpoints before the batch build: ```bash -lean-beam shutdown +lean-beam --root ROOT stop lake clean lake build ``` diff --git a/skills/rocq-beam/SKILL.md b/skills/rocq-beam/SKILL.md index f570b326..38e8ea2b 100644 --- a/skills/rocq-beam/SKILL.md +++ b/skills/rocq-beam/SKILL.md @@ -52,8 +52,8 @@ mutation. Supported command families: -- start and own a Rocq wrapper session: `lean-beam ensure rocq --hold` -- check and warm an already-owned Rocq session: `lean-beam ensure rocq` +- start and own a Rocq wrapper session: `lean-beam serve rocq` +- inspect the selected session state: `lean-beam status` - inspect goals after an existing sentence: `lean-beam rocq-goals-after` - inspect goals before a sentence or after speculative sentence text within that basis: `lean-beam rocq-goals-prev` @@ -68,8 +68,8 @@ What to treat as the current agent workflow surface: Core workflow contract: - use `lean-beam`, not raw JSON and not raw LSP -- before issuing wrapper probes, start one foreground `lean-beam ensure rocq --hold` process and - keep it running; interrupt it or run `lean-beam shutdown` when finished +- before issuing wrapper probes, start one foreground `lean-beam serve rocq` process and + keep it running; interrupt it or run `lean-beam --root ROOT stop` when finished - save the `.v` file before every new probe after a real edit - `lean-beam` only sees the on-disk file, not unsaved editor buffers - treat ` ` as LSP-style coordinates for the saved file: line `0` is the first @@ -86,13 +86,14 @@ Use `lean-beam`, not raw JSON and not raw LSP. `lean-beam` for Rocq: - infers the target project root from the current directory or `--root` -- keeps one Beam daemon per project root and records it in `/.beam/beam-daemon.json` - - in sandboxed or read-only project trees, set `BEAM_CONTROL_ROOT` to a writable directory - - for an exact stable alternate location, pass the same `--control-dir DIR` to the owner and every - attaching command; Beam does not search alternate control directories -- gives daemon startup authority only to `lean-beam ensure rocq --hold`; ordinary commands attach +- keeps one owner per resolved workspace and session-directory selector; the default descriptor is + `/.beam/beam-daemon.json` + - in sandboxed or read-only project trees, set `BEAM_SESSION_ROOT` to a writable directory + - for an exact stable alternate location, pass the same absolute path with `--session-dir DIR` to + the owner and every attaching command; Beam does not search alternate session directories +- gives daemon startup authority only to `lean-beam serve rocq`; ordinary commands attach to its registry generation and never start a daemon implicitly -- owns shutdown and registry handling +- owns stopping and descriptor handling - preserves ambiguous crash state until explicit `recover --generation ID`; recovery does not signal persisted PIDs - resolves `coq-lsp` from the target project's local `_opam` when available @@ -102,7 +103,8 @@ Use `lean-beam`, not raw JSON and not raw LSP. - in Codex-style sandboxes, Beam daemon startup may still require elevated permissions even when all paths resolve correctly - in the same environments, localhost TCP bind/connect for the Beam daemon and client may also require elevated permissions - if startup fails with `operation not permitted`, treat that as a sandbox capability problem first, not as a missing install -- `lean-beam shutdown`, `lean-beam stats`, and `lean-beam reset-stats` apply to the current project only +- `lean-beam --root ROOT stop` requires an explicit root; `lean-beam status`, `lean-beam stats`, and + `lean-beam reset-stats` may infer a unique root Default rules: @@ -121,7 +123,7 @@ from another: ```bash # terminal/session 1: keep running -lean-beam ensure rocq --hold +lean-beam serve rocq # terminal/session 2 lean-beam stats @@ -164,7 +166,7 @@ Execution model: Default loop: ```bash -# with `lean-beam ensure rocq --hold` running in another process +# with `lean-beam serve rocq` running in another process lean-beam rocq-goals-after "Demo.v" 12 4 # make a real edit, save the file @@ -176,14 +178,14 @@ Use cases: 1. Inspect the current proof state after a sentence ```bash -# with `lean-beam ensure rocq --hold` running in another process +# with `lean-beam serve rocq` running in another process lean-beam rocq-goals-after "Demo.v" 12 4 ``` 2. Inspect an intermediate tactic state inside one sentence ```bash -# with `lean-beam ensure rocq --hold` running in another process +# with `lean-beam serve rocq` running in another process lean-beam rocq-goals-prev "Demo.v" 12 4 "intro x." lean-beam rocq-goals-prev "Demo.v" 12 4 "split." ``` @@ -193,7 +195,7 @@ lean-beam rocq-goals-prev "Demo.v" 12 4 "split." Save the file first, then probe again from the saved document. ```bash -# with `lean-beam ensure rocq --hold` running in another process +# with `lean-beam serve rocq` running in another process lean-beam rocq-goals-after "Demo.v" 12 4 # make a real edit in Demo.v and save it diff --git a/skills/rocq-beam/agents/openai.yaml b/skills/rocq-beam/agents/openai.yaml index 1da4eb9b..6a6484a8 100644 --- a/skills/rocq-beam/agents/openai.yaml +++ b/skills/rocq-beam/agents/openai.yaml @@ -5,7 +5,7 @@ interface: display_name: "Rocq Beam Aux" short_description: "Optional Rocq-to-Lean goal probes" - default_prompt: "Use $rocq-beam when an external Rocq project needs the optional Rocq goal-probe surface exposed through lean-beam for Rocq-to-Lean porting; start lean-beam ensure rocq --hold and keep it running while using wrapper commands, save before probing, use lean-beam rocq-goals-after / rocq-goals-prev, and do not assume hidden cross-request proof state, handles, unsaved-buffer access, or a Rocq run-at command." + default_prompt: "Use $rocq-beam when an external Rocq project needs the optional Rocq goal-probe surface exposed through lean-beam for Rocq-to-Lean porting; start lean-beam serve rocq and keep it running while using wrapper commands, save before probing, use lean-beam rocq-goals-after / rocq-goals-prev, and do not assume hidden cross-request proof state, handles, unsaved-buffer access, or a Rocq run-at command." policy: allow_implicit_invocation: true diff --git a/tests/lean/BeamTest/Broker/CliDaemonTest.lean b/tests/lean/BeamTest/Broker/CliDaemonTest.lean index 7db8ecc8..7fe60507 100644 --- a/tests/lean/BeamTest/Broker/CliDaemonTest.lean +++ b/tests/lean/BeamTest/Broker/CliDaemonTest.lean @@ -409,7 +409,11 @@ private def checkCliRootParsing : IO Unit := do expectIoErrorContains "missing explicit CLI root should use the workspace error boundary" "workspace root does not resolve" - (Beam.Cli.parseCliOptions {} ["--root", missingRoot.toString, "ensure", "lean"]) + (Beam.Cli.parseCliOptions {} ["--root", missingRoot.toString, "serve", "lean"]) + expectIoErrorContains + "relative session directory should be rejected" + "--session-dir requires an absolute path" + (Beam.Cli.parseCliOptions {} ["--session-dir", "relative-session", "status"]) let root := System.FilePath.mk s!"/tmp/beam-cli-root-{← IO.monoNanosNow}" let control := root / "shared-control" try @@ -418,17 +422,42 @@ private def checkCliRootParsing : IO Unit := do let expectedControl ← Beam.resolveExistingPath control let opts ← Beam.Cli.parseCliOptions {} [ "--root", root.toString, - "--control-dir", control.toString, + "--session-dir", control.toString, "stats" ] require "explicit CLI root should be canonicalized" (opts.explicitRoot? == some expectedRoot) - require "explicit control directory should remain an exact selection" + require "explicit session directory should remain an exact selection" (opts.explicitControlDir? == some expectedControl) require "global selectors should not leak into command arguments" (opts.args == ["stats"]) finally if ← root.pathExists then IO.FS.removeDirAll root +private def checkProjectRootAmbiguity : IO Unit := do + let root := System.FilePath.mk s!"/tmp/beam-cli-root-selection-{← IO.monoNanosNow}" + let leanRoot := root / "lean" + let rocqRoot := leanRoot / "rocq" + let nested := rocqRoot / "src" + try + IO.FS.createDirAll nested + IO.FS.writeFile (leanRoot / "lean-toolchain") "leanprover/lean4:stable\n" + IO.FS.writeFile (rocqRoot / "_RocqProject") "\n" + expectIoErrorContains + "backend-neutral root inference should reject mixed-root ambiguity" + "project root is ambiguous" + (Beam.Cli.inferProjectRootAny nested) + let explicitLean ← Beam.resolveExistingPath leanRoot + require "an explicit root should resolve mixed-root ambiguity" + ((← Beam.Cli.projectRootAny { explicitRoot? := some explicitLean }) == explicitLean) + + IO.FS.writeFile (rocqRoot / "lean-toolchain") "leanprover/lean4:stable\n" + let sharedRoot ← Beam.resolveExistingPath rocqRoot + require "one directory containing both project markers should be one root candidate" + ((← Beam.Cli.inferProjectRootAny rocqRoot) == sharedRoot) + finally + if ← root.pathExists then + IO.FS.removeDirAll root + private def checkLeanOperationRequests : IO Unit := do let root := System.FilePath.mk "/repo" let rootText := root.toString @@ -442,15 +471,13 @@ private def checkLeanOperationRequests : IO Unit := do text := "exact h" } requireRequestJson "runAt request should share the Lean operation adapter" - (Beam.Cli.leanRunAtRequest root path 12 4 2 (some "exact h")) + (Beam.Cli.leanRunAtRequest root path 12 4 2 "exact h") (runAtInput.toBrokerRequest rootText) requireRequestJson "runAt handle request should share the Lean operation adapter" - (Beam.Cli.leanRunAtRequest root path 12 4 2 (some "exact h") (storeHandle := true)) + (Beam.Cli.leanRunAtRequest root path 12 4 2 "exact h" (storeHandle := true)) (runAtInput.toBrokerRequest rootText (storeHandle := true)) - let missingRunAtText := Beam.Cli.leanRunAtRequest root path 12 4 2 none - require "runAt missing text should remain a broker validation error" missingRunAtText.text?.isNone - require "runAt missing text should still target run_at" (missingRunAtText.op == .runAt) - require "runAt missing text should carry version" (missingRunAtText.version? == some 12) + expectIoErrorContains "runAt missing text should fail at the CLI boundary" + "usage: beam" (Beam.Cli.parseTextArg "lean-run-at Demo.lean 12 4 2" []) let positionInput : Beam.Lean.PositionInput := { path @@ -500,19 +527,13 @@ private def checkLeanOperationRequests : IO Unit := do text := "simp" } requireRequestJson "runWith request should share the Lean operation adapter" - (Beam.Cli.leanRunWithRequest root path sampleBrokerHandle (some "simp")) + (Beam.Cli.leanRunWithRequest root path sampleBrokerHandle "simp") (runWithInput.toBrokerRequest rootText) requireRequestJson "runWith linear request should share the Lean operation adapter" - (Beam.Cli.leanRunWithRequest root path sampleBrokerHandle (some "simp") (linear := true)) + (Beam.Cli.leanRunWithRequest root path sampleBrokerHandle "simp" (linear := true)) (runWithInput.toBrokerRequest rootText (linear := true)) - let missingRunWithText := Beam.Cli.leanRunWithRequest root path sampleBrokerHandle none - require "runWith missing text should remain a broker validation error" missingRunWithText.text?.isNone - require "runWith missing text should keep successor-handle semantics" - (missingRunWithText.storeHandle? == some true) - require "runWith missing text should keep linear flag explicit" - (missingRunWithText.linear? == some false) - require "runWith missing text should keep the supplied handle" - missingRunWithText.handle?.isSome + expectIoErrorContains "runWith missing text should fail at the CLI boundary" + "usage: beam" (Beam.Cli.parseTextArg "lean-run-with Demo.lean HANDLE" []) requireRequestJson "release request should share the Lean operation adapter" (Beam.Cli.leanReleaseRequest root path sampleBrokerHandle) @@ -597,13 +618,12 @@ private def checkDaemonFailureContext : IO Unit := do pid := 999999999 ownerPid := 999999999 port? := some 42424 - workspaces := #[{ + workspace := { workspaceId := Beam.Cli.projectDaemonWorkspaceId root := root.toString - configHash := "config-test" toolchain? := some "leanprover/lean4:test" bundleId? := some "bundle-test" - }] + } configHash := "config-test" startedAt := "2026-07-02T00:00:00Z" } @@ -741,13 +761,12 @@ private def writeTestRegistryEntry pid := 999999999 ownerPid := 999999999 port? - workspaces := #[{ + workspace := { workspaceId := Beam.Cli.projectDaemonWorkspaceId root := root.toString - configHash := "config-test" toolchain? := some "leanprover/lean4:test" bundleId? := some "bundle-test" - }] + } configHash := "config-test" startedAt := "2026-07-05T00:00:00Z" } @@ -775,6 +794,11 @@ private def checkTypedRegistryReads : IO Unit := do | .unsupported 999 => pure () | state => throw <| IO.userError s!"unsupported registry was classified as {state.status}" + IO.FS.writeFile registryPath "{\"schemaVersion\":2}\n" + match ← Beam.Daemon.readRegistry root with + | .unsupported 2 => pure () + | state => throw <| IO.userError s!"superseded multi-workspace registry was classified as {state.status}" + IO.FS.writeFile registryPath "{\"schemaVersion\":\"one\"}\n" match ← Beam.Daemon.readRegistry root with | .malformed detail => @@ -806,11 +830,11 @@ private def checkTypedRegistryReads : IO Unit := do let validText ← IO.FS.readFile registryPath let validJson ← IO.ofExcept <| Json.parse validText IO.FS.writeFile registryPath <| - (validJson.setObjVal! "workspaces" (toJson (#[] : Array Beam.Daemon.WorkspaceBinding))).compress + (validJson.setObjVal! "workspace" (Json.mkObj [])).compress match ← Beam.Daemon.readRegistry root with | .malformed detail => - require "empty workspace descriptors should fail the typed boundary" - (detail.contains "at least one workspace") + require "incomplete workspace descriptors should fail the typed boundary" + (detail.contains "invalid registry schema") | state => throw <| IO.userError s!"empty workspace descriptor was classified as {state.status}" IO.FS.writeFile registryPath validText @@ -1003,14 +1027,41 @@ private def checkPathCanonicalization : IO Unit := do let stamp ← IO.monoNanosNow let root := System.FilePath.mk s!"/tmp/beam-path-canonical-root-{stamp}" let alias := System.FilePath.mk s!"/tmp/beam-path-canonical-alias-{stamp}" + let dotdotAlias := System.FilePath.mk s!"/tmp/beam-path-dotdot-alias-{stamp}" + let missingUnderRoot := root / "missing" / "session" + let missingUnderAlias := alias / "missing" / "session" try IO.FS.createDirAll root createSymlink "path canonicalization fixture" root alias + IO.FS.createDir (root / "existing") + createSymlink "path dotdot canonicalization fixture" (root / "existing") dotdotAlias require "canonical path equality should treat symlinked workspace roots as the same path" (← Beam.sameFilePath root alias) require "missing paths should fall back to exact text equality" - (!(← Beam.sameFilePath (root / "missing") (alias / "missing"))) + (!(← Beam.sameFilePath missingUnderRoot missingUnderAlias)) + let resolvedBeforeCreation ← Beam.resolvePathForCreation missingUnderAlias + let expectedBeforeCreation := (← Beam.resolveExistingPath root) / "missing" / "session" + require "creation-path resolution should canonicalize the longest existing ancestor" + (resolvedBeforeCreation == expectedBeforeCreation) + IO.FS.createDirAll missingUnderAlias + let resolvedAfterCreation ← Beam.resolveExistingPath missingUnderAlias + require "creation-path identity should remain stable after creating the missing suffix" + (resolvedAfterCreation == resolvedBeforeCreation) + let missingAfterSymlinkDotdot := dotdotAlias / ".." / "dotdot-missing" / "session" + let resolvedAfterSymlinkDotdot ← Beam.resolvePathForCreation missingAfterSymlinkDotdot + let expectedAfterSymlinkDotdot := + ((← Beam.resolveExistingPath root) / "dotdot-missing" / "session").normalize + require "creation-path resolution should preserve filesystem semantics for symlink followed by dotdot" + (resolvedAfterSymlinkDotdot == expectedAfterSymlinkDotdot) + IO.FS.createDirAll missingAfterSymlinkDotdot + require "symlink-dotdot path identity should remain stable after creation" + ((← Beam.resolveExistingPath missingAfterSymlinkDotdot) == resolvedAfterSymlinkDotdot) finally + try + if ← dotdotAlias.pathExists then + IO.FS.removeFile dotdotAlias + catch _ => + pure () try if ← alias.pathExists then IO.FS.removeFile alias @@ -1327,6 +1378,7 @@ def main : IO Unit := do checkSyncWaitSpecs checkCancelAcknowledgementDecoding checkCliRootParsing + checkProjectRootAmbiguity checkLeanOperationRequests checkDiagnosticScopeArgs checkStartupRetryPolicy diff --git a/tests/lean/BeamTest/Broker/McpProjectionTest.lean b/tests/lean/BeamTest/Broker/McpProjectionTest.lean index 828e516d..5867c698 100644 --- a/tests/lean/BeamTest/Broker/McpProjectionTest.lean +++ b/tests/lean/BeamTest/Broker/McpProjectionTest.lean @@ -126,6 +126,11 @@ private def checkToolDescriptors : IO Unit := do let projectedTool : Beam.Mcp.ToolName := .leanOperation op require s!"Lean operation {repr op} should derive MCP key from operation key" (projectedTool.key == "lean_" ++ op.key) + require s!"shared Lean operation {repr op} should not contain MCP transport guidance" + (!op.description.contains "tools/call" && !op.description.contains "progressToken") + require s!"projected MCP operation {repr op} should advertise MCP progress controls" + (projectedTool.descriptor.description.contains "tools/call" && + projectedTool.descriptor.description.contains "_meta.progressToken") let matchingTools := Beam.Mcp.ToolName.leanOperationTools.filter (fun tool => tool == .leanOperation op) require s!"Lean operation {repr op} should have exactly one MCP tool" diff --git a/tests/lean/BeamTest/Broker/ProtocolTest.lean b/tests/lean/BeamTest/Broker/ProtocolTest.lean index 015f7310..1b08bdf5 100644 --- a/tests/lean/BeamTest/Broker/ProtocolTest.lean +++ b/tests/lean/BeamTest/Broker/ProtocolTest.lean @@ -819,7 +819,7 @@ private def checkProjectRequestBoundary : IO Unit := do match fromJson? (α := ProjectRequest) (semanticJson.setObjVal! field (toJson "forbidden")) with | .ok _ => throw <| IO.userError s!"project request unexpectedly accepted session field '{field}'" | .error _ => pure () - for op in [Op.initWorkspace, .listWorkspaces, .dropWorkspace, .resetStats, .shutdown] do + for op in [Op.ensure, .initWorkspace, .listWorkspaces, .dropWorkspace, .resetStats, .shutdown] do match fromJson? (α := ProjectRequest) <| Json.mkObj [ ("op", toJson op), ("clientRequestId", toJson "control-request") diff --git a/tests/lib/beam-wrapper-common.sh b/tests/lib/beam-wrapper-common.sh index d1e8f98f..4157ca90 100644 --- a/tests/lib/beam-wrapper-common.sh +++ b/tests/lib/beam-wrapper-common.sh @@ -444,7 +444,7 @@ beam_wrapper_cleanup() { done for root in ${beam_wrapper_managed_roots[@]+"${beam_wrapper_managed_roots[@]}"}; do - "$beam_script" --root "$root" shutdown > /dev/null 2>&1 || true + "$beam_script" --root "$root" stop > /dev/null 2>&1 || true done if [ -n "${beam_wrapper_tmp_root:-}" ] && [ -d "$beam_wrapper_tmp_root" ]; then @@ -488,11 +488,11 @@ beam_wrapper_start_owner() { local err="$root/.beam/test-owner.err" local registry="$root/.beam/beam-daemon.json" - "$beam_script" --root "$root" ensure "$backend" --hold >"$out" 2>"$err" & + "$beam_script" --root "$root" serve "$backend" >"$out" 2>"$err" & beam_wrapper_last_owner_pid="$!" beam_wrapper_register_pid "$beam_wrapper_last_owner_pid" if ! wait_for_file "$registry" "Beam session owner registry" 60 || - ! wait_for_file_text "$err" "owning Beam session" "Beam session owner readiness" 600 0.1; then + ! wait_for_file_text "$err" "serving Beam session" "Beam session owner readiness" 600 0.1; then echo "expected explicit Beam session owner to become ready for $root" >&2 if [ -f "$out" ]; then cat "$out" >&2 diff --git a/tests/test-beam-fast.sh b/tests/test-beam-fast.sh index 44e53b2c..319c90b0 100644 --- a/tests/test-beam-fast.sh +++ b/tests/test-beam-fast.sh @@ -358,7 +358,7 @@ wrapper_todo_owner_err="$(mktemp /tmp/lean-beam-wrapper-todo-owner-err-XXXXXX)" wrapper_todo_owner_pid="" wrapper_todo_cleanup() { scripts/lean-beam --root tests/save_olean_project \ - --control-dir "$wrapper_todo_control_dir" shutdown > /dev/null 2>&1 || true + --session-dir "$wrapper_todo_control_dir" stop > /dev/null 2>&1 || true if [ -n "$wrapper_todo_owner_pid" ]; then wait "$wrapper_todo_owner_pid" 2>/dev/null || true fi @@ -368,11 +368,11 @@ wrapper_todo_cleanup() { } scripts/lean-beam --root tests/save_olean_project \ - --control-dir "$wrapper_todo_control_dir" ensure --hold \ + --session-dir "$wrapper_todo_control_dir" serve \ >"$wrapper_todo_owner_out" 2>"$wrapper_todo_owner_err" & wrapper_todo_owner_pid="$!" for _ in $(seq 1 600); do - if grep -Fq "owning Beam session" "$wrapper_todo_owner_err"; then + if grep -Fq "serving Beam session" "$wrapper_todo_owner_err"; then break fi if ! kill -0 "$wrapper_todo_owner_pid" 2>/dev/null; then @@ -383,7 +383,7 @@ for _ in $(seq 1 600); do fi sleep 0.1 done -if ! grep -Fq "owning Beam session" "$wrapper_todo_owner_err"; then +if ! grep -Fq "serving Beam session" "$wrapper_todo_owner_err"; then echo "timed out waiting for lean-beam todo wrapper owner" >&2 cat "$wrapper_todo_owner_err" >&2 wrapper_todo_cleanup @@ -391,7 +391,7 @@ if ! grep -Fq "owning Beam session" "$wrapper_todo_owner_err"; then fi if ! scripts/lean-beam --root tests/save_olean_project \ - --control-dir "$wrapper_todo_control_dir" \ + --session-dir "$wrapper_todo_control_dir" \ update TodoSmoke.lean \ > "$wrapper_todo_update_out" 2>"$wrapper_todo_update_err"; then echo "expected lean-beam update wrapper smoke to succeed before todo" >&2 @@ -422,7 +422,7 @@ PY fi if ! scripts/lean-beam --root tests/save_olean_project \ - --control-dir "$wrapper_todo_control_dir" \ + --session-dir "$wrapper_todo_control_dir" \ todo TodoSmoke.lean "$wrapper_todo_version" 13 0 14 0 --kind sorry --suggest none \ > "$wrapper_todo_out" 2>"$wrapper_todo_err"; then echo "expected lean-beam todo wrapper smoke to succeed" >&2 diff --git a/tests/test-beam-install.sh b/tests/test-beam-install.sh index a686b77c..49237070 100644 --- a/tests/test-beam-install.sh +++ b/tests/test-beam-install.sh @@ -32,7 +32,7 @@ cleanup() { local owner_pid owner_root if [ -x "${installed_lean_beam:-}" ]; then for owner_root in ${installed_owner_roots[@]+"${installed_owner_roots[@]}"}; do - "$installed_lean_beam" --root "$owner_root" shutdown > /dev/null 2>&1 || true + "$installed_lean_beam" --root "$owner_root" stop > /dev/null 2>&1 || true done fi for owner_pid in ${installed_owner_pids[@]+"${installed_owner_pids[@]}"}; do @@ -736,11 +736,11 @@ start_installed_owner() { local owner_out="$tmp_root/$label-owner.out" local owner_err="$tmp_root/$label-owner.err" local owner_pid - "$installed_lean_beam" --root "$root" ensure --hold > "$owner_out" 2> "$owner_err" & + "$installed_lean_beam" --root "$root" serve > "$owner_out" 2> "$owner_err" & owner_pid="$!" installed_owner_pids+=("$owner_pid") installed_owner_roots+=("$root") - if ! wait_for_file_text "$owner_err" "owning Beam session" "$label session owner" 600 0.1; then + if ! wait_for_file_text "$owner_err" "serving Beam session" "$label session owner" 600 0.1; then echo "expected installed wrapper owner to become ready for $root" >&2 cat "$owner_out" >&2 cat "$owner_err" >&2 @@ -978,13 +978,13 @@ run_custom_toolchain_install_test() ( assert_doctor_contains "custom toolchain" "$custom_doctor_out" 'bundle source: installed' assert_doctor_contains "custom toolchain" "$custom_doctor_out" 'bundle toolchain fingerprint: ' custom_owner_err="$custom_project_root/custom-owner.err" - ELAN_HOME="$custom_elan_home" "$custom_installed_lean_beam" --root "$custom_project_root" ensure --hold \ + ELAN_HOME="$custom_elan_home" "$custom_installed_lean_beam" --root "$custom_project_root" serve \ > /dev/null 2>"$custom_owner_err" & custom_owner_pid="$!" - if ! wait_for_file_text "$custom_owner_err" "owning Beam session" "custom-toolchain session owner" 600 0.1; then + if ! wait_for_file_text "$custom_owner_err" "serving Beam session" "custom-toolchain session owner" 600 0.1; then exit 1 fi - ELAN_HOME="$custom_elan_home" "$custom_installed_lean_beam" --root "$custom_project_root" shutdown > /dev/null + ELAN_HOME="$custom_elan_home" "$custom_installed_lean_beam" --root "$custom_project_root" stop > /dev/null wait_for_exit "$custom_owner_pid" "custom-toolchain session owner" 120 0.1 wait "$custom_owner_pid" ) @@ -1611,7 +1611,7 @@ if ! printf '%s\n' "$unsupported_doctor_out" | grep -q 'bundle toolchain fingerp fi unsupported_err="$(mktemp "$tmp_root/install-unsupported-toolchain-XXXXXX")" -"$installed_lean_beam" --root "$unsupported_project_root" ensure --hold >"$unsupported_err" 2>&1 & +"$installed_lean_beam" --root "$unsupported_project_root" serve >"$unsupported_err" 2>&1 & unsupported_owner_pid="$!" if ! wait_for_exit "$unsupported_owner_pid" "unsupported-toolchain session owner" 120 0.1; then kill -INT "$unsupported_owner_pid" 2>/dev/null || true diff --git a/tests/test-beam-save-olean.sh b/tests/test-beam-save-olean.sh index 627c028e..52b1db15 100755 --- a/tests/test-beam-save-olean.sh +++ b/tests/test-beam-save-olean.sh @@ -42,10 +42,10 @@ beam_start_owner() { local root="$1" local owner_out="$root/.beam-test-owner.out" local owner_err="$root/.beam-test-owner.err" - beam --root "$root" ensure --hold >"$owner_out" 2>"$owner_err" & + beam --root "$root" serve >"$owner_out" 2>"$owner_err" & beam_owner_last_pid="$!" beam_owner_pids+=("$beam_owner_last_pid") - if ! wait_for_file_text "$owner_err" "owning Beam session" "save-replay session owner" 600 0.1; then + if ! wait_for_file_text "$owner_err" "serving Beam session" "save-replay session owner" 600 0.1; then cat "$owner_out" >&2 cat "$owner_err" >&2 exit 1 @@ -371,7 +371,7 @@ cleanup() { local root owner_pid for root in "$tmp2" "$tmp3" "$tmp4" "$tmp5" "$tmp6" "$tmp7" "$tmp8"; do if [ -d "$root" ]; then - beam --root "$root" shutdown > /dev/null 2>&1 || true + beam --root "$root" stop > /dev/null 2>&1 || true fi done for owner_pid in ${beam_owner_pids[@]+"${beam_owner_pids[@]}"}; do @@ -496,12 +496,12 @@ PY echo "expected successful retry to publish a replacement trace" >&2 exit 1 fi - beam --root "$tmp2" shutdown > /dev/null 2>&1 || true + beam --root "$tmp2" stop > /dev/null 2>&1 || true lake_build -v SaveSmoke/B.lean >"$log4" 2>&1 rm -f .lake/build/lib/lean/SaveSmoke/A.olean .lake/build/lib/lean/SaveSmoke/A.ilean .lake/build/lib/lean/SaveSmoke/A.trace .lake/build/ir/SaveSmoke/A.c lake_build -v SaveSmoke/A.lean >"$log5" 2>&1 lake_build >"$log2" 2>&1 - beam --root "$tmp2" shutdown > /dev/null 2>&1 || true + beam --root "$tmp2" stop > /dev/null 2>&1 || true ) if ! grep -Eq "Replayed SaveSmoke\\.B" "$log4"; then echo "expected exact-target lake build to replay SaveSmoke.B after broker save" >&2 @@ -547,7 +547,7 @@ PY exit 1 fi done - beam --root "$tmp8" shutdown > /dev/null 2>&1 || true + beam --root "$tmp8" stop > /dev/null 2>&1 || true lake_build -v SaveSmoke/ModuleB.lean >"$log6" 2>&1 LAKE_ARTIFACT_CACHE=false "$lake_cmd" env lean CheckModuleB.lean > /dev/null ) @@ -619,7 +619,7 @@ PY remove_owned_tmp_file "$unsupported_save_out" remove_owned_tmp_file "$unsupported_save_err" LAKE_ARTIFACT_CACHE=false "$lake_cmd" env lean CheckBatchOnly.lean > /dev/null - beam --root "$tmp7" shutdown > /dev/null 2>&1 || true + beam --root "$tmp7" stop > /dev/null 2>&1 || true ) (cd "$tmp3" && lake_build > /dev/null) @@ -657,7 +657,7 @@ edit_b_slow "$tmp3" exit 1 fi lake_build -v SaveSmoke/A.lean >"$log3" 2>&1 - beam --root "$tmp3" shutdown > /dev/null 2>&1 || true + beam --root "$tmp3" stop > /dev/null 2>&1 || true ) if ! grep -Eq "Built SaveSmoke\\.B|Building SaveSmoke\\.B" "$log3"; then echo "expected save_olean race to leave SaveSmoke.B stale for downstream builds" >&2 @@ -711,7 +711,7 @@ LEAN_BEAM_BROKER_TRACE="$save_race_broker_trace" \ exit 1 fi beam --root "$tmp4" stats > /dev/null - beam --root "$tmp4" shutdown > /dev/null + beam --root "$tmp4" stop > /dev/null rm -f "$close_out" "$close_err" ) @@ -745,7 +745,7 @@ beam_start_owner "$tmp6" exit 1 fi beam --root "$tmp6" stats > /dev/null - beam --root "$tmp6" shutdown > /dev/null + beam --root "$tmp6" stop > /dev/null rm -f "$save_out" "$save_err" ) @@ -808,6 +808,6 @@ beam_start_owner "$tmp5" exit 1 fi beam --root "$tmp5" stats > /dev/null - beam --root "$tmp5" shutdown > /dev/null + beam --root "$tmp5" stop > /dev/null rm -f "$sync_out" "$sync_err" "$save_out" "$save_err" ) diff --git a/tests/test-beam-toolchain-compat.sh b/tests/test-beam-toolchain-compat.sh index 44e729eb..d71099ae 100644 --- a/tests/test-beam-toolchain-compat.sh +++ b/tests/test-beam-toolchain-compat.sh @@ -60,7 +60,7 @@ cleanup() { if [ -n "${stale_project_root:-}" ] && [ -d "$stale_project_root" ]; then HOME="$tmp_env_root/home" CODEX_HOME="$tmp_env_root/codex" CLAUDE_HOME="$tmp_env_root/claude" \ ELAN_HOME="$host_elan_home" BEAM_INSTALL_BUNDLE_DIR="$tmp_bundle_dir" \ - ./scripts/lean-beam --root "$stale_project_root" shutdown > /dev/null 2>&1 || true + ./scripts/lean-beam --root "$stale_project_root" stop > /dev/null 2>&1 || true fi if [ -n "${stale_owner_pid:-}" ]; then if kill -0 "$stale_owner_pid" 2>/dev/null; then @@ -165,7 +165,7 @@ PY run_bundle_install() { local rc=0 ( - unset BEAM_HOME BEAM_CONTROL_ROOT + unset BEAM_HOME BEAM_SESSION_ROOT export HOME="$tmp_env_root/home" export CODEX_HOME="$tmp_env_root/codex" export CLAUDE_HOME="$tmp_env_root/claude" @@ -275,9 +275,9 @@ run_stale_wrapper_checked() { } start_stale_owner() { - run_stale_wrapper ensure --hold > "$stale_owner_stdout" 2> "$stale_owner_stderr" & + run_stale_wrapper serve > "$stale_owner_stdout" 2> "$stale_owner_stderr" & stale_owner_pid="$!" - if ! wait_for_file_text "$stale_owner_stderr" "owning Beam session" \ + if ! wait_for_file_text "$stale_owner_stderr" "serving Beam session" \ "toolchain compatibility session owner" 600 0.1; then print_toolchain_context "explicit session owner failed to start" return 1 @@ -288,7 +288,7 @@ stop_stale_owner() { if [ -z "$stale_owner_pid" ]; then return 0 fi - if ! run_stale_wrapper shutdown > /dev/null 2> "$stale_sync_stderr"; then + if ! run_stale_wrapper stop > /dev/null 2> "$stale_sync_stderr"; then print_toolchain_context "explicit session owner failed to shut down" return 1 fi diff --git a/tests/test-beam-wrapper-daemon.sh b/tests/test-beam-wrapper-daemon.sh index ba5d5de9..5226b299 100644 --- a/tests/test-beam-wrapper-daemon.sh +++ b/tests/test-beam-wrapper-daemon.sh @@ -96,12 +96,12 @@ stop_hold_process() { return fi kill -INT "$hold_pid" > /dev/null 2>&1 || true - if ! wait_for_exit "$hold_pid" "ensure --hold owner" 200 0.05; then + if ! wait_for_exit "$hold_pid" "serve owner" 200 0.05; then kill "$hold_pid" > /dev/null 2>&1 || true wait "$hold_pid" 2>/dev/null || true hold_pid="" if [ "$require_clean_exit" = "true" ]; then - echo "expected ensure --hold owner to exit promptly after SIGINT" >&2 + echo "expected serve owner to exit promptly after SIGINT" >&2 return 1 fi return @@ -113,7 +113,7 @@ stop_hold_process() { set -e hold_pid="" if [ "$require_clean_exit" = "true" ] && [ "$status" -ne 0 ]; then - echo "expected ensure --hold owner to exit cleanly, got $status" >&2 + echo "expected serve owner to exit cleanly, got $status" >&2 return 1 fi } @@ -139,10 +139,10 @@ cleanup() { fi stop_hold_process if [ "$root_removed" != "true" ]; then - "$beam_script" --root "$tmp1" shutdown > /dev/null 2>&1 || true + "$beam_script" --root "$tmp1" stop > /dev/null 2>&1 || true remove_owned_tmp_tree "$tmp1" fi - "$beam_script" --root "$tmp2" shutdown > /dev/null 2>&1 || true + "$beam_script" --root "$tmp2" stop > /dev/null 2>&1 || true remove_owned_tmp_tree "$tmp2" if [ -n "$owned_bundle_dir" ]; then remove_owned_tmp_tree "$owned_bundle_dir" @@ -162,13 +162,15 @@ for tmp in "$tmp1" "$tmp2"; do mkdir -p "$tmp/tests/scenario/docs" cp tests/scenario/docs/SlowPoll.lean "$tmp/tests/scenario/docs/SlowPoll.lean" done +resolved_tmp1="$(beam_test_realpath "$tmp1")" +resolved_tmp2="$(beam_test_realpath "$tmp2")" fixture_toolchain="$(awk 'NR==1 {print $1}' tests/save_olean_project/lean-toolchain)" "$beam_cli" bundle-install "$fixture_toolchain" invalid_backend_out="$tmp1/invalid-backend.out" invalid_backend_err="$tmp1/invalid-backend.err" -if "$beam_script" --root "$tmp1" ensure typo --hold > "$invalid_backend_out" 2> "$invalid_backend_err"; then +if "$beam_script" --root "$tmp1" serve typo > "$invalid_backend_out" 2> "$invalid_backend_err"; then echo "expected an unknown owner backend to be rejected" >&2 cat "$invalid_backend_out" >&2 exit 1 @@ -184,24 +186,63 @@ fi remove_tmp_tree_within "$tmp1/.beam" "$tmp1" missing_owner_out="$tmp1/missing-owner.out" missing_owner_err="$tmp1/missing-owner.err" -if "$beam_script" --root "$tmp1" ensure > "$missing_owner_out" 2> "$missing_owner_err"; then +if "$beam_script" --root "$tmp1" stats > "$missing_owner_out" 2> "$missing_owner_err"; then echo "expected an ordinary wrapper command to require a session owner" >&2 cat "$missing_owner_out" >&2 exit 1 fi -if ! grep -Fq "lean-beam ensure --hold" "$missing_owner_err"; then - echo "expected missing-owner error to name the recovery command" >&2 +missing_owner_command="lean-beam --root '$resolved_tmp1' --session-dir '$resolved_tmp1/.beam' serve" +if ! grep -Fq "$missing_owner_command" "$missing_owner_err"; then + echo "expected missing-owner error to preserve the exact session selector" >&2 cat "$missing_owner_err" >&2 exit 1 fi +missing_status="$("$beam_script" --root "$tmp1" status)" +assert_json_field_equals "absent session status response" "$missing_status" ok true +assert_json_field_equals "absent session status state" "$missing_status" result.state absent +absent_stop="$("$beam_script" --root "$tmp1" stop)" +assert_json_field_equals "absent session stop response" "$absent_stop" ok true +assert_json_field_equals "absent session stop state" "$absent_stop" result.state absent +assert_json_field_equals "absent session stop changed" "$absent_stop" result.changed false +absent_recover="$("$beam_script" --root "$tmp1" recover --force)" +assert_json_field_equals "absent session recovery response" "$absent_recover" ok true +assert_json_field_equals "absent session recovery state" "$absent_recover" result.state absent +assert_json_field_equals "absent session recovery change" "$absent_recover" result.changed false if [ -e "$tmp1/.beam" ]; then - echo "expected missing-owner attachment not to create the project control directory" >&2 + echo "expected absent status, stop, and recovery not to create the project session directory" >&2 find "$tmp1/.beam" -maxdepth 2 -print >&2 || true exit 1 fi -# A control path is an exact security boundary, not a redirect. Reject a symlinked default path -# without changing the target or creating any control files through it. +# A feedback bundle can be the first writer below `.beam`. It must establish the same private +# project-state boundary expected by a later wrapper session rather than creating an incompatible +# umask-derived directory. +feedback_private_input='{"title":"Private Beam state","summary":"Check feedback state setup.","reproduction":"feedback before serve","expected":"Private shared state.","actual":"Private shared state."}' +feedback_private_json="$(printf '%s\n' "$feedback_private_input" | \ + "$beam_script" --root "$tmp1" feedback-report --stdin --bundle dir)" +assert_json_field_equals "feedback bundle mode" "$feedback_private_json" metadata.bundle dir +if [ "$(file_mode "$tmp1/.beam")" != "700" ]; then + echo "expected feedback to create the shared Beam state directory with mode 700" >&2 + exit 1 +fi +feedback_status="$("$beam_script" --root "$tmp1" status)" +assert_json_field_equals \ + "feedback-created state remains a valid session selection" "$feedback_status" result.state absent +remove_tmp_tree_within "$tmp1/.beam/feedback" "$tmp1" +rmdir "$tmp1/.beam" + +mkdir -p "$tmp1/.beam" +chmod 700 "$tmp1/.beam" +"$beam_script" --root "$tmp1" stop > /dev/null +"$beam_script" --root "$tmp1" recover --force > /dev/null +if [ -e "$tmp1/.beam/lock" ]; then + echo "expected absent lifecycle commands not to create a lock in an existing session directory" >&2 + exit 1 +fi +rmdir "$tmp1/.beam" + +# A session path is an exact security boundary, not a redirect. Reject a symlinked default path +# without changing the target or creating any session files through it. symlink_control_target="$tmp2/symlink-control-target" mkdir -p "$symlink_control_target" chmod 755 "$symlink_control_target" @@ -234,7 +275,7 @@ start_owner() { local label="$2" local out="$root/$label.out" local err="$root/$label.err" - "$beam_script" --root "$root" ensure --hold > "$out" 2> "$err" & + "$beam_script" --root "$root" serve > "$out" 2> "$err" & hold_pid="$!" local registry="$root/.beam/beam-daemon.json" local attempts="${BEAM_TEST_HOLD_READY_ATTEMPTS:-1800}" @@ -256,11 +297,22 @@ start_owner() { sleep 0.1 done if [ ! -s "$out" ] || [ ! -f "$registry" ]; then - echo "expected ensure --hold to publish its response and registry" >&2 + echo "expected serve to publish its response and registry" >&2 cat "$err" >&2 exit 1 fi - assert_json_field_equals "ensure --hold response" "$(cat "$out")" ok true "$err" + assert_json_field_equals "serve response" "$(cat "$out")" ok true "$err" + assert_json_field_equals "serve state" "$(cat "$out")" result.state running "$err" + assert_json_field_equals \ + "serve workspace" "$(cat "$out")" result.workspace "$(beam_test_realpath "$root")" "$err" + assert_json_field_equals \ + "serve session directory" "$(cat "$out")" result.sessionDir \ + "$(beam_test_realpath "$root")/.beam" "$err" + assert_json_field_equals \ + "serve generation" "$(cat "$out")" result.generation \ + "$(read_json_field "$registry" daemonId)" "$err" + assert_json_field_absent "serve response" "$(cat "$out")" result.workspace_id "$err" + assert_json_field_absent "serve response" "$(cat "$out")" result.epoch "$err" } registry="$tmp1/.beam/beam-daemon.json" @@ -281,10 +333,15 @@ if ! kill -0 "$owner1_pid" 2>/dev/null || ! kill -0 "$daemon1_pid" 2>/dev/null; exit 1 fi -ensure_json="$("$beam_script" --root "$tmp1" ensure)" -assert_json_field_equals "owned ensure response" "$ensure_json" ok true stats_json="$("$beam_script" --root "$tmp1" stats)" assert_json_field_equals "owned stats response" "$stats_json" ok true +status_json="$("$beam_script" --root "$tmp1" status)" +assert_json_field_equals "running session status response" "$status_json" ok true +assert_json_field_equals "running session status state" "$status_json" result.state running +assert_json_field_equals "running session status generation" "$status_json" result.generation "$daemon1_id" +assert_json_field_equals "running session status workspace" "$status_json" result.workspace "$resolved_tmp1" +assert_json_field_equals \ + "running session status directory" "$status_json" result.sessionDir "$resolved_tmp1/.beam" machine_stats_json="$("$beam_script" --root "$tmp1" request-stream \ '{"op":"stats","clientRequestId":"machine-stats"}')" @@ -343,12 +400,11 @@ import sys registry, root = sys.argv[1:] with open(registry, encoding="utf-8") as stream: entry = json.load(stream) -if entry.get("schemaVersion") != 2: +if entry.get("schemaVersion") != 3: raise SystemExit(f"unexpected session schema: {entry.get('schemaVersion')}") -workspaces = entry.get("workspaces") -if not isinstance(workspaces, list) or len(workspaces) != 1: - raise SystemExit(f"unexpected workspace bindings: {workspaces!r}") -workspace = workspaces[0] +workspace = entry.get("workspace") +if not isinstance(workspace, dict): + raise SystemExit(f"unexpected workspace binding: {workspace!r}") if workspace.get("root") != os.path.realpath(root): raise SystemExit(f"unexpected workspace root: {workspace!r}") if workspace.get("workspaceId") != "beam-cli-project": @@ -368,7 +424,23 @@ fi cross_root_descriptor="$tmp2/cross-root-recovery.before" cp -- "$registry" "$cross_root_descriptor" -if "$beam_script" --root "$tmp2" --control-dir "$tmp1/.beam" \ +if "$beam_script" --root "$tmp2" --session-dir "$tmp1/.beam" status \ + > "$tmp2/cross-root-status.out" 2> "$tmp2/cross-root-status.err"; then + echo "expected status through a mismatched session selector to fail" >&2 + exit 1 +fi +if ! grep -Fq "sessionSelectorMismatch" "$tmp2/cross-root-status.err" || \ + ! grep -Fq -- "--root '$resolved_tmp1' --session-dir '$resolved_tmp1/.beam' status" \ + "$tmp2/cross-root-status.err"; then + echo "expected cross-root status rejection to identify the selector mismatch and exact selector" >&2 + cat "$tmp2/cross-root-status.err" >&2 + exit 1 +fi +if ! cmp -s -- "$cross_root_descriptor" "$registry"; then + echo "cross-root status must preserve the descriptor byte-for-byte" >&2 + exit 1 +fi +if "$beam_script" --root "$tmp2" --session-dir "$tmp1/.beam" \ recover --generation "$daemon1_id" \ > "$tmp2/cross-root-recovery.out" 2> "$tmp2/cross-root-recovery.err"; then echo "expected recovery through a non-member root to fail closed" >&2 @@ -408,19 +480,37 @@ if [ "$(read_json_field "$registry" daemonId)" != "$daemon1_id" ] || \ exit 1 fi -if BEAM_CONTROL_ROOT=relative-control-root \ +if BEAM_SESSION_ROOT=relative-control-root \ "$beam_script" --root "$tmp1" stats \ > "$tmp1/relative-control-root.out" 2> "$tmp1/relative-control-root.err"; then - echo "expected relative BEAM_CONTROL_ROOT to be rejected" >&2 + echo "expected relative BEAM_SESSION_ROOT to be rejected" >&2 exit 1 fi -if ! grep -Fq "BEAM_CONTROL_ROOT must be an absolute path" \ +if ! grep -Fq "BEAM_SESSION_ROOT must be an absolute path" \ "$tmp1/relative-control-root.err"; then - echo "expected relative BEAM_CONTROL_ROOT rejection to explain the stable-path requirement" >&2 + echo "expected relative BEAM_SESSION_ROOT rejection to explain the stable-path requirement" >&2 cat "$tmp1/relative-control-root.err" >&2 exit 1 fi +environment_session_base="$tmp2/environment-session-base" +environment_session_alias="$tmp2/environment-session-alias" +mkdir -p "$environment_session_base" +ln -s "$environment_session_base" "$environment_session_alias" +environment_status="$(BEAM_SESSION_ROOT="$environment_session_alias" \ + "$beam_script" --root "$tmp1" status)" +environment_session_dir="$(json_text_field "$environment_status" result.sessionDir)" +case "$environment_session_dir" in + "$(beam_test_realpath "$environment_session_base")"/*) ;; + *) + echo "expected BEAM_SESSION_ROOT to publish a canonical derived session selector" >&2 + printf '%s\n' "$environment_status" >&2 + exit 1 + ;; +esac +rm -f -- "$environment_session_alias" +rmdir "$environment_session_base" + port1="$(read_json_field "$registry" port)" python3 - "$port1" <<'PY' import json @@ -484,7 +574,7 @@ fi second_owner_out="$tmp1/second-owner.out" second_owner_err="$tmp1/second-owner.err" -if "$beam_script" --root "$tmp1" ensure --hold > "$second_owner_out" 2> "$second_owner_err"; then +if "$beam_script" --root "$tmp1" serve > "$second_owner_out" 2> "$second_owner_err"; then echo "expected a second foreground owner to be rejected" >&2 cat "$second_owner_out" >&2 exit 1 @@ -497,7 +587,7 @@ fi collision_out="$tmp2/collision.out" collision_err="$tmp2/collision.err" -if "$beam_script" --root "$tmp2" --port "$port1" ensure --hold > "$collision_out" 2> "$collision_err"; then +if "$beam_script" --root "$tmp2" --port "$port1" serve > "$collision_out" 2> "$collision_err"; then echo "expected an owner not to claim another project's endpoint" >&2 cat "$collision_out" >&2 exit 1 @@ -520,7 +610,7 @@ import os with open(os.environ["REGISTRY_TEMPLATE"], encoding="utf-8") as stream: entry = json.load(stream) -entry["workspaces"][0]["root"] = os.path.realpath(os.environ["STALE_ROOT"]) +entry["workspace"]["root"] = os.path.realpath(os.environ["STALE_ROOT"]) replacement = os.environ["STALE_REGISTRY"] + ".replacement" with open(replacement, "w", encoding="utf-8") as stream: json.dump(entry, stream, separators=(",", ":")) @@ -529,7 +619,7 @@ os.replace(replacement, os.environ["STALE_REGISTRY"]) PY stale_shutdown_out="$tmp2/stale-cross-root-shutdown.out" stale_shutdown_err="$tmp2/stale-cross-root-shutdown.err" -if "$beam_script" --root "$tmp2" shutdown \ +if "$beam_script" --root "$tmp2" stop \ > "$stale_shutdown_out" 2> "$stale_shutdown_err"; then echo "expected shutdown to reject a registry whose endpoint serves another root" >&2 cat "$stale_shutdown_out" >&2 @@ -570,7 +660,7 @@ PY legacy_before="$(cat "$stale_registry")" legacy_owner_out="$tmp2/legacy-owner.out" legacy_owner_err="$tmp2/legacy-owner.err" -if "$beam_script" --root "$tmp2" ensure --hold \ +if "$beam_script" --root "$tmp2" serve \ > "$legacy_owner_out" 2> "$legacy_owner_err"; then echo "expected owner startup to reject a schema-less legacy registry" >&2 cat "$legacy_owner_out" >&2 @@ -587,12 +677,14 @@ if [ "$(cat "$stale_registry")" != "$legacy_before" ]; then exit 1 fi legacy_recover_json="$("$beam_script" --root "$tmp2" recover --force)" -assert_json_field_equals "opaque registry recovery" "$legacy_recover_json" recovered true +assert_json_field_equals "opaque registry recovery response" "$legacy_recover_json" ok true +assert_json_field_equals "opaque registry recovery state" "$legacy_recover_json" result.state absent +assert_json_field_equals "opaque registry recovery change" "$legacy_recover_json" result.changed true if [ -e "$stale_registry" ]; then echo "expected explicit opaque recovery to quarantine the legacy descriptor" >&2 exit 1 fi -legacy_quarantine="$(json_text_field "$legacy_recover_json" quarantinedPath)" +legacy_quarantine="$(json_text_field "$legacy_recover_json" result.quarantinedPath)" if [ ! -f "$legacy_quarantine" ]; then echo "expected opaque recovery to preserve quarantined evidence" >&2 printf '%s\n' "$legacy_recover_json" >&2 @@ -620,7 +712,7 @@ fi busy_port="$(cat "$busy_port_file")" busy_out="$tmp2/non-beam-port.out" busy_err="$tmp2/non-beam-port.err" -if "$beam_script" --root "$tmp2" --port "$busy_port" ensure --hold > "$busy_out" 2> "$busy_err"; then +if "$beam_script" --root "$tmp2" --port "$busy_port" serve > "$busy_out" 2> "$busy_err"; then echo "expected owner startup to reject a port occupied by a non-Beam service" >&2 cat "$busy_out" >&2 exit 1 @@ -664,7 +756,7 @@ busy_port="$(cat "$busy_port_file")" busy_out="$tmp2/silent-non-beam-port.out" busy_err="$tmp2/silent-non-beam-port.err" silent_probe_started="$SECONDS" -if "$beam_script" --root "$tmp2" --port "$busy_port" ensure --hold > "$busy_out" 2> "$busy_err"; then +if "$beam_script" --root "$tmp2" --port "$busy_port" serve > "$busy_out" 2> "$busy_err"; then echo "expected owner startup to reject a silent non-Beam service" >&2 cat "$busy_out" >&2 exit 1 @@ -691,6 +783,121 @@ busy_pid="" rm -f -- "$busy_port_file" busy_port_file="" +# Once stop commits its draining fence, a delivery failure must remain a successful, typed +# transition result rather than obscuring the state change. This fixture answers the identity +# probe, then drops the separate shutdown connection. +busy_port_file="$(mktemp "$tmp2/drop-shutdown-port-XXXXXX")" +python3 - "$busy_port_file" "$resolved_tmp2" <<'PY' & +import json +import socketserver +import sys + +port_file, root = sys.argv[1:] +daemon_id = "delivery-failure-generation" +config_hash = "delivery-failure-config" + +def receive_frame(sock): + header = bytearray() + while not header.endswith(b"\n"): + chunk = sock.recv(1) + if not chunk: + raise RuntimeError("client closed before sending a frame header") + header.extend(chunk) + size = int(header[:-1]) + payload = bytearray() + while len(payload) < size: + chunk = sock.recv(size - len(payload)) + if not chunk: + raise RuntimeError("client closed during its frame") + payload.extend(chunk) + return json.loads(payload) + +def send_frame(sock, payload): + encoded = json.dumps(payload, separators=(",", ":")).encode() + sock.sendall(str(len(encoded)).encode() + b"\n" + encoded) + +class Server(socketserver.TCPServer): + allow_reuse_address = True + +with Server(("127.0.0.1", 0), socketserver.BaseRequestHandler) as server: + with open(port_file, "w", encoding="utf-8") as stream: + print(server.server_address[1], file=stream, flush=True) + conn, _ = server.get_request() + with conn: + request = receive_frame(conn) + if request.get("op") != "stats": + raise RuntimeError(f"expected stats probe, got {request!r}") + send_frame(conn, { + "kind": "response", + "payload": { + "ok": True, + "result": { + "root": root, + "daemonIdentity": { + "daemonId": daemon_id, + "configHash": config_hash, + }, + }, + }, + }) + conn, _ = server.get_request() + with conn: + receive_frame(conn) + # Deliberately close without a response after the caller has committed `draining`. +PY +busy_pid="$!" +if ! wait_for_nonempty_file "$busy_port_file" "shutdown-delivery fixture"; then + exit 1 +fi +busy_port="$(cat "$busy_port_file")" +DELIVERY_REGISTRY="$stale_registry" DELIVERY_ROOT="$resolved_tmp2" \ + DELIVERY_PORT="$busy_port" python3 - <<'PY' +import json +import os + +entry = { + "schemaVersion": 3, + "lifecycle": "live", + "daemonId": "delivery-failure-generation", + "capability": "delivery-failure-capability", + "pid": 999999999, + "ownerPid": 999999999, + "port": int(os.environ["DELIVERY_PORT"]), + "workspace": { + "workspaceId": "beam-cli-project", + "root": os.environ["DELIVERY_ROOT"], + }, + "configHash": "delivery-failure-config", + "startedAt": "2026-08-30T00:00:00Z", +} +with open(os.environ["DELIVERY_REGISTRY"], "w", encoding="utf-8") as stream: + json.dump(entry, stream, separators=(",", ":")) + stream.write("\n") +PY +delivery_stop_json="$("$beam_script" --root "$tmp2" stop)" +assert_json_field_equals "committed delivery-failure stop response" "$delivery_stop_json" ok true +assert_json_field_equals \ + "committed delivery-failure stop state" "$delivery_stop_json" result.state stopping +assert_json_field_equals \ + "committed delivery-failure stop change" "$delivery_stop_json" result.changed true +assert_json_field_equals \ + "committed delivery-failure stop warning" "$delivery_stop_json" \ + result.warning.code shutdownDeliveryFailed +if [ "$(read_json_field "$stale_registry" lifecycle)" != "draining" ]; then + echo "expected shutdown delivery failure to preserve the committed draining fence" >&2 + cat "$stale_registry" >&2 + exit 1 +fi +wait "$busy_pid" +busy_pid="" +rm -f -- "$busy_port_file" +busy_port_file="" +delivery_recover_json="$( + "$beam_script" --root "$tmp2" recover --generation delivery-failure-generation +)" +assert_json_field_equals \ + "delivery-failure fence recovery" "$delivery_recover_json" result.changed true + start_slow_request "$tmp1" "shutdown-active" "shutdown-active" # The desired owner configuration includes installed bundle paths. An ordinary attaching command @@ -703,7 +910,7 @@ rsync -a "$BEAM_INSTALL_BUNDLE_DIR/" "$drift_bundle_dir/" drift_out="$tmp1/config-drift.out" drift_err="$tmp1/config-drift.err" if ! BEAM_INSTALL_BUNDLE_DIR="$drift_bundle_dir" \ - "$beam_script" --root "$tmp1" ensure > "$drift_out" 2> "$drift_err"; then + "$beam_script" --root "$tmp1" stats > "$drift_out" 2> "$drift_err"; then echo "expected ordinary attachment to use the owner's frozen configuration" >&2 cat "$drift_err" >&2 exit 1 @@ -713,7 +920,7 @@ assert_json_file_field_equals \ drift_owner_out="$tmp1/config-drift-owner.out" drift_owner_err="$tmp1/config-drift-owner.err" if BEAM_INSTALL_BUNDLE_DIR="$drift_bundle_dir" \ - "$beam_script" --root "$tmp1" ensure --hold \ + "$beam_script" --root "$tmp1" serve \ > "$drift_owner_out" 2> "$drift_owner_err"; then echo "expected a mismatched replacement owner to be rejected" >&2 cat "$drift_owner_out" >&2 @@ -742,8 +949,27 @@ if ! kill -0 "$owner1_pid" 2>/dev/null || ! kill -0 "$daemon1_pid" 2>/dev/null | exit 1 fi -shutdown_json="$("$beam_script" --root "$tmp1" shutdown)" -assert_json_field_equals "explicit session shutdown" "$shutdown_json" ok true +if ( + cd "$tmp1" + "$beam_script" stop > "$tmp1/implicit-stop.out" 2> "$tmp1/implicit-stop.err" +); then + echo "expected stop to require an explicit root" >&2 + exit 1 +fi +if ! grep -Fq "stop requires an explicit --root PATH" "$tmp1/implicit-stop.err"; then + echo "expected implicit stop rejection to explain the explicit selector" >&2 + cat "$tmp1/implicit-stop.err" >&2 + exit 1 +fi +if ! kill -0 "$owner1_pid" 2>/dev/null || ! kill -0 "$daemon1_pid" 2>/dev/null; then + echo "implicit stop rejection must preserve the running session" >&2 + exit 1 +fi + +stop_json="$("$beam_script" --root "$tmp1" stop)" +assert_json_field_equals "explicit session stop" "$stop_json" ok true +assert_json_field_equals "explicit session stop state" "$stop_json" result.state stopping +assert_json_field_equals "explicit session stop changed" "$stop_json" result.changed true expect_slow_request_cancelled "$tmp1" "shutdown-active" "shutdown-active" if ! wait_for_exit "$hold_pid" "owner after explicit shutdown" 200 0.05; then cat "$tmp1/owner-1.err" >&2 @@ -767,6 +993,8 @@ if [ -e "$registry" ]; then cat "$registry" >&2 exit 1 fi +stopped_status="$("$beam_script" --root "$tmp1" status)" +assert_json_field_equals "stopped session status state" "$stopped_status" result.state absent start_owner "$tmp1" "owner-2" daemon2_pid="$(read_json_field "$registry" pid)" @@ -800,23 +1028,85 @@ if [ ! -e "$registry" ]; then exit 1 fi if [ "$(read_json_field "$registry" daemonId)" != "$daemon2_id" ] || \ - [ "$(read_json_field "$registry" lifecycle)" != "draining" ]; then - echo "expected an unexpected daemon crash to leave its generation draining" >&2 + [ "$(read_json_field "$registry" lifecycle)" != "live" ]; then + echo "expected an unexpected daemon crash to preserve its live generation fence" >&2 cat "$registry" >&2 exit 1 fi -if "$beam_script" --root "$tmp1" ensure --hold \ +crash_status_json="$("$beam_script" --root "$tmp1" status)" +assert_json_field_equals \ + "unexpected-crash session status" "$crash_status_json" result.state recoveryRequired +assert_json_field_equals \ + "unexpected-crash session generation" "$crash_status_json" result.generation "$daemon2_id" +if "$beam_script" --root "$tmp1" serve \ > "$tmp1/crash-replacement.out" 2> "$tmp1/crash-replacement.err"; then echo "expected crash-fenced state to reject a replacement owner" >&2 exit 1 fi crash_recovery_json="$("$beam_script" --root "$tmp1" recover --generation "$daemon2_id")" -assert_json_field_equals "unexpected-crash recovery" "$crash_recovery_json" recovered true +assert_json_field_equals "unexpected-crash recovery response" "$crash_recovery_json" ok true +assert_json_field_equals "unexpected-crash recovery state" "$crash_recovery_json" result.state absent +assert_json_field_equals "unexpected-crash recovery change" "$crash_recovery_json" result.changed true if [ -e "$registry" ]; then echo "expected exact-generation crash recovery to quarantine the fence" >&2 exit 1 fi +# If the daemon exits abnormally after drain begins, leader exit is not proof of successful cleanup. +# Restore the exact generation to a conservative recovery-required fence instead of admitting a +# replacement owner. +start_owner "$tmp1" "owner-failed-drain" +failed_drain_daemon_pid="$(read_json_field "$registry" pid)" +failed_drain_daemon_id="$(read_json_field "$registry" daemonId)" +kill -STOP "$failed_drain_daemon_pid" +paused_daemon_pid="$failed_drain_daemon_pid" +kill -INT "$hold_pid" +for _ in $(seq 1 40); do + if [ -e "$registry" ] && [ "$(read_json_field "$registry" lifecycle)" = "draining" ]; then + break + fi + sleep 0.05 +done +if [ ! -e "$registry" ] || [ "$(read_json_field "$registry" lifecycle)" != "draining" ]; then + echo "expected interrupted owner to publish the failed-drain fence before cleanup" >&2 + cat "$registry" >&2 + exit 1 +fi +kill -KILL "$failed_drain_daemon_pid" +paused_daemon_pid="" +if ! wait_for_exit "$hold_pid" "owner after abnormal exit during drain" 80 0.05; then + cat "$tmp1/owner-failed-drain.err" >&2 + exit 1 +fi +wait "$hold_pid" +hold_pid="" +if ! wait_for_exit "$failed_drain_daemon_pid" "daemon after abnormal exit during drain" 40 0.05; then + exit 1 +fi +if [ ! -e "$registry" ] || \ + [ "$(read_json_field "$registry" daemonId)" != "$failed_drain_daemon_id" ] || \ + [ "$(read_json_field "$registry" lifecycle)" != "live" ]; then + echo "expected abnormal drain exit to preserve the exact recovery fence" >&2 + if [ -e "$registry" ]; then cat "$registry" >&2; fi + exit 1 +fi +failed_drain_status="$("$beam_script" --root "$tmp1" status)" +assert_json_field_equals \ + "failed-drain session status" "$failed_drain_status" result.state recoveryRequired +assert_json_field_equals \ + "failed-drain session generation" "$failed_drain_status" \ + result.generation "$failed_drain_daemon_id" +if "$beam_script" --root "$tmp1" serve \ + > "$tmp1/failed-drain-replacement.out" 2> "$tmp1/failed-drain-replacement.err"; then + echo "expected failed-drain recovery fence to reject a replacement owner" >&2 + exit 1 +fi +failed_drain_recovery="$( + "$beam_script" --root "$tmp1" recover --generation "$failed_drain_daemon_id" +)" +assert_json_field_equals \ + "failed-drain recovery" "$failed_drain_recovery" result.changed true + start_owner "$tmp1" "owner-draining-fence" draining_daemon_pid="$(read_json_field "$registry" pid)" draining_daemon_id="$(read_json_field "$registry" daemonId)" @@ -844,9 +1134,17 @@ if ! kill -0 "$hold_pid" 2>/dev/null || ! kill -0 "$draining_daemon_pid" 2>/dev/ echo "expected the paused daemon and its owner to remain alive during the drain check" >&2 exit 1 fi +draining_status="$("$beam_script" --root "$tmp1" status)" +assert_json_field_equals "draining session status" "$draining_status" result.state stopping +assert_json_field_equals \ + "draining session status generation" "$draining_status" result.generation "$draining_daemon_id" +repeated_stop_json="$("$beam_script" --root "$tmp1" stop)" +assert_json_field_equals "repeated session stop response" "$repeated_stop_json" ok true +assert_json_field_equals "repeated session stop state" "$repeated_stop_json" result.state stopping +assert_json_field_equals "repeated session stop changed" "$repeated_stop_json" result.changed false draining_lookup_out="$tmp1/draining-lookup.out" draining_lookup_err="$tmp1/draining-lookup.err" -if "$beam_script" --root "$tmp1" ensure > "$draining_lookup_out" 2> "$draining_lookup_err"; then +if "$beam_script" --root "$tmp1" stats > "$draining_lookup_out" 2> "$draining_lookup_err"; then echo "expected an ordinary command not to attach to a draining generation" >&2 cat "$draining_lookup_out" >&2 exit 1 @@ -858,7 +1156,7 @@ if ! grep -Fq "is draining" "$draining_lookup_err"; then fi replacement_owner_out="$tmp1/replacement-during-drain.out" replacement_owner_err="$tmp1/replacement-during-drain.err" -if "$beam_script" --root "$tmp1" ensure --hold \ +if "$beam_script" --root "$tmp1" serve \ > "$replacement_owner_out" 2> "$replacement_owner_err"; then echo "expected a draining generation to fence out a replacement owner" >&2 cat "$replacement_owner_out" >&2 @@ -921,13 +1219,18 @@ fi expect_slow_request_cancelled "$tmp1" "owner-loss-active" "owner-loss-active" owner_loss_out="$tmp1/owner-loss.out" owner_loss_err="$tmp1/owner-loss.err" -if "$beam_script" --root "$tmp1" ensure > "$owner_loss_out" 2> "$owner_loss_err"; then +if "$beam_script" --root "$tmp1" stats > "$owner_loss_out" 2> "$owner_loss_err"; then echo "expected a command after owner loss to preserve the abnormal-session fence" >&2 cat "$owner_loss_out" >&2 exit 1 fi owner_loss_generation="$(read_json_field "$registry" daemonId)" -if ! grep -Fq "recover --generation $owner_loss_generation" "$owner_loss_err"; then +owner_loss_status="$("$beam_script" --root "$tmp1" status)" +assert_json_field_equals \ + "owner-loss session status" "$owner_loss_status" result.state recoveryRequired +assert_json_field_equals \ + "owner-loss session status generation" "$owner_loss_status" result.generation "$owner_loss_generation" +if ! grep -Fq "recover --generation '$owner_loss_generation'" "$owner_loss_err"; then echo "expected owner-loss diagnostics to name exact-generation recovery" >&2 cat "$owner_loss_err" >&2 exit 1 @@ -946,12 +1249,14 @@ if [ ! -e "$registry" ]; then exit 1 fi recover_json="$("$beam_script" --root "$tmp1" recover --generation "$owner_loss_generation")" -assert_json_field_equals "exact-generation recovery" "$recover_json" recovered true +assert_json_field_equals "exact-generation recovery response" "$recover_json" ok true +assert_json_field_equals "exact-generation recovery state" "$recover_json" result.state absent +assert_json_field_equals "exact-generation recovery change" "$recover_json" result.changed true if [ -e "$registry" ]; then echo "expected explicit recovery to quarantine the stale session descriptor" >&2 exit 1 fi -quarantined_registry="$(json_text_field "$recover_json" quarantinedPath)" +quarantined_registry="$(json_text_field "$recover_json" result.quarantinedPath)" if [ ! -f "$quarantined_registry" ]; then echo "expected explicit recovery to preserve quarantined evidence" >&2 printf '%s\n' "$recover_json" >&2 @@ -960,14 +1265,37 @@ fi explicit_control="$tmp2/shared-control" nonprivate_control="$tmp2/nonprivate-control" +explicit_symlink="$tmp2/session-link" +ln -s "$tmp2/.beam" "$explicit_symlink" +if "$beam_script" --root "$tmp2" --session-dir "$explicit_symlink" stats \ + > "$tmp2/symlink-session.out" 2> "$tmp2/symlink-session.err"; then + echo "expected an explicit symbolic-link session directory to be rejected" >&2 + exit 1 +fi +if ! grep -Fq "does not accept a symbolic-link leaf" "$tmp2/symlink-session.err"; then + echo "expected explicit session-directory rejection to name the symbolic-link boundary" >&2 + cat "$tmp2/symlink-session.err" >&2 + exit 1 +fi +rm -f -- "$explicit_symlink" mkdir -p "$nonprivate_control" chmod 755 "$nonprivate_control" nonprivate_mode_before="$(file_mode "$nonprivate_control")" -if "$beam_script" --root "$tmp2" --control-dir "$nonprivate_control" recover --force \ +if "$beam_script" --root "$tmp2" --session-dir "$nonprivate_control" recover --force \ > "$tmp2/nonprivate-control.out" 2> "$tmp2/nonprivate-control.err"; then echo "expected an existing non-private control directory to be rejected" >&2 exit 1 fi +if "$beam_script" --root "$tmp2" --session-dir "$nonprivate_control" stats \ + > "$tmp2/nonprivate-observation.out" 2> "$tmp2/nonprivate-observation.err"; then + echo "expected ordinary attachment to reject a non-private session directory" >&2 + exit 1 +fi +if ! grep -Fq "existing mode is 0755, expected 0700" "$tmp2/nonprivate-observation.err"; then + echo "expected ordinary attachment to apply the session-directory security boundary" >&2 + cat "$tmp2/nonprivate-observation.err" >&2 + exit 1 +fi if ! grep -Fq "existing mode is 0755, expected 0700" "$tmp2/nonprivate-control.err"; then echo "expected non-private control rejection to explain the required mode" >&2 cat "$tmp2/nonprivate-control.err" >&2 @@ -984,7 +1312,7 @@ if find "$nonprivate_control" -mindepth 1 -print -quit | grep -q .; then fi # An absent exact control leaf is safe to create and privatize before descriptor publication. -"$beam_script" --root "$tmp2" --control-dir "$explicit_control" ensure --hold \ +"$beam_script" --root "$tmp2" --session-dir "$explicit_control" serve \ > "$tmp2/explicit-control-owner.out" 2> "$tmp2/explicit-control-owner.err" & hold_pid="$!" explicit_registry="$explicit_control/beam-daemon.json" @@ -992,13 +1320,32 @@ if ! wait_for_nonempty_file "$explicit_registry" "explicit control-directory ses cat "$tmp2/explicit-control-owner.err" >&2 exit 1 fi -explicit_stats="$("$beam_script" --root "$tmp2" --control-dir "$explicit_control" stats)" +explicit_stats="$("$beam_script" --root "$tmp2" --session-dir "$explicit_control" stats)" assert_json_field_equals "explicit control-directory attachment" "$explicit_stats" ok true if [ "$(file_mode "$explicit_control")" != "700" ] || \ [ "$(file_mode "$explicit_registry")" != "600" ]; then echo "expected a newly created explicit control directory and descriptor to use modes 700/600" >&2 exit 1 fi +chmod 755 "$explicit_control" +if "$beam_script" --root "$tmp2" --session-dir "$explicit_control" stats \ + > "$tmp2/changed-mode.out" 2> "$tmp2/changed-mode.err"; then + chmod 700 "$explicit_control" + echo "expected attachment to reject session-directory permission drift" >&2 + exit 1 +fi +chmod 700 "$explicit_control" +if ! grep -Fq "existing mode is 0755, expected 0700" "$tmp2/changed-mode.err"; then + echo "expected permission-drift rejection to explain the session-directory boundary" >&2 + cat "$tmp2/changed-mode.err" >&2 + exit 1 +fi +explicit_stop_command="lean-beam --root '$resolved_tmp2' --session-dir '$(beam_test_realpath "$explicit_control")' stop" +if ! grep -Fq "$explicit_stop_command" "$tmp2/explicit-control-owner.err"; then + echo "expected the foreground owner to print its exact stop command" >&2 + cat "$tmp2/explicit-control-owner.err" >&2 + exit 1 +fi if "$beam_script" --root "$tmp2" stats \ > "$tmp2/default-control-stats.out" 2> "$tmp2/default-control-stats.err"; then echo "expected the default and explicit control selections to remain distinct" >&2 diff --git a/tests/test-beam-wrapper-diagnostics.sh b/tests/test-beam-wrapper-diagnostics.sh index 1903c241..cf961db6 100755 --- a/tests/test-beam-wrapper-diagnostics.sh +++ b/tests/test-beam-wrapper-diagnostics.sh @@ -240,7 +240,7 @@ echo "[beam-wrapper:diagnostics] passed: guard_msgs stderr handling" echo "[beam-wrapper:diagnostics] starting default warning filtering" ( cd "$warn_root" - "$beam_script" ensure lean > /dev/null + "$beam_script" stats > /dev/null cat > SaveSmoke/B.lean <<'EOF' def bVal : Nat := 1 @@ -303,7 +303,7 @@ echo "[beam-wrapper:diagnostics] passed: default warning filtering" echo "[beam-wrapper:diagnostics] starting full warning streaming" ( cd "$warn_full_root" - "$beam_script" ensure lean > /dev/null + "$beam_script" stats > /dev/null cat > SaveSmoke/B.lean <<'EOF' def bVal : Nat := 1 @@ -653,7 +653,7 @@ echo "[beam-wrapper:diagnostics] starting stale-import recovery" ( cd "$stale_root" lake build SaveSmoke/A.lean > /dev/null - "$beam_script" ensure lean > /dev/null + "$beam_script" stats > /dev/null printf 'def bVal : Nat := "broken"\n' > SaveSmoke/B.lean stale_sync_json="$(beam_wrapper_mktemp_file stale-sync-json)" diff --git a/tests/test-beam-wrapper-probe.sh b/tests/test-beam-wrapper-probe.sh index 0c92a461..7373102e 100644 --- a/tests/test-beam-wrapper-probe.sh +++ b/tests/test-beam-wrapper-probe.sh @@ -17,7 +17,7 @@ beam_wrapper_start_owner "$project_root" ( cd "$project_root" - "$beam_script" ensure lean > /dev/null + "$beam_script" stats > /dev/null ) registry_path="$(beam_wrapper_registry_path "$project_root")" @@ -25,7 +25,7 @@ beam_wrapper_expect_file "$registry_path" pid1="$(read_json_field "$registry_path" pid)" port1="$(read_json_field "$registry_path" port)" -root1="$(read_json_field "$registry_path" workspaces.0.root)" +root1="$(read_json_field "$registry_path" workspace.root)" client1="$(read_json_field "$registry_path" clientBin 2>/dev/null || true)" if [ -z "$client1" ]; then client1="$client" @@ -41,7 +41,7 @@ fi ( cd "$project_root" - "$beam_script" ensure lean > /dev/null + "$beam_script" stats > /dev/null command_version="$(beam_wrapper_update_version CommandA "$beam_script" lean-update CommandA.lean)" signature_version="$(beam_wrapper_update_version SignatureHelp "$beam_script" lean-update SignatureHelp.lean)" position_empty_version="$(beam_wrapper_update_version PositionEmptyLine "$beam_script" lean-update PositionEmptyLine.lean)" diff --git a/tests/test-beam-wrapper-rocq.sh b/tests/test-beam-wrapper-rocq.sh index 291185cc..bc0d5628 100755 --- a/tests/test-beam-wrapper-rocq.sh +++ b/tests/test-beam-wrapper-rocq.sh @@ -39,9 +39,9 @@ remove_owned_tmp_tree() { cleanup() { if [ -d "$tmp_repo/tests/rocq/Minimal" ]; then if [ -n "$rocq_cmd" ]; then - BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" shutdown > /dev/null 2>&1 || true + BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" stop > /dev/null 2>&1 || true else - "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" shutdown > /dev/null 2>&1 || true + "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" stop > /dev/null 2>&1 || true fi fi remove_owned_tmp_tree "$tmp_repo" @@ -73,14 +73,14 @@ rsync -a \ fi rocq_owner_err="$tmp_repo/rocq-owner.err" if [ -n "$rocq_cmd" ]; then - BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" ensure rocq --hold \ + BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" serve rocq \ > /dev/null 2>"$rocq_owner_err" & else - "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" ensure rocq --hold \ + "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" serve rocq \ > /dev/null 2>"$rocq_owner_err" & fi rocq_owner_pid="$!" - if ! wait_for_file_text "$rocq_owner_err" "owning Beam session" "Rocq session owner" 600 0.1; then + if ! wait_for_file_text "$rocq_owner_err" "serving Beam session" "Rocq session owner" 600 0.1; then exit 1 fi if [ ! -x ".lake/build/bin/beam-daemon" ] || [ ! -x ".lake/build/bin/beam-client" ]; then @@ -88,27 +88,28 @@ rsync -a \ exit 1 fi if [ -n "$rocq_cmd" ]; then - BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" shutdown > /dev/null + BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" stop > /dev/null else - "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" shutdown > /dev/null + "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" stop > /dev/null fi wait_for_exit "$rocq_owner_pid" "Rocq session owner" 120 0.1 wait "$rocq_owner_pid" rocq_missing_out="$tmp_repo/rocq-missing-owner.out" rocq_missing_err="$tmp_repo/rocq-missing-owner.err" if [ -n "$rocq_cmd" ]; then - if BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" ensure rocq \ + if BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" rocq-goals-after Demo.v 0 0 \ >"$rocq_missing_out" 2>"$rocq_missing_err"; then echo "expected an ordinary Rocq command to require a session owner" >&2 exit 1 fi - elif "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" ensure rocq \ + elif "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" rocq-goals-after Demo.v 0 0 \ >"$rocq_missing_out" 2>"$rocq_missing_err"; then echo "expected an ordinary Rocq command to require a session owner" >&2 exit 1 fi - if ! grep -Fq "lean-beam ensure rocq --hold" "$rocq_missing_err"; then - echo "expected Rocq missing-owner recovery to name the Rocq ownership command" >&2 + if ! grep -Fq -- "--session-dir" "$rocq_missing_err" || \ + ! grep -Fq "serve rocq" "$rocq_missing_err"; then + echo "expected Rocq missing-owner recovery to preserve the exact ownership selector" >&2 cat "$rocq_missing_err" >&2 exit 1 fi diff --git a/tests/test-beam-wrapper-runtime.sh b/tests/test-beam-wrapper-runtime.sh index e523d319..5fb81db8 100644 --- a/tests/test-beam-wrapper-runtime.sh +++ b/tests/test-beam-wrapper-runtime.sh @@ -142,7 +142,7 @@ beam_wrapper_start_owner "$primary_root" primary_owner_pid="$beam_wrapper_last_owner_pid" ( cd "$primary_root" - "$beam_script" ensure lean > /dev/null + "$beam_script" stats > /dev/null ) primary_registry="$(beam_wrapper_registry_path "$primary_root")" @@ -362,7 +362,7 @@ PY fi expect_sigint_cancelled "anonymous non-progress wrapper SIGINT path" "$interrupt_quiet_anon_out" "$interrupt_quiet_anon_err" "" - "$beam_script" --root "$signal_root" shutdown > /dev/null 2>&1 || true + "$beam_script" --root "$signal_root" stop > /dev/null 2>&1 || true ) wait_for_exit "$signal_owner_pid" "first signal-test session owner" 120 0.1 wait "$signal_owner_pid" @@ -456,7 +456,7 @@ signal_owner_pid="$beam_wrapper_last_owner_pid" exit 1 fi - "$beam_script" --root "$signal_root" shutdown > /dev/null 2>&1 || true + "$beam_script" --root "$signal_root" stop > /dev/null 2>&1 || true ) wait_for_exit "$signal_owner_pid" "second signal-test session owner" 120 0.1 wait "$signal_owner_pid" @@ -465,7 +465,7 @@ beam_wrapper_unregister_pid "$signal_owner_pid" beam_wrapper_start_owner "$other_root" ( cd "$other_root" - "$beam_script" ensure lean > /dev/null + "$beam_script" stats > /dev/null ) other_registry="$(beam_wrapper_registry_path "$other_root")" @@ -510,7 +510,7 @@ fi ( cd "$primary_root" - "$beam_script" shutdown > /dev/null + "$beam_script" --root "$primary_root" stop > /dev/null ) wait_for_exit "$primary_owner_pid" "primary session owner" 120 0.1 wait "$primary_owner_pid" diff --git a/tests/test-beam-wrapper-sandbox.sh b/tests/test-beam-wrapper-sandbox.sh index 0a54b4ea..43a7ce43 100755 --- a/tests/test-beam-wrapper-sandbox.sh +++ b/tests/test-beam-wrapper-sandbox.sh @@ -76,7 +76,7 @@ sandbox_beam() { --proc /proc \ --unshare-pid \ --chdir "$project_root" \ - -- /usr/bin/env BEAM_CONTROL_ROOT="$control_root" \ + -- /usr/bin/env BEAM_SESSION_ROOT="$control_root" \ "$beam_script" --root "$project_root" "$@" } @@ -132,8 +132,8 @@ sandbox_owner() { --unshare-pid \ --chdir "$project_root" \ -- /bin/bash -lc \ - "export BEAM_CONTROL_ROOT='$control_root'; \ - '$beam_script' --root '$project_root' ensure --hold >'$out' 2>'$err' & \ + "export BEAM_SESSION_ROOT='$control_root'; \ + '$beam_script' --root '$project_root' serve >'$out' 2>'$err' & \ wrapper_pid=\$!; \ (paused=false; \ while kill -0 \"\$wrapper_pid\" 2>/dev/null; do \ @@ -171,20 +171,22 @@ sandbox_owner() { missing_out="$tmp_root/missing.out" missing_err="$tmp_root/missing.err" -if sandbox_beam ensure >"$missing_out" 2>"$missing_err"; then +if sandbox_beam stats >"$missing_out" 2>"$missing_err"; then echo "expected an ordinary sandbox command not to start an implicit daemon" >&2 sed -n '1,160p' "$missing_out" >&2 exit 1 fi -if ! grep -Fq "start 'lean-beam ensure --hold'" "$missing_err"; then - echo "expected the missing-owner error to provide the ownership command" >&2 +if ! grep -Fq "lean-beam --root '$project_root'" "$missing_err" || \ + ! grep -Fq -- "--session-dir '$control_root/" "$missing_err" || \ + ! grep -Fq " serve" "$missing_err"; then + echo "expected the missing-owner error to preserve the exact sandbox session selector" >&2 sed -n '1,160p' "$missing_err" >&2 exit 1 fi sandbox_owner owner-1 if ! wait_for_registry || ! wait_for_nonempty_file "$owner_out" "sandbox owner response"; then - echo "expected ensure --hold to publish an owned daemon" >&2 + echo "expected serve to publish an owned daemon" >&2 sed -n '1,200p' "$owner_err" >&2 exit 1 fi @@ -199,10 +201,10 @@ if ! printf '%s\n' "$doctor_out" | grep -q 'daemon status: live'; then exit 1 fi -ensure_json="$(sandbox_beam ensure)" -if [ "$(json_text_field "$ensure_json" ok)" != "true" ]; then +stats_json="$(sandbox_beam stats)" +if [ "$(json_text_field "$stats_json" ok)" != "true" ]; then echo "expected a separate PID namespace to attach to the owner session" >&2 - printf '%s\n' "$ensure_json" >&2 + printf '%s\n' "$stats_json" >&2 exit 1 fi if [ "$(read_json_field "$registry" daemonId)" != "$daemon_id_1" ] || \ @@ -213,7 +215,7 @@ fi duplicate_out="$tmp_root/duplicate.out" duplicate_err="$tmp_root/duplicate.err" -if sandbox_beam ensure --hold >"$duplicate_out" 2>"$duplicate_err"; then +if sandbox_beam serve >"$duplicate_out" 2>"$duplicate_err"; then echo "expected a second sandbox owner to be rejected" >&2 exit 1 fi @@ -240,10 +242,10 @@ fi assert_no_lease_artifacts touch "$owner_resume" -shutdown_json="$(sandbox_beam shutdown)" -if [ "$(json_text_field "$shutdown_json" result.shutdown)" != "true" ]; then - echo "expected explicit shutdown to close the owned sandbox session" >&2 - printf '%s\n' "$shutdown_json" >&2 +stop_json="$(sandbox_beam stop)" +if [ "$(json_text_field "$stop_json" result.state)" != "stopping" ]; then + echo "expected explicit stop to close the owned sandbox session" >&2 + printf '%s\n' "$stop_json" >&2 exit 1 fi if ! wait_for_exit "$owner_pid" "sandbox owner after shutdown" 120 0.1; then @@ -294,7 +296,7 @@ sleep 4 after_kill_out="$tmp_root/after-kill.out" after_kill_err="$tmp_root/after-kill.err" -if sandbox_beam ensure >"$after_kill_out" 2>"$after_kill_err"; then +if sandbox_beam stats >"$after_kill_out" 2>"$after_kill_err"; then echo "expected an ordinary command not to replace a dead owner implicitly" >&2 sed -n '1,160p' "$after_kill_out" >&2 exit 1 @@ -312,7 +314,9 @@ fi # This test harness supervised the complete bwrap owner namespace and observed its exit, so it can # now authorize exact-generation recovery that an ordinary client must refuse to infer. recovery_json="$(sandbox_beam recover --generation "$daemon_id_2")" -if [ "$(json_text_field "$recovery_json" recovered)" != "true" ]; then +if [ "$(json_text_field "$recovery_json" ok)" != "true" ] || \ + [ "$(json_text_field "$recovery_json" result.changed)" != "true" ] || \ + [ "$(json_text_field "$recovery_json" result.state)" != "absent" ]; then echo "expected exact-generation sandbox recovery to quarantine the descriptor" >&2 printf '%s\n' "$recovery_json" >&2 exit 1 @@ -321,7 +325,7 @@ if [ -e "$registry" ]; then echo "expected exact-generation recovery to remove the authoritative fence" >&2 exit 1 fi -recovery_path="$(json_text_field "$recovery_json" quarantinedPath)" +recovery_path="$(json_text_field "$recovery_json" result.quarantinedPath)" if [ ! -f "$recovery_path" ]; then echo "expected sandbox recovery to preserve quarantined evidence" >&2 printf '%s\n' "$recovery_json" >&2 diff --git a/tests/test-beam-wrapper-sync-save.sh b/tests/test-beam-wrapper-sync-save.sh index 98cef6f6..a656042b 100755 --- a/tests/test-beam-wrapper-sync-save.sh +++ b/tests/test-beam-wrapper-sync-save.sh @@ -19,11 +19,11 @@ beam_wrapper_start_owner "$standalone_root" ( cd "$lifecycle_root" - "$beam_script" ensure lean > /dev/null + "$beam_script" stats > /dev/null stats_out="$("$beam_script" stats)" if [ "$(BEAM_JSON_PAYLOAD="$stats_out" read_json_text_field result.sessions.lean.openDocCount)" != "0" ]; then - echo "expected ensure lean to start with zero open Beam daemon documents" >&2 + echo "expected a newly served Lean session to start with zero open documents" >&2 printf '%s\n' "$stats_out" >&2 exit 1 fi @@ -256,7 +256,7 @@ beam_wrapper_start_owner "$standalone_root" ( cd "$standalone_root" - "$beam_script" ensure lean > /dev/null + "$beam_script" stats > /dev/null cat > StandaloneSaveSmoke.lean <<'EOF' import SaveSmoke.B diff --git a/tests/test-stage0-toolchain.sh b/tests/test-stage0-toolchain.sh index b7f7a5e6..de39dc62 100755 --- a/tests/test-stage0-toolchain.sh +++ b/tests/test-stage0-toolchain.sh @@ -67,13 +67,13 @@ assert_output_contains "stage0 custom toolchain doctor output" "$doctor_out" 'bu stage0_owner_err="$tmp_root/stage0-owner.err" ELAN_HOME="$host_elan_home" \ - "$install_home/.local/bin/lean-beam" --root "$project_root" ensure --hold \ + "$install_home/.local/bin/lean-beam" --root "$project_root" serve \ >/dev/null 2>"$stage0_owner_err" & stage0_owner_pid="$!" -if ! wait_for_file_text "$stage0_owner_err" "owning Beam session" "stage0 session owner" 600 0.1; then +if ! wait_for_file_text "$stage0_owner_err" "serving Beam session" "stage0 session owner" 600 0.1; then exit 1 fi ELAN_HOME="$host_elan_home" \ - "$install_home/.local/bin/lean-beam" --root "$project_root" shutdown >/dev/null + "$install_home/.local/bin/lean-beam" --root "$project_root" stop >/dev/null wait_for_exit "$stage0_owner_pid" "stage0 session owner" 120 0.1 wait "$stage0_owner_pid"