Claim a source file in import-impact only for a module Lake can build

CHANGELOG.md

@@ -109,6 +109,14 @@ date when the release is tagged.
   in its outline, breadcrumbs, paged inventory and related-reading controls, using safe MathJax
   service and project macros. Code stays literal, canonical links keep focus
   and native modifiers, and graph labels remain as typed (#442).
+- **Import impact.** In `work import-impact`, a library whose `globs` name
+  other modules but not its own root no longer claims the files under that
+  root that no glob matches, which Lake does not build for it. A library
+  nested there no longer makes the command refuse a project Lake builds with
+  "maps to more than one module". A loaded local module that no library
+  builds is now refused with exit 2, and under
+  `--module-scope import-closure` an article naming a declaration in such a
+  file is listed in `unresolved_articles` (#500).
 - **Book navigation.** The generated `SUMMARY.md` nests each book page under
   its chapter's README, written in book order. A landing page that linked a
   deep page before its chapters, or a folder with no README in the book, put a

autoform_cli/README.md

@@ -875,10 +875,12 @@ declaration when one of its `lean:` names equals it or is a dotted prefix of it,
 so `affected_articles` may list more articles and `article_local` is always
 `false`; `affected_unowned_helpers` keep the parent-chain rule, and
 `unresolved_articles` leaves out a name the source index places outside
-`affected_modules`. A `.lean` file outside the captured sources, as in
-`.lake/packages` or a path dependency, that may import a candidate makes the
-command exit 2 and ask for the default scope; use the default scope too when a
-component of a module name is a common word.
+`affected_modules` but lists one in a file no `lean_lib` builds. A `.lean` file
+outside the captured sources, as in `.lake/packages` or a path dependency, that
+may import a candidate makes the command exit 2 and ask for the default scope;
+use the default scope too when a component of a module name is a common word. In
+either scope, and unlike `work impact`, the probe also refuses a loaded module
+that no `lean_lib` builds, as from a leftover `.olean`.
 
 JSON uses `autoform-module-import-impact/v1`, with `module_graph_revision` and
 `module_scope` (`loaded-root-library-graph` or `import-closure`). `article` is

autoform_cli/impact.py

@@ -45,6 +45,7 @@
 from .lean_probe import (
     LeanLibrary,
     SkeletonError,
+    builds,
     lean_libraries,
     lean_name_components,
     lean_name_parts,
@@ -415,7 +416,7 @@ def _module_source_paths(
             # Lake builds only modules a library selects, so a file under a
             # nested srcDir is one module although the outer srcDir holds it,
             # and a file no library selects claims no module.
-            if not _selects(library, module):
+            if not builds(library, module):
                 continue
             existing_path = paths.get(module)
             if existing_path is not None and existing_path != relative:
@@ -630,18 +631,6 @@ def _glob_directories(libraries: Sequence[LeanLibrary]) -> list[tuple[Path, str,
     return directories
 
 
-def _selects(library: LeanLibrary, module: str) -> bool:
-    """Whether ``library`` holds ``module``, as Lake's ``LeanLib.isLocalModule`` decides."""
-
-    if any(module == root or module.startswith(f"{root}.") for root in library.roots):
-        return True
-    for glob in library.globs:
-        base, mode = _glob(glob, library)
-        if (module == base and mode != "+") or (mode and module.startswith(f"{base}.")):
-            return True
-    return False
-
-
 def _glob(glob: str, library: LeanLibrary) -> tuple[str, str]:
     base, mode = glob, ""
     if glob.endswith((".*", ".+")):

autoform_cli/lean_probe.py

@@ -753,12 +753,12 @@ def module_of(path: Path, libraries: tuple[LeanLibrary, ...]) -> str | None:
     held = [lib for lib in libraries if resolved != lib.src_dir and resolved.is_relative_to(lib.src_dir)]
     for library in sorted(held, key=lambda lib: len(lib.src_dir.parts), reverse=True):
         module = ".".join(resolved.relative_to(library.src_dir).with_suffix("").parts)
-        if _builds(library, module):
+        if builds(library, module):
             return module
     return None
 
 
-def _builds(library: LeanLibrary, module: str) -> bool:
+def builds(library: LeanLibrary, module: str) -> bool:
     """Whether Lake builds ``module`` for ``library``, as ``LeanLibConfig.isBuildableModule`` decides.
 
     Lake finds, imports and builds a module by that rule, not by ``isLocalModule``:
@@ -1288,6 +1288,7 @@ def run(module: str) -> object:
     "STALE_BUILD",
     "LeanLibrary",
     "SkeletonError",
+    "builds",
     "default_runner",
     "lean_libraries",
     "lean_name_components",

tests/test_impact.py

@@ -29,6 +29,7 @@
     format_module_import_impact,
     import_closure,
     module_import_impact,
+    _module_source_paths,
     parse_impact_output,
     parse_module_evidence,
     project_modules,
@@ -1433,6 +1434,28 @@ def test_project_modules_accept_a_library_nested_in_another_srcdir(tmp_path: Pat
     )
 
 
+def test_project_modules_claim_only_modules_lake_can_build(tmp_path: Path) -> None:
+    # Root Foo prefixes Foo.Extra, but Lake builds a module under a root only
+    # when a glob also matches the root, and Foo.Basic does not match Foo. So
+    # Foo/Extra.lean is only the root module of the library nested in Foo/.
+    root = _sources(tmp_path, "Foo", "Foo.Basic", "Foo.Extra")
+    configured = (
+        _library(root, "Foo.Basic", roots=("Foo",)),
+        _library(root / "Foo", roots=("Extra",)),
+    )
+
+    snapshot = snapshot_project_sources(tmp_path)
+    assert project_modules(configured, snapshot, strict_module_ownership=True) == (
+        ("Extra", "Foo.Basic"),
+        ("Basic", "Extra", "Foo", "Foo.Basic", "Foo.Extra"),
+    )
+    # Foo.lean is under root Foo too, but no library builds it, so no claim.
+    assert _module_source_paths(configured, snapshot, strict=True) == {
+        "Foo.Basic": "Foo/Basic.lean",
+        "Extra": "Foo/Extra.lean",
+    }
+
+
 def test_project_modules_match_library_roots_by_whole_components(tmp_path: Path) -> None:
     # Root `Demo` selects `Demo.X` but not `DemoTests.DemoTests`, so
     # DemoTests/DemoTests.lean is only the root module of DemoTests.
@@ -2223,6 +2246,71 @@ def test_cli_import_impact_has_the_probe_walk_each_glob_directory(tmp_path: Path
     assert "unless selectedModules.contains (base ++ sub) do" in str(calls[0]["probe"])
 
 
+def _unbuilt_root_lean(tmp_path: Path) -> Path:
+    """Library Foo builds only its glob Foo.Basic; library Extra, nested in Foo/, builds Extra."""
+
+    lean_root = tmp_path / "lean"
+    (lean_root / "Foo").mkdir(parents=True)
+    (lean_root / "lakefile.toml").write_text(
+        'name = "Foo"\n\n[[lean_lib]]\nname = "Foo"\nglobs = ["Foo.Basic"]\n\n'
+        '[[lean_lib]]\nname = "Extra"\nsrcDir = "Foo"\n',
+        encoding="utf-8",
+    )
+    (lean_root / "Foo.lean").write_text("import Foo.Basic\n", encoding="utf-8")
+    (lean_root / "Foo" / "Basic.lean").write_text("def Foo.base (n : Nat) : Nat := n\n", encoding="utf-8")
+    (lean_root / "Foo" / "Extra.lean").write_text("import Foo.Basic\n", encoding="utf-8")
+    return lean_root
+
+
+def test_cli_import_impact_accepts_a_root_lake_does_not_build(tmp_path: Path, monkeypatch, capsys) -> None:
+    # Library Foo builds only its glob Foo.Basic; library Extra, nested in Foo/,
+    # builds Foo/Extra.lean as Extra, so the file has one module.
+    project = _blueprint_project(tmp_path, "Foo")
+    lean_root = _unbuilt_root_lean(tmp_path)
+    _stub_probe(
+        monkeypatch,
+        records=[_payload("Foo.base", kind="def", module="Foo.Basic")],
+        modules=(
+            ModuleEvidence("Foo.Basic", str((lean_root / "Foo/Basic.lean").resolve())),
+            ModuleEvidence("Extra", str((lean_root / "Foo/Extra.lean").resolve()), ("Foo.Basic",)),
+        ),
+    )
+
+    code = cli.main(
+        ["work", "import-impact", _BASE_ID, "Foo.Basic", str(project), "--lean-root", str(lean_root), "--json"]
+    )
+
+    output = capsys.readouterr()
+    assert code == 0, output.err
+    assert json.loads(output.out)["affected_modules"] == ["Extra", "Foo.Basic"]
+
+
+def test_cli_import_impact_refuses_a_loaded_module_no_library_builds(tmp_path: Path, monkeypatch, capsys) -> None:
+    # Foo.lean is under library Foo's root, but no glob matches Foo, so no
+    # library builds it and Lean could load it only from a leftover .olean or
+    # as the root of a lean_exe.
+    project = _blueprint_project(tmp_path, "Foo")
+    lean_root = _unbuilt_root_lean(tmp_path)
+    _stub_probe(
+        monkeypatch,
+        records=[_payload("Foo.base", kind="def", module="Foo.Basic")],
+        modules=(
+            ModuleEvidence("Foo.Basic", str((lean_root / "Foo/Basic.lean").resolve())),
+            ModuleEvidence("Extra", str((lean_root / "Foo/Extra.lean").resolve()), ("Foo.Basic",)),
+            ModuleEvidence("Foo", str((lean_root / "Foo.lean").resolve()), ("Foo.Basic",)),
+        ),
+    )
+
+    code = cli.main(
+        ["work", "import-impact", _BASE_ID, "Foo.Basic", str(project), "--lean-root", str(lean_root), "--json"]
+    )
+
+    output = capsys.readouterr()
+    assert code == 2
+    assert output.out == ""
+    assert "error: the impact probe loaded Foo without a captured root-project source" in output.err
+
+
 def test_cli_import_impact_reports_an_empty_loaded_module_without_false_locality(
     tmp_path: Path, monkeypatch, capsys
 ) -> None: