fix: isolate broker requests across workspace resets

Beam/Broker/Backend/Lean.lean

@@ -21,18 +21,13 @@ open Lean.Lsp
 
 namespace Beam.Broker.Backend.Lean
 
-private def pluginPath (config : BrokerConfig) : IO System.FilePath := do
-  match config.leanPlugin? with
-  | some path => Beam.resolveExistingPath path
-  | none => throw <| IO.userError "missing Beam daemon --lean-plugin configuration"
-
 def command (config : BrokerConfig) : IO (String × Array String × Array (String × Option String)) := do
-  let some cmd := config.leanCmd?
-    | throw <| IO.userError "missing Beam daemon --lean-cmd configuration"
-  let plugin := ← pluginPath config
-  let lakeEnv ← leanServerLakeEnv config.root config.leanCmd? config.leanLakeHelper?
+  let some leanConfig := config.lean?
+    | throw <| IO.userError "Lean backend is not configured"
+  let plugin ← Beam.resolveExistingPath leanConfig.plugin
+  let lakeEnv ← leanServerLakeEnv config.root (some leanConfig.command) leanConfig.lakeHelper?
   pure (
-    cmd,
+    leanConfig.command,
     #["--server"] ++ lakeEnv.moreServerArgs ++
       #[s!"--plugin={plugin}", "-Dexperimental.module=true"],
     lakeEnv.env)

Beam/Broker/Backend/Rocq.lean

@@ -15,13 +15,10 @@ open Lean.Lsp
 
 namespace Beam.Broker.Backend.Rocq
 
-private def lspPath (config : BrokerConfig) : IO String := do
-  match config.rocqCmd? with
-  | some path => pure path
-  | none => throw <| IO.userError "missing Beam daemon --rocq-cmd configuration"
-
 def command (config : BrokerConfig) : IO (String × Array String) := do
-  pure ((← lspPath config), #[])
+  let some rocqConfig := config.rocq?
+    | throw <| IO.userError "Rocq backend is not configured"
+  pure (rocqConfig.command, #[])
 
 def initializeParams (root : System.FilePath) : Json :=
   let rootUri := System.Uri.pathToUri root

Beam/Broker/Config.lean

@@ -8,12 +8,49 @@ import Lean
 
 namespace Beam.Broker
 
+/-- Complete process configuration for one Lean backend. -/
+structure LeanBackendConfig where
+  command : String
+  plugin : System.FilePath
+  lakeHelper? : Option System.FilePath := none
+  deriving BEq, Inhabited, Repr
+
+/-- Complete process configuration for one Rocq backend. -/
+structure RocqBackendConfig where
+  command : String
+  deriving BEq, Inhabited, Repr
+
+/--
+Runtime configuration for one broker workspace.
+
+The optional backends permit an intentionally backend-less standalone bootstrap workspace. Once a
+backend is present, its required process configuration is complete by construction.
+-/
 structure BrokerConfig where
   root : System.FilePath
-  leanCmd? : Option String := none
-  leanPlugin? : Option System.FilePath := none
-  leanLakeHelper? : Option System.FilePath := none
-  rocqCmd? : Option String := none
-  deriving Inhabited, Repr
+  lean? : Option LeanBackendConfig := none
+  rocq? : Option RocqBackendConfig := none
+  deriving BEq, Inhabited, Repr
+
+namespace BrokerConfig
+
+/-- Assemble the typed runtime model from optional fields at a process boundary. -/
+def ofOptions
+    (root : System.FilePath)
+    (leanCommand? : Option String)
+    (leanPlugin? : Option System.FilePath)
+    (rocqCommand? : Option String := none) : Except String BrokerConfig := do
+  let lean? ←
+    match leanCommand?, leanPlugin? with
+    | none, none => pure none
+    | some command, some plugin => pure <| some { command, plugin }
+    | _, _ => throw "Lean backend configuration requires a command and plugin together"
+  pure {
+    root
+    lean?
+    rocq? := rocqCommand?.map fun command => { command }
+  }
+
+end BrokerConfig
 
 end Beam.Broker

Beam/Broker/Protocol.lean

@@ -300,11 +300,14 @@ structure ReleaseRequest where
   path : String
   handle : Handle
 
+structure InitLeanBackendConfig where
+  command : String
+  plugin : String
+
 structure InitWorkspaceRequest where
   workspaceMode? : Option Beam.Workspace.InitMode := none
   root : String
-  leanCmd? : Option String := none
-  leanPlugin? : Option String := none
+  lean? : Option InitLeanBackendConfig := none
   rocqCmd? : Option String := none
 
 /-- The fields owned by exactly one broker operation. -/
@@ -535,8 +538,12 @@ private def RequestPayload.jsonFields : RequestPayload → List (String × Json)
   | .initWorkspace request =>
       optionalJsonField "workspaceMode" request.workspaceMode? ++
       [("root", toJson request.root)] ++
-      optionalJsonField "leanCmd" request.leanCmd? ++
-      optionalJsonField "leanPlugin" request.leanPlugin? ++
+      (match request.lean? with
+      | some lean => [
+          ("leanCmd", toJson lean.command),
+          ("leanPlugin", toJson lean.plugin)
+        ]
+      | none => []) ++
       optionalJsonField "rocqCmd" request.rocqCmd?
   | .stats | .listWorkspaces | .dropWorkspace | .shutdown => []
 
@@ -739,11 +746,18 @@ instance : FromJson Request where
             handle
           }
       | .initWorkspace =>
+          let leanCmd? ← optionalField? (α := String) j "leanCmd"
+          let leanPlugin? ← optionalField? (α := String) j "leanPlugin"
+          let lean? ←
+            match leanCmd?, leanPlugin? with
+            | none, none => pure none
+            | some command, some plugin => pure <| some { command, plugin }
+            | some _, none => throw "'leanCmd' requires 'leanPlugin'"
+            | none, some _ => throw "'leanPlugin' requires 'leanCmd'"
           pure <| .initWorkspace {
             workspaceMode? := ← optionalField? (α := Beam.Workspace.InitMode) j "workspaceMode"
             root := ← requiredField j "root"
-            leanCmd? := ← optionalField? (α := String) j "leanCmd"
-            leanPlugin? := ← optionalField? (α := String) j "leanPlugin"
+            lean?
             rocqCmd? := ← optionalField? (α := String) j "rocqCmd"
           }
       | .listWorkspaces => pure .listWorkspaces