refactor: isolate deps and save support internals (#11)

* refactor: isolate deps and save support internals

* test: ignore zombie workers in broker fast tests

Author: ejgallego

Beam.lean

@@ -10,6 +10,7 @@ import Beam.Broker.Deps
 import Beam.Broker.LakeSave
 import Beam.Broker.Lean
 import Beam.Broker.Protocol
+import Beam.Broker.StaleDirectDeps
 import Beam.Broker.SyncSaveSupport
 import Beam.Broker.Transport
 import Beam.Broker.UnixNative

Beam/Broker/Backend/Lean.lean

@@ -8,7 +8,8 @@ import Lean
 import Lean.Data.Lsp.Extra
 import Lean.Data.Lsp.LanguageFeatures
 import RunAt.Protocol
-import RunAt.Internal.SaveArtifacts
+import RunAt.Internal.DirectImports
+import RunAt.Internal.SaveSupport
 import Beam.Broker.Config
 import Beam.Broker.Protocol
 

Beam/Broker/Deps.lean

@@ -58,25 +58,6 @@ def normalizeModuleForPath (root path : System.FilePath) (uri : DocumentUri) (mo
       | some name => some { name, uri }
       | none => none
 
-structure DirectImportsQueryResult where
-  version : Nat
-  imports : Array String := #[]
-  deriving Inhabited
-
-structure ModuleHistorySnapshot where
-  path : String
-  lastSyncSeq : Nat := 0
-  lastSaveSeq : Nat := 0
-  deriving Inhabited
-
-structure StaleDirectDepHint where
-  module : String
-  path : String
-  needsSave : Bool
-  lastSyncSeq : Nat
-  lastSaveSeq : Nat
-  deriving Inhabited
-
 def moduleJson (root : System.FilePath) (module : LeanModule) : Json :=
   let path? := workspacePath? root module.uri
   Json.mkObj <|
@@ -106,54 +87,6 @@ def depsPayload (root : System.FilePath) (module : LeanModule)
     ("importedByClosure", Json.arr <| importedByClosure.toList.map (fun (_, imp) => importJson root imp) |>.toArray)
   ]
 
-def staleDirectDepHintJson (hint : StaleDirectDepHint) : Json :=
-  Json.mkObj [
-    ("module", toJson hint.module),
-    ("path", toJson hint.path),
-    ("needsSave", toJson hint.needsSave),
-    ("lastSyncSeq", toJson hint.lastSyncSeq),
-    ("lastSaveSeq", toJson hint.lastSaveSeq)
-  ]
-
-def staleSyncErrorData
-    (targetPath : String)
-    (hints : Array StaleDirectDepHint) : Json :=
-  let saveHints := hints.filter (·.needsSave)
-  let recoveryPlan :=
-    (saveHints.map fun hint => s!"lean-beam save \"{hint.path}\"") ++
-    #[s!"lean-beam refresh \"{targetPath}\"", "lake build"]
-  Json.mkObj [
-    ("targetPath", toJson targetPath),
-    ("staleDirectDeps", Json.arr <| hints.map staleDirectDepHintJson),
-    ("saveDeps", Json.arr <| saveHints.map (fun hint => toJson hint.path)),
-    ("recoveryPlan", Json.arr <| recoveryPlan.map toJson)
-  ]
-
-def collectStaleDirectDepHints
-    (importsResult : DirectImportsQueryResult)
-    (version : Nat)
-    (targetLastSyncSeq : Nat)
-    (history : Std.TreeMap String ModuleHistorySnapshot)
-    : Array StaleDirectDepHint :=
-  if importsResult.version != version then
-    #[]
-  else
-    importsResult.imports.foldl (init := #[]) fun hints moduleName =>
-      match history.get? moduleName with
-      | some moduleHistory =>
-          if moduleHistory.lastSaveSeq > targetLastSyncSeq then
-            hints.push {
-              module := moduleName
-              path := moduleHistory.path
-              needsSave := moduleHistory.lastSaveSeq < moduleHistory.lastSyncSeq
-              lastSyncSeq := moduleHistory.lastSyncSeq
-              lastSaveSeq := moduleHistory.lastSaveSeq
-            }
-          else
-            hints
-      | none =>
-          hints
-
 def importInfoToWorkspaceImport?
     (moduleIndex : Std.TreeMap String System.FilePath)
     (info : ImportInfo) : Option LeanImport := do

Beam/Broker/Server.lean

@@ -11,13 +11,15 @@ import Lean.Data.Lsp.LanguageFeatures
 import Lean.Data.Lsp.Internal
 import Lean.Parser.Module
 import RunAt.Protocol
-import RunAt.Internal.SaveArtifacts
+import RunAt.Internal.DirectImports
+import RunAt.Internal.SaveSupport
 import Beam.Broker.Config
 import Beam.Broker.Protocol
 import Beam.Broker.Transport
 import Beam.Broker.Lean
 import Beam.Broker.Deps
 import Beam.Broker.LakeSave
+import Beam.Broker.StaleDirectDeps
 import Beam.Broker.SyncSaveSupport
 import Std.Sync.Mutex
 

Beam/Broker/StaleDirectDeps.lean

@@ -0,0 +1,88 @@
+ /-
+ Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+ Released under Apache 2.0 license as described in the file LICENSE.
+ Author: Emilio J. Gallego Arias
+ -/
+
+ import Lean
+
+ open Lean
+
+ namespace Beam.Broker
+
+ /--
+ Data used by the supported sync/readiness path to explain stale direct dependencies after a failed
+ diagnostics barrier.
+
+ This is intentionally separate from the stopgap `lean-deps` workspace scanner so the real sync
+ recovery path does not conceptually depend on the experimental dependency-inspection surface.
+ -/
+
+ structure DirectImportsQueryResult where
+   version : Nat
+   imports : Array String := #[]
+   deriving Inhabited
+
+ structure ModuleHistorySnapshot where
+   path : String
+   lastSyncSeq : Nat := 0
+   lastSaveSeq : Nat := 0
+   deriving Inhabited
+
+ structure StaleDirectDepHint where
+   module : String
+   path : String
+   needsSave : Bool
+   lastSyncSeq : Nat
+   lastSaveSeq : Nat
+   deriving Inhabited
+
+ def staleDirectDepHintJson (hint : StaleDirectDepHint) : Json :=
+   Json.mkObj [
+     ("module", toJson hint.module),
+     ("path", toJson hint.path),
+     ("needsSave", toJson hint.needsSave),
+     ("lastSyncSeq", toJson hint.lastSyncSeq),
+     ("lastSaveSeq", toJson hint.lastSaveSeq)
+   ]
+
+ def staleSyncErrorData
+     (targetPath : String)
+     (hints : Array StaleDirectDepHint) : Json :=
+   let saveHints := hints.filter (·.needsSave)
+   let recoveryPlan :=
+     (saveHints.map fun hint => s!"lean-beam save \"{hint.path}\"") ++
+     #[s!"lean-beam refresh \"{targetPath}\"", "lake build"]
+   Json.mkObj [
+     ("targetPath", toJson targetPath),
+     ("staleDirectDeps", Json.arr <| hints.map staleDirectDepHintJson),
+     ("saveDeps", Json.arr <| saveHints.map (fun hint => toJson hint.path)),
+     ("recoveryPlan", Json.arr <| recoveryPlan.map toJson)
+   ]
+
+ def collectStaleDirectDepHints
+     (importsResult : DirectImportsQueryResult)
+     (version : Nat)
+     (targetLastSyncSeq : Nat)
+     (history : Std.TreeMap String ModuleHistorySnapshot)
+     : Array StaleDirectDepHint :=
+   if importsResult.version != version then
+     #[]
+   else
+     importsResult.imports.foldl (init := #[]) fun hints moduleName =>
+       match history.get? moduleName with
+       | some moduleHistory =>
+           if moduleHistory.lastSaveSeq > targetLastSyncSeq then
+             hints.push {
+               module := moduleName
+               path := moduleHistory.path
+               needsSave := moduleHistory.lastSaveSeq < moduleHistory.lastSyncSeq
+               lastSyncSeq := moduleHistory.lastSyncSeq
+               lastSaveSeq := moduleHistory.lastSaveSeq
+             }
+           else
+             hints
+       | none =>
+           hints
+
+ end Beam.Broker

Beam/Broker/SyncSaveSupport.lean

@@ -5,7 +5,7 @@ Author: Emilio J. Gallego Arias
 -/
 
 import Lean
-import RunAt.Internal.SaveArtifacts
+import RunAt.Internal.SaveSupport
 import Beam.Broker.LakeSave
 import Beam.Broker.Protocol
 

RunAt/Internal/DirectImports.lean

@@ -0,0 +1,36 @@
+ /-
+ Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+ Released under Apache 2.0 license as described in the file LICENSE.
+ Author: Emilio J. Gallego Arias
+ -/
+
+ import Lean
+
+ open Lean
+
+ namespace RunAt.Internal
+
+ /--
+ Internal broker-only request for parsing the current document header and returning its direct imports
+ from the current tracked text snapshot.
+
+ This supports broker-side stale dependency hints and compatibility-only tooling. It is not part of
+ the supported public `runAt` API.
+ -/
+ def directImportsMethod : String := "$/lean/runAt/directImports"
+
+ /-- Internal request payload for direct-import queries from the current tracked text snapshot. -/
+ structure DirectImportsParams where
+   textDocument : Lean.Lsp.TextDocumentIdentifier
+   deriving FromJson, ToJson
+
+ instance : Lean.Lsp.FileSource DirectImportsParams where
+   fileSource p := p.textDocument.uri
+
+ /-- Internal success payload for direct-import queries from the current tracked text snapshot. -/
+ structure DirectImportsResult where
+   version : Nat
+   imports : Array String := #[]
+   deriving FromJson, ToJson
+
+ end RunAt.Internal

RunAt/Internal/SaveArtifacts.lean

@@ -1,87 +1,17 @@
-/-
-Copyright (c) 2026 Lean FRO LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Emilio J. Gallego Arias
--/
+ /-
+ Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+ Released under Apache 2.0 license as described in the file LICENSE.
+ Author: Emilio J. Gallego Arias
+ -/
 
-import Lean
+ import RunAt.Internal.DirectImports
+ import RunAt.Internal.SaveSupport
 
-open Lean
+ /--
+ Compatibility import for broker-only save support internals.
 
-namespace RunAt.Internal
+ The actual definitions now live in:
 
-/--
-Internal broker-only request for saving the current elaborated document state to
-the Lake artifact locations expected by the workspace.
-
-This is not part of the public `runAt` API.
--/
-def saveArtifactsMethod : String := "$/lean/runAt/saveArtifacts"
-
-/--
-Internal broker-only request for checking whether the current elaborated document
-state is ready for artifact save.
-
-This is not part of the public `runAt` API.
--/
-def saveReadinessMethod : String := "$/lean/runAt/saveReadiness"
-
-/--
-Internal broker-only request for parsing the current document header and
-returning its direct imports from the current tracked text snapshot.
-
-This is not part of the public `runAt` API.
--/
-def directImportsMethod : String := "$/lean/runAt/directImports"
-
-/-- Internal request payload for artifact serialization from the current worker snapshot. -/
-structure SaveArtifactsParams where
-  textDocument : Lean.Lsp.TextDocumentIdentifier
-  oleanFile : String
-  ileanFile : String
-  cFile : String
-  bcFile? : Option String := none
-  deriving FromJson, ToJson
-
-instance : Lean.Lsp.FileSource SaveArtifactsParams where
-  fileSource p := p.textDocument.uri
-
-/-- Internal request payload for save-readiness checks from the current worker snapshot. -/
-structure SaveReadinessParams where
-  textDocument : Lean.Lsp.TextDocumentIdentifier
-  deriving FromJson, ToJson
-
-instance : Lean.Lsp.FileSource SaveReadinessParams where
-  fileSource p := p.textDocument.uri
-
-/-- Internal request payload for direct-import queries from the current tracked text snapshot. -/
-structure DirectImportsParams where
-  textDocument : Lean.Lsp.TextDocumentIdentifier
-  deriving FromJson, ToJson
-
-instance : Lean.Lsp.FileSource DirectImportsParams where
-  fileSource p := p.textDocument.uri
-
-/-- Internal success payload for artifact serialization. -/
-structure SaveArtifactsResult where
-  written : Bool := true
-  version : Nat
-  textHash : UInt64
-  deriving FromJson, ToJson
-
-/-- Internal success payload for save-readiness checks. -/
-structure SaveReadinessResult where
-  version : Nat
-  diagnosticErrorCount : Nat := 0
-  commandErrorCount : Nat := 0
-  saveReady : Bool := true
-  saveReadyReason : String := "ok"
-  deriving FromJson, ToJson
-
-/-- Internal success payload for direct-import queries from the current tracked text snapshot. -/
-structure DirectImportsResult where
-  version : Nat
-  imports : Array String := #[]
-  deriving FromJson, ToJson
-
-end RunAt.Internal
+ - `RunAt.Internal.SaveSupport` for the supported save-after-sync broker path
+ - `RunAt.Internal.DirectImports` for the unsupported direct-import query path
+ -/