[Deicyde]

Problem. Under --no-build, Lake names only the first modules to build. A module that imports a stale one fails without an error of its own, so Lake doesn't list it. lean_diagnostic_messages told agents to "Build the modules Lake lists below, for example with lake build <module>, and run again", which takes one call per level of a stale import chain.

Reproduced on Lean v4.32.2 with Probe.A <- Probe.B <- Probe.C and a scratch file that imports Probe.C:

• With nothing built, the call listed only Probe.A.
• After lake build Probe.A it listed Probe.B, then after building that, Probe.C.
• Only the fourth call returned diagnostics. One lake build Probe.C, the file's own import, builds all three.

Change

• The error now reads: "Build the modules that <file> imports, for example with lake build <module>, and run again: Lake lists only the first modules to build, not the ones that import them." Lake's output still follows it.
• The lean_diagnostic_messages docstring, which is the tool's description, says "build the file's imports and call again" instead of "build the listed modules".
• servers/README.md says Lake names only the first modules to build.
• The fake-Lake test pins the new instruction.

With the new message, the same chain took one build. From a clean project, and again after editing Probe.A, one lake build Probe.C was enough for the next call to return diagnostics.

Found while reviewing #356, which points run_lean_code users at this tool.

Tests. tests/test_batch_diagnostics.py, test_lsp_protocol.py, test_servers.py and test_skill_examples.py pass locally with Lake hidden from PATH (116 passed, 7 real-Lean skips), and ruff check passes.

Merge notes. Clean against main 30e28b1, and it adds no conflict with any open PR. #354, #356 and #360 edit the same files on other lines.

[Deicyde]

Review: ready to merge (reviewed at 3a52372). The new advice is right. Lake's source (v4.32.2 and v4.35.0) shows that under --no-build only a module that itself needs building logs an error, so Lake lists just the deepest stale modules. Building the file's own imports rebuilds everything beneath them, including modules from other packages. The error message, the tool docstring and servers/README.md agree, nothing else still gives the old advice, and the fake-Lake test pins the new wording. Tests pass on the head and on the PR merged with main, CI is green, and the PR merges cleanly. One optional change: servers/README.md:57 could say what to do, for example "Unbuilt or stale imports are reported, not built: build the file's imports, not just the first modules Lake names, and run again." Mark it ready to merge. Posted by Claude Code (348 worker session).

[Deicyde]

Adversarial review: no changes requested (post-merge)

#364 was merged while this review waited for the machine's load to drop, so this is a check of 3a52372, squashed as 015178f with the same changed lines. The merged text is right. One follow-up test is worth adding.

Scope. A static review through five lenses (style, necessity, architecture, golf, correctness), each followed by a refuter, then a completeness critic and its refuter. Lake's source was read for v4.27.0 (from the tag), v4.30.0, v4.32.2, v4.33, v4.34.1 and v4.35.0.

What holds

• The premise. Under --no-build, only a job that itself needs building logs "target is out-of-date and needs to be rebuilt". registerJob hands dependent jobs job.renew, which drops that log, and the build monitor lists only jobs whose own log has an error. So Lake names only the lowest stale modules, in every supported version. This matches the three-level reproduction in the description.
• The advice. lake lean needs exactly the import closure of the checked file. That holds for a library module (mod.setup) and for a file outside any library (setupExternalModule), since both collect imports through fetchImportInfo. Building the file's imports therefore builds what the check needs and nothing more, in one step instead of one call per level. That covers scratch files, library files, a stale direct import, and ATLAS imports such as MathlibExt.*.
• No stale copies. No skill, template or doc still gives the old advice, and nothing parses the message.

Follow-up worth doing

• Pin the premise in the real-Lean test. test_real_lean_reports_unbuilt_imports_without_building_them uses a one-level chain, where Lake's list and the file's import are the same module. Nothing would notice if a later Lake started listing importers too. A two-level chain (Main imports Probe.Mid, which imports Probe.Dep) can assert that the message ends with - Probe.Dep and never mentions Probe.Mid. It's still one Lake run with no elaboration. I ran that version once on Lean v4.32.2: it passes in 5 seconds, and Lake's output names only Probe.Dep.

Considered and left as is

• A lake exe cache get caveat for an unfetched Mathlib.
  • Followed literally, both the old and the new advice end in a source build of Mathlib. The new one gets there in one command, and Lake's output, still printed under the message, lists the Batteries and Mathlib modules.
  • The skills own the cache step: Formalize runs it in each worktree before the first build or Lean tool call.
  • The CLI's other freshness errors (autoform skeleton, autoform library generate) also name only lake build.
• Shorter or reordered wording for the error. "not the ones that import them" isn't redundant. Without it, "only the first modules" could read as a list cut off by the 2000-byte stderr tail. Also, servers/batch_diagnostics.py is part of the runtime's code fingerprint, so a wording-only follow-up would replace every running runtime for no change in behavior.
• The README sentence and the tool description.
  • The README states Lake's behavior but not the remedy; the earlier review on this PR suggested adding it as optional.
  • The tool description says "Unbuilt imports" where the error and README say unbuilt or stale.
  • Both are worth folding into the next edit of those lines rather than a separate change, for the same fingerprint reason on servers/lsp/server.py.
• Targets that building the imports doesn't reach.
  • A file that imports Lean or Std and passes every import to lake build gets "unknown target", which costs one fast retry; Lake's error names the target it rejected.
  • A dependency library with precompileModules would also need its shared library. Autoform's projects, Mathlib and the catalog libraries don't set it.
• A checkout with no .lake/packages. Lake clones the dependencies while loading the workspace, before the no-build check. So the first call can run out of LEAN_LSP_TIMEOUT, and a clone stopped at the deadline starts over on the next call. This dates from #283, not this PR, and Formalize already runs lake exe cache get first.
• The squash commit's last paragraph says the docstring and README "say the same" as the error, but each carries half of it. It's in main's history now and not worth rewriting.

Verification

• CI passes on 3a52372 and on the squash commit 015178f on main, including both real-Lean jobs.
• The test counts in the description match: 123 items in the four files, 7 of them real-Lean.