Summary
In a Lake package whose lakefile sets moreLeanArgs := #["-E", "hasSorry"] (batch-only, so a zero-build save is unsupported by design), lean_save and lean_close_save do not fail with saveUnsupportedSetup. The call sends no response and no progress for the client's full idle timeout (1800 s), the client aborts it, and a retry hangs the same way. The batch-only check exists in the source (Beam/Broker/LakeSave.lean, unsupportedZeroBuildSaveReason?, "Lake module uses batch-only moreLeanArgs"), so the hang happens before that check is reached, apparently in the dependency-trace build that precedes it. Two autonomous agents each lost 30 minutes per call on 2026-09-12; one lost an hour before it was stopped. Installed build: 0.2.0-beta, source commit 8276f4e; upstream main at 6511cd9 is one documentation commit ahead, so the behaviour is current.
- Kind:
bug
- Severity:
high
- Tags:
save, hang, moreLeanArgs, saveUnsupportedSetup, timeout
Reproduction
- A Lake package on Lean v4.33.1 whose
lakefile.lean has package … where moreLeanArgs := #["-E", "hasSorry"] and structured leanOptions, with all dependencies built (lake build green), .lake/packages entries partly symlinks to sibling checkouts. 2. lean_sync a module of the package (succeeds, diagnostics 0). 3. lean_save the same module path (relative, e.g. Pkg/Sub/Module.lean). Observed with the MCP client's default 1800 s idle timeout: no response, no progress notification, abort after 1800 s with "sent no response or progress for 1800s". 4. Retry lean_save on another synced module: same. The Lean worker process for the file stays alive and idle (0 % CPU) throughout.
Expected Behavior
lean_save returns promptly with the saveUnsupportedSetup error code and the guidance to move -D settings to leanOptions or use lake build, as the README and CHANGELOG describe for batch-only moreLeanArgs.
Actual Behavior
The call produces no response or progress for at least 1800 s; the client aborts it; a retry behaves the same. No saveUnsupportedSetup error is ever returned.
Impact
An agent following the documented recovery plan (lean-beam save on stale direct deps, then refresh) loses 30 minutes per attempt and, under a retry loop, the whole session. With the syncBarrierIncomplete recovery plan naming save as step 1, this is the default path an agent takes.
Workaround
Never call save/close-save in such a package; get the in-session verdict from lean_update + lean_todo over the whole file (kinds diagnostic, sorry) and the batch verdict from an external lake build.
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.
Summary
In a Lake package whose lakefile sets
moreLeanArgs := #["-E", "hasSorry"](batch-only, so a zero-build save is unsupported by design),lean_saveandlean_close_savedo not fail withsaveUnsupportedSetup. The call sends no response and no progress for the client's full idle timeout (1800 s), the client aborts it, and a retry hangs the same way. The batch-only check exists in the source (Beam/Broker/LakeSave.lean,unsupportedZeroBuildSaveReason?, "Lake module uses batch-only moreLeanArgs"), so the hang happens before that check is reached, apparently in the dependency-trace build that precedes it. Two autonomous agents each lost 30 minutes per call on 2026-09-12; one lost an hour before it was stopped. Installed build: 0.2.0-beta, source commit 8276f4e; upstream main at 6511cd9 is one documentation commit ahead, so the behaviour is current.bughighsave,hang,moreLeanArgs,saveUnsupportedSetup,timeoutReproduction
lakefile.leanhaspackage … where moreLeanArgs := #["-E", "hasSorry"]and structuredleanOptions, with all dependencies built (lake buildgreen),.lake/packagesentries partly symlinks to sibling checkouts. 2.lean_synca module of the package (succeeds, diagnostics 0). 3.lean_savethe same module path (relative, e.g.Pkg/Sub/Module.lean). Observed with the MCP client's default 1800 s idle timeout: no response, no progress notification, abort after 1800 s with "sent no response or progress for 1800s". 4. Retrylean_saveon another synced module: same. The Lean worker process for the file stays alive and idle (0 % CPU) throughout.Expected Behavior
lean_savereturns promptly with thesaveUnsupportedSetuperror code and the guidance to move-Dsettings toleanOptionsor uselake build, as the README and CHANGELOG describe for batch-onlymoreLeanArgs.Actual Behavior
The call produces no response or progress for at least 1800 s; the client aborts it; a retry behaves the same. No
saveUnsupportedSetuperror is ever returned.Impact
An agent following the documented recovery plan (
lean-beam saveon stale direct deps, then refresh) loses 30 minutes per attempt and, under a retry loop, the whole session. With thesyncBarrierIncompleterecovery plan namingsaveas step 1, this is the default path an agent takes.Workaround
Never call save/close-save in such a package; get the in-session verdict from
lean_update+lean_todoover the whole file (kinds diagnostic, sorry) and the batch verdict from an externallake build.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.