[Deicyde]

A follow-up to #482: lean_libraries refuses a lean_lib that is not an array of named tables, as Lake refuses it, and lean_probe gets four small tidies that change no behavior.

Change

• A lean_lib Lake refuses is refused here too. lean_libraries read config.get("lean_lib", []) or [] and skipped any entry that was not a table with a string name. With name = "Solo" in lakefile.toml:

  • lean_lib = true (or any nonzero number) crashed with a TypeError;
  • lean_lib = "Solo", lean_lib = false (or 0), lean_lib = [1], a [[lean_lib]] with no name, and [lean_lib] written for [[lean_lib]] all fell back to the package library without a word. The single-bracket case also lost its configured roots.

  Lake's TOML loader refuses every one of these shapes ("expected array", "expected table", "missing required key: name"), so lake build never built anything for them. They now raise a SkeletonError: "cannot read the lean_lib targets of ...: Lake expects an array of tables, written [[lean_lib]]", or "...: a [[lean_lib]] target has no name". This reaches skeleton, review prepare, work import-impact and library index.

• What still works. An empty lean_lib = [], or no lean_lib at all, keeps the package fallback. Only a hand-written lakefile.toml can reach the new refusals: for a lakefile.lean project, lean_libraries reads Lake's own translate-config output, which always writes [[lean_lib]].

• Tidies, same behavior:

  • the two if not libraries: blocks at the end of lean_libraries are one block;
  • _check_build_freshness drops its timeout argument, which its one caller, default_runner, never passed;
  • run_module_probes is typed with a TypeVar, dict[str, _T | SkeletonError], so skeleton.py no longer needs # type: ignore[arg-type] on records.update(result). The union stays because a module's SkeletonError is stored as its result;
  • _snapshot_regular_file is inlined into project_control_snapshot, its one caller.

• Tests.

  • New test_a_lean_lib_that_is_not_an_array_is_refused_as_lake_refuses_it in tests/test_lean_probe.py, after the TOML 1.1 test: true, false, a string, single brackets and [1] match "array of tables", and the nameless table matches "has no name".
  • test_a_package_without_library_targets_is_its_own_library now also runs with lean_lib = [], which pins the package fallback for an empty array.
  • test_bounded_command_interruption_kills_the_process returns the real clock on every time.monotonic call but the second (calls != 2, was calls == 1). The interrupt fires at the same point, and a later read during cleanup can no longer raise a second KeyboardInterrupt.

• CHANGELOG. One Fixed entry, "Lake configuration".

Net: +64/−28 across autoform_cli/lean_probe.py, autoform_cli/skeleton.py, tests/test_lean_probe.py and CHANGELOG.md.

Verification

• lean_libraries called directly on lakefile.toml-only projects (no process starts), with name = "Solo" plus each shape:
  • base branch: true and 3 raise TypeError; "Solo", [lean_lib], false, [1] and the nameless table return the package library Solo;
  • this branch: all seven raise SkeletonError with the messages above, and lean_lib = [] still returns Solo.
• When called directly on macOS:
  • the six new refusal cases fail on the base branch (one TypeError, five "DID NOT RAISE") and pass here, and both fallback cases pass on both;
  • 29 selected cases from tests/test_lean_probe.py cover the new test, the interruption test, and the project-layout, TOML, snapshot and probe-pool tests: 26 pass and 2 skip because they need real Lake. The last, test_lake_configuration_snapshot_rejects_content_changed_between_reads, misses under the direct runner on the base branch too, because that runner's temporary directory on macOS is not resolved and pytest's is; called with a resolved directory, it passes;
  • 10 cases from tests/test_skeleton.py that patch _check_build_freshness or run extraction through run_module_probes pass, including test_cli_sets_the_probe_timeout.
