fix(dev): reject missing audit outputs before invoking Lake

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

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

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)")

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")