Deicyde · Oct 31, 2026 · Oct 31, 2026 · Oct 31, 2026
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -166,8 +166,8 @@ date when the release is tagged.
   the client restores their exact IDs before publication. No content is dropped (#442).
 - **Lake configuration.** A `lakefile.toml` whose `lean_lib` is not an array
   of named tables, such as `[lean_lib]` written for `[[lean_lib]]`, is
-  refused as Lake refuses it, instead of crashing or silently reading the
-  package's default library (#505).
+  refused as Lake refuses it, instead of crashing, reading the package's
+  default library, or skipping the entries that are not named tables (#505).
 - **Wiki reading links.** The integrated explorer retains #455's title math
   in its outline, breadcrumbs, paged inventory and related-reading controls, using safe MathJax
   service and project macros. Code stays literal, canonical links keep focus
@@ -180,6 +180,11 @@ date when the release is tagged.
   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).
+- **Empty `globs`.** A `lean_lib` with `globs = []` builds no module, as in
+  Lake, where commands that read the library targets took it to build every
+  module under its roots. When `work import-impact` refuses a loaded module
+  that no library builds, it names the module's source file instead of
+  saying the module has none (#519).
 - **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

diff --git a/autoform_cli/impact.py b/autoform_cli/impact.py
@@ -334,7 +334,7 @@ def project_modules(
         # A glob also selects modules nothing can import; they are refused
         # below like any other non-plain name, not dropped.
         selected = {**unimportable, **sources}
-        for glob in library.globs or library.roots:
+        for glob in library.roots if library.globs is None else library.globs:
             base, mode = _glob(glob, library)
             if mode != "+":
                 if base not in sources:
@@ -557,6 +557,12 @@ def _validated_module_evidence(
         key = _name_key(module)
         relative = expected_paths.get(key)
         if relative is None:
+            # A captured file that no library builds can still load, from a
+            # leftover .olean or as a lean_exe root; say so rather than call it
+            # missing.
+            unbuilt = {_name_key(name): path for name, path in _module_source_paths(libraries, snapshot).items()}
+            if key in unbuilt:
+                raise SkeletonError([f"the impact probe loaded {module} from {unbuilt[key]}, which no lean_lib builds"])
             raise SkeletonError(
                 [f"the impact probe loaded {module} without a captured root-project source"]
             )
@@ -624,7 +630,7 @@ def _glob_directories(libraries: Sequence[LeanLibrary]) -> list[tuple[Path, str,
 
     directories: list[tuple[Path, str, str]] = []
     for library in libraries:
-        for glob in library.globs:
+        for glob in library.globs or ():
             base, mode = _glob(glob, library)
             if mode:
                 directories.append((library.src_dir.joinpath(*base.split(".")), base, glob))

diff --git a/autoform_cli/lean_probe.py b/autoform_cli/lean_probe.py
@@ -636,12 +636,16 @@ def check_output() -> None:
 
 @dataclass(frozen=True, slots=True)
 class LeanLibrary:
-    """One ``lean_lib`` target: where its modules live and what they are called."""
+    """One ``lean_lib`` target: where its modules live and what they are called.
+
+    ``globs`` is ``None`` when the target sets none, so that, as in Lake, each
+    root is its own glob; an empty tuple, from ``globs = []``, selects no module.
+    """
 
     name: str
     src_dir: Path
     roots: tuple[str, ...]
-    globs: tuple[str, ...] = ()
+    globs: tuple[str, ...] | None = None
     artifact_dir: Path | None = None
 
 
@@ -689,7 +693,9 @@ def lean_libraries(lean_root: str | Path) -> tuple[LeanLibrary, ...]:
     libraries: list[LeanLibrary] = []
     for entry in entries:
         if not isinstance(entry.get("name"), str):
-            raise SkeletonError([f"cannot read the lean_lib targets of {root}: a [[lean_lib]] target has no name"])
+            raise SkeletonError(
+                [f"cannot read the lean_lib targets of {root}: a [[lean_lib]] target has no string name"]
+            )
         name = entry["name"]
         src_dir = package_src / str(entry.get("srcDir", "."))
         roots = entry.get("roots")
@@ -701,13 +707,13 @@ def lean_libraries(lean_root: str | Path) -> tuple[LeanLibrary, ...]:
         if isinstance(globs, str):
             globs = [globs]
         if not isinstance(globs, list) or not all(isinstance(item, str) for item in globs):
-            globs = []
+            globs = None
         libraries.append(
             LeanLibrary(
                 name=name,
                 src_dir=src_dir.resolve(),
                 roots=tuple(roots),
-                globs=tuple(globs),
+                globs=None if globs is None else tuple(globs),
                 artifact_dir=artifact_dir,
             )
         )
@@ -771,7 +777,7 @@ def builds(library: LeanLibrary, module: str) -> bool:
     Without ``globs``, each root is its own glob.
     """
 
-    globs = library.globs or library.roots
+    globs = library.roots if library.globs is None else library.globs
 
     def globbed(name: str) -> bool:
         for glob in globs:

diff --git a/autoform_cli/library/generate.py b/autoform_cli/library/generate.py
@@ -177,14 +177,14 @@ def library_sources(root: Path, libraries: Sequence[str] = ()) -> LibrarySources
             base = PurePosixPath(target.src_dir.resolve().relative_to(root).as_posix())
         except ValueError:
             raise GenerateError(f"the source directory of {target.name} is outside the package") from None
-        selecting = [_glob(glob, target.name) for glob in target.globs]
+        selecting = [_glob(glob, target.name) for glob in target.globs or ()]
         for module, mode in selecting:
             if mode != "+" and not (target.src_dir / f"{module.replace('.', '/')}.lean").is_file():
                 raise GenerateError(f"lean_lib {target.name}: module {module} has no source file")
         for module_root in target.roots:
             directory = (base / module_root.replace(".", "/")).as_posix()
             prefixes[directory] = "" if base == PurePosixPath(".") else f"{base.as_posix()}/"
-            if selecting:
+            if target.globs is not None:
                 globs.setdefault(directory, []).extend(selecting)
     source_dirs = tuple(sorted(prefixes))
     digests = _sources(root, source_dirs, GenerateError)

diff --git a/tests/test_impact.py b/tests/test_impact.py
@@ -1318,7 +1318,7 @@ def _sources(root: Path, *modules: str) -> Path:
 
 
 def _library(src: Path, *globs: str, roots: tuple[str, ...] = ("Demo",)) -> LeanLibrary:
-    return LeanLibrary(name="Demo", src_dir=src, roots=roots, globs=globs)
+    return LeanLibrary(name="Demo", src_dir=src, roots=roots, globs=globs or None)
 
 
 def test_project_modules_accept_more_than_ten_thousand_source_files(tmp_path: Path) -> None:
@@ -1432,6 +1432,27 @@ def test_project_modules_accept_a_library_nested_in_another_srcdir(tmp_path: Pat
         ("Demo", "Extra"),
         ("Demo", "Extra", "extra.Demo", "extra.Extra"),
     )
+    assert _module_source_paths(configured, snapshot, strict=True) == {
+        "Demo": "Demo.lean",
+        "Extra": "extra/Extra.lean",
+    }
+
+
+def test_project_modules_claim_nothing_for_an_empty_globs_array(tmp_path: Path) -> None:
+    # `globs = []` replaces Lake's default of one glob per root, so Lake
+    # builds no module of Empty, though its root has a source file.
+    root = _sources(tmp_path, "Demo", "Empty", "Empty.Sub")
+    configured = (
+        _library(root, roots=("Demo",)),
+        LeanLibrary(name="Empty", src_dir=root, roots=("Empty",), globs=()),
+    )
+
+    snapshot = snapshot_project_sources(tmp_path)
+    assert project_modules(configured, snapshot, strict_module_ownership=True) == (
+        ("Demo",),
+        ("Demo", "Empty", "Empty.Sub"),
+    )
+    assert _module_source_paths(configured, snapshot, strict=True) == {"Demo": "Demo.lean"}
 
 
 def test_project_modules_claim_only_modules_lake_can_build(tmp_path: Path) -> None:
@@ -1541,7 +1562,8 @@ def test_project_modules_read_a_dotted_file_stem_as_one_component(tmp_path: Path
         ("Demo.Empty.+", "the Lake configuration selects no modules"),
     ],
 )
-def test_project_modules_fail_closed(tmp_path: Path, glob: str, message: str) -> None:
+@pytest.mark.parametrize("strict", [False, True], ids=["inventory", "strict-ownership"])
+def test_project_modules_fail_closed(tmp_path: Path, glob: str, message: str, strict: bool) -> None:
     src = _sources(tmp_path, "Demo", "Demo.Odd.Fine")
     (tmp_path / "Demo" / "Odd" / "bad-name.lean").write_text("", encoding="utf-8")
     for name in ("Quoted/«Foo».lean", "Unquotable/x»y.lean"):
@@ -1551,7 +1573,7 @@ def test_project_modules_fail_closed(tmp_path: Path, glob: str, message: str) ->
     snapshot = snapshot_project_sources(tmp_path)
 
     with pytest.raises(SkeletonError, match=message):
-        project_modules([_library(src, glob)], snapshot)
+        project_modules([_library(src, glob)], snapshot, strict_module_ownership=strict)
 
 
 def test_import_closure_over_approximates_every_spelling_of_an_import() -> None:
@@ -1582,15 +1604,17 @@ def test_lean_libraries_read_one_glob_or_an_array(tmp_path: Path) -> None:
         '[[lean_lib]]\nname = "One"\nglobs = "One.+"\n\n'
         '[[lean_lib]]\nname = "Many"\nglobs = ["Many", "Many.Sub.*"]\n\n'
         '[[lean_lib]]\nname = "Plain"\n\n'
+        '[[lean_lib]]\nname = "Empty"\nglobs = []\n\n'
         '[[lean_lib]]\nname = "Odd"\nglobs = [1]\n',
         encoding="utf-8",
     )
 
     assert {library.name: (library.roots, library.globs) for library in lean_libraries(tmp_path)} == {
         "One": (("One",), ("One.+",)),
         "Many": (("Many",), ("Many", "Many.Sub.*")),
-        "Plain": (("Plain",), ()),
-        "Odd": (("Odd",), ()),
+        "Plain": (("Plain",), None),
+        "Empty": (("Empty",), ()),
+        "Odd": (("Odd",), None),
     }
     assert {library.artifact_dir for library in lean_libraries(tmp_path)} == {
         (tmp_path / "output/compiled").resolve()
@@ -1899,6 +1923,35 @@ def test_import_closure_scope_leaves_out_unresolved_names_the_index_places_outsi
     ]
 
 
+def test_import_closure_scope_lists_an_unresolved_name_in_a_file_no_library_builds(
+    tmp_path: Path, monkeypatch
+) -> None:
+    project = _blueprint_project(tmp_path, "Demo")
+    lean_root = _closure_lean_root(tmp_path)
+    (lean_root / "lakefile.toml").write_text(
+        'name = "Demo"\n\n[[lean_lib]]\nname = "Demo"\nglobs = ["Demo.A", "Demo.B"]\n', encoding="utf-8"
+    )
+    (lean_root / "Demo" / "Apart.lean").write_text("theorem Demo.loose : True := trivial\n", encoding="utf-8")
+    _stub_probe(
+        monkeypatch,
+        records=[_payload("Demo.base", kind="def", module="Demo.A")],
+        modules=(
+            ModuleEvidence("Demo.A", str((lean_root / "Demo/A.lean").resolve())),
+            ModuleEvidence("Demo.B", str((lean_root / "Demo/B.lean").resolve()), ("Demo.A",)),
+        ),
+    )
+
+    report = module_import_impact(project, _BASE_ID, "Demo.A", lean_root=lean_root, module_scope="import-closure")
+
+    # No glob builds Demo/Apart.lean, so it is in no module the scope can rule
+    # out, and Demo.loose is listed with the names declared nowhere.
+    assert [names for article in report.unresolved_articles for names in article.declarations] == [
+        "Demo.inlines",
+        "Demo.loose",
+        "Demo.uses",
+    ]
+
+
 def test_import_closure_scope_names_only_its_modules_when_stale(tmp_path: Path, monkeypatch) -> None:
     project = _blueprint_project(tmp_path, "Demo")
     lean_root = _closure_lean_root(tmp_path)
@@ -2308,7 +2361,7 @@ def test_cli_import_impact_refuses_a_loaded_module_no_library_builds(tmp_path: P
     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
+    assert "error: the impact probe loaded Foo from Foo.lean, which no lean_lib builds" in output.err
 
 
 def test_cli_import_impact_reports_an_empty_loaded_module_without_false_locality(

diff --git a/tests/test_lean_probe.py b/tests/test_lean_probe.py
@@ -25,10 +25,12 @@
     PROBE_OUTPUT_ENV,
     _PROBE_POOL,
     _PROCESS_TERMINATION_GRACE,
+    LeanLibrary,
     SkeletonError,
     _CommandTimedOut,
     _ProbeEnvironmentError,
     _build_probe_helper,
+    builds,
     _join_readers,
     _leader_has_exited,
     lean_libraries,
@@ -1005,6 +1007,50 @@ def test_a_file_no_library_selects_has_no_module(tmp_path: Path) -> None:
     assert module_of(project / "v1" / "Old.lean", libraries) is None
 
 
+def test_a_library_with_an_empty_globs_array_builds_no_module(tmp_path: Path) -> None:
+    project = tmp_path / "project"
+    project.mkdir()
+    (project / "lakefile.toml").write_text('name = "Demo"\n\n[[lean_lib]]\nname = "Demo"\nglobs = []\n', encoding="utf-8")
+
+    # Lake replaces its default of one glob per root with the array as written,
+    # so no glob matches the root or a module under it.
+    libraries = lean_libraries(project)
+    assert libraries[0].globs == ()
+    assert module_of(project / "Demo.lean", libraries) is None
+    assert module_of(project / "Demo" / "Basic.lean", libraries) is None
+
+
+@pytest.mark.parametrize(
+    ("globs", "module", "expected"),
+    [
+        # Lake's Glob.matches: `M` is M alone, `M.*` M and its submodules, `M.+`
+        # its submodules alone, all by whole name components.
+        (("Demo.Sub",), "Demo.Sub", True),
+        (("Demo.Sub",), "Demo.Sub.Deep", False),
+        (("Demo.Sub.*",), "Demo.Sub", True),
+        (("Demo.Sub.*",), "Demo.Sub.Deep", True),
+        (("Demo.Sub.+",), "Demo.Sub", False),
+        (("Demo.Sub.+",), "Demo.Sub.Deep", True),
+        (("Demo.Sub.*",), "Demo.Subway", False),
+        (("Other.*",), "Other.X", True),
+        # Or root Demo prefixes the module and a glob matches the root.
+        (("Demo",), "Demo.Sub", True),
+        (("Demo",), "DemoTests", False),
+        (("Demo.+",), "Demo", False),
+        (("Other",), "Demo.Sub", False),
+        # No globs key: each root is its own glob. An empty array: no glob.
+        (None, "Demo.Sub", True),
+        ((), "Demo", False),
+    ],
+)
+def test_builds_follows_lakes_buildable_module_rule(
+    globs: tuple[str, ...] | None, module: str, expected: bool
+) -> None:
+    library = LeanLibrary(name="Demo", src_dir=Path("/src"), roots=("Demo",), globs=globs)
+
+    assert builds(library, module) is expected
+
+
 @pytest.mark.parametrize(
     "lakefile",
     [pytest.param('name = "Solo"\n', id="absent"), pytest.param('name = "Solo"\nlean_lib = []\n', id="empty-array")],
@@ -1064,19 +1110,23 @@ def test_lake_toml_1_1_extensions_are_rejected_on_every_python(tmp_path: Path, t
         lean_libraries(project)
 
 
+_NOT_AN_ARRAY = r"lean_lib targets .*: Lake expects an array of tables, written \[\[lean_lib\]\]$"
+_NO_NAME = r"lean_lib targets .*: a \[\[lean_lib\]\] target has no string name$"
+
+
 @pytest.mark.parametrize(
     ("lean_lib", "match"),
     [
-        pytest.param("lean_lib = true\n", r"lean_lib targets .*array of tables", id="boolean"),
-        pytest.param("lean_lib = false\n", r"lean_lib targets .*array of tables", id="false"),
-        pytest.param('lean_lib = "Solo"\n', r"lean_lib targets .*array of tables", id="string"),
-        pytest.param(
-            '[lean_lib]\nname = "Solo"\nroots = ["Other"]\n',
-            r"lean_lib targets .*array of tables",
-            id="single-brackets",
-        ),
-        pytest.param("lean_lib = [1]\n", r"lean_lib targets .*array of tables", id="array-of-int"),
-        pytest.param('[[lean_lib]]\nroots = ["Other"]\n', r"lean_lib targets .*has no name", id="nameless"),
+        pytest.param("lean_lib = true\n", _NOT_AN_ARRAY, id="boolean"),
+        pytest.param("lean_lib = false\n", _NOT_AN_ARRAY, id="false"),
+        pytest.param("lean_lib = 3\n", _NOT_AN_ARRAY, id="number"),
+        pytest.param('lean_lib = "Solo"\n', _NOT_AN_ARRAY, id="string"),
+        pytest.param('[lean_lib]\nname = "Solo"\nroots = ["Other"]\n', _NOT_AN_ARRAY, id="single-brackets"),
+        pytest.param("lean_lib = [1]\n", _NOT_AN_ARRAY, id="array-of-int"),
+        pytest.param('lean_lib = [{name = "A"}, 1]\n', _NOT_AN_ARRAY, id="mixed-array"),
+        pytest.param('[[lean_lib]]\nroots = ["Other"]\n', _NO_NAME, id="nameless"),
+        pytest.param('[[lean_lib]]\nname = "A"\n\n[[lean_lib]]\nroots = ["Other"]\n', _NO_NAME, id="nameless-after-named"),
+        pytest.param("[[lean_lib]]\nname = 1\n", _NO_NAME, id="number-name"),
     ],
 )
 def test_a_lean_lib_that_is_not_an_array_is_refused_as_lake_refuses_it(

diff --git a/tests/test_library_generate.py b/tests/test_library_generate.py
@@ -216,6 +216,8 @@ def test_a_glob_selects_the_modules_lake_builds(tmp_path: Path, globs: list[str]
         # A glob matches whole name components: `Lib.A.*` is not `Lib.AB`.
         (["Lib", "Lib.A.*"], "Lib/AB.lean"),
         (["Lib", "Lib.A", "Lib.AB", "Lib.A.Inner"], "Lib/A/Inner/Leaf.lean"),
+        # No glob: Lake builds no module, where a missing key builds the root.
+        ([], "Lib.lean, Lib/A.lean, Lib/A/Inner.lean, Lib/A/Inner/Leaf.lean, Lib/AB.lean"),
     ],
 )
 def test_a_file_the_globs_leave_out_is_refused_by_name(tmp_path: Path, globs: list[str], unbuilt: str) -> None: