[Deicyde]

Follow-up to #364, from its post-merge review.

Why. #364 tells agents to build the checked file's imports because, under --no-build, Lake lists only the first modules to build, not the ones that import them. The only real-Lean test of that error used a one-level chain (Main imports Probe.Dep), where Lake's list and the file's import are the same module. If a later Lake started listing importers too, nothing would notice that the advice's premise had changed.

Change. In test_real_lean_reports_unbuilt_imports_without_building_them, Main now imports Probe.Mid, which imports Probe.Dep. The test checks three things:

• the error ends with - Probe.Dep;
• Lake doesn't list Probe.Mid;
• no .olean was built.

It's still one Lake run that elaborates nothing.

Tests. On Lean v4.32.2, the fixture toolchain, the test passes locally in about 5 seconds. Lake's output ends with:

✖ [2/4] Building Probe.Dep
error: target is out-of-date and needs to be rebuilt
Some required targets logged failures:
- Probe.Dep

The rest of tests/test_batch_diagnostics.py passes with Lake hidden from PATH, and ruff check passes.

Merge notes. Clean against main eadde9b, and no open PR touches this file.

[Deicyde]

Adversarial review: ready to merge once it's out of draft

Scope. The diff at 7a38c8f, reviewed statically through five lenses (style, necessity, architecture, golf, correctness), each followed by a refuter, then a completeness critic and its refuter. I checked every surviving finding before acting on it, and a must-fix-only pass checked the fixes and the description.

Conclusion: ready to merge at e11d4ec.

• The test now pins the premise of #364's advice. With Main importing Probe.Mid, which imports Probe.Dep, Lake's failure list is just - Probe.Dep. Lake gives a module that imports a stale one a renewed job with an empty log, and it lists only jobs whose own log has an error. That code is the same from v4.30.0 through v4.35.0 and in v4.36.0-rc1, so a fixture bump won't break the test for an unrelated reason.
• The assertions can't pass falsely. - Probe.Dep can only reach the message through Main, then Mid, then Dep, and the failure list is the last thing Lake prints before it exits with status 3.

Fixed

• The Probe.Mid check looked at the whole message. It now looks for - Probe.Mid, a list entry, as the comment says. A later Lake that names Probe.Mid on some other line, such as v4.35.0's "Canceled" line under --fail-fast, won't fail the test for a reason unrelated to the premise.
• The commit message left out the widened .olean check (Dep.olean to *.olean), and that message becomes the squash body. It now names all three checks.

Considered and left as is

• An empty Dep so the call fits on one line. Lake never reads Dep's body under --no-build, but the gain is cosmetic, and the wrapped call matches other calls of the same helper.
• Anchoring on Lake's list header (rpartition("logged failures:\n")). That pins the list exactly, but it would fail if the header wording ever changed. endswith plus the narrowed check covers the premise without depending on the header.
• *.olean under .lake. Under --no-build, Lake writes an .olean there only for a lakefile.lean config, and the helper writes lakefile.toml. The other way is restoring one from its artifact cache, which needs an earlier cache-writable build of this module. Nothing in the suite or CI does that, and a cache hit would fail the endswith check first.

Verification

• The test passes locally on Lean v4.32.2 after the change, and the rest of tests/test_batch_diagnostics.py passes with Lake hidden from PATH.
• CI on e11d4ec passes every check. Its real-Lean step ran this test with the other real-Lean diagnostics and LSP tests: "8 passed, 70 deselected" (run 39118607171).