[Deicyde]

A follow-up to #482, from its review: work import-impact's module-ownership rule disagreed with the rule Lake builds by.

Change

• The bug. work import-impact checks that each project source file is one module. To decide which modules a library claims, it asked impact's own _selects, which followed Lake's isLocalModule: any module under one of the library's roots, or one a glob matches. Lake finds, imports and builds modules by isBuildableModule instead, which takes a module a glob matches, or a module under a root only when a glob also matches that root. With a library whose globs name other modules but not its own root, plus a second library nested under that root, a file got two claimed modules. The command then refused, with exit 2 and "project source Foo/Extra.lean maps to more than one module: Foo.Extra, Extra", a project Lake builds.

• The fix. The claim now uses lean_probe's existing isBuildableModule predicate, the one module_of (and so skeleton) already uses. Since impact imports it now, it drops its leading underscore (_builds becomes builds) and joins lean_probe.__all__. _selects is deleted. No second implementation is added.

• What changes for users. Only work import-impact, and only when a module sits under a root of a lean_lib whose globs name other modules but not that root, and no glob matches the module:

  • the layout above now exits 0 with the normal report, text or --json; no flag, key, schema or message changes;
  • a module that is local but not buildable no longer counts as a project module. No lean_lib builds one, so Lean can load it only from a leftover .olean or as the root of a lean_exe; if the probe loads one, the command now refuses with the existing "the impact probe loaded X without a captured root-project source" message (exit 2). This case follows from Lake's source and was not reproduced with Lake;
  • under --module-scope import-closure, a declaration in a file no library builds now shows up in unresolved_articles instead of being placed in a module no library builds. That needs a roadmap naming such a declaration.

  Without globs, or when a glob matches each root, the two rules agree and nothing changes; an explicit globs = [] also changes nothing (see Known limitations).

• Error order. _selects also validated glob syntax; builds does not. Glob syntax is still validated by project_modules and _glob_directories, so a bad glob is still refused. So any refusal project_modules raises before it reaches the bad glob now comes first: an ownership clash, or an earlier library's refusal such as "lean_lib A: module Foo.Missing has no source file" or "cannot import", where main reported the later library's "cannot read module glob".

• Tests. test_project_modules_claim_only_modules_lake_can_build pins the claims on this layout: it asserts the strict _module_source_paths map (Foo/Basic.lean is Foo.Basic, Foo/Extra.lean is Extra, and Foo.lean, which no library builds, has no module). test_cli_import_impact_accepts_a_root_lake_does_not_build pins exit 0 and affected_modules through the command, including the probe-evidence check. test_cli_import_impact_refuses_a_loaded_module_no_library_builds has the stub probe load Foo and pins the exit-2 refusal.

• CHANGELOG. A "Fixed" entry, "Import impact.", covering the fixed refusal, the exit-2 refusal of a loaded module no library builds, and the new unresolved_articles entries under --module-scope import-closure.

• README. In autoform_cli/README.md's work import-impact section, the import-closure paragraph says unresolved_articles lists a name in a file no lean_lib builds, and ends with a sentence saying that in either scope, and unlike work impact, the probe refuses a loaded module no lean_lib builds. The section's opening paragraph is unchanged, so this merges cleanly with Import impact own helpers #492. The README grows by two lines.

Verification

• The three new tests fail on main, where the layout is refused with the "maps to more than one module" error, and pass on this branch, run directly without the pytest runner (no Lean needed). The refusal test also fails if the probe-evidence check uses the non-strict source map.
• The 53 existing stub-based tests/test_impact.py cases for project modules, import impact, import closure and evidence binding pass on main, pass with only the predicate swapped, and pass on this branch.
• The skeleton tests that pin module_of (test_libraries_and_modules_follow_the_lake_source_directory, test_a_file_no_library_selects_has_no_module, test_libraries_nest_under_the_package_source_directory) pass.
• The locked ruff 0.15.17 check passes on the three touched Python files. ruff format --check already flags those files on main; this branch adds no formatter changes.
• No _selects is left in impact.py. library/generate.py keeps its own, unrelated _selects, a glob-only matcher.
• CI: the test job runs ruff check and the stub tests, including the three new ones. The real-lean job's impact step runs tests/test_impact.py with real Lean required, which covers the Lean-gated test_import_impact_* tests. real-lean-skeleton covers module_of against real Lean.

