fix: order lake build after session cleanup in save refusals

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

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)

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)

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)

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
+  ([#415](https://github.com/leanprover/lean-beam/pull/415), @ejgallego).
 - When the selected Lean compiler has no Beam runtime, setup guidance identifies the compiler
   and bound installation. Reinstall commands retain every target from the confirmed current
   standalone generation; older or unconfirmed generations get manual guidance. Unsupported

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

docs/SETUP.md

@@ -516,8 +516,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.
 

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

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
 

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

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.

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

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:

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

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.

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: