diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index d849b2c70..7dbd89676 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.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. diff --git a/scripts/check_docs.py b/scripts/check_docs.py index 4fd3bde4a..ffbbf939c 100644 --- a/scripts/check_docs.py +++ b/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()) diff --git a/scripts/test_check_docs.py b/scripts/test_check_docs.py index c4ed2a17d..e75c1c6ea 100644 --- a/scripts/test_check_docs.py +++ b/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(