Refuse a lean_lib that is not an array of named tables, and tidy lean_probe

CHANGELOG.md

@@ -105,6 +105,10 @@ date when the release is tagged.
   a bounded fallback for hidden or stalled tabs, rather than relying only on
   timer tasks. Parent references use the same compact node offsets as relations;
   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).
 - **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

autoform_cli/lean_probe.py

@@ -48,6 +48,7 @@
 from concurrent.futures import FIRST_COMPLETED, ThreadPoolExecutor, wait
 from dataclasses import dataclass
 from pathlib import Path
+from typing import TypeVar
 
 import psutil
 import tomli
@@ -207,17 +208,11 @@ def read_snapshot_file(path: Path) -> tuple[bytes, tuple[int, str]] | None:
 )
 
 
-def _snapshot_regular_file(path: Path) -> tuple[int, str] | None:
-    captured = read_snapshot_file(path)
-    return None if captured is None else captured[1]
-
-
 def project_control_snapshot(root: Path) -> tuple[tuple[str, tuple[int, str] | None], ...]:
     """Fingerprint the Lake inputs that select the compiled environment."""
 
-    return tuple(
-        (name, _snapshot_regular_file(root / name)) for name in _PROJECT_CONTROL_FILES
-    )
+    captured = ((name, read_snapshot_file(root / name)) for name in _PROJECT_CONTROL_FILES)
+    return tuple((name, None if snapshot is None else snapshot[1]) for name, snapshot in captured)
 
 
 # --------------------------------------------------------------------------- #
@@ -680,10 +675,15 @@ def lean_libraries(lean_root: str | Path) -> tuple[LeanLibrary, ...]:
     artifact_dir = (root / build_dir / lean_lib_dir).resolve()
     package_src = root / str(config.get("srcDir", "."))
 
+    entries = config.get("lean_lib", [])
+    if not isinstance(entries, list) or not all(isinstance(entry, dict) for entry in entries):
+        raise SkeletonError(
+            [f"cannot read the lean_lib targets of {root}: Lake expects an array of tables, written [[lean_lib]]"]
+        )
     libraries: list[LeanLibrary] = []
-    for entry in config.get("lean_lib", []) or []:
-        if not isinstance(entry, dict) or not isinstance(entry.get("name"), str):
-            continue
+    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"])
         name = entry["name"]
         src_dir = package_src / str(entry.get("srcDir", "."))
         roots = entry.get("roots")
@@ -707,12 +707,11 @@ def lean_libraries(lean_root: str | Path) -> tuple[LeanLibrary, ...]:
         )
     if not libraries:
         package = config.get("name")
-        if isinstance(package, str) and package:
-            libraries.append(
-                LeanLibrary(name=package, src_dir=package_src.resolve(), roots=(package,), artifact_dir=artifact_dir)
-            )
-    if not libraries:
-        raise SkeletonError([f"the Lake configuration of {root} declares no library"])
+        if not isinstance(package, str) or not package:
+            raise SkeletonError([f"the Lake configuration of {root} declares no library"])
+        libraries.append(
+            LeanLibrary(name=package, src_dir=package_src.resolve(), roots=(package,), artifact_dir=artifact_dir)
+        )
     return tuple(libraries)
 
 
@@ -1024,12 +1023,10 @@ def _lake_executable(lean_root: Path, label: str = "skeleton probe") -> str:
     return lake
 
 
-def _check_build_freshness(
-    lean_root: Path, modules: tuple[str, ...], *, timeout: float = DEFAULT_FRESHNESS_TIMEOUT
-) -> None:
+def _check_build_freshness(lean_root: Path, modules: tuple[str, ...]) -> None:
     """Run the Lake freshness check once over every module about to be probed."""
 
-    _check_artifacts_fresh(_lake_executable(lean_root), lean_root, modules, timeout=timeout)
+    _check_artifacts_fresh(_lake_executable(lean_root), lean_root, modules, timeout=DEFAULT_FRESHNESS_TIMEOUT)
 
 
 def _probe_environment() -> dict[str, str]:
