diff --git a/scripts/check_changed_files.py b/scripts/check_changed_files.py index 27b86ad07..d7568c494 100644 --- a/scripts/check_changed_files.py +++ b/scripts/check_changed_files.py @@ -17,6 +17,8 @@ `UPSTREAM_SYNTAX`. Backquoted text that is not an identifier, such as notation or a pattern like `foo_*`, is not checked. Declarations come from the `.ilean` files of `lake build` (and `lake test`); stale outputs are refused unless `--no-build-check` is given. + This is a post-build audit; the default freshness probe invokes Lake and may materialize + dependencies. 2. Restatement-only tests. A new file under `ComplexityTests/` fails when it has examples and every one of them is `example … := name` (or `:= by exact name`) for a name other than `rfl`, `trivial` and the like (`EVALUATION`): such a line only restates a signature, which is not a diff --git a/scripts/check_tidy_surface.py b/scripts/check_tidy_surface.py index 5c5fb1212..ba28d7472 100644 --- a/scripts/check_tidy_surface.py +++ b/scripts/check_tidy_surface.py @@ -23,6 +23,8 @@ files, read by `scripts/lean_outputs.py` and `scripts/LeanOutputs.lean`. The check needs the build outputs of `lake build Complexity ComplexityTests ComplexityAbstracts` (`lake build` and `lake test`), and refuses stale ones unless `--no-build-check` is given. +This is a post-build audit; the default freshness probe invokes Lake and may materialize +dependencies. """ from __future__ import annotations diff --git a/scripts/lean_outputs.py b/scripts/lean_outputs.py index d51e9f4db..8b1d908cb 100644 --- a/scripts/lean_outputs.py +++ b/scripts/lean_outputs.py @@ -115,6 +115,9 @@ def check_outputs(build_dir: Path, skip: bool, current=lake_outputs_current, same outputs as the checked default ones.""" if skip: return "not checked against the sources" + if not reference.is_dir(): + sys.exit(f"build outputs are missing in {reference}; run `lake build " + + " ".join(ROOTS) + "` first") if not current(): sys.exit("build outputs are missing or stale; run `lake build " + " ".join(ROOTS) + "` (or pass --no-build-check)") diff --git a/scripts/test_lean_outputs.py b/scripts/test_lean_outputs.py index e0e6d25b0..796ced1ac 100644 --- a/scripts/test_lean_outputs.py +++ b/scripts/test_lean_outputs.py @@ -7,6 +7,7 @@ import sys import tempfile import unittest +from unittest import mock sys.path.insert(0, str(pathlib.Path(__file__).resolve().parent)) import lean_outputs as lo # noqa: E402 @@ -59,6 +60,23 @@ def test_stale_default_outputs_are_refused(self) -> None: with self.assertRaises(SystemExit): self.check(self.reference, current=False) + def test_missing_output_directory_is_refused_without_lake(self) -> None: + missing = self.reference.parent / "missing" + with mock.patch.object(lo.subprocess, "run", side_effect=AssertionError("Lake ran")) as run: + with self.assertRaises(SystemExit) as error: + lo.check_outputs(missing, False, reference=missing) + self.assertIn("build outputs are missing", str(error.exception.code)) + run.assert_not_called() + self.assertFalse(missing.exists()) + + def test_unchecked_missing_directory_does_not_call_lake(self) -> None: + missing = self.reference.parent / "missing" + with mock.patch.object(lo.subprocess, "run", side_effect=AssertionError("Lake ran")) as run: + status = lo.check_outputs(missing, True, reference=missing) + self.assertIn("not checked", status) + run.assert_not_called() + self.assertFalse(missing.exists()) + def test_stale_root_output_is_refused(self) -> None: for directory in (self.reference, self.copy): self.write(directory, "Complexity.ilean", "root")