From 4362c49eedb8a72ebed74f28f984a1e882cfd6b7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 3 Nov 2026 11:27:55 +0100 Subject: [PATCH 1/3] fix: order lake build after session cleanup in save refusals Save refusals that suggest `lake build` (batch-only moreLeanArgs, deferred compilation, compiler-revision mismatch, stale save traces) did not say to stop the session first. Following them while the session was live left the broker's history marking the dependency as needing a save, so later importer syncs failed with a recovery plan that could not be followed (#256). Share one external-build procedure across these messages and the sync-barrier message, and document it. --- Beam/Broker/Errors.lean | 8 ++++++++ Beam/Broker/LakeSave.lean | 11 +++++++---- Beam/Broker/Server.lean | 4 +++- Beam/Broker/SyncSaveSupport.lean | 3 +-- CHANGELOG.md | 5 +++++ docs/MCP.md | 3 ++- docs/SETUP.md | 5 +++-- docs/STATUS.md | 3 ++- docs/SYNC_AND_DIAGNOSTICS.md | 11 ++++++++--- skills/lean-beam/SKILL.md | 2 +- skills/lean-beam/references/workflow-details.md | 7 ++++--- tests/test-beam-deferred-save.py | 1 + tests/test-beam-save-olean.sh | 12 ++++++++++-- tests/test-recovery-plan.py | 3 +++ 14 files changed, 58 insertions(+), 20 deletions(-) diff --git a/Beam/Broker/Errors.lean b/Beam/Broker/Errors.lean index 7e0aae8f1..8722c1daf 100644 --- a/Beam/Broker/Errors.lean +++ b/Beam/Broker/Errors.lean @@ -11,6 +11,14 @@ open Lean namespace Beam.Broker +/-- +The order for an external Lake build. Every message that suggests one must include it: a build while +the session is live leaves Beam's sync and save history describing artifacts that changed under it. +-/ +def externalLakeBuildProcedure : String := + "first stop the CLI owner or drop the MCP workspace and confirm cleanup; " ++ + "rebuild only after cleanup completes, then start a fresh session or workspace" + inductive BrokerFailureCode where | invalidParams | requestCancelled diff --git a/Beam/Broker/LakeSave.lean b/Beam/Broker/LakeSave.lean index 9eee6d90d..814d6abc0 100644 --- a/Beam/Broker/LakeSave.lean +++ b/Beam/Broker/LakeSave.lean @@ -101,7 +101,8 @@ private def saveTraceStaleMessage (root path : FilePath) : String := let relPath := Beam.pathRelativeToRootOrSelf root path s!"Lake save trace is stale for {relPath}. " ++ "A dependency or build input would need to rebuild before Beam can save this module safely. " ++ - "Save stale direct dependencies with lean-beam save, or run lake build and retry." + "Save stale direct dependencies with lean-beam save, then retry. " ++ + s!"If an external Lake build is required, {externalLakeBuildProcedure}." private def ensureSaveTraceReady (ws : Workspace) @@ -156,7 +157,8 @@ def computeSaveSpecification message := "lean-beam save requires matching compiler revisions for Beam's compiled code, " ++ "its loaded Lean runtime, and the target compiler; " ++ - "rebuild or reinstall Beam for the target Lean build, or use lake build instead" + "rebuild or reinstall Beam for the target Lean build, or use lake build instead: " ++ + externalLakeBuildProcedure } let some mod := ws.findModuleBySrc? path | return .error { @@ -175,7 +177,7 @@ def computeSaveSpecification s!"lean-beam save cannot reuse the Lean server snapshot for {relPath}: {reason}. " ++ "Move shared -D settings from moreLeanArgs to leanOptions so Lake applies them to both " ++ "the language server and batch compilation. If the arguments are intentionally batch-only, " ++ - "run lake build for this module instead." + s!"run lake build for this module instead: {externalLakeBuildProcedure}." data? := some <| Json.mkObj [("reason", toJson reason), ("path", toJson relPath)] } let depTraceResult ← buildDepTrace ws root path mod snapshot @@ -239,7 +241,8 @@ def writePrivateSaveTrace (spec : LeanSaveSpec) : IO Unit := do let expectedSchema ← IO.ofExcept <| (toJson (BuildMetadata.ofStub (Hash.ofNat 0))).getObjValAs? String "schemaVersion" unless schema == expectedSchema do - throw <| IO.userError s!"unsupported Lake trace schema '{schema}'; use lake build instead" + throw <| IO.userError <| + s!"unsupported Lake trace schema '{schema}'; use lake build instead: {externalLakeBuildProcedure}" let outputs ← leanSaveOutputs spec.toLeanSaveOutputs -- Preserve the target's dependency metadata; only completed output descriptors change. let metadata := spec.traceMetadata.setObjVal! "outputs" (toJson outputs) diff --git a/Beam/Broker/Server.lean b/Beam/Broker/Server.lean index 0b68b9fcc..883b10381 100644 --- a/Beam/Broker/Server.lean +++ b/Beam/Broker/Server.lean @@ -2373,7 +2373,9 @@ private def saveOleanCore saveReadiness.saveReadyReason == Beam.LSP.Save.saveReadinessDeferredCompilationReason then withFailureProgress barrierProgress? <| throwBrokerFailure { code := .saveUnsupportedSetup - message := saveReadiness.saveReadyMessage?.getD "Beam cannot save deferred compilation; use lake build instead." + message := + saveReadiness.saveReadyMessage?.getD "Beam cannot save deferred compilation; use lake build instead." ++ + s!" Before that build, {externalLakeBuildProcedure}." data? := some <| (syncResultErrorData syncResult) |>.setObjVal! "reason" (toJson saveReadiness.saveReadyReason) |>.setObjVal! "path" (toJson relPath) diff --git a/Beam/Broker/SyncSaveSupport.lean b/Beam/Broker/SyncSaveSupport.lean index 8d7403526..7d14aec0d 100644 --- a/Beam/Broker/SyncSaveSupport.lean +++ b/Beam/Broker/SyncSaveSupport.lean @@ -216,8 +216,7 @@ def syncBarrierIncompleteMessage "Follow recovery_plan in order; stop if a step fails. After refresh succeeds, inspect its " ++ "diagnostics and save readiness before continuing. If a save is unsupported or the barrier remains " ++ "incomplete, stop retrying and inspect upstream diagnostics and configuration. " ++ - "If an external Lake build is required, first stop the CLI owner or drop the MCP workspace " ++ - "and confirm cleanup; rebuild only after cleanup completes, then start a fresh session or workspace." + s!"If an external Lake build is required, {externalLakeBuildProcedure}." def leanSaveResult (spec : LeanSaveSpec) diff --git a/CHANGELOG.md b/CHANGELOG.md index b78c96ac0..fdc3a46eb 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,6 +12,11 @@ This project keeps a lightweight, reverse-chronological changelog. Dates use `YY ### Fixed +- `save` refusals that suggest `lake build` (`saveUnsupportedSetup`, `saveTraceStale`) now say to + stop the CLI owner or drop the MCP workspace and confirm cleanup before building, then start a + fresh session. Building while the session was live left dependencies marked as needing a save, + so every later sync of an importer failed with a recovery plan that could not be followed + ([#256](https://github.com/leanprover/lean-beam/issues/256), @ejgallego). - `sync` and `refresh` now return `internalError` when a diagnostic burst exhausts pending delivery capacity between complete output frames, rather than losing the terminal response. Recovery replies observe daemon shutdown; existing delivery budgets remain unchanged diff --git a/docs/MCP.md b/docs/MCP.md index 68b112c60..e9a746dae 100644 --- a/docs/MCP.md +++ b/docs/MCP.md @@ -445,7 +445,8 @@ when the client also needs the diagnostics/readiness barrier. `lean_save` and `lean_close_save` create development checkpoints from the accepted Lean server snapshot, including structured Lake options, dynamic libraries, and plugins already applied by the file worker. Modules with batch-only `moreLeanArgs` fail with `saveUnsupportedSetup`; move shared -`-D` settings to `leanOptions`, or use `lake build` when the arguments are intentionally batch-only. +`-D` settings to `leanOptions`, or use `lake build` when the arguments are intentionally batch-only, +after dropping the workspace and confirming cleanup. If an import changed on disk after the file worker loaded it, saving fails with `saveImportsChanged`; call `lean_refresh` so the worker reloads its imports, then save again. Successful checkpoints are normally sufficient for the local development loop, but MCP clients diff --git a/docs/SETUP.md b/docs/SETUP.md index dfddebe24..192721efa 100644 --- a/docs/SETUP.md +++ b/docs/SETUP.md @@ -485,8 +485,9 @@ options, plugins, or dynamic libraries, run `lean-beam --root ROOT stop`, then s includes structured Lake options, dynamic libraries, and plugins already applied by the file worker and avoids repeated module builds. Modules with batch-only `moreLeanArgs` fail with `saveUnsupportedSetup`; move shared `-D` settings to `leanOptions`, or use `lake build` when the -arguments are intentionally batch-only. A successful checkpoint is normally sufficient for local -development, so do not run a clean build after every Beam loop. At the end of the development loop, +arguments are intentionally batch-only, after stopping the session and confirming cleanup. A +successful checkpoint is normally sufficient for local development, so do not run a clean build +after every Beam loop. At the end of the development loop, use a successful CI `lake build` from a clean checkout or clean Lake build directory as batch-build evidence. diff --git a/docs/STATUS.md b/docs/STATUS.md index 0c654cb57..a832b266f 100644 --- a/docs/STATUS.md +++ b/docs/STATUS.md @@ -386,7 +386,8 @@ client protocol. solution. Structured Lake options, dynamic libraries, and plugins are supported when the Lean file worker has already applied them; batch-only `moreLeanArgs` fail with `saveUnsupportedSetup`. Deferred compilation (`compiler.postponeCompile`, including declaration-scoped settings) also - rejects zero-build saves; use `lake build` for that pipeline. See + rejects zero-build saves; use `lake build` for that pipeline after stopping the session and + confirming cleanup. See [SYNC_AND_DIAGNOSTICS.md](SYNC_AND_DIAGNOSTICS.md#command-model) for readiness and preservation guarantees. - Running Lake builds on the workspace while a Beam session has documents open is unsupported. As a temporary safeguard ([#370](https://github.com/leanprover/lean-beam/issues/370)), `save` and diff --git a/docs/SYNC_AND_DIAGNOSTICS.md b/docs/SYNC_AND_DIAGNOSTICS.md index 37a94687e..cb7c06a4a 100644 --- a/docs/SYNC_AND_DIAGNOSTICS.md +++ b/docs/SYNC_AND_DIAGNOSTICS.md @@ -191,7 +191,11 @@ Beam returns `saveUnsupportedSetup` after establishing the sync verdict and reso before Lake dependency-trace preparation. This rejection preserves the sync verdict under `error.data.sync` and leaves prior artifacts and the Lake trace unchanged. A rejected `close-save` also leaves the document open. Move shared `-D` settings from `moreLeanArgs` to `leanOptions`, or use -`lake build` when the arguments are intentionally batch-only. +`lake build` when the arguments are intentionally batch-only. Every save refusal that suggests +`lake build` also states the order from [Failures And Recovery](#failures-and-recovery): stop the +CLI owner or drop the MCP workspace and confirm cleanup before building, then start a fresh session +or workspace. A build while the session is live leaves Beam's sync and save history describing +older artifacts. A checkpoint must describe the imports it was elaborated against. When a Lean file worker loads a document's imports, Beam records the Lake trace (dependency hash and output hashes) of every @@ -226,8 +230,9 @@ A snapshot with `compiler.postponeCompile` enabled, or with declarations still w compilation, is not a complete checkpoint. Its sync result has `readiness.save_ready: false` and `readiness.reason: "deferredCompilation"`, even when elaboration has no errors. `save` and `close-save` reject it with `saveUnsupportedSetup` before changing artifacts or the Lake trace; -use `lake build` for this compilation pipeline. This also applies to declaration-scoped -`set_option compiler.postponeCompile true in`, whose option resets before the end of the file. +use `lake build` for this compilation pipeline, after stopping the session and confirming cleanup. +This also applies to declaration-scoped `set_option compiler.postponeCompile true in`, whose option +resets before the end of the file. ### Project Configuration Changes diff --git a/skills/lean-beam/SKILL.md b/skills/lean-beam/SKILL.md index 763a8c23a..36f477c4e 100644 --- a/skills/lean-beam/SKILL.md +++ b/skills/lean-beam/SKILL.md @@ -59,7 +59,7 @@ lean-beam save MyPkg/Sub/Module.lean - `save` checkpoints only that module. It does not validate importers, and it records the Lean server's environment, which can differ from batch elaboration. Modules with batch-only `moreLeanArgs` fail with `saveUnsupportedSetup`; move shared `-D` settings to `leanOptions`, or - use `lake build` when the arguments are intentionally batch-only. + stop Beam, then `lake build`, when the arguments are intentionally batch-only. - If `close-save` fails with `error.data.reason = "savedDocumentChanged"`, `error.data.saved` is an already committed checkpoint of the earlier version; run `update` or `sync` and save again if needed. diff --git a/skills/lean-beam/references/workflow-details.md b/skills/lean-beam/references/workflow-details.md index 62b344f96..f91f1d539 100644 --- a/skills/lean-beam/references/workflow-details.md +++ b/skills/lean-beam/references/workflow-details.md @@ -137,9 +137,10 @@ evidence. An elaborator that observes server mode can behave differently under ` Structured Lake options, dynamic libraries, and plugins are supported when the file worker has already applied them. Modules with batch-only `moreLeanArgs` fail with `saveUnsupportedSetup`; move shared `-D` settings to `leanOptions`, or use `lake build` when the arguments are intentionally -batch-only. If an import changed on disk after the file worker loaded it, for example through an -external `lake build`, saving fails with `saveImportsChanged`; run `lean-beam refresh FILE` so the -worker reloads its imports, then save again. +batch-only, after the [cleanup order](#before-a-local-batch-build). If an import changed on disk +after the file worker loaded it, for example through an external `lake build`, saving fails with +`saveImportsChanged`; run `lean-beam refresh FILE` so the worker reloads its imports, then save +again. Beam assumes Lake workspace configuration remains unchanged while the Lean server is running. After editing a lakefile, manifest, package override, `lean-toolchain`, Lean options, plugins, or dynamic diff --git a/tests/test-beam-deferred-save.py b/tests/test-beam-deferred-save.py index ad9126019..15932f3c1 100644 --- a/tests/test-beam-deferred-save.py +++ b/tests/test-beam-deferred-save.py @@ -73,6 +73,7 @@ def check_deferred_save(root, scoped): assert failure["code"] == "saveUnsupportedSetup", failure assert failure["data"]["sync"]["readiness"]["save_ready"] is False, failure assert "compiler.postponeCompile" in failure["message"], failure + assert "rebuild only after cleanup completes" in failure["message"], failure assert artifact_family(root) == before, command print(f"deferred compilation ({'scoped' if scoped else 'Lake option'}): rejected, prior family preserved") finally: diff --git a/tests/test-beam-save-olean.sh b/tests/test-beam-save-olean.sh index 0ffbf8259..d82ee2a71 100755 --- a/tests/test-beam-save-olean.sh +++ b/tests/test-beam-save-olean.sh @@ -674,6 +674,13 @@ PY cat "$unsupported_save_err" >&2 exit 1 fi + if ! assert_cli_error_json "$unsupported_save_out" saveUnsupportedSetup \ + "rebuild only after cleanup completes"; then + echo "expected unsupported setup failure to order lake build after session cleanup" >&2 + cat "$unsupported_save_out" >&2 + cat "$unsupported_save_err" >&2 + exit 1 + fi BEAM_BATCH_ONLY_SYNC="$batch_only_sync" python3 - "$unsupported_save_out" <<'PYRECEIPT' import json, os, pathlib, sys @@ -817,8 +824,9 @@ beam_start_owner "$tmp6" cat "$stale_trace_save_err" >&2 exit 1 fi - if ! assert_cli_error_json "$stale_trace_save_out" saveTraceStale; then - echo "expected stale trace save to report saveTraceStale" >&2 + if ! assert_cli_error_json "$stale_trace_save_out" saveTraceStale \ + "rebuild only after cleanup completes"; then + echo "expected stale trace save to report saveTraceStale and order lake build after cleanup" >&2 cat "$stale_trace_save_out" >&2 cat "$stale_trace_save_err" >&2 exit 1 diff --git a/tests/test-recovery-plan.py b/tests/test-recovery-plan.py index d2d4b88b2..b7ff6749e 100644 --- a/tests/test-recovery-plan.py +++ b/tests/test-recovery-plan.py @@ -196,6 +196,9 @@ def check_recovery(case, installation, surface, scenario): else: assert refusal["code"] == "saveUnsupportedSetup", refusal assert refusal["data"]["reason"] == "Lake module uses batch-only moreLeanArgs", refusal + # Building while this session is live would leave its sync history stale (#256). + assert "drop the MCP workspace and confirm cleanup" in refusal["message"], refusal + assert "rebuild only after cleanup completes" in refusal["message"], refusal assert "sync" in refusal["data"], refusal if scenario == "unsupported_save": # Session cleanup above has completed successfully; only now build externally. From fa7b9fdca43c35c0baebbae4bc8545223a631efa Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 3 Nov 2026 11:28:28 +0100 Subject: [PATCH 2/3] doc: link the save refusal changelog entry to its pull request --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index fdc3a46eb..2b074ed9c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -16,7 +16,7 @@ This project keeps a lightweight, reverse-chronological changelog. Dates use `YY stop the CLI owner or drop the MCP workspace and confirm cleanup before building, then start a fresh session. Building while the session was live left dependencies marked as needing a save, so every later sync of an importer failed with a recovery plan that could not be followed - ([#256](https://github.com/leanprover/lean-beam/issues/256), @ejgallego). + ([#415](https://github.com/leanprover/lean-beam/pull/415), @ejgallego). - `sync` and `refresh` now return `internalError` when a diagnostic burst exhausts pending delivery capacity between complete output frames, rather than losing the terminal response. Recovery replies observe daemon shutdown; existing delivery budgets remain unchanged From 09cfb3b436f2f4406b5460880f79d4c4d777e88e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 3 Nov 2026 22:55:51 +0100 Subject: [PATCH 3/3] test: raise the skill body budget to 10,500 bytes The 10,000-byte limit was a round number rather than a measured bound, and the skill body is now within 100 bytes of it. --- docs/TESTING.md | 2 +- tests/test-skill-budget.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/TESTING.md b/docs/TESTING.md index abd6468c6..48f22d040 100644 --- a/docs/TESTING.md +++ b/docs/TESTING.md @@ -687,7 +687,7 @@ selection, failure for an unusable compiler on `PATH`, explicit selection despit compiler, and failure without fallback when the explicit compiler is missing. For a focused run, use `lake build beam-installation-construction-test`, then `python3 tests/test-installation-construction.py`. -`python3 tests/test-skill-budget.py` keeps `skills/lean-beam/SKILL.md` under 10,000 bytes, and +`python3 tests/test-skill-budget.py` keeps `skills/lean-beam/SKILL.md` under 10,500 bytes, and `McpProjectionTest` keeps the combined MCP tool descriptions under 4,500 characters; both run in the fast suite. `python3 tests/test-mcp-application.py` runs discovery from independent frontend payloads copied diff --git a/tests/test-skill-budget.py b/tests/test-skill-budget.py index b77a9ef46..70e9f1764 100755 --- a/tests/test-skill-budget.py +++ b/tests/test-skill-budget.py @@ -12,7 +12,7 @@ SKILL = REPO / "skills" / "lean-beam" / "SKILL.md" # Agents load the whole body whenever the skill triggers. Raising this needs a reason; prefer # moving detail to skills/lean-beam/references/ instead. -SKILL_BUDGET_BYTES = 10_000 +SKILL_BUDGET_BYTES = 10_500 def main() -> int: