fix: explain selected targets and preserve reinstall target sets

Beam/Cli/Installation.lean

@@ -29,9 +29,30 @@ private def _root_.Beam.Installation.admitControl (installation : Installation)
         ("recoveryPrecondition", toJson ("Before manual recovery or restarting, independently verify that the original " ++
           "owner, daemon, and all other producers have stopped."))]
 
+private structure TargetFailureData where
+  selectorPath : String
+  selectorText : String
+  leanCommand : String
+  installationRoot : String
+  retainedTargets : Array String
+  remedyCommand? : Option String
+  deriving ToJson
+
 private def installationFailure (failure : Beam.Installation.Failure) : CliFailure :=
   match failure with
   | .io error => .internal error
+  | .unavailable target =>
+      let remedy := target.remedy
+      let data : TargetFailureData := {
+        selectorPath := target.selected.path.toString
+        selectorText := target.selected.text
+        leanCommand := target.selected.command.toString
+        installationRoot := target.installationRoot.toString
+        retainedTargets := target.retainedTargets
+        remedyCommand? := remedy.command? }
+      { (CliFailure.setup (target.explanation remedy)) with
+        remedyCommand? := data.remedyCommand?
+        failure.error.data? := some (toJson data) }
   | _ => .setup failure.message
 
 private def runtimeFor (lookup : System.FilePath → IO (Except Beam.Installation.Failure Beam.Installation.RuntimeRef))

Beam/Install/Sources.lean

@@ -10,7 +10,8 @@ namespace Beam.Install
 
 /-- Source-checkout files that a target build needs, relative to the checkout root. -/
 def sourceRootFiles : List String :=
-  ["LICENSE", "Beam.lean", "lakefile.lean", "lake-manifest.json", "lean-toolchain"]
+  ["LICENSE", "Beam.lean", "lakefile.lean", "lake-manifest.json", "lean-toolchain",
+    "validated-lean-toolchains", "compatible-lean-release-lines"]
 
 def sourceDirs : List String :=
   ["Beam"]

Beam/Install/Toolchain.lean

@@ -5,6 +5,7 @@ Author: Emilio J. Gallego Arias
 -/
 
 import Lean
+import Beam.Installation.ToolchainPolicy
 import Beam.Installation.Components
 import Beam.Path
 import Beam.System
