diff --git a/Beam/Cli/Broker.lean b/Beam/Cli/Broker.lean index ceb8d119..0283e3f8 100644 --- a/Beam/Cli/Broker.lean +++ b/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 () diff --git a/Beam/Cli/Commands.lean b/Beam/Cli/Commands.lean index 9d91182e..cfce26f3 100644 --- a/Beam/Cli/Commands.lean +++ b/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 => diff --git a/Beam/Cli/Info.lean b/Beam/Cli/Info.lean index e94375e0..eb3bd855 100644 --- a/Beam/Cli/Info.lean +++ b/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 " +def printInstallManifest (payloadHash : String) (sourceCommitArg : String) + (createdWithToolchains : List String) : IO Unit := do + if createdWithToolchains.isEmpty then + throw <| IO.userError + "usage: beam install-manifest " 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 diff --git a/Beam/Cli/InstallLayout.lean b/Beam/Cli/InstallLayout.lean index d0e28cf8..ab36e6f9 100644 --- a/Beam/Cli/InstallLayout.lean +++ b/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 diff --git a/Beam/Cli/InstallPrune.lean b/Beam/Cli/InstallPrune.lean new file mode 100644 index 00000000..863eeeda --- /dev/null +++ b/Beam/Cli/InstallPrune.lean @@ -0,0 +1,269 @@ +/- +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.Cli.InstallLayout +import Beam.Cli.Lock +import Beam.Cli.RuntimeBundle.Metadata +import Beam.Cli.RuntimeBundle.Paths +import Beam.Cli.RuntimeBundle.Source +import Beam.Path + +open Lean + +namespace Beam.Cli + +private structure InstallPruneOptions where + apply : Bool := false + bundles : Bool := false + help : Bool := false + +private structure InstallPruneContext where + home : System.FilePath + installRoot : System.FilePath + versionsRoot : System.FilePath + bundleRoot : System.FilePath + +private structure InstallPrunePlan where + oldRuntimes : Array System.FilePath := #[] + staleBundles : Array System.FilePath := #[] + +private def installPruneUsage : String := + "usage: lean-beam prune [--apply] [--bundles]" + +private def installPruneHelp : String := + String.intercalate "\n" [ + installPruneUsage, + "", + "Preview and optionally remove old installed Beam runtimes.", + "", + "options:", + " --apply remove the displayed paths", + " --bundles also select stale or incomplete installed bundle-cache entries", + " -h, --help show this help", + "", + "Restart active agents and MCP clients before using --apply.", + "Apply removes one validated path at a time and reports each successful removal immediately." + ] + +private def parseInstallPruneOptions (args : List String) : Except String InstallPruneOptions := do + let mut opts : InstallPruneOptions := {} + for arg in args do + match arg with + | "--apply" => opts := { opts with apply := true } + | "--bundles" => opts := { opts with bundles := true } + | "-h" | "--help" => opts := { opts with help := true } + | _ => throw s!"{installPruneUsage}\nunknown prune option: {arg}" + pure opts + +private def fail (message : String) : IO α := + throw <| IO.userError message + +private def requireOwnedInstallRoot (installRoot : System.FilePath) : IO Unit := do + let marker := installRoot / ".lean-beam-install-root" + match ← checkInstallRootMarker installRoot with + | .ok () => pure () + | .error .missing => + fail s!"refusing to prune unmarked Beam install root: {installRoot}" + | .error .invalid => + fail s!"refusing to prune invalid Beam install root marker: {marker}" + | .error .missingRoot => + fail s!"refusing to prune install root marker without root: {marker}" + | .error .mismatchedRoot => + fail s!"refusing to prune install root with mismatched marker root: {marker}" + +private def validatedRuntimePayload (versionsRoot : System.FilePath) + (path : System.FilePath) : IO Unit := do + let resolved ← Beam.resolveExistingPath path + unless resolved.toString == path.toString do + fail s!"refusing to prune symlinked runtime path: {path}" + unless resolved.parent == some versionsRoot do + fail s!"refusing to prune non-canonical runtime path: {path}" + let some location := installedRuntimeLocation? resolved + | fail s!"runtime path has no installed-runtime location: {resolved}" + unless location.versionsRoot == versionsRoot do + fail s!"refusing to prune runtime outside versions root: {resolved}" + match ← resolveRuntimeHome resolved with + | .installed _ => pure () + | .source _ => + fail s!"refusing to prune unmarked runtime directory: {resolved}" + | .invalidInstalled runtime => + match runtime.error with + | .missingManifest => + fail s!"refusing to prune unmarked runtime directory: {resolved}" + | .invalidManifest _ => + fail s!"refusing to prune runtime with invalid manifest: {resolved / "manifest.json"}" + | .mismatchedPayload _ => + fail <| s!"refusing to prune runtime with mismatched manifest payloadHash: {resolved}" + | .invalidInstallRootMarker _ => + fail <| s!"refusing to prune runtime under an invalid Beam install root: {resolved}" + +private def resolveInstallPruneContext (home : System.FilePath) : IO InstallPruneContext := do + let home ← Beam.resolveExistingPath home + let some location := installedRuntimeLocation? home + | fail s!"prune is only available from an installed Beam runtime: {home}" + pure { + home + installRoot := location.installRoot + versionsRoot := location.versionsRoot + bundleRoot := location.installRoot / "state" / installBundlesDirName + } + +private def validateInstallPruneContext (ctx : InstallPruneContext) : IO Unit := do + let home := ctx.home + let installRoot := ctx.installRoot + requireOwnedInstallRoot installRoot + let currentPath := installRoot / "current" + unless ← currentPath.pathExists do + fail s!"missing current Beam runtime link: {currentPath}" + let current ← Beam.resolveExistingPath currentPath + unless current.toString == home.toString do + fail <| String.intercalate "\n" [ + s!"refusing to prune from a non-current Beam runtime: {home}", + s!"current Beam runtime: {current}", + "rerun prune through the installed `lean-beam` command" + ] + validatedRuntimePayload ctx.versionsRoot home + +private def oldRuntimePaths (ctx : InstallPruneContext) : IO (Array System.FilePath) := do + let entries := (← ctx.versionsRoot.readDir).qsort (fun a b => a.fileName < b.fileName) + let mut paths := #[] + for entry in entries do + unless ← entry.path.isDir do + fail s!"refusing to prune unexpected non-directory in versions root: {entry.path}" + let resolved ← Beam.resolveExistingPath entry.path + validatedRuntimePayload ctx.versionsRoot entry.path + if resolved.toString != ctx.home.toString then + paths := paths.push resolved + pure paths + +private def isDecimalName (path : System.FilePath) : Bool := + match path.fileName with + | some name => !name.isEmpty && name.toList.all Char.isDigit + | none => false + +private def staleBundlePath? (bundleRoot : System.FilePath) (currentSourceHash : String) + (path : System.FilePath) : IO Bool := do + unless ← path.isDir do + return false + unless isDecimalName path do + return false + let resolved ← Beam.resolveExistingPath path + unless resolved.toString == path.toString do + return false + let some platformRoot := resolved.parent + | return false + let some resolvedBundleRoot := platformRoot.parent + | return false + unless resolvedBundleRoot.toString == bundleRoot.toString do + return false + return (← completeBundleSourceHash? resolved) != some currentSourceHash + +private def staleBundlePaths (ctx : InstallPruneContext) : IO (Array System.FilePath) := do + unless ← ctx.bundleRoot.pathExists do + return #[] + let bundleRoot ← Beam.resolveExistingPath ctx.bundleRoot + unless bundleRoot.toString == ctx.bundleRoot.toString do + fail s!"refusing to prune symlinked installed bundle cache root: {ctx.bundleRoot}" + let currentSourceHash ← sourceHash ctx.home + let platforms := (← bundleRoot.readDir).qsort (fun a b => a.fileName < b.fileName) + let mut paths := #[] + for platform in platforms do + if ← platform.path.isDir then + let entries := (← platform.path.readDir).qsort (fun a b => a.fileName < b.fileName) + for entry in entries do + if ← staleBundlePath? bundleRoot currentSourceHash entry.path then + paths := paths.push (← Beam.resolveExistingPath entry.path) + pure paths + +private def installPrunePlan (ctx : InstallPruneContext) + (opts : InstallPruneOptions) : IO InstallPrunePlan := do + let oldRuntimes ← oldRuntimePaths ctx + let staleBundles ← if opts.bundles then staleBundlePaths ctx else pure #[] + pure { oldRuntimes, staleBundles } + +private def printInstallPrunePlan (ctx : InstallPruneContext) + (opts : InstallPruneOptions) (plan : InstallPrunePlan) : IO Unit := do + IO.println s!"Beam install prune ({if opts.apply then "apply" else "dry run"})" + IO.println s!"install root: {ctx.installRoot}" + IO.println s!"current runtime: {ctx.home}" + for path in plan.oldRuntimes do + IO.println s!"old runtime: {path}" + for path in plan.staleBundles do + IO.println s!"stale bundle: {path}" + IO.println s!"old runtimes: {plan.oldRuntimes.size}" + if opts.bundles then + IO.println s!"stale bundles: {plan.staleBundles.size}" + if !opts.apply && (!plan.oldRuntimes.isEmpty || !plan.staleBundles.isEmpty) then + let bundleArg := if opts.bundles then " --bundles" else "" + IO.println "restart active agents and MCP clients before applying this cleanup" + IO.println s!"dry run only; rerun `lean-beam prune --apply{bundleArg}` to remove these paths" + +private def removeOldRuntime (ctx : InstallPruneContext) (path : System.FilePath) : IO Bool := do + if !(← path.pathExists) then + return false + let resolved ← Beam.resolveExistingPath path + if resolved.toString == ctx.home.toString then + fail s!"refusing to prune current Beam runtime: {resolved}" + validatedRuntimePayload ctx.versionsRoot resolved + IO.FS.removeDirAll resolved + pure true + +private def removeStaleBundle (ctx : InstallPruneContext) + (currentSourceHash : String) (path : System.FilePath) : IO Bool := do + if !(← path.pathExists) then + return false + let some platformRoot := path.parent + | fail s!"stale bundle path has no platform root: {path}" + let some bundleId := path.fileName + | fail s!"stale bundle path has no bundle id: {path}" + withLockTimeout (bundleBuildLockPath platformRoot bundleId) 1000 do + if ← staleBundlePath? ctx.bundleRoot currentSourceHash path then + IO.FS.removeDirAll path + pure true + else + pure false + +private def applyInstallPrune (ctx : InstallPruneContext) + (opts : InstallPruneOptions) (plan : InstallPrunePlan) : IO (Nat × Nat) := do + let mut runtimesRemoved := 0 + for path in plan.oldRuntimes do + if ← removeOldRuntime ctx path then + runtimesRemoved := runtimesRemoved + 1 + IO.println s!"removed runtime: {path}" + let mut bundlesRemoved := 0 + if opts.bundles then + let currentSourceHash ← sourceHash ctx.home + for path in plan.staleBundles do + if ← removeStaleBundle ctx currentSourceHash path then + bundlesRemoved := bundlesRemoved + 1 + IO.println s!"removed stale bundle: {path}" + pure (runtimesRemoved, bundlesRemoved) + +def runInstallPrune (home : System.FilePath) (args : List String) : IO Unit := do + let opts ← IO.ofExcept <| parseInstallPruneOptions args + if opts.help then + IO.println installPruneHelp + return + let ctx ← resolveInstallPruneContext home + withLockTimeout (ctx.installRoot / ".install-lock") 1000 do + validateInstallPruneContext ctx + let plan ← installPrunePlan ctx opts + printInstallPrunePlan ctx opts plan + if opts.apply then + try + let (runtimesRemoved, bundlesRemoved) ← applyInstallPrune ctx opts plan + IO.println s!"removed runtimes: {runtimesRemoved}" + if opts.bundles then + IO.println s!"removed stale bundles: {bundlesRemoved}" + catch e => + IO.eprintln <| + "prune stopped before completing the displayed plan; any removals reported above were applied" + let bundleArg := if opts.bundles then " --bundles" else "" + IO.eprintln s!"rerun `lean-beam prune{bundleArg}` to preview the remaining paths" + throw e + +end Beam.Cli diff --git a/Beam/Cli/Lock.lean b/Beam/Cli/Lock.lean index 10617e63..c672ff6a 100644 --- a/Beam/Cli/Lock.lean +++ b/Beam/Cli/Lock.lean @@ -5,6 +5,7 @@ Author: Emilio J. Gallego Arias -/ import Lean +import Beam.Path import Beam.System open Lean @@ -31,8 +32,9 @@ private def lockPollMs : Nat := private def readLockPid? (lockDir : System.FilePath) : IO (Option Nat) := do try - if ← (lockDir / "pid").pathExists then - let text ← IO.FS.readFile (lockDir / "pid") + let pidPath := lockDir / "pid" + if ← Beam.regularNonSymlinkFile pidPath then + let text ← IO.FS.readFile pidPath pure <| trimLine text |>.toNat? else pure none @@ -69,10 +71,29 @@ private partial def acquireLockCore if let some parent := lockDir.parent then IO.FS.createDirAll parent let selfPid ← IO.Process.getPID - try - IO.FS.createDir lockDir - IO.FS.writeFile (lockDir / "pid") s!"{selfPid}\n" - catch _ => + let acquired ← + try + IO.FS.createDir lockDir + pure true + catch + | .alreadyExists .. => + pure false + | error => + throw error + if acquired then + try + IO.FS.writeFile (lockDir / "pid") s!"{selfPid}\n" + return + catch error => + try + if ← lockDir.pathExists then + IO.FS.removeDirAll lockDir + catch cleanupError => + throw <| IO.userError <| + s!"failed to publish Beam lock owner at {lockDir}: {error}; " ++ + s!"also failed to remove the acquired lock: {cleanupError}" + throw error + else let ownerPid? ← readLockPid? lockDir if ← removeStaleLock? lockDir ownerPid? then acquireLockCore lockDir timeoutMs? waitedMs diff --git a/Beam/Cli/RuntimeBundle/Build.lean b/Beam/Cli/RuntimeBundle/Build.lean index c61659fe..4a006c08 100644 --- a/Beam/Cli/RuntimeBundle/Build.lean +++ b/Beam/Cli/RuntimeBundle/Build.lean @@ -251,7 +251,9 @@ def ensureToolchainBundleInForFingerprint (cacheRoot home : System.FilePath) (to (fingerprint : ToolchainFingerprint) : IO (BundlePaths × String) := do let (bundleDir, bundleId, srcHash) ← bundleDirForFingerprint cacheRoot home toolchain fingerprint let workspace := bundleWorkspaceFor bundleDir - withLock (bundleDir / "lock") do + let some platformRoot := bundleDir.parent + | throw <| IO.userError s!"bundle directory has no platform root: {bundleDir}" + withLock (bundleBuildLockPath platformRoot bundleId) do unless ← bundleReady bundleDir toolchain srcHash fingerprint do buildToolchainBundle home toolchain srcHash fingerprint cacheRoot bundleDir workspace pure (bundlePathsFor workspace, bundleId) diff --git a/Beam/Cli/RuntimeBundle/Metadata.lean b/Beam/Cli/RuntimeBundle/Metadata.lean index ea2c27e8..883cb972 100644 --- a/Beam/Cli/RuntimeBundle/Metadata.lean +++ b/Beam/Cli/RuntimeBundle/Metadata.lean @@ -7,6 +7,7 @@ Author: Emilio J. Gallego Arias import Lean import Beam.Cli.RuntimeBundle.Fingerprint import Beam.Cli.RuntimeBundle.Paths +import Beam.Path open Lean @@ -23,13 +24,58 @@ private structure BundleMetadata where builtAt : String deriving FromJson, ToJson -def bundleArtifactsReady (workspace : System.FilePath) : IO Bool := do +private def checkBundleMetadataShape (metadata : BundleMetadata) : Except String Unit := do + if metadata.schemaVersion != bundleMetadataSchemaVersion then + throw s!"unsupported bundle metadata schemaVersion {metadata.schemaVersion}" + if metadata.toolchain.isEmpty then + throw "bundle metadata toolchain must not be empty" + if metadata.toolchainFingerprint.leanVersion.isEmpty || + metadata.toolchainFingerprint.leanPrefix.isEmpty || + metadata.toolchainFingerprint.leanLibDir.isEmpty || + metadata.toolchainFingerprint.lakeVersion.isEmpty then + throw "bundle metadata toolchain fingerprint fields must not be empty" + if metadata.sourceHash.isEmpty then + throw "bundle metadata sourceHash must not be empty" + if metadata.workspace.isEmpty then + throw "bundle metadata workspace must not be empty" + if metadata.builtAt.isEmpty then + throw "bundle metadata builtAt must not be empty" + +private def checkBundleMetadataMatches + (toolchain srcHash : String) + (fingerprint : ToolchainFingerprint) + (metadata : BundleMetadata) : Except String Unit := do + if metadata.toolchain != toolchain then + throw s!"bundle metadata toolchain mismatch: expected {toolchain}, got {metadata.toolchain}" + if metadata.toolchainFingerprint != fingerprint then + throw "bundle metadata toolchain fingerprint mismatch" + if metadata.sourceHash != srcHash then + throw s!"bundle metadata sourceHash mismatch: expected {srcHash}, got {metadata.sourceHash}" + +private def bundleMetadataWorkspaceMatches + (metadata : BundleMetadata) (workspace : System.FilePath) : IO Bool := + Beam.sameFilePath (System.FilePath.mk metadata.workspace) workspace + +private def bundleArtifactsReady (workspace : System.FilePath) : IO Bool := do let paths := bundlePathsFor workspace - return (← paths.daemon.pathExists) && (← paths.client.pathExists) && (← paths.plugin.pathExists) + return (← Beam.regularNonSymlinkFile paths.daemon) && + (← Beam.regularNonSymlinkFile paths.client) && + (← Beam.regularNonSymlinkFile paths.plugin) def bundleMetadataPath (bundleDir : System.FilePath) : System.FilePath := bundleDir / "metadata.json" +private def readBundleMetadata? (bundleDir : System.FilePath) : IO (Option BundleMetadata) := do + let path := bundleMetadataPath bundleDir + unless ← Beam.regularNonSymlinkFile path do + return none + try + let json ← IO.ofExcept <| Json.parse (← IO.FS.readFile path) + let metadata : BundleMetadata ← IO.ofExcept <| fromJson? json + pure (some metadata) + catch _ => + pure none + def bundleMetadataJson (toolchain srcHash : String) (fingerprint : ToolchainFingerprint) @@ -44,46 +90,30 @@ def bundleMetadataJson builtAt } : BundleMetadata) -def checkBundleMetadataJson - (toolchain srcHash : String) - (fingerprint : ToolchainFingerprint) - (_workspace : System.FilePath) - (json : Json) : Except String Unit := do - let metadata : BundleMetadata ← fromJson? json - if metadata.schemaVersion != bundleMetadataSchemaVersion then - throw s!"unsupported bundle metadata schemaVersion {metadata.schemaVersion}" - if metadata.toolchain != toolchain then - throw s!"bundle metadata toolchain mismatch: expected {toolchain}, got {metadata.toolchain}" - if metadata.toolchainFingerprint != fingerprint then - throw "bundle metadata toolchain fingerprint mismatch" - if metadata.sourceHash != srcHash then - throw s!"bundle metadata sourceHash mismatch: expected {srcHash}, got {metadata.sourceHash}" - if metadata.workspace.isEmpty then - throw "bundle metadata workspace must not be empty" - if metadata.builtAt.isEmpty then - throw "bundle metadata builtAt must not be empty" +private def completeBundleMetadata? (bundleDir : System.FilePath) : IO (Option BundleMetadata) := do + let workspace := bundleWorkspaceFor bundleDir + unless ← bundleArtifactsReady workspace do + return none + let some metadata ← readBundleMetadata? bundleDir + | return none + match checkBundleMetadataShape metadata with + | .error _ => return none + | .ok () => pure () + unless ← bundleMetadataWorkspaceMatches metadata workspace do + return none + pure (some metadata) -def bundleMetadataReady - (bundleDir : System.FilePath) - (toolchain srcHash : String) - (fingerprint : ToolchainFingerprint) - (workspace : System.FilePath) : IO Bool := do - let path := bundleMetadataPath bundleDir - unless ← path.pathExists do - return false - try - let json ← IO.ofExcept <| Json.parse (← IO.FS.readFile path) - match checkBundleMetadataJson toolchain srcHash fingerprint workspace json with - | .ok _ => return true - | .error _ => return false - catch _ => - return false +/-- Return the source hash only for a structurally complete, artifact-ready bundle. -/ +def completeBundleSourceHash? (bundleDir : System.FilePath) : IO (Option String) := do + pure <| (← completeBundleMetadata? bundleDir).map (·.sourceHash) def bundleReady (bundleDir : System.FilePath) (toolchain srcHash : String) (fingerprint : ToolchainFingerprint) : IO Bool := do - let workspace := bundleWorkspaceFor bundleDir - return (← bundleArtifactsReady workspace) && - (← bundleMetadataReady bundleDir toolchain srcHash fingerprint workspace) + let some metadata ← completeBundleMetadata? bundleDir + | return false + match checkBundleMetadataMatches toolchain srcHash fingerprint metadata with + | .ok () => pure true + | .error _ => pure false def writeBundleMetadata (bundleDir : System.FilePath) (toolchain srcHash : String) (fingerprint : ToolchainFingerprint) (workspace : System.FilePath) : IO Unit := do diff --git a/Beam/Cli/RuntimeBundle/Paths.lean b/Beam/Cli/RuntimeBundle/Paths.lean index ef2e6c0e..0264a59f 100644 --- a/Beam/Cli/RuntimeBundle/Paths.lean +++ b/Beam/Cli/RuntimeBundle/Paths.lean @@ -63,6 +63,13 @@ def installBundlesDirName : String := def runtimeBundlesDirName : String := "bundles" +/-- +The build lock lives beside a bundle rather than inside it so cleanup can remove the complete +bundle directory without deleting the lock that protects that removal. +-/ +def bundleBuildLockPath (platformRoot : System.FilePath) (bundleId : String) : System.FilePath := + platformRoot / ".locks" / bundleId + def beamStateDir (root : System.FilePath) : System.FilePath := root / beamStateDirName diff --git a/Beam/Cli/Usage.lean b/Beam/Cli/Usage.lean index bc5fae8f..562a281d 100644 --- a/Beam/Cli/Usage.lean +++ b/Beam/Cli/Usage.lean @@ -37,6 +37,7 @@ def usage : String := " beam [--root PATH] [--port N] rocq-goals-prev [text...]", " beam [--root PATH] feedback --stdin|--input [--bundle none|dir|zip] [--output-dir ] [--no-redact]", " beam bundle-install ", + " beam install-prune [--apply] [--bundles]", " beam validated-toolchains lean", " beam compatible-release-lines", " beam [--root PATH] doctor lean|rocq", diff --git a/Beam/Feedback.lean b/Beam/Feedback.lean index 56f57f7c..5bd5dc63 100644 --- a/Beam/Feedback.lean +++ b/Beam/Feedback.lean @@ -389,6 +389,8 @@ private def runtimeSummarySection (collection : Collection) : String := optionalLine "MCP protocol" (jsonStringField? identity "mcp_protocol") ++ optionalLine "active root" activeRoot? ++ optionalLine "runtime active" ((jsonBoolField? identity "runtime_active").map boolText) ++ + optionalLine "runtime current" ((jsonBoolField? identity "runtime_current").map boolText) ++ + optionalLine "runtime error" (jsonStringField? identity "runtime_error") ++ optionalLine "source" source? ++ optionalLine "daemon registry pid" (jsonStringField? daemon "registryPidStatus") ++ optionalLine "daemon endpoint" (jsonStringField? daemon "registryEndpoint") ++ diff --git a/Beam/Path.lean b/Beam/Path.lean index d8a20d20..63c62d31 100644 --- a/Beam/Path.lean +++ b/Beam/Path.lean @@ -8,6 +8,14 @@ import Lean namespace Beam +/-- Return whether `path` itself is a regular file, without following symbolic links. -/ +def regularNonSymlinkFile (path : System.FilePath) : IO Bool := do + try + let metadata ← path.symlinkMetadata + pure (metadata.type == IO.FS.FileType.file) + catch _ => + pure false + /-- Resolve a path that must already exist. -/ def resolveExistingPath (path : System.FilePath) : IO System.FilePath := IO.FS.realPath path diff --git a/Beam/Version.lean b/Beam/Version.lean index c372b0aa..8f2e462d 100644 --- a/Beam/Version.lean +++ b/Beam/Version.lean @@ -5,7 +5,9 @@ Author: Emilio J. Gallego Arias -/ import Lean +import Beam.Cli.InstallLayout import Beam.Git +import Beam.Path open Lean @@ -33,32 +35,12 @@ private def optionalBoolField (key : String) (value? : Option Bool) : List (Stri | some value => [(key, toJson value)] | none => [] -private def runtimePayload? (home : System.FilePath) : Option String := do - let parent ← home.parent - let parentName ← parent.fileName - if parentName == "versions" then - home.fileName - else - none - -private def manifestPath? (home : System.FilePath) : IO (Option System.FilePath) := do - let path := home / "manifest.json" - if ← path.pathExists then - pure (some path) - else - pure none - -private def manifestSourceCommit? (manifest? : Option System.FilePath) : IO (Option String) := do - match manifest? with - | none => pure none - | some manifest => - try - let json ← IO.ofExcept <| Json.parse (← IO.FS.readFile manifest) - match json.getObjVal? "sourceCommit" with - | .ok (.str commit) => pure (some commit) - | _ => pure none - catch _ => - pure none +private def installedRuntimeCurrent + (home : System.FilePath) (location : Beam.Cli.InstalledRuntimeLocation) : IO Bool := do + let current := location.installRoot / "current" + unless ← current.pathExists do + return false + Beam.sameFilePath current home structure Identity where name : String @@ -75,6 +57,8 @@ structure Identity where sourceDirty? : Option Bool := none activeRoot? : Option String := none runtimeActive? : Option Bool := none + runtimeCurrent? : Option Bool := none + runtimeError? : Option String := none def Identity.asJson (identity : Identity) : Json := Json.mkObj <| @@ -93,7 +77,9 @@ def Identity.asJson (identity : Identity) : Json := optionalField "source_branch" identity.sourceBranch? ++ optionalBoolField "source_dirty" identity.sourceDirty? ++ optionalField "active_root" identity.activeRoot? ++ - optionalBoolField "runtime_active" identity.runtimeActive? + optionalBoolField "runtime_active" identity.runtimeActive? ++ + optionalBoolField "runtime_current" identity.runtimeCurrent? ++ + optionalField "runtime_error" identity.runtimeError? def Identity.textLines (identity : Identity) : List String := [s!"{identity.name} {identity.version}"] ++ @@ -134,6 +120,12 @@ def Identity.textLines (identity : Identity) : List String := | none => []) ++ (match identity.runtimeActive? with | some active => [s!"runtime active: {active}"] + | none => []) ++ + (match identity.runtimeCurrent? with + | some current => [s!"runtime current: {current}"] + | none => []) ++ + (match identity.runtimeError? with + | some error => [s!"runtime error: {error}"] | none => []) def Identity.text (identity : Identity) : String := @@ -148,24 +140,50 @@ def mkRuntimeIdentity (mcpProtocol? : Option String := none) (activeRoot? : Option System.FilePath := none) (runtimeActive? : Option Bool := none) : IO Identity := do - let manifest? ← + let runtimeResolution? ← match home? with - | some home => manifestPath? home + | some home => pure <| some (← Beam.Cli.resolveRuntimeHome home) | none => pure none - let manifestCommit? ← manifestSourceCommit? manifest? + let installedRuntime? := + match runtimeResolution? with + | some (.installed runtime) => some runtime + | _ => none + let invalidRuntime? := + match runtimeResolution? with + | some (.invalidInstalled runtime) => some runtime + | _ => none + let sourceHome? := + match runtimeResolution? with + | some (.source home) => some home + | _ => none + let manifest? := installedRuntime?.map (·.manifestPath) + |>.orElse (fun _ => invalidRuntime?.bind (·.manifestPath?)) + let manifestCommit? := installedRuntime?.bind (fun runtime => runtime.manifest.sourceCommit) let sourceCommit? ← - match home?, manifestCommit? with - | _, some commit => pure (some commit) - | some home, none => Beam.Git.fullCommitAt? home + match manifestCommit?, sourceHome? with + | some commit, _ => pure (some commit) + | none, some home => Beam.Git.fullCommitAt? home | none, none => pure none let sourceBranch? ← - match home?, manifest? with - | some home, none => Beam.Git.branchAt? home - | _, some _ | none, none => pure none + match sourceHome? with + | some home => Beam.Git.branchAt? home + | none => pure none let sourceDirty? ← - match home?, manifest? with - | some home, none => Beam.Git.dirtyAt? home - | _, some _ | none, none => pure none + match sourceHome? with + | some home => Beam.Git.dirtyAt? home + | none => pure none + let runtimeCurrent? ← + match installedRuntime?, invalidRuntime? with + | some runtime, _ => + pure <| some (← installedRuntimeCurrent runtime.home runtime.location) + | none, some runtime => + pure <| some (← installedRuntimeCurrent runtime.home runtime.location) + | none, none => pure none + let runtimePayload? := + installedRuntime?.map (·.location.payload) + |>.orElse (fun _ => invalidRuntime?.map (·.location.payload)) + let runtimeError? := + invalidRuntime?.map Beam.Cli.describeInstalledRuntimeError pure { name mcpProtocol? @@ -173,13 +191,15 @@ def mkRuntimeIdentity beamHome? := home?.map (·.toString) beamCli? serverBinary? - runtimePayload? := home?.bind runtimePayload? + runtimePayload? manifest? := manifest?.map (·.toString) sourceCommit? sourceBranch? sourceDirty? activeRoot? := activeRoot?.map (·.toString) runtimeActive? + runtimeCurrent? + runtimeError? } def mcpServerIdentity diff --git a/CHANGELOG.md b/CHANGELOG.md index d5d3a87e..e3dafdd3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,6 +8,11 @@ This project keeps a lightweight, reverse-chronological changelog. Dates use `YY ### Added +- `lean-beam prune` previews obsolete installed runtime snapshots; `--apply` removes them, and + `--bundles` also selects stale or incomplete installed bundle-cache entries. +- Installed runtime identities report whether the running CLI or MCP process still belongs to the + current runtime selected by the installer and expose invalid installed state without + misclassifying it as a source checkout. - Canonical Lean RC and patch toolchains from declared compatible release lines can now build exact-fingerprint bundles that pass a local plugin qualification probe before use. - Validated Lean `v4.33.0-rc2` support. @@ -28,6 +33,9 @@ This project keeps a lightweight, reverse-chronological changelog. Dates use `YY - Lean MCP tool descriptions now state the source-file invariant: Beam reads saved `.lean` source but never applies source edits. Speculative tools do not persist source, save commands write build artifacts only, and code-action edits are returned for clients to apply. +- Install manifest schema 3 names immutable creation-time toolchain provenance explicitly and lists + only required staged artifacts; schema-2 runtimes remain readable for identity and safe cleanup but + are not reused by reinstall. ### Fixed @@ -36,6 +44,14 @@ This project keeps a lightweight, reverse-chronological changelog. Dates use `YY with `saveUnsupportedSetup`, now with guidance to use `leanOptions` or `lake build`. Running Lean sessions must be restarted after Lake workspace configuration changes before the next operation that uses the Lean server. +- Reinstalling an existing content-addressed runtime now validates its owned install marker, typed + manifest, required artifacts, executable commands, and payload contents instead of silently + reusing corrupted installed state, and failed validation releases the installer lock. +- Bundle readiness and installed-cache pruning now require regular, non-symlinked runtime artifacts + 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-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/ejgallego/lean-beam/pull/217), @ejgallego). diff --git a/README.md b/README.md index b602915b..9cb44ab0 100644 --- a/README.md +++ b/README.md @@ -119,6 +119,10 @@ Setup details, validated and compatible toolchains, agent-skill installation, MC direct CLI examples, installer locations, overrides, and offline advice live in [docs/SETUP.md](docs/SETUP.md). +Beam retains prior immutable runtimes so updates remain atomic. Use `lean-beam prune` to preview +old installed state and follow the [prune guide](docs/SETUP.md#prune-old-installed-state) before +applying cleanup. + Lean Beam fully validates exact toolchains listed in [`validated-lean-toolchains`](validated-lean-toolchains) and locally qualifies canonical RC/patch variants from [`compatible-lean-release-lines`](compatible-lean-release-lines). See diff --git a/docs/COMPATIBILITY.md b/docs/COMPATIBILITY.md index eccfad0a..97a7b1ac 100644 --- a/docs/COMPATIBILITY.md +++ b/docs/COMPATIBILITY.md @@ -17,7 +17,9 @@ A Lean release line is the canonical `major.minor` family recorded in variants must build and pass the local plugin qualification probe for their exact fingerprint. Shims must name the Lean/Lake API boundary they support and should be removed when the support window no longer needs them. -- Versioned runtime bundle metadata and install-layout schemas. +- 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. - The MCP protocol revision currently advertised by `lean-beam-mcp` and its conformance baseline. - Documented real client requirements, when they name an owner and removal condition. diff --git a/docs/DEVELOPMENT.md b/docs/DEVELOPMENT.md index 2ee5ecfc..db179c8b 100644 --- a/docs/DEVELOPMENT.md +++ b/docs/DEVELOPMENT.md @@ -403,12 +403,16 @@ Daemon registry management, daemon startup/reuse, endpoint selection, and wrappe [Beam/Cli/DaemonManager.lean](../Beam/Cli/DaemonManager.lean). Broker request plumbing, progress messages, cancellation-on-interrupt, and response failure notes live in [Beam/Cli/Broker.lean](../Beam/Cli/Broker.lean). User-facing stdout/stderr formatting helpers live -in [Beam/Cli/Output.lean](../Beam/Cli/Output.lean). Doctor, supported-toolchain, install-manifest, -and MCP config reporting live in [Beam/Cli/Info.lean](../Beam/Cli/Info.lean). The command dispatch +in [Beam/Cli/Output.lean](../Beam/Cli/Output.lean). Doctor, validated/compatible toolchain registry, +install layout/manifest, and MCP config reporting live in +[Beam/Cli/Info.lean](../Beam/Cli/Info.lean). The command dispatch table lives in [Beam/Cli/Commands.lean](../Beam/Cli/Commands.lean), and [Beam/Cli/Usage.lean](../Beam/Cli/Usage.lean) owns the help text. Lean command to broker-request projection lives in -[Beam/Cli/LeanOperation.lean](../Beam/Cli/LeanOperation.lean). Install and bundle layout metadata lives in -[Beam/Cli/InstallLayout.lean](../Beam/Cli/InstallLayout.lean). Runtime bundle compatibility imports +[Beam/Cli/LeanOperation.lean](../Beam/Cli/LeanOperation.lean). Install and bundle layout metadata, +typed manifest parsing, install-root ownership checks, and source/installed/invalid runtime +classification live in [Beam/Cli/InstallLayout.lean](../Beam/Cli/InstallLayout.lean). Conservative +installed-state planning and removal lives in +[Beam/Cli/InstallPrune.lean](../Beam/Cli/InstallPrune.lean). Runtime bundle compatibility imports live in [Beam/Cli/RuntimeBundle.lean](../Beam/Cli/RuntimeBundle.lean); implementation details are split under [Beam/Cli/RuntimeBundle](../Beam/Cli/RuntimeBundle). Keep source hashing, resolved toolchain fingerprinting, metadata acceptance, and fallback bundle builds in their focused @@ -416,6 +420,11 @@ submodules instead of growing the umbrella import. Bundle IDs and metadata must Beam runtime source hash and the resolved Lean/Lake fingerprint so local custom toolchain relinks and reported identity changes cannot silently reuse stale helpers. The user-facing model is in [CUSTOM_TOOLCHAINS.md](CUSTOM_TOOLCHAINS.md). + +Install manifests describe required staged artifacts, not optional future layout. New manifests +write schema 3 and name creation-time toolchain provenance explicitly. Schema 2 remains readable for +identity and `lean-beam prune`, but installer reuse requires the current schema; the compatibility +window and removal trigger live in [COMPATIBILITY.md](COMPATIBILITY.md). Keep [Beam/Cli.lean](../Beam/Cli.lean) as the executable entry point: parse top-level options, resolve `BEAM_HOME`, and delegate to `runCommand`. diff --git a/docs/FEEDBACK.md b/docs/FEEDBACK.md index 6f7d34e9..25c5bcbe 100644 --- a/docs/FEEDBACK.md +++ b/docs/FEEDBACK.md @@ -57,9 +57,10 @@ daemon registry status, startup log tail, and recent daemon incident records. Call `beam_feedback` with the same required fields plus the `workspace_id` whose project and runtime context should be collected. MCP returns compact report-card JSON in `structuredContent`: `markdown`, `metadata`, `collection_warnings`, and any bundle paths. The -default Markdown includes a short Beam runtime summary instead of the full collected debug JSON. -Pass `include_collected: true` to include the full collected Beam debug context inline and render -the full debug-context section in Markdown. +default Markdown includes a short Beam runtime summary instead of the full collected debug JSON, +including stale-runtime or invalid-install identity when available. Pass `include_collected: true` +to include the full collected Beam debug context inline and render the full debug-context section in +Markdown. MCP does not start a Lean runtime just to collect feedback. For the selected workspace, it includes daemon registry and recent daemon incident context. When a runtime is active, it also includes diff --git a/docs/MCP.md b/docs/MCP.md index d18642cc..4014d7f5 100644 --- a/docs/MCP.md +++ b/docs/MCP.md @@ -101,6 +101,16 @@ Dropping the default workspace does not stop remaining named workspaces. `lean_l map and contains any remaining named workspaces; statistics are not projected through an implicit default workspace. +`beam_version` returns the running server identity in `structuredContent`. Installed runtime +identities include the optional Boolean `runtime_current`: `true` means the process belongs to the +runtime selected by the install root's `current` link, while `false` means it is stale or that the +link is missing. Source-checkout identities omit this field. Invalid installed state also includes +the optional string `runtime_error`; the tool call still succeeds so clients can report the broken +identity. Restart an agent or MCP client for `runtime_current: false`. For `runtime_error`, stop Beam +clients and follow the error-specific +[installed-runtime recovery guidance](SETUP.md#prune-old-installed-state) before resuming normal +work. + Direct MCP clients should call `lean_update` before snapshot-bound tools such as `lean_run_at`, `lean_run_at_handle`, `lean_hover`, `lean_signature_help`, `lean_definition`, `lean_references`, `lean_document_symbols`, `lean_goals`, `lean_todo`, and `lean_code_action_resolve`; those calls diff --git a/docs/SETUP.md b/docs/SETUP.md index 949b3030..cbbc20d9 100644 --- a/docs/SETUP.md +++ b/docs/SETUP.md @@ -124,6 +124,70 @@ If you are unsure which runtime bundle is active or why a toolchain is rejected, lean-beam doctor ``` +## Prune Old Installed State + +The installer publishes each distinct content payload as an immutable runtime under +`BEAM_INSTALL_ROOT/versions`. Reinstalling an identical payload reuses its existing runtime only +after validating its ownership marker, manifest, required files, executable commands, and payload +contents. The schema-3 manifest field `createdWithToolchains` records the toolchain selection that +first created that immutable payload; later prebuilds add mutable bundle-cache entries without +rewriting that provenance. Beam keeps prior distinct runtimes so publishing `current` stays atomic, +but those snapshots are not removed automatically. Schema-2 manifests are readable only for +identity and cleanup; reinstalling never republishes a schema-2 runtime. Preview old state with: + +```bash +lean-beam prune +``` + +The preview validates the Beam ownership marker, requires the command to come from the current +installed runtime, and checks every candidate's manifest. It never selects the current runtime. +Apply the displayed runtime cleanup with: + +```bash +lean-beam prune --apply +``` + +Installed bundle-cache keys include the toolchain name and resolved fingerprint, runtime source +hash, and platform. To also preview stale-source or incomplete entries while preserving bundles +that match the current runtime source, add `--bundles`: + +```bash +lean-beam prune --bundles +lean-beam prune --apply --bundles +``` + +This only scans the installer-owned cache under `BEAM_INSTALL_ROOT/state/install-bundles`; it does +not remove project-local fallback bundles under `/.beam/bundles`. A complete installed +bundle is preserved when its runtime source still matches, even when that toolchain fingerprint is +not currently in use. + +Restart active agent and MCP client sessions before any `prune --apply`; otherwise a process may +still be running from a runtime selected for removal. A later request rebuilds any needed bundle +that was pruned. Pruning uses the same install lock as the installer and each selected bundle's +build lock, and refuses symlinked installed bundle-cache roots or symlinked and unmarked runtime +directories. + +Apply is incremental rather than transactional: Beam validates and removes one displayed path at a +time and reports each successful removal immediately. If a later path fails validation or its lock +cannot be acquired, earlier reported removals remain applied. Resolve the reported error and rerun +`lean-beam prune` (with `--bundles` when applicable) to preview what remains. + +If reinstalling reports that an existing runtime does not match its payload hash, stop active Beam +agents and MCP clients first. Move only the exact reported runtime directory out of +`BEAM_INSTALL_ROOT/versions` and preserve it for inspection, then rerun the installer. Do not remove +the whole `versions` directory. `lean-beam prune` deliberately refuses invalid state and the current +runtime, so it is not the repair path for this case. Use the same recovery when reinstalling refuses +to reuse a cleanup-only schema-2 runtime. + +If `runtime_error` instead reports an invalid install-root marker, do not recreate that ownership +marker in place or move only one runtime: the marker protects the boundary of the whole managed +root. Stop active Beam clients, rename the exact `BEAM_INSTALL_ROOT` as a unit and preserve it for +inspection, then rerun the installer so it creates a fresh owned root. Do not delete the preserved +root until its contents are understood. + +The command is intentionally unavailable from a source checkout because there is no owned +immutable install root to prune there. + ## Use Beam From A Lean Project Move to the Lean project you want to work on and check the resolved setup: @@ -335,7 +399,14 @@ The wrapper resolves the matching installed Beam runtime for each project. Use `lean-beam --version` for bug reports and CLI refresh checks. Use `lean-beam-mcp --version` to check which MCP server command a client registration resolves. From a live MCP session, call the -`beam_version` tool to report the running server process identity as structured content. +`beam_version` tool to report the running server process identity as structured content. Installed +identities include `runtime_current`: `false` means that process is not selected by the install +root's `current` link, usually because it belongs to a superseded runtime but also when that link is +missing. Restart the agent or MCP client after reinstalling. A newly resolved installed wrapper +should report `runtime current: true`; if it does not, treat the missing or broken `current` link as +an installation-integrity failure. An owned runtime with an invalid marker or manifest reports +`runtime_error` instead of being presented as a source checkout. Follow the error-specific recovery +guidance in [Prune Old Installed State](#prune-old-installed-state). Use `lean-beam feedback --stdin` when reporting setup or runtime issues; see [FEEDBACK.md](FEEDBACK.md). diff --git a/docs/STATUS.md b/docs/STATUS.md index a805ba8b..a17bb362 100644 --- a/docs/STATUS.md +++ b/docs/STATUS.md @@ -47,6 +47,8 @@ Pre-stable compatibility policy lives in [Compatibility Policy](COMPATIBILITY.md notifications were observed while the request was pending - explicit support for installed custom elan-linked Lean toolchains through `--custom-toolchain `, recorded in the runtime's `custom-lean-toolchains` registry +- conservative installed-state maintenance through `lean-beam prune`, with a dry run by default, + ownership and manifest validation, and optional stale installed bundle-cache cleanup ### MCP And Agent Integration @@ -56,7 +58,8 @@ Pre-stable compatibility policy lives in [Compatibility Policy](COMPATIBILITY.md connection - bug-report identity surfaces: `lean-beam --version`, `lean-beam-mcp --version`, and MCP `beam_version` for the running server process, including manifest commit or source checkout - commit/branch/dirty data + commit/branch/dirty data, installed `runtime_current` status, and structural `runtime_error` + reporting for invalid owned markers or manifests - feedback report-card surfaces: `lean-beam feedback` and MCP `beam_feedback` return structured JSON containing pasteable Markdown, metadata, collection warnings, and optional evidence bundle paths; CLI output and MCP `include_collected: true` include collected version/stats/open-file diff --git a/docs/TESTING.md b/docs/TESTING.md index 920af2e9..e8e929e6 100644 --- a/docs/TESTING.md +++ b/docs/TESTING.md @@ -88,7 +88,9 @@ Additional Beam lanes: Current Beam coverage includes: -- fast Beam daemon smoke, request-stream, save-stream, startup-handshake, tracked-diagnostic dedup, protocol tests, and supported-toolchain CI matrix consistency through [tests/test-beam-fast.sh](../tests/test-beam-fast.sh) +- fast Beam daemon smoke, request-stream, save-stream, startup-handshake, tracked-diagnostic dedup, + protocol tests, and validated-toolchain/release-line CI policy consistency through + [tests/test-beam-fast.sh](../tests/test-beam-fast.sh) - wrapper coverage through [tests/test-beam-wrapper.sh](../tests/test-beam-wrapper.sh), which aggregates focused probe, runtime, sync/save, handle, and diagnostic slices - focused daemon lifecycle coverage in [tests/test-beam-wrapper-daemon.sh](../tests/test-beam-wrapper-daemon.sh) - Linux-only PID-isolated sandbox wrapper coverage in [tests/test-beam-wrapper-sandbox.sh](../tests/test-beam-wrapper-sandbox.sh) @@ -96,8 +98,12 @@ Current Beam coverage includes: race coverage in [tests/test-beam-save-olean.sh](../tests/test-beam-save-olean.sh) - install flow, installed runtime layout, manifest metadata, exact/compatible toolchain selection, - `validated-toolchains`, `compatible-release-lines`, `doctor`, and installed MCP wrapper coverage - in [tests/test-beam-install.sh](../tests/test-beam-install.sh) + shell/Lean owned-root marker parity, required artifact and executable-mode validation, + content-addressed runtime reuse, schema-2 reuse rejection and cleanup compatibility, + `validated-toolchains`, + `compatible-release-lines`, `doctor`, installed-state pruning, and installed MCP wrapper coverage + in [tests/test-beam-install.sh](../tests/test-beam-install.sh), with focused prune safety and + invalid-runtime identity cases in [tests/test-beam-prune.sh](../tests/test-beam-prune.sh) - MCP protocol, projection, stdio, HTTP bridge, self-check, and external conformance coverage - Rocq wrapper and broker smoke coverage in [tests/test-beam-wrapper-rocq.sh](../tests/test-beam-wrapper-rocq.sh) and [tests/lean/BeamTest/Broker/RocqSmokeTest.lean](../tests/lean/BeamTest/Broker/RocqSmokeTest.lean) @@ -233,7 +239,9 @@ to `BEAM_MCP_STDIO_WAIT_DIAGNOSTICS_WATCHDOG_MS=10000`. Set `BEAM_MCP_STDIO_SERV when intentionally checking the quiet stderr path. The fast suite's installed-wrapper self-check uses `BEAM_MCP_SELF_CHECK_TIMEOUT_MS`, defaulting to 120 seconds, because first-time bundle setup may build the local fixture under CI contention. Keep `--timeout 30` for local repro attempts unless you -are specifically checking the CI budget. +are specifically checking the CI budget. The focused daemon lifecycle fixture explicitly prebuilds +its toolchain into one owned shared cache before timing daemon startup, so cold bundle compilation +is not misdiagnosed as a daemon-readiness timeout. The focused harness also accepts `progress-explicit-sync`, `no-progress-roots-sync`, and `no-progress-explicit-sync` as `--scenario` values. Use those variants to isolate whether a timeout diff --git a/scripts/install-beam.sh b/scripts/install-beam.sh index 92b229fa..3b36726b 100755 --- a/scripts/install-beam.sh +++ b/scripts/install-beam.sh @@ -78,6 +78,8 @@ beam_lsp_plugin_shared_lib="$(beam_shared_lib_name beam_Beam_LSP)" install_root_marker=".lean-beam-install-root" skill_owner_marker=".lean-beam-skill" install_lock_dir="" +install_lock_owned=0 +active_staging_root="" set_bin_home() { bin_home="$1" @@ -135,24 +137,22 @@ set_opencode_config_dir "${OPENCODE_CONFIG_DIR:-$HOME/.config/opencode}" set_vibe_home "${VIBE_HOME:-$HOME/.vibe}" runtime_payload_spec=( - "copy|rootFiles|Beam.lean|Beam.lean" - "copy|rootFiles|lakefile.lean|lakefile.lean" - "copy|rootFiles|lakefile.toml|lakefile.toml" - "copy|rootFiles|lake-manifest.json|lake-manifest.json" - "copy|rootFiles|lean-toolchain|lean-toolchain" - "copy|rootFiles|validated-lean-toolchains|validated-lean-toolchains" - "copy|rootFiles|compatible-lean-release-lines|compatible-lean-release-lines" + "required|rootFiles|Beam.lean|Beam.lean" + "required|rootFiles|lakefile.lean|lakefile.lean" + "required|rootFiles|lake-manifest.json|lake-manifest.json" + "required|rootFiles|lean-toolchain|lean-toolchain" + "required|rootFiles|validated-lean-toolchains|validated-lean-toolchains" + "required|rootFiles|compatible-lean-release-lines|compatible-lean-release-lines" "generated|rootFiles|custom-lean-toolchains|custom-lean-toolchains" - "copy|sourceDirs|Beam|Beam" - "copy|runtimePaths|.lake/build/bin/beam-cli|libexec/beam-cli" - "copy|runtimePaths|.lake/build/bin/beam-daemon|libexec/beam-daemon" - "copy|runtimePaths|.lake/build/bin/beam-client|libexec/beam-client" - "copy|runtimePaths|.lake/build/bin/lean-beam-mcp|libexec/lean-beam-mcp" - "copy|runtimePaths|.lake/build/lib/$beam_lsp_plugin_shared_lib|libexec/$beam_lsp_plugin_shared_lib" - "copy|runtimePaths|.lake/packages|.lake/packages" - "copy|wrapperPaths|scripts/lean-beam|bin/lean-beam" - "copy|wrapperPaths|scripts/lean-beam-search|bin/lean-beam-search" - "copy|wrapperPaths|scripts/lean-beam-mcp|bin/lean-beam-mcp" + "required|sourceDirs|Beam|Beam" + "required|runtimePaths|.lake/build/bin/beam-cli|libexec/beam-cli" + "required|runtimePaths|.lake/build/bin/beam-daemon|libexec/beam-daemon" + "required|runtimePaths|.lake/build/bin/beam-client|libexec/beam-client" + "required|runtimePaths|.lake/build/bin/lean-beam-mcp|libexec/lean-beam-mcp" + "required|runtimePaths|.lake/build/lib/$beam_lsp_plugin_shared_lib|libexec/$beam_lsp_plugin_shared_lib" + "required|wrapperPaths|scripts/lean-beam|bin/lean-beam" + "required|wrapperPaths|scripts/lean-beam-search|bin/lean-beam-search" + "required|wrapperPaths|scripts/lean-beam-mcp|bin/lean-beam-mcp" ) usage() { @@ -327,13 +327,75 @@ require_owned_staging_dir() { esac } -ensure_replaceable_path() { - local path="$1" - local root="$2" - local label="$3" - require_path_within "$path" "$root" "$label" - if [ -d "$path" ] && [ ! -L "$path" ]; then - die "refusing to replace directory at $path" +validate_install_root_marker() { + local marker="$install_root/$install_root_marker" + local field="" + local marked_root="" + local marked_root_count=0 + local schema_count=0 + local schema_valid=0 + local owner_count=0 + local owner_valid=0 + local resolved_install_root="" + local resolved_marked_root="" + + if [ -L "$marker" ] || [ ! -f "$marker" ]; then + die "refusing to use non-file Beam install root marker: $marker" + fi + while IFS= read -r field || [ -n "$field" ]; do + case "$field" in + schema=*) + schema_count=$((schema_count + 1)) + if [ "$field" = "schema=1" ]; then + schema_valid=$((schema_valid + 1)) + fi + ;; + owner=*) + owner_count=$((owner_count + 1)) + if [ "$field" = "owner=lean-beam" ]; then + owner_valid=$((owner_valid + 1)) + fi + ;; + root=*) + marked_root_count=$((marked_root_count + 1)) + if [ "$marked_root_count" -eq 1 ]; then + marked_root="${field#root=}" + fi + ;; + esac + done <"$marker" + if [ "$schema_count" -eq 0 ]; then + die "refusing to use Beam install root marker without schema=1: $marker" + fi + if [ "$schema_count" -ne 1 ] || [ "$schema_valid" -ne 1 ]; then + die "refusing to use Beam install root marker with invalid schema fields: $marker" + fi + if [ "$owner_count" -eq 0 ]; then + die "refusing to use Beam install root marker without owner=lean-beam: $marker" + fi + if [ "$owner_count" -ne 1 ] || [ "$owner_valid" -ne 1 ]; then + die "refusing to use Beam install root marker with invalid owner fields: $marker" + fi + if [ "$marked_root_count" -eq 0 ] || [ -z "$marked_root" ]; then + die "refusing to use Beam install root marker without root: $marker" + fi + if [ "$marked_root_count" -ne 1 ]; then + die "refusing to use Beam install root marker with multiple roots: $marker" + fi + case "$marked_root" in + /*) + ;; + *) + die "refusing to use Beam install root marker with non-absolute root: $marker" + ;; + esac + if [ ! -d "$marked_root" ]; then + die "refusing to use Beam install root marker with missing root: $marker" + fi + resolved_install_root="$(cd -P "$install_root" && pwd)" + resolved_marked_root="$(cd -P "$marked_root" && pwd)" + if [ "$resolved_install_root" != "$resolved_marked_root" ]; then + die "refusing to use Beam install root marker naming a different root: $marker" fi } @@ -349,7 +411,8 @@ ensure_install_root_claimable() { if [ ! -d "$install_root" ]; then die "refusing to use non-directory install root: $install_root" fi - if [ -f "$install_root/$install_root_marker" ]; then + if [ -e "$install_root/$install_root_marker" ] || [ -L "$install_root/$install_root_marker" ]; then + validate_install_root_marker return 0 fi while IFS= read -r entry; do @@ -367,7 +430,8 @@ ensure_install_root_claimable() { write_install_root_marker() { local marker="$install_root/$install_root_marker" - if [ -f "$marker" ]; then + if [ -e "$marker" ] || [ -L "$marker" ]; then + validate_install_root_marker return 0 fi confirm_path_edit "mark Beam install root as installer-owned" "$marker" @@ -387,22 +451,33 @@ ensure_install_root_ready() { } release_install_lock() { - if [ -d "$install_lock_dir" ] && [ -f "$install_lock_dir/pid" ]; then - rm -f -- "$install_lock_dir/pid" - rmdir "$install_lock_dir" 2>/dev/null || true + if [ "$install_lock_owned" -eq 1 ]; then + if [ -d "$install_lock_dir" ]; then + rm -f -- "$install_lock_dir/pid" + rmdir "$install_lock_dir" 2>/dev/null || true + fi + install_lock_owned=0 fi } acquire_install_lock() { require_path_within "$install_lock_dir" "$install_root" "install lock" if mkdir "$install_lock_dir"; then - printf '%s\n' "$$" >"$install_lock_dir/pid" + install_lock_owned=1 trap 'release_install_lock' EXIT + printf '%s\n' "$$" >"$install_lock_dir/pid" else die "another Beam install appears to be running: $install_lock_dir" fi } +cleanup_failed_install() { + release_install_lock + if [ -n "$active_staging_root" ]; then + remove_owned_staging_dir "$active_staging_root" + fi +} + symlink_target_text() { local link_path="$1" local target="" @@ -445,16 +520,17 @@ remove_owned_staging_dir() { rm -rf -- "$path" } -copy_repo_path_if_present() { +copy_required_repo_path() { local src="$1" local dest="$2" local dest_root="$3" require_path_within "$src" "$repo_root" "copy source" require_path_within "$dest" "$dest_root" "copy destination" - if [ -e "$src" ]; then - ensure_dir_for_install "$(dirname "$dest")" "copy destination parent" - cp -Rp "$src" "$dest" + if [ ! -e "$src" ] && [ ! -L "$src" ]; then + die "missing required runtime payload source: $src" fi + ensure_dir_for_install "$(dirname "$dest")" "copy destination parent" + cp -Rp "$src" "$dest" } move_staging_dir_into_versions() { @@ -1050,27 +1126,77 @@ print_install_plan() { fi } -hash_tree() { +hash_runtime_payload() { local root="$1" local tool tool="$(hash_tool)" if [ "$tool" = "sha256sum" ]; then ( cd "$root" - find . -type f -print | LC_ALL=C sort | while IFS= read -r rel; do + find . -type f ! -path './manifest.json' -print | LC_ALL=C sort | while IFS= read -r rel; do sha256sum "$rel" done | sha256sum | awk '{print $1}' ) else ( cd "$root" - find . -type f -print | LC_ALL=C sort | while IFS= read -r rel; do + find . -type f ! -path './manifest.json' -print | LC_ALL=C sort | while IFS= read -r rel; do shasum -a 256 "$rel" done | shasum -a 256 | awk '{print $1}' ) fi } +validate_runtime_payload_layout() { + local root="$1" + local entry="" + local category="" + local dest_rel="" + local path="" + for entry in ${runtime_payload_spec[@]+"${runtime_payload_spec[@]}"}; do + IFS='|' read -r _ category _ dest_rel <<< "$entry" + path="$root/$dest_rel" + case "$category" in + sourceDirs) + if [ -L "$path" ] || [ ! -d "$path" ]; then + die "installed runtime is missing required source directory: $path" + fi + ;; + rootFiles|runtimePaths|wrapperPaths) + if [ -L "$path" ] || [ ! -f "$path" ]; then + die "installed runtime is missing required regular file: $path" + fi + ;; + *) + die "unknown runtime payload category: $category" + ;; + esac + case "$dest_rel" in + libexec/beam-cli|libexec/beam-daemon|libexec/beam-client|libexec/lean-beam-mcp|bin/lean-beam|bin/lean-beam-search|bin/lean-beam-mcp) + if [ ! -x "$path" ]; then + die "installed runtime has a non-executable command: $path" + fi + ;; + esac + done + if [ -L "$root/manifest.json" ] || [ ! -f "$root/manifest.json" ]; then + die "installed runtime manifest must be a regular non-symlinked file: $root/manifest.json" + fi +} + +validate_runtime_version_for_reuse() { + local version_root="$1" + local expected_payload_id="$2" + local actual_payload_id="" + require_path_within "$version_root" "$versions_root" "installed runtime version" + "$beam_cli" install-runtime-validate "$version_root" + validate_runtime_payload_layout "$version_root" + actual_payload_id="$(hash_runtime_payload "$version_root")" + if [ "$actual_payload_id" != "$expected_payload_id" ]; then + die "refusing to reuse installed Beam runtime whose contents do not match its payload hash: $version_root; stop active Beam clients, move this exact runtime aside for inspection, and rerun the installer" + fi +} + ensure_runtime_artifacts() { confirm_path_edit "build Beam runtime artifacts in the source checkout" "$repo_root/.lake/build" echo "building beam runtime artifacts" >&2 @@ -1113,8 +1239,8 @@ stage_runtime_tree() { for entry in ${runtime_payload_spec[@]+"${runtime_payload_spec[@]}"}; do IFS='|' read -r mode _ src_rel dest_rel <<< "$entry" case "$mode" in - copy) - copy_repo_path_if_present "$repo_root/$src_rel" "$dest/$dest_rel" "$dest" + required) + copy_required_repo_path "$repo_root/$src_rel" "$dest/$dest_rel" "$dest" ;; generated) case "$dest_rel" in @@ -1137,11 +1263,6 @@ stage_runtime_tree() { done } -stage_install_version() { - local dest="$1" - stage_runtime_tree "$dest" -} - write_install_manifest() { local dest="$1" local payload_id="$2" @@ -1271,8 +1392,8 @@ prepare_install_environment() { prepare_install_version() { local staging_root="$1" - stage_install_version "$staging_root" - prepared_payload_id="$(hash_tree "$staging_root")" + stage_runtime_tree "$staging_root" + prepared_payload_id="$(hash_runtime_payload "$staging_root")" prepared_version_root="$versions_root/$prepared_payload_id" prepared_source_commit="$(repo_source_commit)" write_install_manifest \ @@ -1280,21 +1401,13 @@ prepare_install_version() { "$prepared_payload_id" \ "$prepared_source_commit" \ ${prepared_selected_toolchains[@]+"${prepared_selected_toolchains[@]}"} - if [ ! -d "$prepared_version_root" ]; then - move_staging_dir_into_versions "$staging_root" "$prepared_version_root" - else - if [ ! -f "$prepared_version_root/manifest.json" ]; then - die "refusing to reuse unmarked existing version directory: $prepared_version_root" - fi + if [ -d "$prepared_version_root" ]; then + validate_runtime_version_for_reuse "$prepared_version_root" "$prepared_payload_id" remove_owned_staging_dir "$staging_root" + return 0 fi - if [ ! -f "$prepared_version_root/manifest.json" ]; then - write_install_manifest \ - "$prepared_version_root/manifest.json" \ - "$prepared_payload_id" \ - "$prepared_source_commit" \ - ${prepared_selected_toolchains[@]+"${prepared_selected_toolchains[@]}"} - fi + move_staging_dir_into_versions "$staging_root" "$prepared_version_root" + validate_runtime_version_for_reuse "$prepared_version_root" "$prepared_payload_id" } prebuild_install_bundles() { @@ -1550,17 +1663,16 @@ print_install_summary() { } main() { - local staging_root="" setup_styles parse_args "$@" validate_install_config prepare_install_environment confirm_path_edit "create Beam staging directory" "$install_root/.staging-XXXXXX" - staging_root="$(mktemp -d "$install_root/.staging-XXXXXX")" - trap 'remove_owned_staging_dir "$staging_root"; release_install_lock' EXIT - prepare_install_version "$staging_root" - staging_root="" + active_staging_root="$(mktemp -d "$install_root/.staging-XXXXXX")" + trap 'cleanup_failed_install' EXIT + prepare_install_version "$active_staging_root" + active_staging_root="" trap 'release_install_lock' EXIT prebuild_install_bundles "$prepared_version_root" ${prepared_selected_toolchains[@]+"${prepared_selected_toolchains[@]}"} diff --git a/scripts/lean-beam b/scripts/lean-beam index c757ef75..b2e7468b 100755 --- a/scripts/lean-beam +++ b/scripts/lean-beam @@ -34,6 +34,7 @@ usage: lean-beam [--root PATH] [--port N] rocq-goals-after [text...] lean-beam [--root PATH] [--port N] rocq-goals-prev [text...] lean-beam [--root PATH] feedback --stdin|--input [--bundle none|dir|zip] [--output-dir ] [--no-redact] + lean-beam prune [--apply] [--bundles] lean-beam validated-toolchains [lean] lean-beam compatible-release-lines lean-beam [--root PATH] doctor [lean|rocq] @@ -54,6 +55,8 @@ notes: - 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 - validated-toolchains lists exact CI-validated versions; compatible-release-lines lists canonical RC/patch families qualified locally + - prune previews old installed runtimes; restart active agents and MCP clients before using --apply + - prune --bundles also selects stale installed bundle-cache entries - use `lean-beam feedback` with JSON object input to produce a pasteable Beam report card with debug context EOF } @@ -225,6 +228,9 @@ case "$cmd" in mapped=("lean-close-save") display_cmd="$cmd" ;; + prune) + mapped=("install-prune") + ;; ensure) if [ "${#rest[@]}" -eq 0 ]; then mapped=("ensure" "lean") diff --git a/skills/lean-beam/SKILL.md b/skills/lean-beam/SKILL.md index fb568207..d2c380c6 100644 --- a/skills/lean-beam/SKILL.md +++ b/skills/lean-beam/SKILL.md @@ -38,7 +38,17 @@ Use `lean-beam --version` for CLI bug reports and installed runtime identity che `lean-beam-mcp --version` to verify which installed MCP server wrapper, server binary, runtime payload hash, manifest, and source commit a client command resolves. Source checkout runs also report git commit/branch/dirty state when available. From a live MCP session, call `beam_version` -to report the running server process identity as structured content. +to report the running server process identity as structured content. Installed identities include +`runtime_current`; if a live session reports `false` after reinstalling, restart the agent or MCP +client so it launches the current runtime. If a newly resolved installed wrapper still reports +`false`, the install root's `current` link is missing or broken; stop normal Beam work and reinstall. +If an installed identity reports `runtime_error`, do not treat it as a source checkout or try to +clean it with `lean-beam prune`. After stopping active Beam agents and MCP clients, move an invalid +manifest runtime out of `BEAM_INSTALL_ROOT/versions`, preserve it for inspection, and rerun the +installer. For an invalid install-root marker, preserve and rename the exact `BEAM_INSTALL_ROOT` as +a unit before reinstalling; do not recreate its ownership marker in place or delete the preserved +state. + `lean_init_workspace` with `mode: "reset"` restarts the Lean runtime inside the current MCP server process; it does not prove the MCP server binary itself was refreshed. @@ -280,6 +290,8 @@ Use `lean-beam`, not raw JSON and not raw LSP. `lean-beam compatible-release-lines`, and `lean-beam doctor` to inspect the decision - restarts the Beam daemon if the effective Lean startup configuration for that root changes - `lean-beam shutdown`, `lean-beam stats`, and `lean-beam reset-stats` apply to the current project only +- `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, keeps the wrapper process alive until interrupted, and is only for environments that reap background daemons when diff --git a/tests/lean/BeamTest/Broker/CliDaemonTest.lean b/tests/lean/BeamTest/Broker/CliDaemonTest.lean index 5eba9ed1..cf2e16b2 100644 --- a/tests/lean/BeamTest/Broker/CliDaemonTest.lean +++ b/tests/lean/BeamTest/Broker/CliDaemonTest.lean @@ -750,18 +750,22 @@ private def checkLeanModuleNamePathHelpers : IO Unit := do require "outside rooted Lean path should not become module name" (Beam.leanModuleNameForPath? root (p "/tmp/other-root/Foo.lean") == none) +private def createSymlink + (label : String) (target link : System.FilePath) : IO Unit := do + let out ← IO.Process.output { + cmd := "ln" + args := #["-s", target.toString, link.toString] + } + if out.exitCode != 0 then + throw <| IO.userError s!"failed to create {label} symlink\n{out.stderr}" + 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}" try IO.FS.createDirAll root - let out ← IO.Process.output { - cmd := "ln" - args := #["-s", root.toString, alias.toString] - } - if out.exitCode != 0 then - throw <| IO.userError s!"failed to create symlink alias for path canonicalization test\n{out.stderr}" + createSymlink "path canonicalization fixture" root alias 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" @@ -799,6 +803,17 @@ private def checkLockLifecycle : IO Unit := do expectIoErrorContains "live lock timeout" s!"lock owner: pid {selfPid}" <| Beam.Cli.withLockTimeout lockDir 100 do pure () + IO.FS.removeDirAll lockDir + + let deadPidTarget := root / "dead-pid" + IO.FS.writeFile deadPidTarget "999999999\n" + IO.FS.createDirAll lockDir + createSymlink "lock PID fixture" deadPidTarget (lockDir / "pid") + expectIoErrorContains "symlinked lock PID timeout" "lock owner: unknown owner" <| + Beam.Cli.withLockTimeout lockDir 100 do + pure () + require "a lock with a non-regular PID file should not be removed as stale" + (← lockDir.pathExists) finally try if ← root.pathExists then @@ -1021,17 +1036,57 @@ private def checkRuntimeBundleMetadataAcceptance : IO Unit := do require "bundle should reject stale toolchain fingerprint metadata" (!(← Beam.Cli.bundleReady bundleDir toolchain sourceHash sampleFingerprint)) + writeBundleMetadataFile bundleDir toolchain sourceHash sampleFingerprint (root / "elsewhere") + require "bundle should reject metadata for a different workspace" + (!(← Beam.Cli.bundleReady bundleDir toolchain sourceHash sampleFingerprint)) + require "bundle with mismatched workspace should not expose a source hash" + ((← Beam.Cli.completeBundleSourceHash? bundleDir).isNone) + writeBundleMetadataFile bundleDir toolchain sourceHash sampleFingerprint workspace require "bundle should accept matching artifacts and metadata" (← Beam.Cli.bundleReady bundleDir toolchain sourceHash sampleFingerprint) - writeBundleMetadataFile bundleDir toolchain sourceHash sampleFingerprint (System.FilePath.mk <| "/private" ++ workspace.toString) + writeBundleMetadataFile bundleDir toolchain sourceHash sampleFingerprint (workspace / ".") require "bundle should accept metadata with equivalent diagnostic workspace spelling" (← Beam.Cli.bundleReady bundleDir toolchain sourceHash sampleFingerprint) - IO.FS.removeFile (Beam.Cli.bundlePathsFor workspace).client + require "complete bundle source hash should use typed ready metadata" + ((← Beam.Cli.completeBundleSourceHash? bundleDir) == some sourceHash) + + let metadataPath := Beam.Cli.bundleMetadataPath bundleDir + let metadataTarget := root / "metadata-symlink-target.json" + IO.FS.writeFile metadataTarget (← IO.FS.readFile metadataPath) + IO.FS.removeFile metadataPath + createSymlink "bundle metadata fixture" metadataTarget metadataPath + require "bundle should reject symlinked metadata" + (!(← Beam.Cli.bundleReady bundleDir toolchain sourceHash sampleFingerprint)) + require "bundle with symlinked metadata should not expose a source hash" + ((← Beam.Cli.completeBundleSourceHash? bundleDir).isNone) + IO.FS.removeFile metadataPath + writeBundleMetadataFile bundleDir toolchain sourceHash sampleFingerprint workspace + + let client := (Beam.Cli.bundlePathsFor workspace).client + IO.FS.removeFile client + IO.FS.createDir client + require "bundle should reject a required artifact path that is a directory" + (!(← Beam.Cli.bundleReady bundleDir toolchain sourceHash sampleFingerprint)) + require "bundle with a directory artifact should not expose a source hash" + ((← Beam.Cli.completeBundleSourceHash? bundleDir).isNone) + IO.FS.removeDir client + + let symlinkTarget := root / "client-symlink-target" + IO.FS.writeFile symlinkTarget "fake artifact\n" + createSymlink "bundle artifact fixture" symlinkTarget client + require "bundle should reject a symlinked required artifact" + (!(← Beam.Cli.bundleReady bundleDir toolchain sourceHash sampleFingerprint)) + require "bundle with a symlinked artifact should not expose a source hash" + ((← Beam.Cli.completeBundleSourceHash? bundleDir).isNone) + IO.FS.removeFile client + require "bundle should reject matching metadata without required artifacts" (!(← Beam.Cli.bundleReady bundleDir toolchain sourceHash sampleFingerprint)) + require "incomplete bundle should not expose a source hash" + ((← Beam.Cli.completeBundleSourceHash? bundleDir).isNone) finally try if ← root.pathExists then diff --git a/tests/lean/BeamTest/Broker/FeedbackTest.lean b/tests/lean/BeamTest/Broker/FeedbackTest.lean index 70421010..6b253f7c 100644 --- a/tests/lean/BeamTest/Broker/FeedbackTest.lean +++ b/tests/lean/BeamTest/Broker/FeedbackTest.lean @@ -42,7 +42,9 @@ private def sampleCollection (home : String) : Beam.Feedback.Collection := { ("source_commit", toJson "0123456789abcdef"), ("source_branch", toJson "feedback"), ("source_dirty", toJson true), - ("runtime_active", toJson true) + ("runtime_active", toJson true), + ("runtime_current", toJson false), + ("runtime_error", toJson "invalid install manifest") ]), ("stats", Json.mkObj [("requests", toJson (3 : Nat))]), ("openFiles", Json.arr #[Json.mkObj [("path", toJson s!"{home}/project/Demo.lean")]]), @@ -63,6 +65,10 @@ private def checkRenderAndRedaction : IO Unit := do require "report card summary includes kind" (result.markdown.contains "- Kind: `bug`") require "report card summary includes severity" (result.markdown.contains "- Severity: `high`") require "report card runtime section" (result.markdown.contains "## Beam Runtime") + require "report card runtime section includes stale installed runtime" + (result.markdown.contains "- runtime current: `false`") + require "report card runtime section includes installed runtime error" + (result.markdown.contains "- runtime error: `invalid install manifest`") require "report card runtime section includes source" (result.markdown.contains "commit 0123456789ab") require "report card debug context section" (result.markdown.contains "## Beam Debug Context") require "report card should render collection warnings" diff --git a/tests/lean/BeamTest/Broker/McpProtocolTest.lean b/tests/lean/BeamTest/Broker/McpProtocolTest.lean index 925c3fcc..bb6e966a 100644 --- a/tests/lean/BeamTest/Broker/McpProtocolTest.lean +++ b/tests/lean/BeamTest/Broker/McpProtocolTest.lean @@ -145,6 +145,20 @@ private def checkIncoming : IO Unit := do | .ok _ => throw <| IO.userError s!"invalid response decoded: {invalidResponse.compress}" | .error _ => pure () +private def checkVersionIdentityJson : IO Unit := do + let current := Beam.Version.Identity.asJson { + name := "identity-fixture" + runtimeCurrent? := some true + } + requireJsonBool "runtime identity json" "runtime_current" true current + let source := Beam.Version.Identity.asJson { name := "source-fixture" } + requireFieldAbsent "source identity json" "runtime_current" source + let invalid := Beam.Version.Identity.asJson { + name := "invalid-installed-fixture" + runtimeError? := some "invalid install manifest" + } + requireJsonString "invalid runtime identity json" "runtime_error" "invalid install manifest" invalid + private def requireJsonArray (label : String) : Json → IO (Array Json) | Json.arr values => pure values | other => throw <| IO.userError s!"{label} is not an array: {other.compress}" @@ -1033,6 +1047,7 @@ private def checkDiagnosticLogForwarding : IO Unit := do def main : IO Unit := do checkJsonHelpers + checkVersionIdentityJson checkIncoming checkToolsListShape checkRootsProtocol diff --git a/tests/lib/beam-wrapper-common.sh b/tests/lib/beam-wrapper-common.sh index 4a82d4e4..f6093f24 100644 --- a/tests/lib/beam-wrapper-common.sh +++ b/tests/lib/beam-wrapper-common.sh @@ -37,10 +37,6 @@ beam_wrapper_require_bins() { fi } -beam_wrapper_realpath() { - python3 -c 'import os,sys; print(os.path.realpath(sys.argv[1]))' "$1" -} - read_json_field() { python3 - "$1" "$2" <<'PY' import json, sys diff --git a/tests/lib/tmp-guards.sh b/tests/lib/tmp-guards.sh index 6808e282..6fb49802 100644 --- a/tests/lib/tmp-guards.sh +++ b/tests/lib/tmp-guards.sh @@ -4,6 +4,10 @@ # Released under Apache 2.0 license as described in the file LICENSE. # Author: Emilio J. Gallego Arias +beam_test_realpath() { + python3 -c 'import os,sys; print(os.path.realpath(sys.argv[1]))' "$1" +} + beam_test_tmp_prefix_matches() { if [ "$#" -lt 2 ]; then return 1 diff --git a/tests/test-beam-install.sh b/tests/test-beam-install.sh index a4fc62f2..975cd24d 100644 --- a/tests/test-beam-install.sh +++ b/tests/test-beam-install.sh @@ -40,6 +40,8 @@ export BEAM_INSTALL_ROOT="$tmp_root/install-root" mkdir -p "$HOME" "$BEAM_INSTALL_ROOT" +run_step "install prune" bash tests/test-beam-prune.sh + validated_toolchains=() while IFS= read -r line; do [ -n "$line" ] || continue @@ -75,8 +77,8 @@ assert_symlink_target() { local path="$1" local expected="$2" local actual resolved_expected - actual="$(python3 -c 'import os,sys; print(os.path.realpath(sys.argv[1]))' "$path")" - resolved_expected="$(python3 -c 'import os,sys; print(os.path.realpath(sys.argv[1]))' "$expected")" + actual="$(beam_test_realpath "$path")" + resolved_expected="$(beam_test_realpath "$expected")" if [ "$actual" != "$resolved_expected" ]; then echo "unexpected symlink target for $path: expected $resolved_expected, got $actual" >&2 exit 1 @@ -120,14 +122,16 @@ with open(manifest_path, "r", encoding="utf-8") as f: manifest = json.load(f) layout = json.loads(os.environ["BEAM_INSTALL_LAYOUT_JSON"]) -if manifest.get("schemaVersion") != 2: +if manifest.get("schemaVersion") != 3: raise SystemExit(f"unexpected manifest schemaVersion: {manifest.get('schemaVersion')}") if manifest.get("payloadHash") != expected_payload: raise SystemExit(f"unexpected manifest payloadHash: {manifest.get('payloadHash')}") -if manifest.get("toolchains") != expected_toolchains: - raise SystemExit(f"unexpected manifest toolchains: {manifest.get('toolchains')}") -if "toolchain" in manifest: - raise SystemExit(f"unexpected obsolete manifest toolchain field: {manifest.get('toolchain')}") +if manifest.get("createdWithToolchains") != expected_toolchains: + raise SystemExit( + f"unexpected manifest createdWithToolchains: {manifest.get('createdWithToolchains')}" + ) +if "toolchain" in manifest or "toolchains" in manifest: + raise SystemExit("manifest contains an obsolete toolchain field") actual_source_commit = manifest.get("sourceCommit", None) if expected_source_commit: if actual_source_commit != expected_source_commit: @@ -158,6 +162,20 @@ if set(runtime_paths or []) != expected_runtime_paths: raise SystemExit(f"unexpected manifest runtimePaths: {runtime_paths}") if set(wrapper_paths or []) != expected_wrapper_paths: raise SystemExit(f"unexpected manifest wrapperPaths: {wrapper_paths}") + +runtime_root = os.path.dirname(manifest_path) +for rel in root_files or []: + path = os.path.join(runtime_root, rel) + if not os.path.isfile(path) or os.path.islink(path): + raise SystemExit(f"manifest rootFiles entry is not a regular runtime file: {path}") +for rel in source_dirs or []: + path = os.path.join(runtime_root, rel) + if not os.path.isdir(path) or os.path.islink(path): + raise SystemExit(f"manifest sourceDirs entry is not a runtime directory: {path}") +for rel in (runtime_paths or []) + (wrapper_paths or []): + path = os.path.join(runtime_root, rel) + if not os.path.isfile(path) or os.path.islink(path): + raise SystemExit(f"manifest executable/file entry is not a regular runtime file: {path}") PY } @@ -251,6 +269,28 @@ run_install_from_source() { ) } +assert_install_rejects_marker() { + local label="$1" + local install_root="$2" + local expected="$3" + local marker_err="$tmp_root/${label}.err" + local marker_home="$tmp_root/${label}-home" + mkdir -p "$marker_home" + if ( + cd "$source_checkout" + HOME="$marker_home" BEAM_INSTALL_ROOT="$install_root" \ + bash scripts/install-beam.sh --dont-ask --toolchain "$toolchain" \ + > /dev/null 2>"$marker_err" + ); then + echo "expected install to reject $label" >&2 + cat "$marker_err" >&2 + exit 1 + fi + assert_contains_literal "$marker_err" "$expected" + assert_not_exists "$install_root/versions" + remove_tmp_file "$marker_err" +} + rsync -a --exclude='.git' ./ "$source_checkout"/ path_no_elan="$(path_without_elan)" if PATH="$path_no_elan" command -v elan >/dev/null 2>&1; then @@ -302,6 +342,109 @@ fi remove_tmp_file "$relative_root_err" assert_not_exists "$source_checkout/relative" +missing_owner_root="$tmp_root/install-marker-missing-owner" +mkdir -p "$missing_owner_root" +printf '%s\n' \ + 'schema=1' \ + "root=$missing_owner_root" >"$missing_owner_root/.lean-beam-install-root" +assert_install_rejects_marker \ + "install marker missing owner" \ + "$missing_owner_root" \ + 'refusing to use Beam install root marker without owner=lean-beam' + +missing_marker_root="$tmp_root/install-marker-missing-root" +mkdir -p "$missing_marker_root" +printf '%s\n' \ + 'schema=1' \ + 'owner=lean-beam' >"$missing_marker_root/.lean-beam-install-root" +assert_install_rejects_marker \ + "install marker missing root" \ + "$missing_marker_root" \ + 'refusing to use Beam install root marker without root' + +mismatched_marker_root="$tmp_root/install-marker-mismatched-root" +other_marker_root="$tmp_root/install-marker-other-root" +mkdir -p "$mismatched_marker_root" "$other_marker_root" +printf '%s\n' \ + 'schema=1' \ + 'owner=lean-beam' \ + "root=$other_marker_root" >"$mismatched_marker_root/.lean-beam-install-root" +assert_install_rejects_marker \ + "install marker mismatched root" \ + "$mismatched_marker_root" \ + 'refusing to use Beam install root marker naming a different root' + +relative_marker_root="$tmp_root/install-marker-relative-root" +mkdir -p "$relative_marker_root" +printf '%s\n' \ + 'schema=1' \ + 'owner=lean-beam' \ + 'root=.' >"$relative_marker_root/.lean-beam-install-root" +assert_install_rejects_marker \ + "install marker relative root" \ + "$relative_marker_root" \ + 'refusing to use Beam install root marker with non-absolute root' + +blank_marker_root="$tmp_root/install-marker-blank-root" +mkdir -p "$blank_marker_root" +printf '%s\n' \ + 'schema=1' \ + 'owner=lean-beam' \ + 'root=' >"$blank_marker_root/.lean-beam-install-root" +assert_install_rejects_marker \ + "install marker blank root" \ + "$blank_marker_root" \ + 'refusing to use Beam install root marker without root' + +multiple_marker_root="$tmp_root/install-marker-multiple-roots" +mkdir -p "$multiple_marker_root" +printf '%s\n' \ + 'schema=1' \ + 'owner=lean-beam' \ + "root=$multiple_marker_root" \ + "root=$multiple_marker_root" >"$multiple_marker_root/.lean-beam-install-root" +assert_install_rejects_marker \ + "install marker multiple roots" \ + "$multiple_marker_root" \ + 'refusing to use Beam install root marker with multiple roots' + +conflicting_schema_marker_root="$tmp_root/install-marker-conflicting-schema" +mkdir -p "$conflicting_schema_marker_root" +printf '%s\n' \ + 'schema=1' \ + 'schema=2' \ + 'owner=lean-beam' \ + "root=$conflicting_schema_marker_root" >"$conflicting_schema_marker_root/.lean-beam-install-root" +assert_install_rejects_marker \ + "install marker conflicting schema" \ + "$conflicting_schema_marker_root" \ + 'refusing to use Beam install root marker with invalid schema fields' + +conflicting_owner_marker_root="$tmp_root/install-marker-conflicting-owner" +mkdir -p "$conflicting_owner_marker_root" +printf '%s\n' \ + 'schema=1' \ + 'owner=lean-beam' \ + 'owner=other' \ + "root=$conflicting_owner_marker_root" >"$conflicting_owner_marker_root/.lean-beam-install-root" +assert_install_rejects_marker \ + "install marker conflicting owner" \ + "$conflicting_owner_marker_root" \ + 'refusing to use Beam install root marker with invalid owner fields' + +symlink_marker_root="$tmp_root/install-marker-symlink" +symlink_marker_target="$tmp_root/install-marker-symlink-target" +mkdir -p "$symlink_marker_root" +printf '%s\n' \ + 'schema=1' \ + 'owner=lean-beam' \ + "root=$symlink_marker_root" >"$symlink_marker_target" +ln -s "$symlink_marker_target" "$symlink_marker_root/.lean-beam-install-root" +assert_install_rejects_marker \ + "install marker symlink" \ + "$symlink_marker_root" \ + 'refusing to use non-file Beam install root marker' + unsupported_install_err="$(mktemp "$tmp_root/install-unsupported-toolchain-XXXXXX")" if ( cd "$source_checkout" @@ -594,7 +737,7 @@ assert_not_exists "$HOME/.local/bin/beam-lean-search" assert_runtime_layout "$installed_runtime_root" assert_file "$BEAM_INSTALL_ROOT/.lean-beam-install-root" assert_version_count "$BEAM_INSTALL_ROOT/versions" 1 -installed_version_root="$(python3 -c 'import os,sys; print(os.path.realpath(sys.argv[1]))' "$installed_runtime_root")" +installed_version_root="$(beam_test_realpath "$installed_runtime_root")" installed_payload_id="$(basename "$installed_version_root")" assert_file "$installed_runtime_root/manifest.json" BEAM_INSTALL_LAYOUT_JSON="$install_layout_json" assert_manifest_metadata "$installed_runtime_root/manifest.json" "$installed_payload_id" "$expected_source_commit" "$toolchain" @@ -605,6 +748,7 @@ assert_output_contains "installed lean-beam --version" "$installed_lean_beam_ver assert_output_contains "installed lean-beam --version" "$installed_lean_beam_version" "beam cli: $installed_version_root/libexec/beam-cli" assert_output_contains "installed lean-beam --version" "$installed_lean_beam_version" "runtime payload: $installed_payload_id" assert_output_contains "installed lean-beam --version" "$installed_lean_beam_version" "manifest: $installed_version_root/manifest.json" +assert_output_contains "installed lean-beam --version" "$installed_lean_beam_version" "runtime current: true" if [ -n "$expected_source_commit" ]; then assert_output_contains "installed lean-beam --version" "$installed_lean_beam_version" "source commit: $expected_source_commit" fi @@ -616,10 +760,105 @@ assert_output_contains "installed lean-beam-mcp --version" "$installed_mcp_versi assert_output_contains "installed lean-beam-mcp --version" "$installed_mcp_version" "beam cli: $installed_version_root/libexec/beam-cli" assert_output_contains "installed lean-beam-mcp --version" "$installed_mcp_version" "runtime payload: $installed_payload_id" assert_output_contains "installed lean-beam-mcp --version" "$installed_mcp_version" "manifest: $installed_version_root/manifest.json" +assert_output_contains "installed lean-beam-mcp --version" "$installed_mcp_version" "runtime current: true" if [ -n "$expected_source_commit" ]; then assert_output_contains "installed lean-beam-mcp --version" "$installed_mcp_version" "source commit: $expected_source_commit" fi +reuse_guard_backup="$tmp_root/runtime-reuse-Beam.lean" +reuse_guard_err="$tmp_root/runtime-reuse.err" +cp "$installed_version_root/Beam.lean" "$reuse_guard_backup" +printf '\n-- corrupt installed runtime reuse fixture\n' >>"$installed_version_root/Beam.lean" +if run_install_from_source --toolchain "$toolchain" 2>"$reuse_guard_err"; then + mv "$reuse_guard_backup" "$installed_version_root/Beam.lean" + echo "expected reinstall to reject a corrupted content-addressed runtime" >&2 + exit 1 +fi +mv "$reuse_guard_backup" "$installed_version_root/Beam.lean" +assert_contains_literal "$reuse_guard_err" \ + 'refusing to reuse installed Beam runtime whose contents do not match its payload hash' +assert_symlink_target "$installed_runtime_root" "$installed_version_root" +assert_version_count "$BEAM_INSTALL_ROOT/versions" 1 +assert_not_exists "$BEAM_INSTALL_ROOT/.install-lock" +remove_tmp_file "$reuse_guard_err" + +reuse_mode_err="$tmp_root/runtime-reuse-mode.err" +chmod -x "$installed_version_root/libexec/beam-cli" +if run_install_from_source --toolchain "$toolchain" 2>"$reuse_mode_err"; then + chmod +x "$installed_version_root/libexec/beam-cli" + echo "expected reinstall to reject a runtime with a non-executable command" >&2 + exit 1 +fi +chmod +x "$installed_version_root/libexec/beam-cli" +assert_contains_literal "$reuse_mode_err" \ + 'installed runtime has a non-executable command:' +assert_symlink_target "$installed_runtime_root" "$installed_version_root" +assert_version_count "$BEAM_INSTALL_ROOT/versions" 1 +assert_not_exists "$BEAM_INSTALL_ROOT/.install-lock" +remove_tmp_file "$reuse_mode_err" + +reuse_legacy_manifest_backup="$tmp_root/runtime-reuse-legacy-manifest.json" +reuse_legacy_manifest_err="$tmp_root/runtime-reuse-legacy-manifest.err" +cp "$installed_version_root/manifest.json" "$reuse_legacy_manifest_backup" +python3 - "$installed_version_root/manifest.json" <<'PY' +import json +import sys + +path = sys.argv[1] +with open(path, encoding="utf-8") as stream: + manifest = json.load(stream) +manifest["schemaVersion"] = 2 +manifest["toolchains"] = manifest.pop("createdWithToolchains") +# Recreate the final layout that Beam actually emitted under schema 2. +artifacts = manifest["artifacts"] +artifacts["rootFiles"].insert(2, "lakefile.toml") +artifacts["runtimePaths"].append(".lake/packages") +artifacts["sourceHashInputs"] = artifacts["rootFiles"] + ["Beam/**"] +with open(path, "w", encoding="utf-8") as stream: + json.dump(manifest, stream) + stream.write("\n") +PY +if run_install_from_source --toolchain "$toolchain" 2>"$reuse_legacy_manifest_err"; then + mv "$reuse_legacy_manifest_backup" "$installed_version_root/manifest.json" + echo "expected reinstall to reject a cleanup-only schema-2 runtime manifest" >&2 + exit 1 +fi +mv "$reuse_legacy_manifest_backup" "$installed_version_root/manifest.json" +assert_contains_literal "$reuse_legacy_manifest_err" \ + 'refusing to reuse legacy Beam install manifest schemaVersion 2' +assert_symlink_target "$installed_runtime_root" "$installed_version_root" +assert_version_count "$BEAM_INSTALL_ROOT/versions" 1 +assert_not_exists "$BEAM_INSTALL_ROOT/.install-lock" +remove_tmp_file "$reuse_legacy_manifest_err" + +reuse_manifest_backup="$tmp_root/runtime-reuse-manifest.json" +reuse_manifest_err="$tmp_root/runtime-reuse-manifest.err" +cp "$installed_version_root/manifest.json" "$reuse_manifest_backup" +python3 - "$installed_version_root/manifest.json" <<'PY' +import json +import sys + +path = sys.argv[1] +with open(path, encoding="utf-8") as stream: + manifest = json.load(stream) +manifest["schemaVersion"] = 999 +with open(path, "w", encoding="utf-8") as stream: + json.dump(manifest, stream) + stream.write("\n") +PY +if run_install_from_source --toolchain "$toolchain" 2>"$reuse_manifest_err"; then + mv "$reuse_manifest_backup" "$installed_version_root/manifest.json" + echo "expected reinstall to reject an invalid typed runtime manifest" >&2 + exit 1 +fi +mv "$reuse_manifest_backup" "$installed_version_root/manifest.json" +assert_contains_literal "$reuse_manifest_err" \ + 'unsupported install manifest schemaVersion 999' +assert_symlink_target "$installed_runtime_root" "$installed_version_root" +assert_version_count "$BEAM_INSTALL_ROOT/versions" 1 +assert_not_exists "$BEAM_INSTALL_ROOT/.install-lock" +remove_tmp_file "$reuse_manifest_err" + assert_not_exists "$CODEX_HOME" assert_not_exists "$CLAUDE_HOME" assert_not_exists "$PI_CODING_AGENT_DIR" @@ -685,7 +924,7 @@ run_custom_toolchain_install_test() ( assert_runtime_layout "$custom_installed_runtime_root" assert_contains_literal "$custom_installed_runtime_root/custom-lean-toolchains" "$custom_toolchain" assert_version_count "$custom_install_root/versions" 1 - custom_installed_version_root="$(python3 -c 'import os,sys; print(os.path.realpath(sys.argv[1]))' "$custom_installed_runtime_root")" + custom_installed_version_root="$(beam_test_realpath "$custom_installed_runtime_root")" custom_installed_payload_id="$(basename "$custom_installed_version_root")" BEAM_INSTALL_LAYOUT_JSON="$install_layout_json" assert_manifest_metadata \ "$custom_installed_runtime_root/manifest.json" \ diff --git a/tests/test-beam-prune.sh b/tests/test-beam-prune.sh new file mode 100644 index 00000000..8c6faa38 --- /dev/null +++ b/tests/test-beam-prune.sh @@ -0,0 +1,546 @@ +#!/usr/bin/env bash + +# 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 + +set -euo pipefail + +cd "$(dirname "$0")/.." + +# shellcheck source=tests/lib/assertions.sh +. tests/lib/assertions.sh +# shellcheck source=tests/lib/tmp-guards.sh +. tests/lib/tmp-guards.sh +# shellcheck source=tests/lib/wait.sh +. tests/lib/wait.sh +# shellcheck source=scripts/shared-lib.sh +. scripts/shared-lib.sh + +tmp_root="$(mktemp -d /tmp/beam-prune-XXXXXX)" +install_root="$tmp_root/install-root" +versions_root="$install_root/versions" +current_runtime="$versions_root/current-payload" +old_runtime="$versions_root/old-payload" +install_bundle_root="$install_root/state/install-bundles" +bundle_root="$install_bundle_root/linux-test" +current_bundle="$bundle_root/100" +stale_bundle="$bundle_root/200" +incomplete_bundle="$bundle_root/300" +malformed_bundle="$bundle_root/350" +beam_cli="$PWD/.lake/build/bin/beam-cli" +race_pid="" +lock_writer_pid="" + +cleanup() { + chmod u+w "$install_root" 2>/dev/null || true + if [ -n "$race_pid" ]; then + kill "$race_pid" > /dev/null 2>&1 || true + wait "$race_pid" 2>/dev/null || true + fi + if [ -n "$lock_writer_pid" ]; then + kill "$lock_writer_pid" > /dev/null 2>&1 || true + wait "$lock_writer_pid" 2>/dev/null || true + fi + beam_test_remove_owned_tmp_tree "$tmp_root" beam-prune +} +trap cleanup EXIT + +if [ ! -x "$beam_cli" ]; then + lake build beam-cli +fi + +write_runtime_manifest() { + local payload="$1" + local path="$2" + "$beam_cli" install-manifest "$payload" - fixture-toolchain >"$path" +} + +mkdir -p \ + "$current_runtime/bin" \ + "$current_runtime/libexec" \ + "$old_runtime" \ + "$current_bundle" \ + "$stale_bundle" \ + "$incomplete_bundle" \ + "$malformed_bundle" + +printf '%s\n' \ + 'schema=1' \ + 'owner=lean-beam' \ + "root=$install_root" >"$install_root/.lean-beam-install-root" +write_runtime_manifest current-payload "$current_runtime/manifest.json" +write_runtime_manifest old-payload "$old_runtime/manifest.json" +cp scripts/lean-beam "$current_runtime/bin/lean-beam" +cp "$beam_cli" "$current_runtime/libexec/beam-cli" +ln -s "$current_runtime" "$install_root/current" + +resolved_current_runtime="$(beam_test_realpath "$current_runtime")" +resolved_old_runtime="$(beam_test_realpath "$old_runtime")" +resolved_stale_bundle="$(beam_test_realpath "$stale_bundle")" +resolved_incomplete_bundle="$(beam_test_realpath "$incomplete_bundle")" +resolved_malformed_bundle="$(beam_test_realpath "$malformed_bundle")" + +current_version_out="$("$install_root/current/bin/lean-beam" --version)" +assert_output_contains "current installed runtime identity" "$current_version_out" \ + 'runtime current: true' +current_link_version_out="$(BEAM_HOME="$install_root/current" "$beam_cli" version)" +assert_output_contains "current installed runtime identity through current link" \ + "$current_link_version_out" 'runtime current: true' +old_version_out="$(BEAM_HOME="$old_runtime" "$beam_cli" version)" +assert_output_contains "old installed runtime identity" "$old_version_out" \ + 'runtime current: false' + +source_like_runtime="$tmp_root/source-like/versions/checkout" +mkdir -p "$source_like_runtime" +printf '%s\n' '{"payloadHash":"checkout"}' >"$source_like_runtime/manifest.json" +source_like_version_out="$(BEAM_HOME="$source_like_runtime" "$beam_cli" version)" +assert_output_not_contains "source-like runtime identity" "$source_like_version_out" \ + 'runtime current:' +assert_output_contains "source-like runtime identity" "$source_like_version_out" \ + 'runtime payload: (source tree)' +assert_output_contains "source-like runtime identity" "$source_like_version_out" \ + 'manifest: (none)' + +# An otherwise empty runtime source tree hashes to the FNV-1a offset basis. +bundle_plugin_name="$(beam_shared_lib_name beam_Beam_LSP)" +write_bundle_artifacts() { + local bundle_dir="$1" + local workspace="$bundle_dir/workspace" + mkdir -p "$workspace/.lake/build/bin" "$workspace/.lake/build/lib" + : >"$workspace/.lake/build/bin/beam-daemon" + : >"$workspace/.lake/build/bin/beam-client" + : >"$workspace/.lake/build/lib/$bundle_plugin_name" +} +write_complete_bundle() { + local bundle_dir="$1" + local source_hash="$2" + local workspace="$bundle_dir/workspace" + write_bundle_artifacts "$bundle_dir" + printf '%s\n' \ + '{' \ + ' "schemaVersion": 2,' \ + ' "toolchain": "fixture-toolchain",' \ + ' "toolchainFingerprint": {' \ + ' "leanVersion": "fixture-lean",' \ + ' "leanPrefix": "/fixture/lean",' \ + ' "leanLibDir": "/fixture/lean/lib",' \ + ' "lakeVersion": "fixture-lake"' \ + ' },' \ + " \"sourceHash\": \"$source_hash\"," \ + " \"workspace\": \"$workspace\"," \ + ' "builtAt": "2026-08-05T00:00:00Z"' \ + '}' >"$bundle_dir/metadata.json" +} +write_complete_bundle "$current_bundle" '14695981039346656037' +write_complete_bundle "$stale_bundle" 'stale-source' +write_bundle_artifacts "$malformed_bundle" +printf '%s\n' '{"sourceHash":"14695981039346656037"}' >"$malformed_bundle/metadata.json" + +help_out="$(./scripts/lean-beam prune --help)" +assert_output_contains "prune help" "$help_out" 'usage: lean-beam prune [--apply] [--bundles]' +assert_output_contains "prune help" "$help_out" 'remove the displayed paths' +assert_output_contains "prune help" "$help_out" \ + 'Apply removes one validated path at a time and reports each successful removal immediately.' + +source_wrapper_err="$tmp_root/source-wrapper.err" +if ./scripts/lean-beam prune > /dev/null 2>"$source_wrapper_err"; then + echo "expected source-checkout prune to fail" >&2 + exit 1 +fi +assert_contains_literal "$source_wrapper_err" 'prune is only available from an installed Beam runtime' + +unknown_err="$tmp_root/unknown.err" +if "$install_root/current/bin/lean-beam" prune --unknown > /dev/null 2>"$unknown_err"; then + echo "expected unknown prune option to fail" >&2 + exit 1 +fi +assert_contains_literal "$unknown_err" 'usage: lean-beam prune [--apply] [--bundles]' +assert_contains_literal "$unknown_err" 'unknown prune option: --unknown' + +noncurrent_err="$tmp_root/noncurrent.err" +if BEAM_HOME="$old_runtime" "$beam_cli" install-prune > /dev/null 2>"$noncurrent_err"; then + echo "expected prune from a non-current runtime to fail" >&2 + exit 1 +fi +assert_contains_literal "$noncurrent_err" 'refusing to prune from a non-current Beam runtime' + +ln -s "$current_runtime" "$versions_root/current-alias" +current_alias_err="$tmp_root/current-alias.err" +if "$install_root/current/bin/lean-beam" prune > /dev/null 2>"$current_alias_err"; then + echo "expected prune to reject a symlink alias to the current runtime" >&2 + exit 1 +fi +assert_contains_literal "$current_alias_err" 'refusing to prune symlinked runtime path' +rm -f "$versions_root/current-alias" + +dry_run_out="$("$install_root/current/bin/lean-beam" prune --bundles)" +assert_output_contains "prune dry run" "$dry_run_out" 'Beam install prune (dry run)' +assert_output_contains "prune dry run" "$dry_run_out" "current runtime: $resolved_current_runtime" +assert_output_contains "prune dry run" "$dry_run_out" "old runtime: $resolved_old_runtime" +assert_output_contains "prune dry run" "$dry_run_out" 'old runtimes: 1' +assert_output_contains "prune dry run" "$dry_run_out" "stale bundle: $resolved_stale_bundle" +assert_output_contains "prune dry run" "$dry_run_out" "stale bundle: $resolved_incomplete_bundle" +assert_output_contains "prune dry run" "$dry_run_out" "stale bundle: $resolved_malformed_bundle" +assert_output_contains "prune dry run" "$dry_run_out" 'stale bundles: 3' +assert_output_contains "prune dry run" "$dry_run_out" \ + 'restart active agents and MCP clients before applying this cleanup' +# shellcheck disable=SC2016 +assert_output_contains "prune dry run" "$dry_run_out" \ + 'dry run only; rerun `lean-beam prune --apply --bundles` to remove these paths' +assert_file "$old_runtime/manifest.json" +assert_file "$current_bundle/metadata.json" +assert_file "$stale_bundle/metadata.json" + +permission_lock_err="$tmp_root/permission-lock.err" +chmod u-w "$install_root" +set +e +BEAM_HOME="$current_runtime" "$beam_cli" install-prune \ + > /dev/null 2>"$permission_lock_err" +permission_lock_status="$?" +set -e +chmod u+w "$install_root" +if [ "$permission_lock_status" -eq 0 ]; then + echo "expected prune to report an install-lock creation error" >&2 + exit 1 +fi +assert_contains_literal "$permission_lock_err" '.install-lock' +assert_not_contains "$permission_lock_err" 'timed out after' + +race_lock="$install_root/.install-lock" +race_lock_held="$tmp_root/race-lock-held" +race_lock_release="$tmp_root/race-lock-release" +race_err="$tmp_root/race.err" +( + touch "$race_lock_held" + while [ ! -e "$race_lock_release" ]; do + sleep 0.05 + done +) & +lock_writer_pid="$!" +wait_for_file "$race_lock_held" "prune install-lock holder" 10 +mkdir "$race_lock" +printf '%s\n' "$lock_writer_pid" >"$race_lock/pid" +BEAM_HOME="$current_runtime" "$beam_cli" install-prune --apply > /dev/null 2>"$race_err" & +race_pid="$!" +sleep 0.3 +rm -f "$install_root/current" +ln -s "$old_runtime" "$install_root/current" +touch "$race_lock_release" +wait "$lock_writer_pid" +lock_writer_pid="" +set +e +wait "$race_pid" +race_status="$?" +set -e +race_pid="" +if [ "$race_status" -eq 0 ]; then + echo "expected prune to revalidate the current runtime after acquiring the install lock" >&2 + exit 1 +fi +assert_contains_literal "$race_err" 'refusing to prune from a non-current Beam runtime' +assert_file "$old_runtime/manifest.json" +rm -f "$install_root/current" +ln -s "$current_runtime" "$install_root/current" + +mkdir "$install_root/.install-lock" +printf '%s\n' "$$" >"$install_root/.install-lock/pid" +install_lock_err="$tmp_root/install-lock.err" +if "$install_root/current/bin/lean-beam" prune --apply > /dev/null 2>"$install_lock_err"; then + echo "expected prune to respect the active install lock" >&2 + exit 1 +fi +assert_contains_literal "$install_lock_err" 'timed out after 1000 ms waiting for Beam lock' +rm -f "$install_root/.install-lock/pid" +rmdir "$install_root/.install-lock" +assert_file "$old_runtime/manifest.json" + +apply_runtime_out="$("$install_root/current/bin/lean-beam" prune --apply)" +assert_output_contains "runtime prune apply" "$apply_runtime_out" 'removed runtimes: 1' +assert_not_exists "$old_runtime" +assert_file "$current_runtime/manifest.json" +assert_file "$current_bundle/metadata.json" +assert_file "$stale_bundle/metadata.json" + +partial_runtime="$versions_root/partial-payload" +mkdir "$partial_runtime" +write_runtime_manifest partial-payload "$partial_runtime/manifest.json" +python3 - "$partial_runtime/manifest.json" <<'PY' +import json +import sys + +path = sys.argv[1] +with open(path, encoding="utf-8") as stream: + manifest = json.load(stream) +manifest["schemaVersion"] = 2 +manifest["toolchains"] = manifest.pop("createdWithToolchains") +# Recreate the final layout that Beam actually emitted under schema 2. +artifacts = manifest["artifacts"] +artifacts["rootFiles"].insert(2, "lakefile.toml") +artifacts["runtimePaths"].append(".lake/packages") +artifacts["sourceHashInputs"] = artifacts["rootFiles"] + ["Beam/**"] +with open(path, "w", encoding="utf-8") as stream: + json.dump(manifest, stream) + stream.write("\n") +PY +resolved_partial_runtime="$(beam_test_realpath "$partial_runtime")" + +stale_bundle_lock="$bundle_root/.locks/200" +mkdir -p "$stale_bundle_lock" +printf '%s\n' "$$" >"$stale_bundle_lock/pid" +bundle_lock_out="$tmp_root/bundle-lock.out" +bundle_lock_err="$tmp_root/bundle-lock.err" +if "$install_root/current/bin/lean-beam" prune --apply --bundles \ + >"$bundle_lock_out" 2>"$bundle_lock_err"; then + echo "expected prune to respect an active bundle lock" >&2 + exit 1 +fi +assert_contains_literal "$bundle_lock_out" "removed runtime: $resolved_partial_runtime" +assert_contains_literal "$bundle_lock_err" 'timed out after 1000 ms waiting for Beam lock' +assert_contains_literal "$bundle_lock_err" \ + 'prune stopped before completing the displayed plan; any removals reported above were applied' +# shellcheck disable=SC2016 +assert_contains_literal "$bundle_lock_err" \ + 'rerun `lean-beam prune --bundles` to preview the remaining paths' +assert_not_exists "$partial_runtime" +rm -f "$stale_bundle_lock/pid" +rmdir "$stale_bundle_lock" +assert_file "$stale_bundle/metadata.json" + +apply_bundle_out="$("$install_root/current/bin/lean-beam" prune --apply --bundles)" +assert_output_contains "bundle prune apply" "$apply_bundle_out" 'removed runtimes: 0' +assert_output_contains "bundle prune apply" "$apply_bundle_out" \ + "removed stale bundle: $resolved_stale_bundle" +assert_output_contains "bundle prune apply" "$apply_bundle_out" \ + "removed stale bundle: $resolved_incomplete_bundle" +assert_output_contains "bundle prune apply" "$apply_bundle_out" \ + "removed stale bundle: $resolved_malformed_bundle" +assert_output_contains "bundle prune apply" "$apply_bundle_out" 'removed stale bundles: 3' +assert_file "$current_bundle/metadata.json" +assert_not_exists "$stale_bundle" +assert_not_exists "$incomplete_bundle" +assert_not_exists "$malformed_bundle" + +owned_bundle_root="$install_root/state/owned-install-bundles" +external_bundle_root="$tmp_root/external-install-bundles" +external_stale_bundle="$external_bundle_root/linux-test/500" +mkdir -p "$external_stale_bundle" +printf '%s\n' '{"sourceHash":"stale-source"}' >"$external_stale_bundle/metadata.json" +mv "$install_bundle_root" "$owned_bundle_root" +ln -s "$external_bundle_root" "$install_bundle_root" +symlinked_bundle_root_err="$tmp_root/symlinked-bundle-root.err" +if "$install_root/current/bin/lean-beam" prune --apply --bundles \ + > /dev/null 2>"$symlinked_bundle_root_err"; then + echo "expected prune to reject a symlinked installed bundle cache root" >&2 + exit 1 +fi +assert_contains_literal "$symlinked_bundle_root_err" \ + 'refusing to prune symlinked installed bundle cache root' +assert_file "$external_stale_bundle/metadata.json" +rm -f "$install_bundle_root" +mv "$owned_bundle_root" "$install_bundle_root" + +mkdir "$versions_root/unmarked" +unmarked_err="$tmp_root/unmarked.err" +if "$install_root/current/bin/lean-beam" prune --apply > /dev/null 2>"$unmarked_err"; then + echo "expected prune to reject an unmarked runtime directory" >&2 + exit 1 +fi +assert_contains_literal "$unmarked_err" 'refusing to prune unmarked runtime directory' +if [ ! -d "$versions_root/unmarked" ]; then + echo "expected unmarked runtime directory to remain untouched" >&2 + exit 1 +fi +rmdir "$versions_root/unmarked" + +invalid_manifest_runtime="$versions_root/invalid-payload" +mkdir "$invalid_manifest_runtime" +write_runtime_manifest invalid-payload "$invalid_manifest_runtime/manifest.json" +python3 - "$invalid_manifest_runtime/manifest.json" <<'PY' +import json +import sys + +path = sys.argv[1] +with open(path, encoding="utf-8") as stream: + manifest = json.load(stream) +manifest["schemaVersion"] = 1 +with open(path, "w", encoding="utf-8") as stream: + json.dump(manifest, stream) + stream.write("\n") +PY +invalid_manifest_version_out="$(BEAM_HOME="$invalid_manifest_runtime" "$beam_cli" version)" +assert_output_contains "invalid installed runtime identity" "$invalid_manifest_version_out" \ + 'runtime payload: invalid-payload' +assert_output_contains "invalid installed runtime identity" "$invalid_manifest_version_out" \ + 'runtime current: false' +assert_output_contains "invalid installed runtime identity" "$invalid_manifest_version_out" \ + 'runtime error: invalid install manifest:' +assert_output_not_contains "invalid installed runtime identity" "$invalid_manifest_version_out" \ + 'runtime payload: (source tree)' +invalid_manifest_err="$tmp_root/invalid-manifest.err" +if "$install_root/current/bin/lean-beam" prune --apply > /dev/null 2>"$invalid_manifest_err"; then + echo "expected prune to reject a runtime with an invalid manifest schema" >&2 + exit 1 +fi +assert_contains_literal "$invalid_manifest_err" 'refusing to prune runtime with invalid manifest' +assert_file "$invalid_manifest_runtime/manifest.json" +rm -f "$invalid_manifest_runtime/manifest.json" +rmdir "$invalid_manifest_runtime" + +symlink_manifest_runtime="$versions_root/symlink-manifest-payload" +symlink_manifest_target="$tmp_root/symlink-manifest-target.json" +mkdir "$symlink_manifest_runtime" +write_runtime_manifest symlink-manifest-payload "$symlink_manifest_target" +ln -s "$symlink_manifest_target" "$symlink_manifest_runtime/manifest.json" +symlink_manifest_err="$tmp_root/symlink-manifest.err" +if "$install_root/current/bin/lean-beam" prune --apply \ + > /dev/null 2>"$symlink_manifest_err"; then + echo "expected prune to reject a symlinked runtime manifest" >&2 + exit 1 +fi +assert_contains_literal "$symlink_manifest_err" \ + 'refusing to prune runtime with invalid manifest' +assert_file "$symlink_manifest_target" +rm -f "$symlink_manifest_runtime/manifest.json" +rmdir "$symlink_manifest_runtime" + +external_runtime="$tmp_root/external-runtime" +mkdir "$external_runtime" +write_runtime_manifest external-runtime "$external_runtime/manifest.json" +ln -s "$external_runtime" "$versions_root/symlink-payload" +symlink_runtime_err="$tmp_root/symlink-runtime.err" +if "$install_root/current/bin/lean-beam" prune --apply \ + > /dev/null 2>"$symlink_runtime_err"; then + echo "expected prune to reject a symlinked runtime directory" >&2 + exit 1 +fi +assert_contains_literal "$symlink_runtime_err" 'refusing to prune symlinked runtime path' +assert_file "$external_runtime/manifest.json" +rm -f "$versions_root/symlink-payload" + +external_bundle="$tmp_root/external-bundle" +mkdir "$external_bundle" +printf '%s\n' '{"sourceHash":"stale-source"}' >"$external_bundle/metadata.json" +ln -s "$external_bundle" "$bundle_root/400" + +final_out="$("$install_root/current/bin/lean-beam" prune --bundles)" +assert_output_contains "final prune dry run" "$final_out" 'old runtimes: 0' +assert_output_contains "final prune dry run" "$final_out" 'stale bundles: 0' +if [ ! -L "$bundle_root/400" ]; then + echo "expected symlinked bundle directory to remain untouched" >&2 + exit 1 +fi +assert_file "$external_bundle/metadata.json" + +printf '%s\n' \ + 'schema=1' \ + 'owner=lean-beam' \ + 'root=.' >"$install_root/.lean-beam-install-root" +relative_marker_version_out="$( + cd "$install_root" + BEAM_HOME="$current_runtime" "$beam_cli" version +)" +assert_output_contains "relative install marker identity" "$relative_marker_version_out" \ + 'runtime error: invalid Beam install root marker' +relative_marker_err="$tmp_root/relative-marker.err" +if ( + cd "$install_root" + BEAM_HOME="$current_runtime" "$beam_cli" install-prune +) > /dev/null 2>"$relative_marker_err"; then + echo "expected prune to reject a relative install root marker" >&2 + exit 1 +fi +assert_contains_literal "$relative_marker_err" \ + 'refusing to prune invalid Beam install root marker' + +printf '%s\n' \ + 'schema=1' \ + 'owner=lean-beam' \ + 'root=' >"$install_root/.lean-beam-install-root" +blank_marker_err="$tmp_root/blank-marker.err" +if "$install_root/current/bin/lean-beam" prune > /dev/null 2>"$blank_marker_err"; then + echo "expected prune to reject a blank install root marker" >&2 + exit 1 +fi +assert_contains_literal "$blank_marker_err" \ + 'refusing to prune install root marker without root' + +printf '%s\n' \ + 'schema=1' \ + 'owner=lean-beam' \ + "root=$install_root" \ + "root=$install_root" >"$install_root/.lean-beam-install-root" +multiple_marker_err="$tmp_root/multiple-marker.err" +if "$install_root/current/bin/lean-beam" prune > /dev/null 2>"$multiple_marker_err"; then + echo "expected prune to reject an install root marker with multiple roots" >&2 + exit 1 +fi +assert_contains_literal "$multiple_marker_err" \ + 'refusing to prune invalid Beam install root marker' + +printf '%s\n' \ + 'schema=1' \ + 'schema=2' \ + 'owner=lean-beam' \ + "root=$install_root" >"$install_root/.lean-beam-install-root" +conflicting_schema_marker_err="$tmp_root/conflicting-schema-marker.err" +if "$install_root/current/bin/lean-beam" prune > /dev/null 2>"$conflicting_schema_marker_err"; then + echo "expected prune to reject conflicting install root marker schema fields" >&2 + exit 1 +fi +assert_contains_literal "$conflicting_schema_marker_err" \ + 'refusing to prune invalid Beam install root marker' + +printf '%s\n' \ + 'schema=1' \ + 'owner=lean-beam' \ + 'owner=other' \ + "root=$install_root" >"$install_root/.lean-beam-install-root" +conflicting_owner_marker_err="$tmp_root/conflicting-owner-marker.err" +if "$install_root/current/bin/lean-beam" prune > /dev/null 2>"$conflicting_owner_marker_err"; then + echo "expected prune to reject conflicting install root marker owner fields" >&2 + exit 1 +fi +assert_contains_literal "$conflicting_owner_marker_err" \ + 'refusing to prune invalid Beam install root marker' + +symlink_marker_target="$tmp_root/install-root-marker-target" +printf '%s\n' \ + 'schema=1' \ + 'owner=lean-beam' \ + "root=$install_root" >"$symlink_marker_target" +rm -f "$install_root/.lean-beam-install-root" +ln -s "$symlink_marker_target" "$install_root/.lean-beam-install-root" +symlink_marker_err="$tmp_root/symlink-marker.err" +if "$install_root/current/bin/lean-beam" prune > /dev/null 2>"$symlink_marker_err"; then + echo "expected prune to reject a symlinked install root marker" >&2 + exit 1 +fi +assert_contains_literal "$symlink_marker_err" \ + 'refusing to prune invalid Beam install root marker' +rm -f "$install_root/.lean-beam-install-root" + +ln -s "$tmp_root/missing-install-root-marker-target" \ + "$install_root/.lean-beam-install-root" +broken_symlink_marker_err="$tmp_root/broken-symlink-marker.err" +if "$install_root/current/bin/lean-beam" prune > /dev/null 2>"$broken_symlink_marker_err"; then + echo "expected prune to reject a broken symlinked install root marker" >&2 + exit 1 +fi +assert_contains_literal "$broken_symlink_marker_err" \ + 'refusing to prune invalid Beam install root marker' +rm -f "$install_root/.lean-beam-install-root" + +printf '%s\n' \ + 'schema=1' \ + 'owner=lean-beam' \ + "root=$tmp_root/not-the-install-root" >"$install_root/.lean-beam-install-root" +mismatched_marker_err="$tmp_root/mismatched-marker.err" +if "$install_root/current/bin/lean-beam" prune > /dev/null 2>"$mismatched_marker_err"; then + echo "expected prune to reject a mismatched install root marker" >&2 + exit 1 +fi +assert_contains_literal "$mismatched_marker_err" \ + 'refusing to prune install root with mismatched marker root' + +echo "beam install prune tests passed" diff --git a/tests/test-beam-wrapper-daemon.sh b/tests/test-beam-wrapper-daemon.sh index dce6182e..a9e48b23 100644 --- a/tests/test-beam-wrapper-daemon.sh +++ b/tests/test-beam-wrapper-daemon.sh @@ -12,20 +12,40 @@ cd "$(dirname "$0")/.." . tests/lib/beam-wrapper-common.sh beam_script="$PWD/scripts/lean-beam" +beam_cli="$PWD/.lake/build/bin/beam-cli" if [ ! -x "$beam_script" ]; then echo "missing lean-beam wrapper at $beam_script" >&2 exit 1 fi +if [ ! -x "$beam_cli" ]; then + echo "missing beam-cli at $beam_cli" >&2 + exit 1 +fi stop_hold_process() { + local require_clean_exit="${1:-false}" if [ -n "$hold_pid" ]; then kill -INT "$hold_pid" > /dev/null 2>&1 || true if ! wait_for_exit "$hold_pid" "ensure --hold wrapper" 20 0.1; 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 wrapper to exit promptly after SIGINT" >&2 + return 1 + fi else - wait "$hold_pid" 2>/dev/null || true + local hold_status=0 + set +e + wait "$hold_pid" 2>/dev/null + hold_status="$?" + set -e + hold_pid="" + if [ "$require_clean_exit" = "true" ] && [ "$hold_status" -ne 0 ]; then + echo "expected ensure --hold wrapper to exit cleanly after SIGINT, got $hold_status" >&2 + return 1 + fi fi hold_pid="" fi @@ -34,6 +54,11 @@ stop_hold_process() { tmp1="$(mktemp -d /tmp/beam-wrapper-daemon-a-XXXXXX)" tmp3="$(mktemp -d /tmp/beam-wrapper-daemon-c-XXXXXX)" tmp9="$(mktemp -d /tmp/beam-wrapper-daemon-i-XXXXXX)" +owned_bundle_dir="" +if [ -z "${BEAM_INSTALL_BUNDLE_DIR:-}" ]; then + owned_bundle_dir="$(mktemp -d /tmp/beam-wrapper-daemon-bundles-XXXXXX)" + export BEAM_INSTALL_BUNDLE_DIR="$owned_bundle_dir" +fi busy_pid="" hold_pid="" @@ -49,9 +74,19 @@ cleanup() { remove_owned_tmp_tree "$tmp1" remove_owned_tmp_tree "$tmp3" remove_owned_tmp_tree "$tmp9" + if [ -n "$owned_bundle_dir" ]; then + remove_owned_tmp_tree "$owned_bundle_dir" + fi } trap cleanup EXIT +if [ -n "$owned_bundle_dir" ]; then + expect_owned_tmp_dir "$owned_bundle_dir" +fi + +fixture_toolchain="$(awk 'NR==1 {print $1}' tests/save_olean_project/lean-toolchain)" +"$beam_cli" bundle-install "$fixture_toolchain" + for tmp in "$tmp1" "$tmp3" "$tmp9"; do expect_owned_tmp_dir "$tmp" rsync -a tests/save_olean_project/ "$tmp"/ @@ -80,7 +115,7 @@ if ! kill -0 "$hold_pid" 2>/dev/null; then fi hold_json="$(cat "$tmp9/hold.out")" assert_json_field_equals "ensure --hold response" "$hold_json" ok true "$tmp9/hold.err" -stop_hold_process +stop_hold_process true "$beam_script" --root "$tmp9" shutdown > /dev/null stale_lease_dir="$tmp9/.beam/wrapper-leases" @@ -119,7 +154,7 @@ expect_file "$reg1" pid1="$(read_json_field "$reg1" pid)" port1="$(read_json_field "$reg1" port)" root1="$(read_json_field "$reg1" root)" -if [ "$root1" != "$(python3 -c 'import os,sys; print(os.path.realpath(sys.argv[1]))' "$tmp1")" ]; then +if [ "$root1" != "$(beam_test_realpath "$tmp1")" ]; then echo "wrapper registry root mismatch: expected $tmp1, got $root1" >&2 exit 1 fi diff --git a/tests/test-beam-wrapper-probe.sh b/tests/test-beam-wrapper-probe.sh index a4b1b8a8..338e0e61 100644 --- a/tests/test-beam-wrapper-probe.sh +++ b/tests/test-beam-wrapper-probe.sh @@ -29,7 +29,7 @@ client1="$(read_json_field "$registry_path" clientBin 2>/dev/null || true)" if [ -z "$client1" ]; then client1="$client" fi -if [ "$root1" != "$(beam_wrapper_realpath "$project_root")" ]; then +if [ "$root1" != "$(beam_test_realpath "$project_root")" ]; then echo "wrapper registry root mismatch: expected $project_root, got $root1" >&2 exit 1 fi