fix: run Lake operations in target process

Beam/Broker/Backend/Lean.lean

@@ -30,7 +30,7 @@ def command (config : BrokerConfig) : IO (String × Array String × Array (Strin
   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?
+  let lakeEnv ← leanServerLakeEnv config.root config.leanCmd? config.leanLakeHelper?
   pure (
     cmd,
     #["--server"] ++ lakeEnv.moreServerArgs ++

Beam/Broker/Config.lean

@@ -12,6 +12,7 @@ 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
 

Beam/Broker/LakeEnv.lean

@@ -8,9 +8,11 @@ import Lake.Config.Env
 import Lake.Config.InstallPath
 import Lake.CLI.Serve
 import Lake.Load.Workspace
+import Beam.Broker.LakeHelper
 
 open System
 open Std
+open Lean
 
 namespace Beam.Broker
 
@@ -41,6 +43,10 @@ private def computeLakeEnv (leanCmd? : Option String) : IO Lake.Env := do
   | .ok env => pure env
   | .error err => throw <| IO.userError s!"failed to compute Lake environment: {err}"
 
+/-- A `Workspace` contains live Lean values, so only load it across an exact Lean ABI match. -/
+private def canLoadWorkspaceInProcess (lakeEnv : Lake.Env) : Bool :=
+  !lakeEnv.lean.githash.isEmpty && lakeEnv.lean.githash == Lean.githash
+
 private def detectConfigFile? (root : FilePath) : IO (Option (FilePath × FilePath)) := do
   let leanConfig := root / "lakefile.lean"
   if ← leanConfig.pathExists then
@@ -74,31 +80,46 @@ private def loadWorkspaceWithConfig (root : FilePath) (lakeEnv : Lake.Env)
 
 private def loadWorkspaceFailureMessage
     (root : FilePath)
-    (messages : Array String)
-    (extra : Array String := #[]) : String :=
+    (messages : Array String) : String :=
   let lines :=
     #[s!"failed to load Lake workspace at {root}"] ++
-    (if messages.isEmpty then #[] else #["Lake log:"] ++ messages) ++
-    extra
+    (if messages.isEmpty then #[] else #["Lake log:"] ++ messages)
   String.intercalate "\n" lines.toList
 
-def loadWorkspaceForRoot (root : FilePath) (leanCmd? : Option String) : IO Workspace := do
+inductive WorkspaceLoadResult where
+  | loaded (workspace : Workspace)
+  | leanBuildMismatch
+
+def loadWorkspaceForRoot (root : FilePath) (leanCmd? : Option String) : IO WorkspaceLoadResult := do
   let (relConfigFile, configFile) ← detectConfigFile root
   let lakeEnv ← computeLakeEnv leanCmd?
+  unless canLoadWorkspaceInProcess lakeEnv do
+    return .leanBuildMismatch
   let (ws?, messages) ← loadWorkspaceWithConfig root lakeEnv relConfigFile configFile
   if let some ws := ws? then
-    pure ws
+    pure <| .loaded ws
   else
     throw <| IO.userError <| loadWorkspaceFailureMessage root messages
 
 structure LeanServerLakeEnv where
-  env : Array (String × Option String) := #[]
-  moreServerArgs : Array String := #[]
+  env : Array (String × Option String)
+  moreServerArgs : Array String
+  deriving FromJson, ToJson
 
-def leanServerLakeEnv (root : FilePath) (leanCmd? : Option String) : IO LeanServerLakeEnv := do
-  let some (relConfigFile, configFile) ← detectConfigFile? root
-    | pure {}
+private def leanServerLakeEnvInProcess
+    (root : FilePath)
+    (leanCmd? : Option String) : IO LeanServerLakeEnv := do
   let lakeEnv ← computeLakeEnv leanCmd?
+  -- Always preserve the target runtime environment: the Beam plugin links against target Lean/Lake
+  -- libraries even when there is no Lake configuration or this Lake version cannot load it.
+  let fallback : LeanServerLakeEnv := {
+    env := lakeEnv.vars
+    moreServerArgs := #[]
+  }
+  if !canLoadWorkspaceInProcess lakeEnv then
+    return fallback
+  let some (relConfigFile, configFile) ← detectConfigFile? root
+    | pure fallback
   let (ws?, messages) ← loadWorkspaceWithConfig root lakeEnv relConfigFile configFile
   if let some ws := ws? then
     pure {
@@ -107,8 +128,28 @@ def leanServerLakeEnv (root : FilePath) (leanCmd? : Option String) : IO LeanServ
     }
   else
     pure {
-      env := lakeEnv.baseVars.push (Lake.invalidConfigEnvVar, some <| String.intercalate "\n" messages.toList)
+      env := lakeEnv.vars.push
+        (Lake.invalidConfigEnvVar, some <| String.intercalate "\n" messages.toList)
       moreServerArgs := #[]
     }
 
+def leanServerLakeEnv
+    (root : FilePath)
+    (leanCmd? : Option String)
+    (lakeHelper? : Option FilePath := none) : IO LeanServerLakeEnv := do
+  match lakeHelper?, leanCmd? with
+  | some helper, some leanCmd =>
+      match ← runLakeHelper helper "server-env" <| toJson ({
+          root := root.toString
+          leanCmd
+        } : LakeHelperEnvRequest) with
+      | .ok result =>
+          match fromJson? result with
+          | .ok serverEnv => pure serverEnv
+          | .error err =>
+              throw <| IO.userError s!"target Lake helper returned an invalid server environment: {err}"
+      | .error failure => throw <| IO.userError failure.message
+  | _, _ =>
+      leanServerLakeEnvInProcess root leanCmd?
+
 end Beam.Broker

Beam/Broker/LakeHelper.lean

@@ -0,0 +1,100 @@
+/-
+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 Beam.Broker.Errors
+
+open Lean
+
+namespace Beam.Broker
+
+structure LakeHelperEnvRequest where
+  root : String
+  leanCmd : String
+  deriving FromJson, ToJson
+
+structure LakeHelperSaveRequest where
+  root : String
+  path : String
+  leanCmd : String
+  sourceHash : String
+  sourceMTimeSec : Int
+  sourceMTimeNsec : Nat
+  deriving FromJson, ToJson
+
+structure LakeHelperWriteTraceRequest where
+  oleanPath : String
+  oleanServerPath? : Option String := none
+  oleanPrivatePath? : Option String := none
+  ileanPath : String
+  irPath? : Option String := none
+  cPath : String
+  bcPath? : Option String := none
+  tracePath : String
+  traceMetadata : Json
+  deriving FromJson, ToJson
+
+structure LakeHelperSaveSpec extends LakeHelperWriteTraceRequest where
+  relPath : String
+  moduleName : String
+  unsupportedSetupReason? : Option String := none
+  deriving FromJson, ToJson
+
+def BrokerFailureCode.ofName? (name : String) : Option BrokerFailureCode :=
+  if name == "invalidParams" then some .invalidParams
+  else if name == "requestCancelled" then some .requestCancelled
+  else if name == "contentModified" then some .contentModified
+  else if name == "workerExited" then some .workerExited
+  else if name == syncBarrierIncompleteCode then some .syncBarrierIncomplete
+  else if name == saveTraceStaleCode then some .saveTraceStale
+  else if name == saveUnsupportedSetupCode then some .saveUnsupportedSetup
+  else if name == saveTargetNotModuleCode then some .saveTargetNotModule
+  else if name == "internalError" then some .internalError
+  else none
+
+private def helperOutputSummary (stdout stderr : String) : String :=
+  let stderr := stderr.trimAscii.toString
+  let stdout := stdout.trimAscii.toString
+  if !stderr.isEmpty then stderr else if !stdout.isEmpty then stdout else "(no output)"
+
+/-- Invoke a target-built helper without a shell and keep its structured failures typed. -/
+def runLakeHelper
+    (helper : System.FilePath)
+    (operation : String)
+    (request : Json) : IO (Except BrokerFailure Json) := do
+  let out ← IO.Process.output {
+    cmd := helper.toString
+    args := #["lake-helper", operation]
+  } (some request.compress)
+  if out.exitCode != 0 then
+    return .error {
+      code := .internalError
+      message :=
+        s!"target Lake helper '{operation}' exited with code {out.exitCode}: " ++
+          helperOutputSummary out.stdout out.stderr
+    }
+  let response ←
+    match Json.parse out.stdout >>= fromJson? (α := Response) with
+    | .ok response => pure response
+    | .error err =>
+        return .error {
+          code := .internalError
+          message :=
+            s!"target Lake helper '{operation}' returned invalid JSON: {err}: " ++
+              helperOutputSummary out.stdout out.stderr
+        }
+  match response with
+  | .successResult result _ => pure <| .ok result
+  | .errorResult failure =>
+      let error := failure.error
+      let some code := BrokerFailureCode.ofName? error.code
+        | return .error {
+            code := .internalError
+            message := s!"target Lake helper '{operation}' returned unknown error code '{error.code}'"
+          }
+      pure <| .error { code, message := error.message, data? := error.data? }
+
+end Beam.Broker

Beam/Broker/LakeHelperMain.lean

@@ -0,0 +1,52 @@
+/-
+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 Beam.Broker.LakeEnv
+import Beam.Broker.LakeSave
+
+open Lean
+
+namespace Beam.Broker.LakeHelperMain
+
+private def readRequest [FromJson α] : IO α := do
+  let input ← (← IO.getStdin).readToEnd
+  let json ← IO.ofExcept <| Json.parse input
+  IO.ofExcept <| fromJson? json
+
+private def writeResponse (response : Response) : IO Unit := do
+  IO.println (toJson response).compress
+
+private def runServerEnv : IO Unit := do
+  let request : LakeHelperEnvRequest ← readRequest
+  let serverEnv ← leanServerLakeEnv
+    (System.FilePath.mk request.root) (some request.leanCmd)
+  writeResponse <| Response.success (toJson serverEnv)
+
+private def runPrepareSave : IO Unit := do
+  let request : LakeHelperSaveRequest ← readRequest
+  match ← lakeHelperSaveSpec request with
+  | .ok spec => writeResponse <| Response.success (toJson spec)
+  | .error failure => writeResponse failure.toResponse
+
+private def runWriteSaveTrace : IO Unit := do
+  let request : LakeHelperWriteTraceRequest ← readRequest
+  lakeHelperWriteLeanSaveTrace request
+  writeResponse <| Response.success (Json.mkObj [])
+
+def main (args : List String) : IO Unit := do
+  try
+    match args with
+    | ["server-env"] => runServerEnv
+    | ["prepare-save"] => runPrepareSave
+    | ["write-save-trace"] => runWriteSaveTrace
+    | _ => throw <| IO.userError "invalid target Lake helper operation"
+  catch error =>
+    writeResponse <| BrokerFailure.toResponse {
+      code := .internalError
+      message := error.toString
+    }
+
+end Beam.Broker.LakeHelperMain