@@ -49,34 +50,9 @@ private def readRequiredToolchainCmdTrim (toolchain exe : String) (args : Array
       s!"failed to fingerprint Lean toolchain {toolchain}: `elan run {toolchain} {exe}` returned empty stdout"
   pure text
 
-private def canonicalNat? (text : String) : Option Nat := do
-  let value ← text.toNat?
-  if s!"{value}" == text then some value else none
-
-/-- The exact version of a canonical `leanprover/lean4:vX.Y.Z[-rcN]` selector, if it is one. -/
-def canonicalLeanVersion? (toolchain : String) : Option String := do
-  let selectorPrefix := "leanprover/lean4:v"
-  unless toolchain.startsWith selectorPrefix do none
-  let version := (toolchain.drop selectorPrefix.length).toString
-  let (stable, rc?) ← match version.splitOn "-" with
-    | [stable] => some (stable, none)
-    | [stable, prerelease] => do
-        unless prerelease.startsWith "rc" do none
-        let rc ← canonicalNat? (prerelease.drop 2).toString
-        unless rc > 0 do none
-        some (stable, some rc)
-    | _ => none
-  let [major, minor, patch] := stable.splitOn "." | none
-  let parts ← [major, minor, patch].mapM canonicalNat?
-  let rendered := ".".intercalate (parts.map toString) ++
-    match rc? with
-    | some rc => s!"-rc{rc}"
-    | none => ""
-  if rendered == version then some rendered else none
-
 /-- A canonical selector must name the compiler that `lean --version` reports. -/
 def expectedCanonicalLeanVersionPrefix? (toolchain : String) : Option String := do
-  some s!"Lean (version {← canonicalLeanVersion? toolchain},"
+  some s!"Lean (version {← Beam.Installation.ToolchainPolicy.canonicalLeanVersion? toolchain},"
 
 /-- Observe one already selected SDK; every command uses this concrete installation. -/
 def fingerprintLeanInstallation (root : System.FilePath) : IO ToolchainFingerprint := do

Beam/Installation/LocalTarget.lean

@@ -9,6 +9,15 @@ import Beam.System
 
 namespace Beam.Installation.LocalTarget
 
+/-- The selector observation that chose one concrete compiler. This is diagnostic context, not
+permission to resolve it again or substitute a different installation. -/
+structure Selection where
+  path : System.FilePath
+  text : String
+  command : System.FilePath
+  /-- An exact Elan name usable by the installer; direct filesystem selections have none. -/
+  installerToolchain? : Option String := none
+
 inductive Failure where
   | unavailable (selector : String)
   | floating (selector : String)
@@ -70,17 +79,19 @@ private def selectorPresent (root marker : System.FilePath) : IO Bool := do
 /-- Resolve regular selector files through local context.
 No candidate executable, elan command, download, or build runs. -/
 def resolve (root : System.FilePath) (home? : Option System.FilePath) :
-    IO (Except Failure (Option System.FilePath)) := do
+    IO (Except Failure (Option Selection)) := do
   try
     let marker := root / "lean-toolchain"
     unless ← selectorPresent root marker do return .ok none
     unless (← marker.metadata).type == .file do
       throw <| IO.userError s!"project selector must resolve to a regular file: {marker}"
     let selector := ((← IO.FS.readFile marker).splitOn "\n").headD "" |>.trimAscii.toString
+    let selected := fun command installerToolchain? =>
+      some { path := marker, text := selector, command, installerToolchain? : Selection }
     if selector.isEmpty then return .error (.unavailable selector)
     let path := System.FilePath.mk selector
     let toolchainRoot := if path.isAbsolute then path else root / path
-    if let some command ← leanIn? toolchainRoot then return .ok (some command)
+    if let some command ← leanIn? toolchainRoot then return .ok (selected command none)
     if path.isAbsolute || ["./", "../", ".\\", "..\\"].any (fun start => selector.startsWith start) then
       return .error (.unavailable selector)
     let (origin, release) ← match selector.splitOn ":" with
@@ -89,15 +100,16 @@ def resolve (root : System.FilePath) (home? : Option System.FilePath) :
       | _ => return .error (.unavailable selector)
     let some home := home? | return .error (.unavailable selector)
     -- Elan gives a locally linked release name precedence over the remote descriptor.
-    if let some command ← linkedLean? home release then return .ok (some command)
+    if let some command ← linkedLean? home release then return .ok (selected command (some release))
     if ["stable", "beta", "nightly", "lean-toolchain"].contains release then
       return .error (.floating selector)
     let origin := if release.startsWith "nightly" && !origin.endsWith "-nightly" then
       origin ++ "-nightly" else origin
     let release := if release.toList.head?.any Char.isDigit then "v" ++ release else release
     let some name := directoryName? (origin ++ ":" ++ release)
       | return .error (.unavailable selector)
-    if let some command ← leanIn? (home / "toolchains" / name) then return .ok (some command)
+    if let some command ← leanIn? (home / "toolchains" / name) then
+      return .ok (selected command (some (origin ++ ":" ++ release)))
     return .error (.unavailable selector)
   catch error => return .error (.io error)
 

Beam/Installation/Lookup.lean

@@ -7,6 +7,8 @@ Author: Emilio J. Gallego Arias
 import Beam.Installation.Manifest
 import Beam.Installation.Bundled
 import Beam.Installation.LocalTarget
+import Beam.Installation.StandaloneLayout
+import Beam.Installation.ToolchainPolicy
 import Beam.Project
 import Beam.Runtime
 import Beam.Version
@@ -19,21 +21,107 @@ inductive Role where
   | cli | mcp | daemon
   deriving BEq
 
+/-- Observed installation context, used only to decide which remedy guidance is appropriate. -/
+inductive TargetInstallContext where
+  | bundled
+  | unrecognized
+  | current (installRoot : System.FilePath)
+  | unconfirmed (installRoot : System.FilePath)
+  deriving BEq
+
+/-- The unavailable selected target and the complete installation it was checked against. -/
+structure UnavailableTarget where
+  selected : LocalTarget.Selection
+  installationRoot : System.FilePath
+  installContext : TargetInstallContext := .unrecognized
+  retainedTargets : Array String
+  sourceCommit? : Option String
+
+inductive TargetRemedy where
+  | install (command precondition : String)
+  | manual (detail : String)
+
+def TargetRemedy.command? : TargetRemedy → Option String
+  | .install command _ => some command
+  | .manual _ => none
+
+private def quoteArgument (text : String) : String :=
+  "'" ++ text.replace "'" "'\\''" ++ "'"
+
+/-- Only suggest commands the existing source installer accepts; never execute a candidate. -/
+private def installerTargetArguments (toolchain : String) : Except String (List String) := do
+  if toolchain.isEmpty || toolchain.toList.any (fun c => c.isWhitespace || c.toNat < 32) then
+    throw "the installer requires a nonempty Elan toolchain name without whitespace"
+  if (System.FilePath.mk toolchain).isAbsolute ||
+      ["./", "../", ".\\", "..\\"].any (fun start => toolchain.startsWith start) then
+    throw "a filesystem selector must be registered under an Elan link name before installation"
+  if Beam.Installation.ToolchainPolicy.releaseToolchainSupported toolchain then
+    return ["--toolchain", toolchain]
+  if toolchain.startsWith "leanprover/lean4:" then
+    throw <| s!"this Beam revision does not support official target '{toolchain}' for installation. " ++
+      "Use a Beam revision that supports the project's existing Lean toolchain; " ++
+      "leave the project's lean-toolchain and dependency pins unchanged"
+  return ["--custom-toolchain", toolchain]
+
+def UnavailableTarget.remedy (target : UnavailableTarget) : TargetRemedy := Id.run do
+  if let some requested := target.selected.installerToolchain? then
+    if let .error detail := installerTargetArguments requested then return .manual detail
+  if let .bundled := target.installContext then
+    return .manual <| "bundled Beam serves only its containing Lean installation; use Beam bundled " ++
+      "with the selected SDK, or construct a separate standalone Beam installation for that target"
+  if let .unconfirmed installRoot := target.installContext then
+    return .manual <| s!"this bound generation could not be confirmed as current for {installRoot}; " ++
+      "inspect the current installation before choosing the complete target set to retain. " ++
+      "No reinstall command was generated from this older or unconfirmed selection"
+  let .current installRoot := target.installContext
+    | return .manual <| "this installation has no recognized standalone installer location; " ++
+        "use a Beam source checkout to construct an installation containing the selected target and all retained targets"
+  let some requested := target.selected.installerToolchain?
+    | return .manual <| "the source installer accepts Elan toolchain names, not project-local SDK paths; " ++
+        "link this SDK with `elan toolchain link NAME SDK_ROOT`, then install it with --custom-toolchain NAME " ++
+        "alongside every retained target"
+  let mut names := target.retainedTargets.toList
+  unless names.contains requested do names := names ++ [requested]
+  let mut arguments := []
+  for name in names do
+    match installerTargetArguments name with
+    | .error detail => return .manual <| detail ++ "; no installer command was generated that would drop retained targets"
+    | .ok flags => arguments := arguments ++ flags
+  let command := "BEAM_INSTALL_ROOT=" ++ quoteArgument installRoot.toString ++
+    " ./scripts/install-beam.sh " ++ String.intercalate " " (arguments.map quoteArgument)
+  let revision := target.sourceCommit?.map (fun commit => s!" at revision {commit}") |>.getD ""
+  return .install command <| s!"From a Beam source checkout{revision}, run this POSIX-shell command. " ++
+    "It includes the inspected generation's targets. Before running it, confirm that the current target set " ++
+    "still matches this snapshot; the installer replaces the complete selection and will show its write plan. " ++
+    "Restart Beam clients to use the newly installed target set."
+
+/-- Render the explanation without embedding the separately typed remedy command. -/
+def UnavailableTarget.explanation (target : UnavailableTarget) (remedy : TargetRemedy) : String :=
+  let selected := target.selected
+  let message := s!"This Beam installation has no runtime for {selected.command}. " ++
+    s!"The project's Lean compiler was found via selector '{selected.text}' in {selected.path}; " ++
+    s!"bound Beam installation: {target.installationRoot}. "
+  match remedy with
+  | .install _ precondition => message ++ precondition
+  | .manual detail => message ++ detail ++
+      ". For custom-target setup, see https://github.com/leanprover/lean-beam/blob/main/docs/CUSTOM_TOOLCHAINS.md"
+
+def UnavailableTarget.message (target : UnavailableTarget) : String :=
+  let remedy := target.remedy
+  target.explanation remedy ++ (remedy.command?.map ("\n" ++ ·)).getD ""
+
 inductive Failure where
   | invalid (detail : String)
   | changed
-  | unavailable (command : System.FilePath)
+  | unavailable (target : UnavailableTarget)
   | noTarget
   | selection (error : Beam.Installation.LocalTarget.Failure)
   | io (error : IO.Error)
 
 def Failure.message : Failure → String
   | .invalid detail => s!"invalid Beam installation: {detail}; reinstall Beam before starting runtime work"
   | .changed => "Beam installation generation changed; restart with a complete installation"
-  | .unavailable command =>
-      s!"This Beam installation has no runtime for {command}. " ++
-        "The project's Lean compiler was found; install Beam for this exact target. " ++
-        "For a local Lean build, see https://github.com/leanprover/lean-beam/blob/main/docs/CUSTOM_TOOLCHAINS.md"
+  | .unavailable target => target.message
   | .noTarget => "missing project lean-toolchain; select an exact installed target before starting standalone Beam"
   | .selection error => error.message
   | .io error => error.toString
@@ -200,24 +288,39 @@ structure RuntimeRef where
   private mk ::
   description : Beam.Runtime.Description
 
+private def Observation.installContext (observation : Observation) : IO TargetInstallContext := do
+  if observation.record.isBundled then return .bundled
+  let some location := installedRuntimeLocation? observation.home | return .unrecognized
+  unless location.payload == observation.record.generation &&
+      (← checkInstallRootMarker location.installRoot).isOk do return .unrecognized
+  try
+    let current ← Beam.resolveExistingPath (location.installRoot / "current")
+    if Beam.sameCanonicalPath current observation.home then return .current location.installRoot
+  catch _ => pure ()
+  return .unconfirmed location.installRoot
+
 /-- Select from checked members; no installation member is resolved a second time. -/
 def Observation.lookup (observation : Observation) (root : System.FilePath) : IO (Except Failure RuntimeRef) := do
   let selected ← Beam.Installation.LocalTarget.resolve root (← Beam.Installation.LocalTarget.elanHome)
   let selected ← match selected with
     | .error error => return .error (.selection error)
     | .ok selected => pure selected
   for (resolved, index) in observation.targets.toList.zipIdx do
-    if selected.any (Beam.sameCanonicalPath resolved.command) || (selected.isNone && observation.record.isBundled) then
+    if selected.any (fun selected => Beam.sameCanonicalPath resolved.command selected.command) ||
+        (selected.isNone && observation.record.isBundled) then
       if observation.daemonTarget?.any (· != index) then
         return .error (.invalid "this target belongs to a different installation-owned daemon")
       return .ok ⟨{
         command := resolved.command.toString
         plugin := resolved.plugin, daemonBin := resolved.daemon, toolchain := resolved.target.toolchain
         identity := ⟨observation.home, observation.record.generation⟩
       }⟩
-  return .error <| match selected with
-    | some command => .unavailable command
-    | none => .noTarget
+  let some selected := selected | return .error .noTarget
+  return .error <| .unavailable {
+    selected, installationRoot := observation.home
+    installContext := ← observation.installContext
+    retainedTargets := observation.record.components.targets.map (·.toolchain)
+    sourceCommit? := observation.record.sourceCommit? }
 
 /-- Exact local lookup; no compiler probe, provider search, or provisioning is possible here. -/
 def lookup (installation : Installation) (root : System.FilePath) : IO (Except Failure RuntimeRef) := do

Beam/Installation/ToolchainPolicy.lean

@@ -0,0 +1,54 @@
+/-
+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
+
+namespace Beam.Installation.ToolchainPolicy
+
+private def canonicalNat? (text : String) : Option Nat := do
+  let value ← text.toNat?
+  if s!"{value}" == text then some value else none
+
+/-- The exact version of a canonical `leanprover/lean4:vX.Y.Z[-rcN]` selector, if it is one. -/
+def canonicalLeanVersion? (toolchain : String) : Option String := do
+  let selectorPrefix := "leanprover/lean4:v"
+  unless toolchain.startsWith selectorPrefix do none
+  let version := (toolchain.drop selectorPrefix.length).toString
+  let (stable, rc?) ← match version.splitOn "-" with
+    | [stable] => some (stable, none)
+    | [stable, prerelease] => do
+        unless prerelease.startsWith "rc" do none
+        let rc ← canonicalNat? (prerelease.drop 2).toString
+        unless rc > 0 do none
+        some (stable, some rc)
+    | _ => none
+  let [major, minor, patch] := stable.splitOn "." | none
+  let parts ← [major, minor, patch].mapM canonicalNat?
+  let rendered := ".".intercalate (parts.map toString) ++
+    match rc? with
+    | some rc => s!"-rc{rc}"
+    | none => ""
+  if rendered == version then some rendered else none
+
+private def registryEntries (text : String) : List String :=
+  text.splitOn "\n" |>.map (fun line => line.trimAscii.toString)
+    |>.filter (fun line => !line.isEmpty && !line.startsWith "#")
+
+/-- Frozen installer policy for diagnostics; ordinary admission still uses exact membership. -/
+def validatedToolchains : List String :=
+  registryEntries (include_str "../../validated-lean-toolchains")
+
+private def compatibleReleaseLines : List String :=
+  registryEntries (include_str "../../compatible-lean-release-lines")
+
+/-- Mirrors the installer's canonical release-line admission, using the same policy files. -/
+def releaseToolchainSupported (toolchain : String) : Bool :=
+  validatedToolchains.contains toolchain || Id.run do
+    let some version := canonicalLeanVersion? toolchain | return false
+    let [major, minor, _] := ((version.splitOn "-").headD "").splitOn "." | return false
+    return compatibleReleaseLines.contains s!"leanprover/lean4:v{major}.{minor}"
+
+end Beam.Installation.ToolchainPolicy