Docs: lean_sync runs setup-file and builds stale imports; the daemon pins the toolchain under .beam

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.

Start by locating the README and skill text that describe lean_sync, lake setup-file, and the local fallback bundle. Verify the wording against the reproduction using lean_sync and lean_run_at with #eval Lean.versionString. Done means the docs clearly explain dependency builds, memory implications, and removing or refreshing <root>/.beam after a toolchain bump.