ci(docs): check docs-project lockfiles against the root pin at PR time

.github/workflows/lean_action_ci.yml

@@ -38,6 +38,13 @@ jobs:
         run: python3 -m unittest discover -s scripts -p 'test_*.py'
       - name: "Source hygiene"
         run: python3 -B scripts/check_hygiene.py --check-simp
+      # The API documentation (docbuild/) and the guide (guide/) are separate Lake projects that
+      # share the library's toolchain and `.lake/packages`, so their lockfiles must follow the root
+      # pins. Their own workflows run only nightly or on guide changes; checking here makes a root
+      # cslib or Mathlib bump without matching lockfile updates fail at PR time. It reads only
+      # checked-in files: no Lean, network or `.lake`.
+      - name: "Documentation pins"
+        run: python3 -B scripts/check_docs.py --config-only
       # lean-action has no hook between installing the toolchain and building, so here it only
       # installs elan and fetches Mathlib's cache. The steps around it do the rest of what it did:
       # restore and save `.lake` under the same Actions cache key, then build, test and lint.

scripts/check_docs.py

@@ -77,14 +77,20 @@ def require(condition, message):
 
 def check_project(project, label, generator_name, root_packages, toolchain):
     """Check a documentation project that shares the library's toolchain and package checkouts."""
-    manifest = json.loads((ROOT / project / "lake-manifest.json").read_text())
+    lockfile = f"{project}/lake-manifest.json"
+    manifest = json.loads((ROOT / lockfile).read_text())
     packages = {p["name"].strip("«»"): p for p in manifest["packages"]}
     for package in root_packages:
         locked = packages.get(package["name"])
-        require(locked is not None, f"{label} lockfile omits {package['name']}")
+        require(locked is not None,
+                f"{label} lockfile omits {package['name']}; copy its entry from "
+                f"lake-manifest.json into {lockfile}")
         for key in LOCKED_KEYS:
             require(package.get(key) == locked.get(key),
-                    f"{label} lockfile differs for {package['name']}: {key}")
+                    f"{label} lockfile differs for {package['name']}: {key} is "
+                    f"{json.dumps(locked.get(key))} in {lockfile} but "
+                    f"{json.dumps(package.get(key))} in lake-manifest.json; update {lockfile} "
+                    f"to match the root pin")
     require((ROOT / project / "lean-toolchain").read_text().strip() == toolchain,
             f"{label} toolchain differs from the library")
     config = tomllib.loads((ROOT / project / "lakefile.toml").read_text())

scripts/test_check_docs.py

@@ -799,10 +799,13 @@ def package(name, rev, input_rev="main"):
         return {"name": name, "type": "git", "url": f"https://example.com/{name}", "rev": rev,
                 "inputRev": input_rev, "subDir": None}
 
-    def check(self):
+    def write_manifests(self):
         for project, packages in self.manifests.items():
             (self.root / project / "lake-manifest.json").write_text(
                 json.dumps({"packages": packages}))
+
+    def check(self):
+        self.write_manifests()
         check_docs.check_config()
 
     def assert_failure(self, message):
@@ -815,7 +818,34 @@ def test_consistent_projects_pass(self):
 
     def test_guide_lockfile_follows_the_library(self):
         self.manifests["guide"][1]["rev"] = "b"
-        self.assert_failure("Guide lockfile differs for cslib: rev")
+        self.assert_failure(
+            'Guide lockfile differs for cslib: rev is "b" in guide/lake-manifest.json but "a" in '
+            "lake-manifest.json; update guide/lake-manifest.json to match the root pin")
+
+    def test_root_pin_bump_requires_documentation_lockfiles(self):
+        # #1372 moved the root cslib pin without the docs projects' lockfiles (#1397).
+        self.manifests[""][0]["rev"] = "b"
+        self.assert_failure(
+            'Documentation lockfile differs for cslib: rev is "a" in docbuild/lake-manifest.json '
+            'but "b" in lake-manifest.json; update docbuild/lake-manifest.json to match the '
+            "root pin")
+
+    def test_root_dependency_must_be_locked(self):
+        self.manifests[""].append(self.package("mathlib", "x"))
+        self.assert_failure(
+            "Documentation lockfile omits mathlib; copy its entry from lake-manifest.json into "
+            "docbuild/lake-manifest.json")
+
+    def test_command_line_reports_drift(self):
+        self.manifests[""][0]["rev"] = "b"
+        stderr = io.StringIO()
+        with patch("sys.argv", ["check_docs.py", "--config-only"]), \
+                patch("sys.stderr", stderr), self.assertRaises(SystemExit) as raised:
+            self.write_manifests()
+            check_docs.main()
+        self.assertEqual(raised.exception.code, 1)
+        self.assertIn("Documentation check failed: Documentation lockfile differs for cslib: rev",
+                      stderr.getvalue())
 
     def test_verso_tag_follows_the_toolchain(self):
         (self.root / "guide/lakefile.toml").write_text(