[Deicyde]

Follow-ups to #500 and #505 from their review notes (jackmccarthy-da on #500, jackmccarthy-63 on #505). One behavior fix, one reworded refusal, and tests.

Change

• globs = [] builds no module. Lake's TOML loader keeps an explicit globs array as written and only fills in its default, one glob per root, when the key is missing (decodeRoots in Lake/Load/Toml.lean, v4.35.0). With no glob, isBuildableModule is false for every module. lean_libraries stored [] as (), like a missing key, and builds, project_modules and library generate then fell back to the roots, so they claimed or indexed modules Lake does not build.
  • LeanLibrary.globs is now None for a missing key and () for an empty array; a globs value that is neither a string nor an array of strings is read as missing, as before.
  • builds and project_modules use the roots only for None. _glob_directories reads globs or ().
  • library generate treats a library with globs = [] like any library with globs: a file under its roots that no glob selects is refused with the existing "no indexed library builds it" message. Without the key it still indexes the roots' directories and leaves the rest to the freshness check.
  • Every command that reads library targets through lean_libraries sees the change: skeleton, library generate, work impact and work import-impact.
• The import-impact refusal of an unbuilt module names its file. When the probe loads a module whose source is captured but that no library builds (a leftover .olean, or a lean_exe root), the error was "loaded Foo without a captured root-project source". It is now "loaded Foo from Foo.lean, which no lean_lib builds". A module with no captured source keeps the old message. Exit status is 2 in both cases, as before.
• Refuse a lean_lib that is not an array of named tables, and tidy lean_probe #505's refusals. "a [[lean_lib]] target has no name" becomes "has no string name", since name = 1 has a name. The CHANGELOG entry now says main also skipped the bad entries of a mixed array, not only crashed or read the default library. work impact reaches these refusals too, through _load_impact_evidence; Refuse a lean_lib that is not an array of named tables, and tidy lean_probe #505's description left it out.
• Tests.
  • tests/test_lean_probe.py: the refusal matrix gains lean_lib = 3, [{name = "A"}, 1], a nameless target after a named one and name = 1, and both patterns now match the whole message, including ", written [[lean_lib]]". New: test_a_library_with_an_empty_globs_array_builds_no_module, and test_builds_follows_lakes_buildable_module_rule, 14 cases covering M, M.*, M.+, whole components, the root clause, a missing key and an empty array.
  • tests/test_impact.py: the nested-library test also asserts the strict module map; new tests for globs = [] in project_modules, for the import-closure listing of a name declared in a file no library builds (Claim a source file in import-impact only for a module Lake can build #500's change, which no test pinned), and the glob refusals now also run under strict ownership. test_lean_libraries_read_one_glob_or_an_array reads None, () and the odd [1].
  • tests/test_library_generate.py: globs = [] refuses every file under the root.
  • The _library test helper passes None when given no globs, so existing tests keep their meaning.
• CHANGELOG: an "Empty globs." entry under Fixed, and the Refuse a lean_lib that is not an array of named tables, and tidy lean_probe #505 correction.

Verification

• The locked ruff 0.15.17 check passes on autoform_cli and the changed tests.
• Called directly on macOS: tests/test_lean_probe.py 103 passed, 3 skipped (real Lean); tests/test_library_generate.py 90 passed, 13 skipped; tests/test_impact.py 147 passed, 8 skipped, 1 failed: test_unselected_source_with_a_quoted_module_name_stays_local, which fails the same way on main under Python 3.14.
• Against main's code with this branch's tests: the new globs = [] tests (probe, impact, generate), the () case of the builds matrix, the updated lean_libraries test and the reworded CLI refusal fail; everything else passes. With _module_source_paths reverted to Claim a source file in import-impact only for a module Lake can build #500's predecessor rule (a root prefix alone claims the file), the new import-closure test fails.
• CI runs the real-Lean jobs, which this PR does not change.

Overlap

• Import impact own helpers #492, Name files by path in input and output errors, and correct the path-free claim #506, Leave generated import roots that Git marks linguist-generated out of import-edit claims #514 and Use servers/_process.py for the CLI's process checks #518 edit some of the same files. Each merges with this branch without conflict, and none reads LeanLibrary.globs.

Not in this PR

• library generate decides what a library with globs builds from the globs alone, which matches what lake build <lib> builds, not Lake's isBuildableModule; that difference predates this PR and is deliberate there.
• A globs value of the wrong type is still read as missing, where Lake refuses it.

[Deicyde]

Review at ccbef4a: merge.

Nothing blocks merge, and there are no notes.

• globs = [] now matches Lake. In v4.35.0, decodeRoots (Lake/Load/Toml.lean:275-282) fills in the default globs only when the key is missing, and isBuildableModule (Lake/Config/LeanLibConfig.lean:140-142) needs a glob that matches. So an empty array builds nothing, as builds, project_modules and library generate now read it. Every reader of LeanLibrary.globs handles None and () apart: impact.py:337 and :633, lean_probe.py:780 and library/generate.py:180 and :187.
• The tests pin the changes. Putting back if selecting: in library_sources fails the globs = [] generate case. Making the new unbuilt-module branch never fire fails test_cli_import_impact_refuses_a_loaded_module_no_library_builds. The Refuse a lean_lib that is not an array of named tables, and tidy lean_probe #505 refusal cases now match the whole message, including ", written [[lean_lib]]".

Checks

• Locally at this head, tests/test_lean_probe.py, tests/test_library_generate.py and tests/test_impact.py give 340 passed and 24 skipped (real Lean). I left out test_unselected_source_with_a_quoted_module_name_stays_local, which fails on main too under Python 3.14.
• The PR merges cleanly with main a87797f, and CI passes 9 of 9.

Posted by Claude Code (session jackmccarthy-eb).