feat: prune obsolete installed Beam state

Beam/Cli/Broker.lean

@@ -93,8 +93,8 @@ private def mkInterruptWatcher? (clientRequestId? : Option String) : IO (Option
   | none => pure none
   | some _ =>
       let signal ← Std.Internal.UV.Signal.mk 2 false
+      let promise ← Std.Internal.UV.Signal.next signal
       let task ← IO.asTask (prio := Task.Priority.dedicated) do
-        let promise ← Std.Internal.UV.Signal.next signal
         let some _ ← IO.wait promise.result?
           | throw <| IO.userError "SIGINT watcher promise dropped"
         pure ()

Beam/Cli/Commands.lean

@@ -10,6 +10,7 @@ import Beam.Cli.Broker
 import Beam.Cli.DaemonManager
 import Beam.Cli.Feedback
 import Beam.Cli.Info
+import Beam.Cli.InstallPrune
 import Beam.Cli.LeanOperation
 import Beam.Cli.Lock
 import Beam.Cli.Project
@@ -128,13 +129,18 @@ private def shutdownProjectDaemon (opts : CliOptions) : IO Unit := do
 private def backendOfName (name : String) : Backend :=
   if name == "rocq" then .rocq else .lean
 
-private def holdUntilInterrupted : IO Unit := do
+private def runThenHoldUntilInterrupted (act : IO Unit) : IO Unit := do
   let signal ← Std.Internal.UV.Signal.mk 2 false
-  try
-    let promise ← Std.Internal.UV.Signal.next signal
+  let promise ← Std.Internal.UV.Signal.next signal
+  let task ← IO.asTask (prio := Task.Priority.dedicated) do
     let some _ ← IO.wait promise.result?
       | throw <| IO.userError "SIGINT watcher promise dropped"
     pure ()
+  try
+    act
+    match ← IO.wait task with
+    | .ok () => pure ()
+    | .error err => throw err
   finally
     Std.Internal.UV.Signal.stop signal
 
@@ -146,11 +152,15 @@ private def ensureBackend
   let root ← projectRoot opts backend
   let daemon ← ensureProjectDaemon home root backend opts
   withWrapperLease root daemon.startedNew do
-    callBroker root daemon.endpoint { op := .ensure, backend := backend, root? := some root.toString }
     if hold then
-      (← IO.getStdout).flush
-      IO.eprintln "beam: holding ensured daemon; interrupt this wrapper process when finished"
-      holdUntilInterrupted
+      runThenHoldUntilInterrupted do
+        callBroker root daemon.endpoint {
+          op := .ensure, backend := backend, root? := some root.toString
+        }
+        (← IO.getStdout).flush
+        IO.eprintln "beam: holding ensured daemon; interrupt this wrapper process when finished"
+    else
+      callBroker root daemon.endpoint { op := .ensure, backend := backend, root? := some root.toString }
 
 def runCommand (home : System.FilePath) (opts : CliOptions) : IO Unit := do
   match opts.args with
@@ -167,14 +177,18 @@ def runCommand (home : System.FilePath) (opts : CliOptions) : IO Unit := do
             pure <| roots.headD (beamStateDir home / installBundlesDirName)
       let _ ← ensureToolchainBundleIn cacheRoot home toolchain
       pure ()
+  | "install-prune" :: args =>
+      runInstallPrune home args
   | "validated-toolchains" :: backend :: [] =>
       printValidatedToolchains home backend
   | "compatible-release-lines" :: [] =>
       printCompatibleReleaseLines home
   | "install-layout" :: [] =>
       printInstallLayout
-  | "install-manifest" :: payloadHash :: sourceCommitArg :: toolchains =>
-      printInstallManifest payloadHash sourceCommitArg toolchains
+  | "install-manifest" :: payloadHash :: sourceCommitArg :: createdWithToolchains =>
+      printInstallManifest payloadHash sourceCommitArg createdWithToolchains
+  | "install-runtime-validate" :: path :: [] =>
+      validateInstalledRuntimeForReuse (System.FilePath.mk path)
   | "mcp-config" :: [] =>
       printMcpConfig home opts
   | "feedback" :: args =>

Beam/Cli/Info.lean

@@ -200,15 +200,17 @@ def printCompatibleReleaseLines (home : System.FilePath) : IO Unit := do
 def printInstallLayout : IO Unit := do
   printJsonLine (toJson installLayout)
 
-def printInstallManifest (payloadHash : String) (sourceCommitArg : String) (toolchains : List String) : IO Unit := do
-  if toolchains.isEmpty then
-    throw <| IO.userError "usage: beam install-manifest <payload-hash> <source-commit|-> <toolchain...>"
+def printInstallManifest (payloadHash : String) (sourceCommitArg : String)
+    (createdWithToolchains : List String) : IO Unit := do
+  if createdWithToolchains.isEmpty then
+    throw <| IO.userError
+      "usage: beam install-manifest <payload-hash> <source-commit|-> <creation-toolchain...>"
   let sourceCommit? :=
     if sourceCommitArg == "-" then
       none
     else
       some sourceCommitArg
-  printJsonLine (installManifestJson payloadHash sourceCommit? toolchains)
+  printJsonLine (installManifestJson payloadHash sourceCommit? createdWithToolchains)
 
 def printMcpConfig (home : System.FilePath) (opts : CliOptions) : IO Unit := do
   let root ← projectRoot opts .lean

Beam/Cli/InstallLayout.lean

@@ -6,6 +6,7 @@ Author: Emilio J. Gallego Arias
 
 import Lean
 import Beam.LSP.Lib.NativeLib
+import Beam.Path
 
 open Lean
 
@@ -17,10 +18,63 @@ structure InstallLayout where
   runtimePaths : List String
   wrapperPaths : List String
   sourceHashInputs : List String
-  deriving ToJson
+  deriving BEq, FromJson, ToJson
+
+def installManifestSchemaVersion : Nat :=
+  3
+
+structure InstallManifest where
+  schemaVersion : Nat
+  payloadHash : String
+  createdWithToolchains : List String
+  sourceCommit : Option String
+  artifacts : InstallLayout
+  deriving FromJson, ToJson
+
+private structure InstallManifestV2 where
+  schemaVersion : Nat
+  payloadHash : String
+  toolchains : List String
+  sourceCommit : Option String
+  artifacts : InstallLayout
+  deriving FromJson
+
+structure InstalledRuntimeLocation where
+  installRoot : System.FilePath
+  versionsRoot : System.FilePath
+  payload : String
+
+structure InstalledRuntime where
+  home : System.FilePath
+  location : InstalledRuntimeLocation
+  manifestPath : System.FilePath
+  manifest : InstallManifest
+
+inductive InstallRootMarkerError where
+  | missing
+  | invalid
+  | missingRoot
+  | mismatchedRoot
+
+inductive InstalledRuntimeError where
+  | invalidInstallRootMarker (error : InstallRootMarkerError)
+  | missingManifest
+  | invalidManifest (message : String)
+  | mismatchedPayload (manifestPayload : String)
+
+structure InvalidInstalledRuntime where
+  home : System.FilePath
+  location : InstalledRuntimeLocation
+  manifestPath? : Option System.FilePath
+  error : InstalledRuntimeError
+
+inductive RuntimeHomeResolution where
+  | source (home : System.FilePath)
+  | installed (runtime : InstalledRuntime)
+  | invalidInstalled (runtime : InvalidInstalledRuntime)
 
 def bundleRootFiles : List String :=
-  ["Beam.lean", "lakefile.lean", "lakefile.toml", "lake-manifest.json", "lean-toolchain",
+  ["Beam.lean", "lakefile.lean", "lake-manifest.json", "lean-toolchain",
     "validated-lean-toolchains", "compatible-lean-release-lines", "custom-lean-toolchains"]
 
 def bundleSourceDirs : List String :=
@@ -31,7 +85,7 @@ def bundleSourceHashInputLabels : List String :=
 
 def installRuntimePaths : List String :=
   ["libexec/beam-cli", "libexec/beam-daemon", "libexec/beam-client",
-    "libexec/lean-beam-mcp", s!"libexec/{Beam.LSP.Lib.pluginSharedLibName}", ".lake/packages"]
+    "libexec/lean-beam-mcp", s!"libexec/{Beam.LSP.Lib.pluginSharedLibName}"]
 
 def installWrapperPaths : List String :=
   ["bin/lean-beam", "bin/lean-beam-search", "bin/lean-beam-mcp"]
@@ -45,14 +99,180 @@ def installLayout : InstallLayout :=
     sourceHashInputs := bundleSourceHashInputLabels
   }
 
-def installManifestJson (payloadHash : String) (sourceCommit? : Option String) (toolchains : List String) :
+def installedRuntimeLocation? (home : System.FilePath) : Option InstalledRuntimeLocation := do
+  let versionsRoot ← home.parent
+  guard (versionsRoot.fileName == some "versions")
+  let installRoot ← versionsRoot.parent
+  let payload ← home.fileName
+  pure { installRoot, versionsRoot, payload }
+
+def checkInstallRootMarker
+    (installRoot : System.FilePath) : IO (Except InstallRootMarkerError Unit) := do
+  let marker := installRoot / ".lean-beam-install-root"
+  let markerMetadata? ←
+    try
+      pure <| some (← marker.symlinkMetadata)
+    catch _ =>
+      pure none
+  let some markerMetadata := markerMetadata?
+    | return .error .missing
+  unless markerMetadata.type == IO.FS.FileType.file do
+    return .error .invalid
+  try
+    let resolvedInstallRoot ← Beam.resolveExistingPath installRoot
+    let resolvedMarker ← Beam.resolveExistingPath marker
+    unless resolvedMarker.toString ==
+        (resolvedInstallRoot / ".lean-beam-install-root").toString do
+      return .error .invalid
+    let fields := (← IO.FS.readFile marker).splitOn "\n"
+    let schemaFields := fields.filter (fun field => field.startsWith "schema=")
+    unless schemaFields == ["schema=1"] do
+      return .error .invalid
+    let ownerFields := fields.filter (fun field => field.startsWith "owner=")
+    unless ownerFields == ["owner=lean-beam"] do
+      return .error .invalid
+    let rootFields := fields.filter (fun field => field.startsWith "root=")
+    let rootField ←
+      match rootFields with
+      | [] => return .error .missingRoot
+      | [rootField] => pure rootField
+      | _ => return .error .invalid
+    let markedRoot := System.FilePath.mk (rootField.drop 5).toString
+    if markedRoot.toString.isEmpty then
+      return .error .missingRoot
+    unless markedRoot.isAbsolute do
+      return .error .invalid
+    if ← Beam.sameFilePath markedRoot installRoot then
+      pure <| .ok ()
+    else
+      pure <| .error .mismatchedRoot
+  catch _ =>
+    pure <| .error .invalid
+
+private def checkInstallManifest (manifest : InstallManifest) : Except String InstallManifest := do
+  if manifest.payloadHash.isEmpty then
+    throw "install manifest payloadHash must not be empty"
+  if manifest.createdWithToolchains.isEmpty then
+    throw "install manifest createdWithToolchains must not be empty"
+  if manifest.createdWithToolchains.any (·.isEmpty) then
+    throw "install manifest createdWithToolchains entries must not be empty"
+  if manifest.artifacts != installLayout then
+    throw "install manifest artifacts do not match the current install layout"
+  pure manifest
+
+def parseInstallManifest (json : Json) : Except String InstallManifest := do
+  let schemaVersion ← json.getObjValAs? Nat "schemaVersion"
+  if schemaVersion == 2 then
+    -- Schema 2 remained unchanged while its artifact list evolved. Decode that list structurally
+    -- instead of comparing it with one historical layout: cleanup removes only the validated
+    -- direct runtime directory and never uses manifest artifact paths as deletion targets.
+    let legacy : InstallManifestV2 ← fromJson? json
+    if legacy.payloadHash.isEmpty then
+      throw "install manifest payloadHash must not be empty"
+    if legacy.toolchains.isEmpty || legacy.toolchains.any (·.isEmpty) then
+      throw "install manifest toolchains must not be empty"
+    pure {
+      schemaVersion := legacy.schemaVersion
+      payloadHash := legacy.payloadHash
+      createdWithToolchains := legacy.toolchains
+      sourceCommit := legacy.sourceCommit
+      artifacts := legacy.artifacts
+    }
+  else if schemaVersion == installManifestSchemaVersion then
+    checkInstallManifest (← fromJson? json)
+  else
+    throw s!"unsupported install manifest schemaVersion {schemaVersion}"
+
+def readInstallManifest (path : System.FilePath) : IO InstallManifest := do
+  let json ← IO.ofExcept <| Json.parse (← IO.FS.readFile path)
+  IO.ofExcept <| parseInstallManifest json
+
+def describeInstalledRuntimeError (runtime : InvalidInstalledRuntime) : String :=
+  match runtime.error with
+  | .invalidInstallRootMarker .missing =>
+      "missing Beam install root marker"
+  | .invalidInstallRootMarker .invalid =>
+      "invalid Beam install root marker"
+  | .invalidInstallRootMarker .missingRoot =>
+      "Beam install root marker has no root"
+  | .invalidInstallRootMarker .mismatchedRoot =>
+      "Beam install root marker names a different root"
+  | .missingManifest =>
+      "missing install manifest"
+  | .invalidManifest message =>
+      s!"invalid install manifest: {message}"
+  | .mismatchedPayload manifestPayload =>
+      s!"install manifest payloadHash {manifestPayload} does not match runtime directory {runtime.location.payload}"
+
+def resolveRuntimeHome (home : System.FilePath) : IO RuntimeHomeResolution := do
+  let home ← Beam.resolveExistingPath home
+  let some location := installedRuntimeLocation? home
+    | return .source home
+  match ← checkInstallRootMarker location.installRoot with
+  | .error .missing => return .source home
+  | .error error =>
+      return .invalidInstalled {
+        home
+        location
+        manifestPath? := none
+        error := .invalidInstallRootMarker error
+      }
+  | .ok () => pure ()
+  let manifestPath := home / "manifest.json"
+  unless ← manifestPath.pathExists do
+    return .invalidInstalled {
+      home
+      location
+      manifestPath? := none
+      error := .missingManifest
+    }
+  try
+    unless ← Beam.regularNonSymlinkFile manifestPath do
+      throw <| IO.userError "install manifest must be a regular non-symlinked file"
+    let resolvedManifestPath ← Beam.resolveExistingPath manifestPath
+    unless resolvedManifestPath.toString == manifestPath.toString do
+      throw <| IO.userError "install manifest must be a regular non-symlinked file"
+    let manifest ← readInstallManifest manifestPath
+    unless manifest.payloadHash == location.payload do
+      return .invalidInstalled {
+        home
+        location
+        manifestPath? := some manifestPath
+        error := .mismatchedPayload manifest.payloadHash
+      }
+    pure <| .installed { home, location, manifestPath, manifest }
+  catch e =>
+    pure <| .invalidInstalled {
+      home
+      location
+      manifestPath? := some manifestPath
+      error := .invalidManifest (toString e)
+    }
+
+def validateInstalledRuntimeForReuse (home : System.FilePath) : IO Unit := do
+  match ← resolveRuntimeHome home with
+  | .installed runtime =>
+      unless runtime.manifest.schemaVersion == installManifestSchemaVersion do
+        throw <| IO.userError <|
+          s!"refusing to reuse legacy Beam install manifest schemaVersion " ++
+            s!"{runtime.manifest.schemaVersion} at {runtime.manifestPath}; " ++
+            "stop active Beam clients, move this exact runtime aside for inspection, and rerun the installer"
+  | .source resolved =>
+      throw <| IO.userError s!"refusing to reuse non-installed Beam runtime: {resolved}"
+  | .invalidInstalled runtime =>
+      throw <| IO.userError <|
+        s!"refusing to reuse invalid installed Beam runtime at {runtime.home}: " ++
+          describeInstalledRuntimeError runtime
+
+def installManifestJson (payloadHash : String) (sourceCommit? : Option String)
+    (createdWithToolchains : List String) :
     Json :=
-  Json.mkObj [
-    ("schemaVersion", toJson (2 : Nat)),
-    ("payloadHash", toJson payloadHash),
-    ("toolchains", toJson toolchains),
-    ("sourceCommit", sourceCommit?.map toJson |>.getD Json.null),
-    ("artifacts", toJson installLayout)
-  ]
+  toJson ({
+    schemaVersion := installManifestSchemaVersion
+    payloadHash
+    createdWithToolchains
+    sourceCommit := sourceCommit?
+    artifacts := installLayout
+  } : InstallManifest)
 
 end Beam.Cli