From 5b4a3ca701876d3ead11ac740d830a1fe3388586 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 27 Oct 2026 10:09:54 +0100 Subject: [PATCH 1/8] fix: explain selected targets and retain installer target sets --- Beam/Cli/Installation.lean | 11 +++ Beam/Install/Sources.lean | 3 +- Beam/Install/Toolchain.lean | 26 +----- Beam/Install/ToolchainPolicy.lean | 54 +++++++++++ Beam/Installation/LocalTarget.lean | 20 +++- Beam/Installation/Lookup.lean | 91 +++++++++++++++++-- Beam/Output.lean | 13 +++ docs/CUSTOM_TOOLCHAINS.md | 13 +++ lakefile.lean | 7 ++ .../BeamTest/Broker/McpProjectionTest.lean | 10 ++ .../BeamTest/Installation/LookupTest.lean | 84 ++++++++++++++++- tests/lib/bundled-mcp-lifetime.py | 5 +- tests/test-installation-entrypoints.py | 5 + tests/test-installation-lookup.py | 19 ++++ tests/test-native-toolchain.py | 2 + 15 files changed, 320 insertions(+), 43 deletions(-) create mode 100644 Beam/Install/ToolchainPolicy.lean diff --git a/Beam/Cli/Installation.lean b/Beam/Cli/Installation.lean index b01bbdd74..c689f62b6 100644 --- a/Beam/Cli/Installation.lean +++ b/Beam/Cli/Installation.lean @@ -32,6 +32,17 @@ private def _root_.Beam.Installation.admitControl (installation : Installation) private def installationFailure (failure : Beam.Installation.Failure) : CliFailure := match failure with | .io error => .internal error + | .unavailable target => + let data := [ + ("selectorPath", toJson target.selected.path.toString), + ("selectorText", toJson target.selected.text), + ("leanCommand", toJson target.selected.command.toString), + ("installationRoot", toJson target.installationRoot.toString), + ("retainedTargets", toJson target.retainedTargets)] + let failure := CliFailure.setup target.message + match target.remedy with + | .install command _ => failure.withRemedy command data + | .manual _ => { failure with failure.error.data? := some <| Json.mkObj data } | _ => .setup failure.message private def runtimeFor (lookup : System.FilePath → IO (Except Beam.Installation.Failure Beam.Installation.RuntimeRef)) diff --git a/Beam/Install/Sources.lean b/Beam/Install/Sources.lean index 5fcd11f42..793b6ad69 100644 --- a/Beam/Install/Sources.lean +++ b/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"] diff --git a/Beam/Install/Toolchain.lean b/Beam/Install/Toolchain.lean index 20c0bad21..454bf0dba 100644 --- a/Beam/Install/Toolchain.lean +++ b/Beam/Install/Toolchain.lean @@ -5,6 +5,7 @@ Author: Emilio J. Gallego Arias -/ import Lean +import Beam.Install.ToolchainPolicy import Beam.Installation.Components import Beam.Path import Beam.System @@ -49,31 +50,6 @@ 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}," diff --git a/Beam/Install/ToolchainPolicy.lean b/Beam/Install/ToolchainPolicy.lean new file mode 100644 index 000000000..164cc37ea --- /dev/null +++ b/Beam/Install/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.Install + +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.Install diff --git a/Beam/Installation/LocalTarget.lean b/Beam/Installation/LocalTarget.lean index a422140a6..3f13d3dc3 100644 --- a/Beam/Installation/LocalTarget.lean +++ b/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,7 +100,7 @@ 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 @@ -97,7 +108,8 @@ def resolve (root : System.FilePath) (home? : Option System.FilePath) : 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) diff --git a/Beam/Installation/Lookup.lean b/Beam/Installation/Lookup.lean index 01b4fcb50..508698a0b 100644 --- a/Beam/Installation/Lookup.lean +++ b/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.Install.ToolchainPolicy import Beam.Project import Beam.Runtime import Beam.Version @@ -19,10 +21,75 @@ inductive Role where | cli | mcp | daemon deriving BEq +/-- The unavailable selected target and the complete installation it was checked against. -/ +structure UnavailableTarget where + selected : LocalTarget.Selection + installationRoot : System.FilePath + /-- Present only for an observed, marked standalone install root and matching payload leaf. -/ + installRoot? : Option System.FilePath := none + retainedTargets : Array String + bundled : Bool + sourceCommit? : Option String + +inductive TargetRemedy where + | install (command precondition : String) + | manual (detail : String) + +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.Install.releaseToolchainSupported toolchain then + return ["--toolchain", toolchain] + if toolchain.startsWith "leanprover/lean4:" then + throw <| s!"this Beam revision does not admit official target '{toolchain}' for installation; " ++ + s!"select a supported exact target such as {Beam.Install.validatedToolchains.headD "a validated Lean toolchain"}" + return ["--custom-toolchain", toolchain] + +def UnavailableTarget.remedy (target : UnavailableTarget) : TargetRemedy := Id.run do + if target.bundled 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" + let some installRoot := target.installRoot? + | 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 every retained target; the installer will qualify the selected compilers and show its write plan. " ++ + "Restart Beam clients to use the newly installed target set." + +def UnavailableTarget.message (target : UnavailableTarget) : 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 target.remedy with + | .install command precondition => message ++ precondition ++ "\n" ++ command + | .manual detail => message ++ detail + 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) @@ -30,10 +97,7 @@ inductive Failure where 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 @@ -207,7 +271,8 @@ def Observation.lookup (observation : Observation) (root : System.FilePath) : IO | .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 ⟨{ @@ -215,8 +280,20 @@ def Observation.lookup (observation : Observation) (root : System.FilePath) : IO plugin := resolved.plugin, daemonBin := resolved.daemon, toolchain := resolved.target.toolchain identity := ⟨observation.home, observation.record.generation⟩ }⟩ + let installRoot? ← do + if observation.record.isBundled then pure none else + match installedRuntimeLocation? observation.home with + | none => pure none + | some location => + if location.payload == observation.record.generation && + (← checkInstallRootMarker location.installRoot).isOk then + pure (some location.installRoot) + else pure none return .error <| match selected with - | some command => .unavailable command + | some selected => .unavailable { + selected, installationRoot := observation.home, installRoot? + retainedTargets := observation.record.components.targets.map (·.toolchain) + bundled := observation.record.isBundled, sourceCommit? := observation.record.sourceCommit? } | none => .noTarget /-- Exact local lookup; no compiler probe, provider search, or provisioning is possible here. -/ diff --git a/Beam/Output.lean b/Beam/Output.lean index b9625e0af..85f4b71b2 100644 --- a/Beam/Output.lean +++ b/Beam/Output.lean @@ -501,6 +501,10 @@ private def validateBoolField (json : Json) : Except String Json := do let _ ← fromJson? (α := Bool) json pure json +private def validateStringArray (json : Json) : Except String Json := do + let _ ← fromJson? (α := Array String) json + pure json + /-- CLI-owned codes with structured recovery metadata. Contract tests require representative producer coverage for every entry; backend-only codes are not inferred from payload keys. -/ def controlErrorDataCodes : Array String := #[ @@ -522,6 +526,7 @@ private def controlCodeOwns (code field : String) : Bool := | "installationRoot" => ["setupError", "sessionShutdownUnconfirmed", "sessionInstallationMismatch"].contains code | "currentInstallationRoot" => code == "sessionInstallationMismatch" + | "selectorPath" | "selectorText" | "leanCommand" | "retainedTargets" => code == "setupError" | "operationMayHaveCompleted" | "operationResponse" => ["requestCancelled", "brokerUnavailable", "internalError"].contains code | "recordedConfigHash" | "requestedConfigHash" => @@ -554,6 +559,14 @@ private def projectControlErrorDataImpl (code : String) (data : Json) : Except S (validateStringField value).map (fun projected => ("installation_root", projected, true)) | "currentInstallationRoot" => (validateStringField value).map (fun projected => ("current_installation_root", projected, true)) + | "selectorPath" => + (validateStringField value).map (fun projected => ("selector_path", projected, true)) + | "selectorText" => + (validateStringField value).map (fun projected => ("selector_text", projected, true)) + | "leanCommand" => + (validateStringField value).map (fun projected => ("lean_command", projected, true)) + | "retainedTargets" => + (validateStringArray value).map (fun projected => ("retained_targets", projected, true)) | "operationMayHaveCompleted" => (validateBoolField value).map (fun projected => ("operation_may_have_completed", projected, true)) | "operationResponse" => pure ("operation_response", value, true) diff --git a/docs/CUSTOM_TOOLCHAINS.md b/docs/CUSTOM_TOOLCHAINS.md index de2d560cf..e29e981bf 100644 --- a/docs/CUSTOM_TOOLCHAINS.md +++ b/docs/CUSTOM_TOOLCHAINS.md @@ -76,6 +76,19 @@ and needs a matching Beam runtime. Follow the custom-target installation steps a SDK. Beam matches canonical compiler paths, so the existing relative project selector can stay in place. +If a locally selected compiler is missing from the Beam target set, the CLI error identifies the +`lean-toolchain` file, its interpreted selector, the resolved compiler, and the bound installation. +Its JSON data includes `selector_path`, `selector_text`, `lean_command`, `installation_root`, and +`retained_targets`. When the standalone installer can provide the target, `remedy_command` names +the install root and includes every retained target alongside the requested one. Run it from the +Beam source checkout named in the message; the command uses POSIX shell syntax and retains the +installer's normal confirmation and qualification steps. Restart clients after installing. + +Bundled SDKs, direct filesystem selectors, unsupported official releases, and unrecognized +installation layouts receive manual guidance instead of an invented installer command. A raw SDK +path can first be registered under an explicit Elan link name for `--custom-toolchain`. Runtime +admission remains local and exact; displaying a remedy never executes it or changes selection. + ## Layout qualification The POSIX fast suite runs `tests/test-nonstandard-toolchain.py` with the selected installed SDK. diff --git a/lakefile.lean b/lakefile.lean index 2e9e29f23..dd60bc2d0 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -140,8 +140,15 @@ lean_lib Beam.LSP where moreLinkArgs := if System.Platform.isOSX then #["-Wl,-install_name,@rpath/" ++ nameToSharedLib "beam_Beam_LSP"] else #[] +/-- Policy included in diagnostics is a real build input, including for incremental builds. -/ +target beamInstallerPolicy (pkg) : Unit := do + let inputs ← (#[("validated-lean-toolchains" : FilePath), "compatible-lean-release-lines"]).mapM fun file => + inputBinFile (pkg.dir / file) + return (Job.collectArray inputs).map fun _ => () + lean_lib Beam where defaultFacets := #[`shared] + extraDepTargets := #[`beamInstallerPolicy] moreLinkObjs := #[beamControlDirObj, beamProcessJobObj] lean_lib BeamTest where diff --git a/tests/lean/BeamTest/Broker/McpProjectionTest.lean b/tests/lean/BeamTest/Broker/McpProjectionTest.lean index b4c62d4fe..c3b65d918 100644 --- a/tests/lean/BeamTest/Broker/McpProjectionTest.lean +++ b/tests/lean/BeamTest/Broker/McpProjectionTest.lean @@ -1176,6 +1176,8 @@ private def checkControlProjectionCatalog : IO Unit := do ("setupError", #[("remedyCommand", "remedy_command"), ("installationRoot", "installation_root"), ("sessionDir", "session_dir"), ("descriptorPath", "descriptor_path"), + ("selectorPath", "selector_path"), ("selectorText", "selector_text"), + ("leanCommand", "lean_command"), ("retainedTargets", "retained_targets"), ("recoveryPrecondition", "recovery_precondition"), ("recordedConfigHash", "recorded_config_hash"), ("requestedConfigHash", "requested_config_hash")]), @@ -1224,6 +1226,10 @@ private def checkControlProjectionCatalog : IO Unit := do | "recoveryPrecondition" => toJson "confirm the original worker has stopped" | "recordedConfigHash" => toJson "recorded-config" | "requestedConfigHash" => toJson "requested-config" + | "selectorPath" => toJson "/repo/lean-toolchain" + | "selectorText" => toJson "leanprover/lean4:v4.35.0" + | "leanCommand" => toJson "/sdk/bin/lean" + | "retainedTargets" => toJson (#["kept-alias", "leanprover/lean4:v4.34.1"] : Array String) | "root" => toJson "/repo" | "path" => toJson "Demo.lean" | "generation" => toJson "generation-7" @@ -1252,6 +1258,10 @@ private def checkControlProjectionCatalog : IO Unit := do | "recordedConfigHash" => toJson "recorded-config" | "requestedConfigHash" => toJson "requested-config" | "root" => toJson "/repo" + | "selectorPath" => toJson "/repo/lean-toolchain" + | "selectorText" => toJson "leanprover/lean4:v4.35.0" + | "leanCommand" => toJson "/sdk/bin/lean" + | "retainedTargets" => toJson (#["kept-alias", "leanprover/lean4:v4.34.1"] : Array String) | "path" => toJson "Demo.lean" | "generation" => toJson "generation-7" | "detail" => toJson "control fixture" diff --git a/tests/lean/BeamTest/Installation/LookupTest.lean b/tests/lean/BeamTest/Installation/LookupTest.lean index eaf680d35..0012c9f7f 100644 --- a/tests/lean/BeamTest/Installation/LookupTest.lean +++ b/tests/lean/BeamTest/Installation/LookupTest.lean @@ -6,6 +6,7 @@ Author: Emilio J. Gallego Arias import Beam.Install.Construction import Beam.Cli.Installation +import Beam.Cli.Output open Beam Beam.Cli Beam.Installation @@ -27,6 +28,67 @@ private def rejected (installation : Installation) (project : System.FilePath) : | .error _ => pure () | .ok _ => throw <| IO.userError "unavailable or invalid installation unexpectedly admitted a runtime" +private def checkUnavailableContext (installation : Installation) (project : System.FilePath) + (installRoot? : Option System.FilePath := none) : IO Unit := do + IO.FS.writeFile (project / "lean-toolchain") "foreign-alias\n" + let .error (.unavailable target) ← installation.lookup project + | throw <| IO.userError "expected a typed unavailable target" + require (target.selected.path == project / "lean-toolchain" && target.selected.text == "foreign-alias") + "lookup lost its selected file or text" + require (target.retainedTargets == #["fixture-0", "fixture-1"]) + "lookup lost part of the installation's target set" + require (target.installRoot? == installRoot?) "lookup guessed or lost the standalone installation root" + let .error failure ← (installation.runtime.resolve project).run + | throw <| IO.userError "CLI admitted an unavailable target" + require (failure.failure.error.code == "setupError") "target failure changed its CLI code" + let publicJson := (prepareFailureResponse failure).json + let data ← IO.ofExcept <| publicJson.getObjVal? "error" >>= (·.getObjVal? "data") + require ((data.getObjValAs? String "selector_path").toOption == some (project / "lean-toolchain").toString) + "public failure omitted the selecting path" + require ((data.getObjValAs? String "selector_text").toOption == some "foreign-alias") + "public failure omitted the requested selector" + require ((data.getObjValAs? (Array String) "retained_targets").toOption == some target.retainedTargets) + "public failure lost retained targets" + require ((data.getObjVal? "projection_error").toOption.isNone) "target data failed its public schema" + match target.remedy with + | .install command _ => + require (failure.remedyCommand? == some command && + (data.getObjValAs? String "remedy_command").toOption == some command) + "CLI lost the copyable installer command" + | .manual _ => + require (failure.remedyCommand?.isNone && (data.getObjVal? "remedy_command").toOption.isNone) + "CLI invented an installer command without a supported context" + +private def remedyExample (directory : System.FilePath) : IO Unit := do + let root := directory / "install root's" + let target : UnavailableTarget := { + selected := { + path := directory / "project's/lean-toolchain" + text := "requested'alias" + command := directory / "sdk/bin/lean" + installerToolchain? := some "requested'alias" } + installationRoot := root / "versions" / String.ofList (List.replicate 64 'a') + installRoot? := some root + retainedTargets := #["leanprover/lean4:v4.35.0", "retained'alias"] + bundled := false, sourceCommit? := some (String.ofList (List.replicate 40 'b')) } + let .install command precondition := target.remedy + | throw <| IO.userError "named targets did not produce an installer remedy" + require ((precondition.splitOn "source checkout").length > 1) "remedy omitted its checkout precondition" + for unsupported in ["leanprover/lean4:v4.33.1", "leanprover/lean4:stable", "alias with spaces"] do + let bad := { target with selected.installerToolchain? := some unsupported } + match bad.remedy with + | .manual _ => pure () + | .install .. => throw <| IO.userError "unsupported selector received an installer command" + for manual in [{ target with bundled := true }, { target with installRoot? := none }, + { target with selected.installerToolchain? := none }, + { target with retainedTargets := #["/unregistered-sdk"] }, + { target with retainedTargets := #["leanprover/lean4:v4.33.1"] }] do + match manual.remedy with + | .manual _ => pure () + | .install .. => throw <| IO.userError "unestablished installer context received a command" + IO.println <| Lean.Json.compress <| Lean.Json.mkObj [ + ("command", Lean.toJson command), ("install_root", Lean.toJson root.toString)] + private def admitsControl (installation : Installation) (owner daemon : System.FilePath) : IO Bool := do let entry : Beam.Daemon.SessionDescriptor := { schemaVersion := Beam.Daemon.registrySchemaVersion @@ -79,9 +141,13 @@ private def checkShadowedAlias (directory : System.FilePath) (phase : String) : let exact ← Beam.resolveExistingPath (directory / "sdk-0/bin" / ("lean" ++ suffix)) require (Beam.sameCanonicalPath exact reference.description.command) "removing the alias did not restore the exact installed release" - | "healthy", .error (.unavailable command) => + | "healthy", .error (.unavailable target) => let foreign ← Beam.resolveExistingPath (directory / "foreign/bin" / ("lean" ++ suffix)) - require (Beam.sameCanonicalPath command foreign) "healthy alias did not shadow the exact release" + require (Beam.sameCanonicalPath target.selected.command foreign) "healthy alias did not shadow the exact release" + require (target.selected.path == project / "lean-toolchain" && + target.selected.text == "leanprover/lean4:v4.34.1" && + target.selected.installerToolchain? == some "v4.34.1") + "unavailable shadowing alias lost the selecting file, text, or local link" | "missing-compiler", .error (.selection (.io _)) | "nonfile-compiler", .error (.selection (.io _)) | "dangling", .error (.selection (.io _)) => pure () @@ -106,6 +172,15 @@ private def runFullFixture (directory : System.FilePath) : IO Unit := do require (record.payloadHash == foreignRecord.payloadHash) "fixture installations must have identical versions and bytes" let installation ← Beam.Installation.openExecutable (g / ("libexec/beam-cli" ++ suffix)) .cli false let other ← Beam.Installation.openExecutable (h / ("libexec/beam-cli" ++ suffix)) .cli false + checkUnavailableContext installation project + let installRoot := directory / "owned install's" + let ownedHome := installRoot / "versions" / record.payloadHash + let ownedRecord ← stage directory ownedHome + require (ownedRecord.payloadHash == record.payloadHash) "fixture payload changed with its installation root" + write installRoot ".lean-beam-install-root" + s!"schema=1\nowner=lean-beam\nroot={installRoot}\n" + let owned ← Beam.Installation.openExecutable (ownedHome / ("libexec/beam-cli" ++ suffix)) .cli false + checkUnavailableContext owned project (some installRoot) let selector := fun text => IO.FS.writeFile (project / "lean-toolchain") (text ++ "\n") let selectors := ["absent", "valid-link", "dangling-link", "unreadable"] ++ if System.Platform.isWindows then [] else ["fifo", "fifo-link"] @@ -114,8 +189,8 @@ private def runFullFixture (directory : System.FilePath) : IO Unit := do (some (directory / "elan")) match name, selected with | "absent", .ok none => pure () - | "valid-link", .ok (some command) => - require (command.toString == first.lean) "selector symlink chose the wrong target" + | "valid-link", .ok (some selected) => + require (selected.command.toString == first.lean) "selector symlink chose the wrong target" | "dangling-link", .error (.io _) | "unreadable", .error (.io _) | "fifo", .error (.io _) | "fifo-link", .error (.io _) => pure () | _, _ => throw <| IO.userError s!"selector absence/error distinction failed: {name}" @@ -190,6 +265,7 @@ private def runFullFixture (directory : System.FilePath) : IO Unit := do def main (args : List String) : IO Unit := do match args with | [directory] => runFullFixture directory + | [directory, "remedy"] => remedyExample directory | [directory, "shadowed-alias", phase] => checkShadowedAlias (← Beam.resolveExistingPath directory) phase | _ => throw <| IO.userError "expected owned fixture directory and optional shadowing-alias phase" diff --git a/tests/lib/bundled-mcp-lifetime.py b/tests/lib/bundled-mcp-lifetime.py index 0897bd88e..347454aa1 100644 --- a/tests/lib/bundled-mcp-lifetime.py +++ b/tests/lib/bundled-mcp-lifetime.py @@ -87,8 +87,9 @@ def check(server, provenance, foreign_selector, *, env, matching_selectors=None) if scenario == "generation": assert "generation changed" in message and "restart" in message, rejected elif scenario == "foreign selector": - assert "has no runtime for" in message and "compiler was found" in message, rejected - assert "install Beam for this exact target" in message, rejected + assert "has no runtime for" in message, rejected + assert "bundled Beam serves only its containing Lean installation" in message, rejected + assert "lean-toolchain" in message and selector in message, rejected else: assert "unavailable locally" in message and "install or link" in message, rejected if scenario == "generation": diff --git a/tests/test-installation-entrypoints.py b/tests/test-installation-entrypoints.py index 52825cfa8..a2624fd93 100644 --- a/tests/test-installation-entrypoints.py +++ b/tests/test-installation-entrypoints.py @@ -84,6 +84,11 @@ def run(command, *arguments, env, cwd, ok=True, input=None): refused = run(cli_g, *arguments, "serve", env=admission_env, cwd=rejected_project, ok=False) assert "has no runtime for" in refused.stderr, refused.stderr + error = json.loads(refused.stdout)["error"] + assert error["code"] == "setupError", error + assert error["data"]["selector_path"] == str(rejected_project / "lean-toolchain"), error + assert error["data"]["selector_text"] == str(foreign), error + assert "remedy_command" not in error["data"], error if existing: assert [path.name for path in control.iterdir()] == ["retained-owner-state"] assert (control / "retained-owner-state").read_bytes() == b"must not change\n" diff --git a/tests/test-installation-lookup.py b/tests/test-installation-lookup.py index 1c385b22c..81ec7c43d 100644 --- a/tests/test-installation-lookup.py +++ b/tests/test-installation-lookup.py @@ -3,6 +3,7 @@ # Released under Apache 2.0 license as described in the file LICENSE. """Local target lookup never executes candidate compilers, providers, or construction tools.""" +import json import os from pathlib import Path import shutil @@ -114,3 +115,21 @@ def run_lookup(*arguments): else: unreadable.parent.chmod(0o700) assert not calls.exists(), "lookup invoked a candidate compiler before rejecting it" + + # Execute only a fake source installer: verify the emitted POSIX quoting and complete target set. + recipe = subprocess.run( + [ROOT / ".lake/build/bin" / ("beam-installation-lookup-test" + suffix), directory, "remedy"], + env=environment, check=True, capture_output=True, text=True, timeout=30) + remedy = json.loads(recipe.stdout) + checkout = directory / "Beam checkout's" + (checkout / "scripts").mkdir(parents=True) + installer = checkout / "scripts/install-beam.sh" + installer.write_text("#!/bin/sh\nexec python3 -c 'import json,os,sys; " + "print(json.dumps([os.environ[\"BEAM_INSTALL_ROOT\"], *sys.argv[1:]]))' \"$@\"\n") + installer.chmod(0o755) + executed = subprocess.run(["bash", "-c", remedy["command"]], cwd=checkout, + env=environment, capture_output=True, text=True, check=True, timeout=15) + assert json.loads(executed.stdout) == [ + remedy["install_root"], "--toolchain", "leanprover/lean4:v4.35.0", + "--custom-toolchain", "retained'alias", "--custom-toolchain", "requested'alias"] + assert not calls.exists(), "rendering a remedy invoked a candidate compiler" diff --git a/tests/test-native-toolchain.py b/tests/test-native-toolchain.py index 30df46f52..e8ea16d22 100644 --- a/tests/test-native-toolchain.py +++ b/tests/test-native-toolchain.py @@ -598,6 +598,8 @@ def artifact_family(): assert mismatch.returncode == 1, mismatch assert json.loads(mismatch.stdout)["error"]["code"] == "setupError", mismatch assert "has no runtime for" in mismatch.stderr and "compiler was found" in mismatch.stderr, mismatch + assert "native-other" in mismatch.stderr and "lean-toolchain" in mismatch.stderr, mismatch + assert "bundled Beam serves only its containing Lean installation" in mismatch.stderr, mismatch # An inherited elan override must neither hide a foreign project selector nor reject # a project that explicitly selects this installation. From b56bcee103a905eba4f53b42960cf49221c2c32a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 27 Oct 2026 10:14:35 +0100 Subject: [PATCH 2/8] fix: reject unsupported installer remedies before layout guidance --- Beam/Installation/Lookup.lean | 2 ++ tests/lean/BeamTest/Installation/LookupTest.lean | 8 ++++++++ 2 files changed, 10 insertions(+) diff --git a/Beam/Installation/Lookup.lean b/Beam/Installation/Lookup.lean index 508698a0b..e02ab04f3 100644 --- a/Beam/Installation/Lookup.lean +++ b/Beam/Installation/Lookup.lean @@ -53,6 +53,8 @@ private def installerTargetArguments (toolchain : String) : Except String (List 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 target.bundled 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" diff --git a/tests/lean/BeamTest/Installation/LookupTest.lean b/tests/lean/BeamTest/Installation/LookupTest.lean index 0012c9f7f..64771e1cc 100644 --- a/tests/lean/BeamTest/Installation/LookupTest.lean +++ b/tests/lean/BeamTest/Installation/LookupTest.lean @@ -79,6 +79,14 @@ private def remedyExample (directory : System.FilePath) : IO Unit := do match bad.remedy with | .manual _ => pure () | .install .. => throw <| IO.userError "unsupported selector received an installer command" + let unsupportedBundle := { target with + bundled := true + selected.installerToolchain? := some "leanprover/lean4:v4.33.1" } + match unsupportedBundle.remedy with + | .manual detail => + require ((detail.splitOn "does not admit official target").length > 1) + "bundled guidance suggested provisioning an unsupported official release" + | .install .. => throw <| IO.userError "unsupported bundled target received an installer command" for manual in [{ target with bundled := true }, { target with installRoot? := none }, { target with selected.installerToolchain? := none }, { target with retainedTargets := #["/unregistered-sdk"] }, From aebe689af096d38c037cd586e5f60006b83fee03 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 27 Oct 2026 10:17:37 +0100 Subject: [PATCH 3/8] refactor: isolate pure toolchain policy from construction --- Beam/Install/Toolchain.lean | 4 ++-- Beam/Installation/Lookup.lean | 6 +++--- Beam/{Install => Installation}/ToolchainPolicy.lean | 4 ++-- tests/lean/BeamTest/Installation/ConstructionTest.lean | 4 ++-- 4 files changed, 9 insertions(+), 9 deletions(-) rename Beam/{Install => Installation}/ToolchainPolicy.lean (96%) diff --git a/Beam/Install/Toolchain.lean b/Beam/Install/Toolchain.lean index 454bf0dba..25f016414 100644 --- a/Beam/Install/Toolchain.lean +++ b/Beam/Install/Toolchain.lean @@ -5,7 +5,7 @@ Author: Emilio J. Gallego Arias -/ import Lean -import Beam.Install.ToolchainPolicy +import Beam.Installation.ToolchainPolicy import Beam.Installation.Components import Beam.Path import Beam.System @@ -52,7 +52,7 @@ private def readRequiredToolchainCmdTrim (toolchain exe : String) (args : Array /-- 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 diff --git a/Beam/Installation/Lookup.lean b/Beam/Installation/Lookup.lean index e02ab04f3..2b9dd25a4 100644 --- a/Beam/Installation/Lookup.lean +++ b/Beam/Installation/Lookup.lean @@ -8,7 +8,7 @@ import Beam.Installation.Manifest import Beam.Installation.Bundled import Beam.Installation.LocalTarget import Beam.Installation.StandaloneLayout -import Beam.Install.ToolchainPolicy +import Beam.Installation.ToolchainPolicy import Beam.Project import Beam.Runtime import Beam.Version @@ -45,11 +45,11 @@ private def installerTargetArguments (toolchain : String) : Except String (List 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.Install.releaseToolchainSupported toolchain then + if Beam.Installation.ToolchainPolicy.releaseToolchainSupported toolchain then return ["--toolchain", toolchain] if toolchain.startsWith "leanprover/lean4:" then throw <| s!"this Beam revision does not admit official target '{toolchain}' for installation; " ++ - s!"select a supported exact target such as {Beam.Install.validatedToolchains.headD "a validated Lean toolchain"}" + s!"select a supported exact target such as {Beam.Installation.ToolchainPolicy.validatedToolchains.headD "a validated Lean toolchain"}" return ["--custom-toolchain", toolchain] def UnavailableTarget.remedy (target : UnavailableTarget) : TargetRemedy := Id.run do diff --git a/Beam/Install/ToolchainPolicy.lean b/Beam/Installation/ToolchainPolicy.lean similarity index 96% rename from Beam/Install/ToolchainPolicy.lean rename to Beam/Installation/ToolchainPolicy.lean index 164cc37ea..c2d138871 100644 --- a/Beam/Install/ToolchainPolicy.lean +++ b/Beam/Installation/ToolchainPolicy.lean @@ -6,7 +6,7 @@ Author: Emilio J. Gallego Arias import Lean -namespace Beam.Install +namespace Beam.Installation.ToolchainPolicy private def canonicalNat? (text : String) : Option Nat := do let value ← text.toNat? @@ -51,4 +51,4 @@ def releaseToolchainSupported (toolchain : String) : Bool := let [major, minor, _] := ((version.splitOn "-").headD "").splitOn "." | return false return compatibleReleaseLines.contains s!"leanprover/lean4:v{major}.{minor}" -end Beam.Install +end Beam.Installation.ToolchainPolicy diff --git a/tests/lean/BeamTest/Installation/ConstructionTest.lean b/tests/lean/BeamTest/Installation/ConstructionTest.lean index 63879817c..49da45ca8 100644 --- a/tests/lean/BeamTest/Installation/ConstructionTest.lean +++ b/tests/lean/BeamTest/Installation/ConstructionTest.lean @@ -63,11 +63,11 @@ private def checkStageOutput (directory : System.FilePath) : IO Unit := do private def checkCanonicalVersions : IO Unit := do for (toolchain, version) in [("leanprover/lean4:v4.34.0", "4.34.0"), ("leanprover/lean4:v4.34.0-rc2", "4.34.0-rc2"), ("leanprover/lean4:v4.34.2", "4.34.2")] do - require (canonicalLeanVersion? toolchain == some version) s!"canonical selector was not parsed: {toolchain}" + require (Beam.Installation.ToolchainPolicy.canonicalLeanVersion? toolchain == some version) s!"canonical selector was not parsed: {toolchain}" for invalid in ["leanprover/lean4:v4.34", "leanprover/lean4:v4.34.0-rc0", "leanprover/lean4:v4.34.0-rc01", "leanprover/lean4:v04.34.0", "leanprover/lean4:v4.34.0-beta1", "leanprover/lean4-nightly:nightly-2026-08-01", "lean4-stage0"] do - require (canonicalLeanVersion? invalid).isNone s!"noncanonical selector was accepted: {invalid}" + require (Beam.Installation.ToolchainPolicy.canonicalLeanVersion? invalid).isNone s!"noncanonical selector was accepted: {invalid}" require (expectedCanonicalLeanVersionPrefix? "leanprover/lean4:v4.34.0-rc2" == some "Lean (version 4.34.0-rc2,") "canonical Lean version prefix should use the exact RC" From 99d3c609dd7e022960f838b745bb6ae739ad3449 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 28 Oct 2026 18:31:27 +0100 Subject: [PATCH 4/8] fix: retain custom-target setup link in manual guidance --- Beam/Installation/Lookup.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Beam/Installation/Lookup.lean b/Beam/Installation/Lookup.lean index 2b9dd25a4..4ce2e40f5 100644 --- a/Beam/Installation/Lookup.lean +++ b/Beam/Installation/Lookup.lean @@ -86,7 +86,8 @@ def UnavailableTarget.message (target : UnavailableTarget) : String := s!"bound Beam installation: {target.installationRoot}. " match target.remedy with | .install command precondition => message ++ precondition ++ "\n" ++ command - | .manual detail => message ++ detail + | .manual detail => message ++ detail ++ + ". For custom-target setup, see https://github.com/leanprover/lean-beam/blob/main/docs/CUSTOM_TOOLCHAINS.md" inductive Failure where | invalid (detail : String) From 3cf1a666faeca443b299cf3764b374f9ca614961 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 29 Oct 2026 13:14:25 +0100 Subject: [PATCH 5/8] test: isolate native doctor copies and use a portable remedy recorder --- tests/test-client-doctor-native.py | 24 ++++++++++++++++++++++-- tests/test-installation-lookup.py | 24 +++++++++++++++++++----- tests/test-native-provenance.py | 30 ++++++++++++++++++++++++++++++ 3 files changed, 71 insertions(+), 7 deletions(-) diff --git a/tests/test-client-doctor-native.py b/tests/test-client-doctor-native.py index 7511e8552..b77429285 100644 --- a/tests/test-client-doctor-native.py +++ b/tests/test-client-doctor-native.py @@ -4,9 +4,11 @@ """Portable static client checks against the already-built native CLI; no client is launched.""" import hashlib +from contextlib import contextmanager import json import os from pathlib import Path +import shutil import stat import subprocess import tempfile @@ -16,6 +18,23 @@ CLI = REPO / ".lake/build/bin" / ("beam-cli" + EXE) +@contextmanager +def inspection_cli(): + # Darwin may resolve a cache hard link by its cache pathname. Keep an independent + # executable beside the staged libraries, without editing the build or cache entry. + descriptor, name = tempfile.mkstemp(prefix="beam-client-doctor-", suffix=EXE, dir=CLI.parent) + os.close(descriptor) + command = Path(name) + try: + shutil.copyfile(CLI, command) + assert not command.is_symlink() and command.stat().st_nlink == 1, command + assert not command.samefile(CLI) and command.read_bytes() == CLI.read_bytes(), command + command.chmod(0o700) + yield command + finally: + command.unlink() + + def snapshot(root): result = {} for path in root.rglob("*"): @@ -28,7 +47,8 @@ def snapshot(root): def main(): - with tempfile.TemporaryDirectory(prefix="beam client doctor Ω ") as temporary: + with (tempfile.TemporaryDirectory(prefix="beam client doctor Ω ") as temporary, + inspection_cli() as cli): root = Path(temporary).resolve() home, workspace = root / "home", root / "workspace" home.mkdir() @@ -42,7 +62,7 @@ def main(): def inspect(*args, expected=0, environment=None, report=True): before = snapshot(root) - result = subprocess.run([CLI, "doctor", "clients", *args, "--json"], cwd=workspace, + result = subprocess.run([cli, "doctor", "clients", *args, "--json"], cwd=workspace, env=env if environment is None else environment, capture_output=True, text=True, encoding="utf-8", timeout=15) assert result.returncode == expected, (result.returncode, result.stdout, result.stderr) diff --git a/tests/test-installation-lookup.py b/tests/test-installation-lookup.py index 81ec7c43d..02011d3fa 100644 --- a/tests/test-installation-lookup.py +++ b/tests/test-installation-lookup.py @@ -124,12 +124,26 @@ def run_lookup(*arguments): checkout = directory / "Beam checkout's" (checkout / "scripts").mkdir(parents=True) installer = checkout / "scripts/install-beam.sh" - installer.write_text("#!/bin/sh\nexec python3 -c 'import json,os,sys; " - "print(json.dumps([os.environ[\"BEAM_INSTALL_ROOT\"], *sys.argv[1:]]))' \"$@\"\n") + # Explicit LF is required for a POSIX shebang on native Windows Python. Record shell + # values directly, avoiding another interpreter or MSYS argument conversion boundary. + installer.write_text('#!/bin/sh\nprintf \'%s\\0\' "$BEAM_INSTALL_ROOT" "$@" > remedy-arguments\n', + encoding="utf-8", newline="\n") installer.chmod(0o755) - executed = subprocess.run(["bash", "-c", remedy["command"]], cwd=checkout, - env=environment, capture_output=True, text=True, check=True, timeout=15) - assert json.loads(executed.stdout) == [ + bash = shutil.which("bash") + if os.name == "nt": + # Windows' ambient bash.exe can be the WSL launcher. Use the POSIX shell + # belonging to the Git/MSYS installation already required by native qualification. + git = shutil.which("git") + assert git, "remedy qualification requires Git and its POSIX Bash" + bash = next((parent / "bin/bash.exe" for parent in Path(git).resolve().parents + if (parent / "bin/bash.exe").is_file()), None) + assert bash, "remedy qualification requires POSIX Bash" + executed = subprocess.run([bash, "-c", remedy["command"]], cwd=checkout, + env=environment, capture_output=True, text=True, timeout=15) + assert executed.returncode == 0, (executed.args, executed.stdout, executed.stderr) + arguments = (checkout / "remedy-arguments").read_bytes().split(b"\0") + assert arguments.pop() == b"", arguments + assert [argument.decode("utf-8") for argument in arguments] == [ remedy["install_root"], "--toolchain", "leanprover/lean4:v4.35.0", "--custom-toolchain", "retained'alias", "--custom-toolchain", "requested'alias"] assert not calls.exists(), "rendering a remedy invoked a candidate compiler" diff --git a/tests/test-native-provenance.py b/tests/test-native-provenance.py index e1fe04579..47bf46bf2 100644 --- a/tests/test-native-provenance.py +++ b/tests/test-native-provenance.py @@ -538,5 +538,35 @@ def test_timeout_retains_compiler_output(self): self.assertEqual(report["stderr"], "compiler stderr\n") +class ClientDoctorExecutableTest(unittest.TestCase): + def test_inspection_copy_preserves_cache_alias_and_cleans_up_after_failure(self): + spec = importlib.util.spec_from_file_location( + "client_doctor_native", REPO / "tests/test-client-doctor-native.py") + doctor = importlib.util.module_from_spec(spec) + spec.loader.exec_module(doctor) + with tempfile.TemporaryDirectory(prefix="beam-client-doctor-cache-") as temporary: + root = Path(temporary) + source, cached = root / ("beam-cli" + EXE), root / "cached-artifact" + source.write_bytes(b"cached executable bytes") + os.link(source, cached) + source.chmod(0o555) + before = source.stat() + with mock.patch.object(doctor, "CLI", source): + with self.assertRaisesRegex(RuntimeError, "inspection failed"): + with doctor.inspection_cli() as executable: + self.assertEqual(executable.parent, source.parent) + self.assertEqual(executable.stat().st_nlink, 1) + self.assertFalse(executable.samefile(cached)) + self.assertEqual(executable.read_bytes(), cached.read_bytes()) + executable.write_bytes(b"independent copy") + raise RuntimeError("inspection failed") + self.assertFalse(executable.exists()) + self.assertEqual(source.read_bytes(), b"cached executable bytes") + self.assertEqual(cached.read_bytes(), source.read_bytes()) + after = source.stat() + for field in ["st_dev", "st_ino", "st_mode", "st_mtime_ns", "st_nlink", "st_size"]: + self.assertEqual(getattr(after, field), getattr(before, field), field) + + if __name__ == "__main__": unittest.main() From 94a891cda29f1c57e3a0b3555faf424e645d4fcd Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 2 Nov 2026 13:42:09 +0100 Subject: [PATCH 6/8] fix: withhold stale-generation reinstall recipes and type their context --- Beam/Cli/Installation.lean | 30 +++++--- Beam/Installation/Lookup.lean | 70 ++++++++++++------ docs/CUSTOM_TOOLCHAINS.md | 16 +++- .../BeamTest/Installation/LookupTest.lean | 73 ++++++++++++++++--- tests/test-installation-lookup.py | 2 +- 5 files changed, 140 insertions(+), 51 deletions(-) diff --git a/Beam/Cli/Installation.lean b/Beam/Cli/Installation.lean index c689f62b6..2418d3247 100644 --- a/Beam/Cli/Installation.lean +++ b/Beam/Cli/Installation.lean @@ -29,20 +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 data := [ - ("selectorPath", toJson target.selected.path.toString), - ("selectorText", toJson target.selected.text), - ("leanCommand", toJson target.selected.command.toString), - ("installationRoot", toJson target.installationRoot.toString), - ("retainedTargets", toJson target.retainedTargets)] - let failure := CliFailure.setup target.message - match target.remedy with - | .install command _ => failure.withRemedy command data - | .manual _ => { failure with failure.error.data? := some <| Json.mkObj data } + 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)) diff --git a/Beam/Installation/Lookup.lean b/Beam/Installation/Lookup.lean index 4ce2e40f5..6c3da78fc 100644 --- a/Beam/Installation/Lookup.lean +++ b/Beam/Installation/Lookup.lean @@ -21,20 +21,30 @@ 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 - /-- Present only for an observed, marked standalone install root and matching payload leaf. -/ - installRoot? : Option System.FilePath := none + installContext : TargetInstallContext := .unrecognized retainedTargets : Array String - bundled : Bool 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 "'" "'\\''" ++ "'" @@ -55,10 +65,14 @@ private def installerTargetArguments (toolchain : String) : Except String (List 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 target.bundled then + 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" - let some installRoot := target.installRoot? + 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? @@ -76,19 +90,25 @@ def UnavailableTarget.remedy (target : UnavailableTarget) : TargetRemedy := Id.r " ./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 every retained target; the installer will qualify the selected compilers and show its write plan. " ++ + "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." -def UnavailableTarget.message (target : UnavailableTarget) : String := +/-- 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 target.remedy with - | .install command precondition => message ++ precondition ++ "\n" ++ command + 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 @@ -267,6 +287,17 @@ 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) @@ -283,21 +314,12 @@ def Observation.lookup (observation : Observation) (root : System.FilePath) : IO plugin := resolved.plugin, daemonBin := resolved.daemon, toolchain := resolved.target.toolchain identity := ⟨observation.home, observation.record.generation⟩ }⟩ - let installRoot? ← do - if observation.record.isBundled then pure none else - match installedRuntimeLocation? observation.home with - | none => pure none - | some location => - if location.payload == observation.record.generation && - (← checkInstallRootMarker location.installRoot).isOk then - pure (some location.installRoot) - else pure none - return .error <| match selected with - | some selected => .unavailable { - selected, installationRoot := observation.home, installRoot? - retainedTargets := observation.record.components.targets.map (·.toolchain) - bundled := observation.record.isBundled, sourceCommit? := observation.record.sourceCommit? } - | 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 diff --git a/docs/CUSTOM_TOOLCHAINS.md b/docs/CUSTOM_TOOLCHAINS.md index e29e981bf..0804090f2 100644 --- a/docs/CUSTOM_TOOLCHAINS.md +++ b/docs/CUSTOM_TOOLCHAINS.md @@ -79,10 +79,18 @@ place. If a locally selected compiler is missing from the Beam target set, the CLI error identifies the `lean-toolchain` file, its interpreted selector, the resolved compiler, and the bound installation. Its JSON data includes `selector_path`, `selector_text`, `lean_command`, `installation_root`, and -`retained_targets`. When the standalone installer can provide the target, `remedy_command` names -the install root and includes every retained target alongside the requested one. Run it from the -Beam source checkout named in the message; the command uses POSIX shell syntax and retains the -installer's normal confirmation and qualification steps. Restart clients after installing. +`retained_targets`. That list describes the inspected generation, including when a process is +still bound to an older generation. A reinstall recipe is offered only when the inspected +generation can also be confirmed as `current`. Its `remedy_command` names the install root and +includes that generation's targets alongside the requested one. + +The recipe is a snapshot, not an atomic update. Before running it, confirm that the current target +set still matches the inspected list: the installer replaces the complete selection. Run it from +a Beam source checkout at the revision given in the message, when available. The command uses +POSIX shell syntax and retains the installer's normal confirmation and qualification steps. +Restart clients after installing. If `current` has changed or cannot be confirmed, inspect the +current installation before choosing a target set; Beam supplies manual guidance instead of a +recipe based on an older selection. Bundled SDKs, direct filesystem selectors, unsupported official releases, and unrecognized installation layouts receive manual guidance instead of an invented installer command. A raw SDK diff --git a/tests/lean/BeamTest/Installation/LookupTest.lean b/tests/lean/BeamTest/Installation/LookupTest.lean index 64771e1cc..364649989 100644 --- a/tests/lean/BeamTest/Installation/LookupTest.lean +++ b/tests/lean/BeamTest/Installation/LookupTest.lean @@ -29,7 +29,7 @@ private def rejected (installation : Installation) (project : System.FilePath) : | .ok _ => throw <| IO.userError "unavailable or invalid installation unexpectedly admitted a runtime" private def checkUnavailableContext (installation : Installation) (project : System.FilePath) - (installRoot? : Option System.FilePath := none) : IO Unit := do + (context : TargetInstallContext := .unrecognized) : IO Unit := do IO.FS.writeFile (project / "lean-toolchain") "foreign-alias\n" let .error (.unavailable target) ← installation.lookup project | throw <| IO.userError "expected a typed unavailable target" @@ -37,7 +37,7 @@ private def checkUnavailableContext (installation : Installation) (project : Sys "lookup lost its selected file or text" require (target.retainedTargets == #["fixture-0", "fixture-1"]) "lookup lost part of the installation's target set" - require (target.installRoot? == installRoot?) "lookup guessed or lost the standalone installation root" + require (target.installContext == context) "lookup guessed or lost its installation context" let .error failure ← (installation.runtime.resolve project).run | throw <| IO.userError "CLI admitted an unavailable target" require (failure.failure.error.code == "setupError") "target failure changed its CLI code" @@ -55,10 +55,17 @@ private def checkUnavailableContext (installation : Installation) (project : Sys require (failure.remedyCommand? == some command && (data.getObjValAs? String "remedy_command").toOption == some command) "CLI lost the copyable installer command" + require (!failure.failure.error.message.endsWith ("\n" ++ command)) + "CLI embedded the separately rendered remedy in its explanation" | .manual _ => require (failure.remedyCommand?.isNone && (data.getObjVal? "remedy_command").toOption.isNone) "CLI invented an installer command without a supported context" +private structure RemedyFixtureOutput where + command : String + installRoot : String + deriving Lean.ToJson + private def remedyExample (directory : System.FilePath) : IO Unit := do let root := directory / "install root's" let target : UnavailableTarget := { @@ -68,9 +75,9 @@ private def remedyExample (directory : System.FilePath) : IO Unit := do command := directory / "sdk/bin/lean" installerToolchain? := some "requested'alias" } installationRoot := root / "versions" / String.ofList (List.replicate 64 'a') - installRoot? := some root + installContext := .current root retainedTargets := #["leanprover/lean4:v4.35.0", "retained'alias"] - bundled := false, sourceCommit? := some (String.ofList (List.replicate 40 'b')) } + sourceCommit? := some (String.ofList (List.replicate 40 'b')) } let .install command precondition := target.remedy | throw <| IO.userError "named targets did not produce an installer remedy" require ((precondition.splitOn "source checkout").length > 1) "remedy omitted its checkout precondition" @@ -80,22 +87,24 @@ private def remedyExample (directory : System.FilePath) : IO Unit := do | .manual _ => pure () | .install .. => throw <| IO.userError "unsupported selector received an installer command" let unsupportedBundle := { target with - bundled := true + installContext := .bundled selected.installerToolchain? := some "leanprover/lean4:v4.33.1" } match unsupportedBundle.remedy with | .manual detail => require ((detail.splitOn "does not admit official target").length > 1) "bundled guidance suggested provisioning an unsupported official release" | .install .. => throw <| IO.userError "unsupported bundled target received an installer command" - for manual in [{ target with bundled := true }, { target with installRoot? := none }, + for manual in [{ target with installContext := .bundled }, + { target with installContext := .unrecognized }, + { target with installContext := .unconfirmed root }, { target with selected.installerToolchain? := none }, { target with retainedTargets := #["/unregistered-sdk"] }, { target with retainedTargets := #["leanprover/lean4:v4.33.1"] }] do match manual.remedy with | .manual _ => pure () | .install .. => throw <| IO.userError "unestablished installer context received a command" - IO.println <| Lean.Json.compress <| Lean.Json.mkObj [ - ("command", Lean.toJson command), ("install_root", Lean.toJson root.toString)] + let output : RemedyFixtureOutput := { command, installRoot := root.toString } + IO.println (Lean.toJson output).compress private def admitsControl (installation : Installation) (owner daemon : System.FilePath) : IO Bool := do let entry : Beam.Daemon.SessionDescriptor := { @@ -116,16 +125,17 @@ private def admitsControl (installation : Installation) (owner daemon : System.F "ownership admission must preserve the typed installation mismatch" pure false -private def stage (directory root : System.FilePath) : IO InstallManifest := do +private def stage (directory root : System.FilePath) (extraTarget := false) : IO InstallManifest := do let suffix := if System.Platform.isWindows then ".exe" else "" let mut targets := #[] - for i in [:2] do + for i in [:if extraTarget then 3 else 2] do let daemon := s!"runtimes/{i}/bin/daemon{suffix}" let plugin := s!"runtimes/{i}/plugin" write root daemon "fixture daemon must never be invoked during lookup" write root plugin "fixture plugin must never be loaded during lookup" + let sdk := if i < 2 then s!"sdk-{i}" else "foreign" targets := targets.push { - lean := (← Beam.resolveExistingPath (directory / s!"sdk-{i}" / "bin" / ("lean" ++ suffix))).toString + lean := (← Beam.resolveExistingPath (directory / sdk / "bin" / ("lean" ++ suffix))).toString daemon, plugin, toolchain := s!"fixture-{i}" compilerRevision := Lean.githash, leanVersion := "Lean fixture", lakeVersion := "Lake fixture" } @@ -137,6 +147,15 @@ private def stage (directory root : System.FilePath) : IO InstallManifest := do license := "LICENSE", targets } +private def linkCurrent (home current : System.FilePath) : IO Unit := do + let out ← IO.Process.output <| if System.Platform.isWindows then { + cmd := "cmd", args := #["/d", "/c", "mklink", "/J", current.toString, home.toString] } + else { cmd := "ln", args := #["-s", home.toString, current.toString] } + unless out.exitCode == 0 do throw <| IO.userError s!"cannot create current fixture: {out.stderr}" + +private def unlinkCurrent (current : System.FilePath) : IO Unit := + if System.Platform.isWindows then IO.FS.removeDir current else IO.FS.removeFile current + private def checkShadowedAlias (directory : System.FilePath) (phase : String) : IO Unit := do let suffix := if System.Platform.isWindows then ".exe" else "" let home := directory / s!"shadowed-alias-{phase}" @@ -188,7 +207,37 @@ private def runFullFixture (directory : System.FilePath) : IO Unit := do write installRoot ".lean-beam-install-root" s!"schema=1\nowner=lean-beam\nroot={installRoot}\n" let owned ← Beam.Installation.openExecutable (ownedHome / ("libexec/beam-cli" ++ suffix)) .cli false - checkUnavailableContext owned project (some installRoot) + let current := installRoot / "current" + checkUnavailableContext owned project (.unconfirmed installRoot) + linkCurrent ownedHome current + checkUnavailableContext owned project (.current installRoot) + -- A valid successor adds a third target. An older bound process must not publish a + -- recipe based on its two-target snapshot that would remove the successor's addition. + let staging := directory / "successor staging" + let successorRecord ← stage directory staging true + let successor := installRoot / "versions" / successorRecord.payloadHash + IO.FS.rename staging successor + unlinkCurrent current + linkCurrent successor current + let successorBytes ← IO.FS.readFile (successor / "manifest.json") + checkUnavailableContext owned project (.unconfirmed installRoot) + let fresh ← Beam.Installation.openExecutable (successor / ("libexec/beam-cli" ++ suffix)) .cli false + discard <| accepted fresh project + require (Beam.sameCanonicalPath (← Beam.resolveExistingPath current) successor) + "diagnosing the older generation changed current" + require ((← IO.FS.readFile (successor / "manifest.json")) == successorBytes) + "diagnosing the older generation changed its successor" + unlinkCurrent current + let missing := installRoot / "missing generation" + IO.FS.createDirAll missing + linkCurrent missing current + IO.FS.removeDir missing + checkUnavailableContext owned project (.unconfirmed installRoot) + unlinkCurrent current + IO.FS.writeFile current "not an installation directory" + checkUnavailableContext owned project (.unconfirmed installRoot) + IO.FS.removeFile current + IO.println "current-generation recipes and superseded, missing, broken, and invalid current checks passed" let selector := fun text => IO.FS.writeFile (project / "lean-toolchain") (text ++ "\n") let selectors := ["absent", "valid-link", "dangling-link", "unreadable"] ++ if System.Platform.isWindows then [] else ["fifo", "fifo-link"] diff --git a/tests/test-installation-lookup.py b/tests/test-installation-lookup.py index 02011d3fa..21b1cdb49 100644 --- a/tests/test-installation-lookup.py +++ b/tests/test-installation-lookup.py @@ -144,6 +144,6 @@ def run_lookup(*arguments): arguments = (checkout / "remedy-arguments").read_bytes().split(b"\0") assert arguments.pop() == b"", arguments assert [argument.decode("utf-8") for argument in arguments] == [ - remedy["install_root"], "--toolchain", "leanprover/lean4:v4.35.0", + remedy["installRoot"], "--toolchain", "leanprover/lean4:v4.35.0", "--custom-toolchain", "retained'alias", "--custom-toolchain", "requested'alias"] assert not calls.exists(), "rendering a remedy invoked a candidate compiler" From 82d5c50784b3085c346e0a003f011a5e43974a45 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 2 Nov 2026 14:39:35 +0100 Subject: [PATCH 7/8] test: use native Python encoding for Windows junction fixtures --- tests/lean/BeamTest/Installation/LookupTest.lean | 13 ++++++++++--- tests/test-installation-lookup.py | 3 ++- 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/tests/lean/BeamTest/Installation/LookupTest.lean b/tests/lean/BeamTest/Installation/LookupTest.lean index 364649989..a0a4e9940 100644 --- a/tests/lean/BeamTest/Installation/LookupTest.lean +++ b/tests/lean/BeamTest/Installation/LookupTest.lean @@ -148,9 +148,16 @@ private def stage (directory root : System.FilePath) (extraTarget := false) : IO } private def linkCurrent (home current : System.FilePath) : IO Unit := do - let out ← IO.Process.output <| if System.Platform.isWindows then { - cmd := "cmd", args := #["/d", "/c", "mklink", "/J", current.toString, home.toString] } - else { cmd := "ln", args := #["-s", home.toString, current.toString] } + let out ← if System.Platform.isWindows then do + let some python ← IO.getEnv "BEAM_TEST_PYTHON" + | throw <| IO.userError "lookup fixture requires its driver's Python interpreter" + -- Lean quotes every Windows argument, including cmd's builtin name. Python's + -- command-line encoder preserves the mklink syntax already used by this fixture's driver. + IO.Process.output { + cmd := python + args := #["-c", "import subprocess,sys; subprocess.run(['cmd','/d','/c','mklink','/J',*sys.argv[1:]],check=True)", + current.toString, home.toString] } + else IO.Process.output { cmd := "ln", args := #["-s", home.toString, current.toString] } unless out.exitCode == 0 do throw <| IO.userError s!"cannot create current fixture: {out.stderr}" private def unlinkCurrent (current : System.FilePath) : IO Unit := diff --git a/tests/test-installation-lookup.py b/tests/test-installation-lookup.py index 21b1cdb49..e724230ba 100644 --- a/tests/test-installation-lookup.py +++ b/tests/test-installation-lookup.py @@ -8,6 +8,7 @@ from pathlib import Path import shutil import subprocess +import sys import tempfile ROOT = Path(__file__).resolve().parent.parent @@ -23,7 +24,7 @@ command.write_text(f'#!/bin/sh\nprintf invoked >> "{calls}"\nexit 99\n') command.chmod(0o755) environment = dict(os.environ, ELAN_HOME=str(directory / "elan"), - BEAM_HOME=str(directory / "foreign")) + BEAM_HOME=str(directory / "foreign"), BEAM_TEST_PYTHON=sys.executable) elan = shutil.which("elan") assert elan, "local link fixtures require elan" From 60a2a72b08f5a1d3935e6fd6c9454413b7c68747 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 2 Nov 2026 14:56:52 +0100 Subject: [PATCH 8/8] fix: preserve project toolchain pins in unsupported-target guidance --- Beam/Installation/Lookup.lean | 5 +++-- tests/lean/BeamTest/Installation/LookupTest.lean | 16 ++++++++++++---- 2 files changed, 15 insertions(+), 6 deletions(-) diff --git a/Beam/Installation/Lookup.lean b/Beam/Installation/Lookup.lean index 6c3da78fc..c1659107c 100644 --- a/Beam/Installation/Lookup.lean +++ b/Beam/Installation/Lookup.lean @@ -58,8 +58,9 @@ private def installerTargetArguments (toolchain : String) : Except String (List if Beam.Installation.ToolchainPolicy.releaseToolchainSupported toolchain then return ["--toolchain", toolchain] if toolchain.startsWith "leanprover/lean4:" then - throw <| s!"this Beam revision does not admit official target '{toolchain}' for installation; " ++ - s!"select a supported exact target such as {Beam.Installation.ToolchainPolicy.validatedToolchains.headD "a validated Lean toolchain"}" + 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 diff --git a/tests/lean/BeamTest/Installation/LookupTest.lean b/tests/lean/BeamTest/Installation/LookupTest.lean index a0a4e9940..d7a368f26 100644 --- a/tests/lean/BeamTest/Installation/LookupTest.lean +++ b/tests/lean/BeamTest/Installation/LookupTest.lean @@ -66,6 +66,15 @@ private structure RemedyFixtureOutput where installRoot : String deriving Lean.ToJson +private def checkUnsupportedOfficialGuidance (detail : String) : IO Unit := do + require ((detail.splitOn "does not support official target").length > 1) + "unsupported official target lost its explanation" + require ((detail.splitOn "supports the project's existing Lean toolchain").length > 1 && + (detail.splitOn "leave the project's lean-toolchain and dependency pins unchanged").length > 1) + "unsupported target guidance invited changing the project's toolchain or dependency pins" + require ((detail.splitOn "select a supported exact target").length == 1) + "unsupported target guidance suggested selecting another project toolchain" + private def remedyExample (directory : System.FilePath) : IO Unit := do let root := directory / "install root's" let target : UnavailableTarget := { @@ -84,15 +93,14 @@ private def remedyExample (directory : System.FilePath) : IO Unit := do for unsupported in ["leanprover/lean4:v4.33.1", "leanprover/lean4:stable", "alias with spaces"] do let bad := { target with selected.installerToolchain? := some unsupported } match bad.remedy with - | .manual _ => pure () + | .manual detail => + if unsupported.startsWith "leanprover/lean4:" then checkUnsupportedOfficialGuidance detail | .install .. => throw <| IO.userError "unsupported selector received an installer command" let unsupportedBundle := { target with installContext := .bundled selected.installerToolchain? := some "leanprover/lean4:v4.33.1" } match unsupportedBundle.remedy with - | .manual detail => - require ((detail.splitOn "does not admit official target").length > 1) - "bundled guidance suggested provisioning an unsupported official release" + | .manual detail => checkUnsupportedOfficialGuidance detail | .install .. => throw <| IO.userError "unsupported bundled target received an installer command" for manual in [{ target with installContext := .bundled }, { target with installContext := .unrecognized },