From eaa0cca1f3951eff5d1f3736e8ee4b477aee7789 Mon Sep 17 00:00:00 2001 From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com> Date: Thu, 29 Oct 2026 22:03:23 -0400 Subject: [PATCH 1/2] Refuse a lean_lib that Lake refuses, and tidy lean_probe lean_libraries read `lean_lib` with `config.get("lean_lib", []) or []` and skipped every entry that was not a table with a string name. So `lean_lib = true` crashed with a TypeError, while `lean_lib = "Solo"`, `lean_lib = false`, `lean_lib = [1]`, a nameless `[[lean_lib]]` and `[lean_lib]` written for `[[lean_lib]]` all fell back to the package library without a word; the single-bracket case dropped 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. lean_libraries now raises a SkeletonError naming the problem. An empty array keeps the package fallback. Only a hand-written lakefile.toml reaches the check: for a lakefile.lean project, Lake's own translate-config output always writes `[[lean_lib]]`. The rest is tidying with no change in behavior: - merge the two `if not libraries:` blocks in lean_libraries; - drop `_check_build_freshness`'s `timeout` argument, which its one caller never passed; - type run_module_probes with a TypeVar, so a probe's result type reaches the caller and skeleton.py's `type: ignore[arg-type]` on `records.update(result)` goes away; - inline `_snapshot_regular_file` into project_control_snapshot, its one caller. The bounded-command interruption test now returns the real clock on every call but the second, so a later read of time.monotonic during cleanup cannot raise a second KeyboardInterrupt. A new test covers the six refused lean_lib shapes, and the package-fallback test now also runs with `lean_lib = []`. --- CHANGELOG.md | 4 ++++ autoform_cli/lean_probe.py | 48 +++++++++++++++++++------------------- autoform_cli/skeleton.py | 2 +- tests/test_lean_probe.py | 38 +++++++++++++++++++++++++++--- 4 files changed, 64 insertions(+), 28 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index cecfde79f..138ac74b2 100644 --- a/CHANGELOG.md +++ b/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 (#NNN). - **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 diff --git a/autoform_cli/lean_probe.py b/autoform_cli/lean_probe.py index 5eb56b431..9f3cc6545 100644 --- a/autoform_cli/lean_probe.py +++ b/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: diff --git a/autoform_cli/skeleton.py b/autoform_cli/skeleton.py index e8c9f106c..ad6031360 100644 --- a/autoform_cli/skeleton.py +++ b/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] = {} diff --git a/tests/test_lean_probe.py b/tests/test_lean_probe.py index b992544f3..49e86f26a 100644 --- a/tests/test_lean_probe.py +++ b/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() From af9826fd00ef9b18d7c7e6591b14bcff3589d9d3 Mon Sep 17 00:00:00 2001 From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com> Date: Thu, 29 Oct 2026 23:32:30 -0400 Subject: [PATCH 2/2] Name #505 in its CHANGELOG entry --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 138ac74b2..c9a0f8a62 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -108,7 +108,7 @@ date when the release is tagged. - **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 (#NNN). + 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