Summary
Two behaviours that cost time until measured and that the README/skill text does not state plainly. (1) lean_sync runs lake setup-file, which builds every stale import of the synced module first. After editing a module that hundreds of others import (a backend model), a sync is a dependency build with a build's memory footprint: on a 14 GB box the OOM guard killed one such sync while another build ran, and an agent's sync rebuilt about 20 modules it did not intend to. (2) The daemon pins the toolchain under <root>/.beam/bundles/... (309 MB here); after a toolchain bump the pinned bundle keeps serving the old Lean until the directory is removed, and an agent cannot tell from the tool results which Lean it is talking to unless it runs #eval Lean.versionString.
- Kind:
docs
- Severity:
low
- Tags:
docs, sync, setup-file, toolchain, bundle
Reproduction
(1) Edit a module M that many modules import; lean_sync any importer; observe lake building the stale importers before the barrier (worker RSS and wall time of a full dependency build). (2) Bump lean-toolchain (v4.32.x → v4.33.1) without removing <root>/.beam; lean_run_at with #eval Lean.versionString reports the old version.
Expected Behavior
The reference states that a sync after a root-module edit is a dependency build and names the memory cost, and that a toolchain bump requires removing (or Beam refreshing) the pinned bundle; ideally lean_sync reports the number of modules it is about to build and the tool results carry the Lean version.
Actual Behavior
Both behaviours are discoverable only by measurement; the docs mention a "local fallback bundle" and lake setup-file without the consequences.
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
Two behaviours that cost time until measured and that the README/skill text does not state plainly. (1)
lean_syncrunslake setup-file, which builds every stale import of the synced module first. After editing a module that hundreds of others import (a backend model), a sync is a dependency build with a build's memory footprint: on a 14 GB box the OOM guard killed one such sync while another build ran, and an agent's sync rebuilt about 20 modules it did not intend to. (2) The daemon pins the toolchain under<root>/.beam/bundles/...(309 MB here); after a toolchain bump the pinned bundle keeps serving the old Lean until the directory is removed, and an agent cannot tell from the tool results which Lean it is talking to unless it runs#eval Lean.versionString.docslowdocs,sync,setup-file,toolchain,bundleReproduction
(1) Edit a module M that many modules import;
lean_syncany importer; observe lake building the stale importers before the barrier (worker RSS and wall time of a full dependency build). (2) Bumplean-toolchain(v4.32.x → v4.33.1) without removing<root>/.beam;lean_run_atwith#eval Lean.versionStringreports the old version.Expected Behavior
The reference states that a sync after a root-module edit is a dependency build and names the memory cost, and that a toolchain bump requires removing (or Beam refreshing) the pinned bundle; ideally
lean_syncreports the number of modules it is about to build and the tool results carry the Lean version.Actual Behavior
Both behaviours are discoverable only by measurement; the docs mention a "local fallback bundle" and
lake setup-filewithout the consequences.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.