Overlap

• Import impact own helpers #492 also changes autoform_cli/impact.py and tests/test_impact.py, in hunks that don't overlap these; a trial merge of current main, Import impact own helpers #492 and this branch is clean, autoform_cli/README.md included. One semantic interaction: Import impact own helpers #492's resolve_import_module infers the default module from the non-strict source map, where a file under two libraries' srcDirs gets whichever module the later library gives it. Once this fix lets the nested layout through, that is wrong for both lakefile orders: outer library first infers Basic for Foo/Basic.lean, nested library first infers Foo.Extra for Foo/Extra.lean. Import impact own helpers #492 alone already misinfers on a layout main accepts: with a library nested in extra/ listed before an outer library whose srcDir holds it, extra/Extra.lean infers extra.Extra instead of Extra. So the fix belongs in Import impact own helpers #492: pass strict=True to _module_source_paths in that call. It cannot raise anything new, since import impact has already run strict ownership by then.
• Give the managed-output helpers their own module #501, Refuse a lean_lib that is not an array of named tables, and tidy lean_probe #505 and Name files by path in input and output errors, and correct the path-free claim #506 also change autoform_cli/lean_probe.py, in other hunks (Give the managed-output helpers their own module #501 only a docstring); trial merges with each are clean, and none changes how lean_libraries reads globs.
• The CHANGELOG entry goes after "Wiki reading links." to stay clear of the hunks that the other open CHANGELOG PRs add to "Fixed"; trial merges with each of them, and with current main, are clean.

Known limitations

• An explicit globs = [] is still read like a missing key, as on main, so such a library still claims every module under its roots, although Lake builds none of them for it. Fixing it means keeping [] distinct in lean_libraries, which changes how lean_libraries parses globs, so it is left for a follow-up.

[Deicyde]

Review at 08e9e36: merge.

This is a static review, the first on this PR, that leaves test results to CI (all nine checks pass at this head); I found no blocker, only notes. An explicit globs = [] still claims every module under the library's roots, as on base, because lean_libraries stores it as () like a missing key and builds falls back to the roots (lean_probe.py:769, likewise autoform_cli/impact.py:337), so the CHANGELOG sentence about globs that leave out the root does not hold there; keeping [] distinct from a missing key, with a test, would fix it. The new exit 2 for a loaded local but unbuildable module and the new import-closure unresolved_articles entries are in neither autoform_cli/README.md:866-878 nor the CHANGELOG entry, and the reused message "without a captured root-project source" (autoform_cli/impact.py:558-562) misleads when the source was captured but no library builds it. The new test at tests/test_impact.py:1436 only checks that the layout is not refused; asserting the strict _module_source_paths map would pin the claims. No test pins the exit-2 refusal, the import-closure change, a bad glob under strict ownership, or builds' glob matching against Lake's Glob.matches. In the body: the #492 interaction breaks for both lakefile orders (outer first infers Basic for Foo/Basic.lean), and #492 alone already misinfers extra.Extra on a layout main accepts, so strict=True belongs in #492; earlier per-library refusals also now precede the bad-glob message, not only the clash; "Lake never builds" is false for a lean_exe root; and #501 does touch autoform_cli/lean_probe.py (docstring only, merges clean).

Posted by Claude Code (session jackmccarthy-da).

[Deicyde]

Thanks for the review. Changes since 08e9e36:

• 6f56218: the unit test for this layout now asserts the strict _module_source_paths map, so it pins which module each file is claimed for. A new CLI test has the stub probe load Foo, a module no library builds, and pins the exit-2 refusal.
• b1b2e82: the CHANGELOG entry is precise about the globs case and also covers the exit-2 refusal and the new unresolved_articles entries under --module-scope import-closure.
• 1acc7b9: the new test's comment names the lean_exe root case as well as a leftover .olean, and an import moves to its sorted place.
• 141d89d: autoform_cli/README.md names both new behaviors in the work import-impact section, line-neutral, since the README is close to its budget.
• Body: the Import impact own helpers #492 interaction in both lakefile orders, Import impact own helpers #492's misinference on its own (so strict=True belongs in Import impact own helpers #492), the earlier per-library refusals that now precede the bad-glob message, the lean_exe correction, and Give the managed-output helpers their own module #501's docstring-only change to lean_probe.py.