• The locked ruff 0.15.17 check passes on the three Python files, and they compile. ruff format --check flags lean_probe.py, skeleton.py and tests/test_lean_probe.py as it flags them on the base branch; the changed lines add no formatter hunks, and CI does not run the formatter.
• No type checker ran. No CI job type-checks either, so the TypeVar change is a typing claim only; nothing changes at runtime.
• CI coverage:
  • test (Python 3.10 and 3.13) runs ruff check autoform_cli servers tests and pytest -q, which collects the new test and the interruption test.
  • real-lean-skeleton runs tests/test_skeleton.py and tests/test_lean_probe.py on real Lake, including the two translate-config layout tests that read a lakefile.lean through lean_libraries.
  • real-lean's impact and library index steps run tests/test_impact.py and tests/test_library_generate.py on real Lean; work import-impact and library index call lean_libraries.
  • windows-hardening runs only the node IDs it lists. test_bounded_command_interruption_kills_the_process is one of them; the new lean_lib test is not.

Overlap

• Stacked on Move the lean_probe runner tests into tests/test_lean_probe.py #504 (cleanup/lean-probe-tests), which moves the runner tests into tests/test_lean_probe.py; the two tests here land in that file. Merge Move the lean_probe runner tests into tests/test_lean_probe.py #504 first.
• Give the managed-output helpers their own module #501 and Claim a source file in import-impact only for a module Lake can build #500 also change autoform_cli/lean_probe.py, and Give the managed-output helpers their own module #501 also changes autoform_cli/skeleton.py. Read a link definition as Python-Markdown does when rewriting links #484, Report every code fence autoform reads as left open, not only one at the margin #487, Bump opentelemetry-api, and document stop's timeout and #481's nesting #489, Fix the book's copy: whole landing leads, Lean-specific Next up, one-line progress, no failure text in search #494, Read the book in one order: outline, numbers, Next up, Previous/Next and the nav follow the containment tree #495 and Claim a source file in import-impact only for a module Lake can build #500 also change CHANGELOG.md. Each merges with this branch without conflict.

[Deicyde]

Review at af9826f: merge.

Nothing blocks merge. This covers #505's own commits (eaa0cca, af9826f) on top of #504. lean_libraries now refuses exactly the shapes Lake's TOML loader refuses (decodeTargetDecls in Lake/Load/Toml.lean, v4.35.0): true, false, numbers, a string, [1], a nameless target and the single-bracket form. An empty lean_lib = [], or none, keeps the package fallback. The four tidies change no behaviour.

Notes

1. Untested refusals. Main read the valid entries and silently dropped the bad one for lean_lib = [{name = "A"}, 1] and for a nameless [[lean_lib]] after a named one. This PR refuses both, which is right, since Lake refuses them, but no test covers either. lean_lib = 3, which the body names as a former TypeError, is not a parameter either. Adding the three cases to test_a_lean_lib_that_is_not_an_array_is_refused_as_lake_refuses_it would pin them.
2. name = 1 is reported as "has no name". The target does have a name, just not a string one. Wording such as "has no string name" would be exact. Also, the test's regexes stop before the advice, so ", written [[lean_lib]]" can change or disappear without a failure. Matching array of tables, written \[\[lean_lib\]\] would pin it.
3. Description. work impact reaches the refusal too: revision_impact goes through _load_impact_evidence, which calls lean_libraries (impact.py:1517). The body's list leaves it out. The CHANGELOG says such files were refused "instead of crashing or silently reading the package's default library"; in the mixed case main skipped the bad entries instead.
4. After Move the lean_probe runner tests into tests/test_lean_probe.py #504 merges. The repository does not delete merged branches, and tests.yml does not run on a base-branch edit. So retarget this PR to main (gh pr edit 505 --base main) and close and reopen it, so that CI runs against main before merge.

Checks

Every lean_lib shape in the body, plus mixed arrays and non-string names, was run on #504's head and on this head, and compared with Lake's loader source. Of 23 mutants, 14 were killed; the survivors are the untested cases in notes 1 and 2, plus two gaps that already existed on main. Merged with current main, the probe, skeleton, impact, library, review, doc-budget, release and skill-example suites gave 970 passed, 77 skipped (real Lean) and 1 failed. The failure is a Python 3.14 quirk that also fails on plain main. The 8 new collected IDs are the six refusal cases and the now-parametrized fallback test. CI passed 9 of 9.

Posted by Claude Code (session jackmccarthy-63).