@@ -1233,7 +1230,10 @@ def _probe_workers(jobs: int) -> int:
     return max(1, min(jobs, _MAX_PROBE_WORKERS, cpus or 1))
 
 
-def run_module_probes(modules: list[str], probe: Callable[[str], object]) -> dict[str, object]:
+_T = TypeVar("_T")
+
+
+def run_module_probes(modules: list[str], probe: Callable[[str], _T]) -> dict[str, _T | SkeletonError]:
     """Run ``probe(module)`` for each module in a bounded pool and collect the results.
 
     A ``SkeletonError`` from one probe is that module's result. Anything else,
@@ -1246,14 +1246,14 @@ def run_module_probes(modules: list[str], probe: Callable[[str], object]) -> dic
 
     cancelled = threading.Event()
 
-    def run(module: str) -> object:
+    def run(module: str) -> _T:
         _PROBE_POOL.cancelled = cancelled
         try:
             return probe(module)
         finally:
             _PROBE_POOL.cancelled = None
 
-    results: dict[str, object] = {}
+    results: dict[str, _T | SkeletonError] = {}
     pool = ThreadPoolExecutor(max_workers=_probe_workers(len(modules)), thread_name_prefix="autoform-probe")
     with _signal_guard() as guard:
         try:

autoform_cli/skeleton.py

@@ -1526,7 +1526,7 @@ def probe(module: str) -> dict[str, dict[str, object]]:
                     f"probe of module {module} failed: {result}", lean_root
                 )
             else:
-                records.update(result)  # type: ignore[arg-type]
+                records.update(result)
 
     nodes: list[NodeSkeleton] = []
     module_hashes: dict[tuple[str, str], str] = {}

tests/test_lean_probe.py

@@ -557,7 +557,7 @@ def test_bounded_command_interruption_kills_the_process(tmp_path: Path, monkeypa
     def interrupt_after_start() -> float:
         nonlocal calls
         calls += 1
-        if calls == 1:
+        if calls != 2:
             return monotonic()
         deadline = monotonic() + 5
         while not process_pid.exists() and monotonic() < deadline:
@@ -918,10 +918,14 @@ 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_package_without_library_targets_is_its_own_library(tmp_path: Path) -> None:
+@pytest.mark.parametrize(
+    "lakefile",
+    [pytest.param('name = "Solo"\n', id="absent"), pytest.param('name = "Solo"\nlean_lib = []\n', id="empty-array")],
+)
+def test_a_package_without_library_targets_is_its_own_library(tmp_path: Path, lakefile: str) -> None:
     project = tmp_path / "project"
     project.mkdir()
-    (project / "lakefile.toml").write_text('name = "Solo"\n', encoding="utf-8")
+    (project / "lakefile.toml").write_text(lakefile, encoding="utf-8")
 
     (library,) = lean_libraries(project)
 
@@ -973,6 +977,34 @@ def test_lake_toml_1_1_extensions_are_rejected_on_every_python(tmp_path: Path, t
         lean_libraries(project)
 
 
+@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"),
+    ],
+)
+def test_a_lean_lib_that_is_not_an_array_is_refused_as_lake_refuses_it(
+    tmp_path: Path, lean_lib: str, match: str
+) -> None:
+    project = tmp_path / "project"
+    project.mkdir()
+    (project / "lakefile.toml").write_text('name = "Solo"\n' + lean_lib, encoding="utf-8")
+
+    # Lake's TOML loader fails with "expected array", "expected table" or
+    # "missing required key: name" (Lake/Load/Toml.lean, decodeTargetDecls).
+    with pytest.raises(SkeletonError, match=match):
+        lean_libraries(project)
+
+
 def test_lake_toml_parser_limits_fail_closed(tmp_path: Path) -> None:
     project = tmp_path / "project"
     project.mkdir()