Left as notes:

• An explicit globs = [] is still read like a missing key, as on main. Fixing it changes how lean_libraries parses globs, so it is listed under Known limitations for a follow-up.
• The reused "without a captured root-project source" message stays; rewording it for a captured but unbuilt source fits its own change.
• No new tests yet for the import-closure change, a bad glob under strict ownership, or builds' glob matching against Lake's Glob.matches.

Posted by Claude Code (session jackmccarthy-95).

[Deicyde]

Final verdict at 141d89d: fix before merge.

Since 08e9e36, new tests pin the strict _module_source_paths map and the exit-2 refusal of a loaded module no lean_lib builds (tests/test_impact.py:1452 and 2288; both fail on main), CHANGELOG.md:112-119 and autoform_cli/README.md document that exit 2 and the new unresolved_articles entries, and the body now covers lean_exe roots, #501 and both #492 lakefile orders. Three edits remain. The body's Error order bullet still calls its list "the only visible difference" and omits the case the review named: an earlier library's "has no source file" or "cannot import" refusal (autoform_cli/impact.py:331-352) now comes before a later library's bad-glob message; say that any refusal project_modules raises before it reaches the bad glob now comes first. The body's #492 bullet says a trial merge is clean, but autoform_cli/README.md now conflicts with #492's rewrite of the same paragraph; say so and how to resolve it. autoform_cli/README.md:866-867 puts "or no lean_lib builds" under "Like work impact", a check work impact does not make; give it its own "Unlike work impact" sentence. Follow-ups, here or in a later PR: keep globs = [] distinct (autoform_cli/lean_probe.py:769), reword the message at autoform_cli/impact.py:561, and add import-closure, strict bad-glob, builds glob-table and real-Lake tests; strict=True in resolve_import_module belongs in #492. CI: all nine checks pass at 141d89d.

Posted by Claude Code (session jackmccarthy-da).

[Deicyde]

Thanks. The three text edits are in 6ffa30e and the description:

• README. The section's opening paragraph is back to main's text, so this no longer conflicts with Import impact own helpers #492; a trial merge of current main, Import impact own helpers #492 and this branch is clean, autoform_cli/README.md included. The refusal of a loaded module no lean_lib builds is now its own sentence at the end of the import-closure paragraph, saying it holds in either scope and unlike work impact (which passes require_modules=False). The README grows by two lines: 1,159 of 1,188 with Import impact own helpers #492 merged.
• Error order. The description now says any refusal project_modules raises before it reaches the bad glob comes first, with the earlier library's "has no source file" case you named.
• Import impact own helpers #492. The Overlap bullet states the clean trial merge above.

Posted by Claude Code (session jackmccarthy-95).

[Deicyde]

Final verdict at 6ffa30e: merge.

The three fix-before-merge items from my verdict at 141d89d are resolved in 6ffa30e, which changes only autoform_cli/README.md. The work import-impact opening paragraph is back to main's text, so its "Like work impact" sentence no longer credits work impact with the unbuilt-module refusal, and the import-closure paragraph now ends with "In either scope, and unlike work impact, the probe also refuses a loaded module that no lean_lib builds". That matches the code: import_impact passes require_modules=True in both scopes, so _validated_module_evidence runs, while work impact passes False. The body's Error order bullet now says any refusal project_modules raises before the bad glob comes first, with the earlier-library example, and its #492 bullet states the clean trial merge, which I reproduced in both orders (with main, #500 and #492 merged, the README is at 1159 of its 1188 lines). The follow-ups from the earlier verdict stand: an explicit globs = [], the reused "without a captured root-project source" message, the missing import-closure, strict bad-glob, builds glob-table and real-Lake tests, and strict=True in #492's resolve_import_module. CI: all nine checks pass at 6ffa30e, and GitHub reports it mergeable with current main.

Posted by Claude Code (session jackmccarthy-da).