An external Lake build never clears a dependency's needsSave; the sync barrier then refuses the importer and the recovery plan points at save

Summary

StaleDirectDeps marks a direct dependency needsSave when the broker's module history has lastSaveEventSeq < lastTextChangeEventSeq, i.e. the module was edited through Beam and never saved through Beam. A module that was edited through Beam and then built by an external lake build (fresh .olean, newer than the source by 12 minutes) stays needsSave for the life of the broker, so every lean_sync of an importer fails with syncBarrierIncomplete, staleDirectDeps: [{module, needsSave: true}], and a recoveryPlan whose first step is lean-beam save of that dependency. In a package where save is unsupported (batch-only moreLeanArgs) the plan cannot be followed (and, per the companion report, the save call hangs). The flag reflects broker event history, not artifact freshness: the source hash and mtime of the dependency's .olean are not consulted. Installed build 0.2.0-beta, source commit 8276f4e; Beam/Broker/StaleDirectDeps.lean line 64 is the rule.

• Kind: bug
• Severity: medium
• Tags: sync, staleDirectDeps, needsSave, external-build

Reproduction

1. Package on Lean v4.33.1 with batch-only moreLeanArgs. 2. Create a new module A.lean, lean_sync it, edit it through lean_update (text-change events recorded). 3. Outside Beam, run lake build Pkg.A (produces a fresh .olean newer than the source). 4. Create B.lean with public import Pkg.A, lean_sync it. Observed: syncBarrierIncomplete, staleDirectDeps: [{module: Pkg.A, needsSave: true}], saveDeps: [A.lean], recoveryPlan: [lean-beam save A.lean, lean-beam refresh B.lean, lake build], fileProgress.done: false. lean_drop_workspace and re-sync clears it once (the history is dropped), which confirms the flag is history, not freshness.

Expected Behavior

A direct dependency whose on-disk .olean (and its trace) is newer than its source, or whose current source hash matches the built trace, is not stale; the barrier completes, or at least the hint distinguishes "unsaved in Beam" from "artifact stale".

Actual Behavior

The dependency is reported needsSave: true indefinitely after an external build, the importer's sync barrier never completes, and the recovery plan sends the caller to save.

Impact

In a workflow where the orchestrator builds (external lake) and agents verify through Beam, every agent that touches a module later imported by another agent's module hits this; today two agents stalled on it.

Workaround

lean_update + lean_todo (kinds diagnostic, sorry) over the importer give a full-file verdict without the barrier; lean_drop_workspace once after the external build resets the history.

Environment: lean-beam-mcp 0.2.0-beta (source commit 8276f4e), MCP protocol 2026-07-28, Lean v4.33.1, Linux; the client is Claude Code with its default 1800 s MCP idle timeout.

Start at Beam/Broker/StaleDirectDeps.lean line 64 and reproduce the external lake build with batch-only moreLeanArgs, then inspect how broker event history relates to the dependency’s .olean and trace freshness. Done means a fresh external artifact no longer leaves the importer blocked with needsSave or directs recovery to an unsupported save operation.