ci: skip catalog shards for docs-only main pushes

scripts/select_ci_problems.py

@@ -4,8 +4,8 @@
 Pull requests validate changed problem modules and every manifest root that
 imports them, transitively. Lean itself parses module headers and provides the
 dependency graph consumed here. Changes to shared generator/infrastructure
-inputs are conservative full-catalog sentinels. Pushes validate the full
-catalog.
+inputs are conservative full-catalog sentinels. Relevant pushes validate the
+full catalog; documentation-only pushes do not launch catalog shards.
 """
 
 from __future__ import annotations
@@ -206,9 +206,16 @@ def select(
 
     all_ids = tuple(sorted(by_id))
     all_modules = tuple(sorted(by_module))
-    if event == "push":
+    initial_push = "<initial-push>" in changed_paths
+    documentation_only = bool(changed_paths) and all(
+        path.startswith("docs/")
+        or ("/" not in path and path.endswith(".md"))
+        for path in changed_paths
+    )
+    if event == "push" and not documentation_only:
         return Selection(
-            "full", ("push to main",), all_ids, all_modules,
+            "full", ("initial push" if initial_push else "non-documentation push to main",),
+            all_ids, all_modules,
             source_changed, generated_changed, run_checks,
         )
 

tests/python/test_select_ci_problems.py

@@ -103,8 +103,33 @@ def test_deleted_generated_file_selects_its_workspace(self):
         self.assertEqual(selection.mode, "targeted")
         self.assertEqual(selection.problems, ("c",))
 
-    def test_push_always_selects_full_catalog(self):
-        selection = self.select((Change("M", ("README.md",)),), event="push")
+    def test_relevant_push_selects_full_catalog(self):
+        for path in (
+            "LeanEval/A.lean",
+            "LeanEval.lean",
+            "EvalTools.lean",
+            "generated/index.json",
+            "scripts/validate_catalog.py",
+            ".github/workflows/other.yml",
+            ".gitignore",
+            "future-input.unknown",
+        ):
+            with self.subTest(path=path):
+                selection = self.select((Change("M", (path,)),), event="push")
+                self.assertEqual(selection.mode, "full")
+                self.assertEqual(len(selection.problems), 4)
+
+    def test_docs_only_push_selects_no_catalog_work(self):
+        for path in ("README.md", "SECURITY.md", "docs/overhaul.md"):
+            with self.subTest(path=path):
+                selection = self.select((Change("M", (path,)),), event="push")
+                self.assertEqual(selection.mode, "none")
+                self.assertFalse(selection.run_catalog)
+
+    def test_initial_push_selects_full_catalog(self):
+        selection = self.select(
+            (Change("A", ("<initial-push>",)),), event="push"
+        )
         self.assertEqual(selection.mode, "full")
         self.assertEqual(len(selection.problems), 4)