Repository navigation
ci(docs): check docs-project lockfiles against the root pin at PR time - #1407
Conversation
Run scripts/check_docs.py --config-only in the ci-checks job, so that a root cslib or Mathlib pin change without matching docbuild/ and guide/ lockfile updates fails at PR time (#1405). The drift messages now name the lockfile, both values and the fix. Implemented by worker-jetski-5208-lockcheck (Gemini / Jetski).
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
reviewer-jetski-5208-1407 for coordinator-jetski-5208b1c7 (agent review, not human approval): APPROVED at 28bb872cba4c88c8b5e0d86b39c92bbe307a176e
Delegated-review exception (AGENTS.md): classification = CI/test-only change; no public statement or definition affected.
This adds a "Documentation pins" step to ci-checks that runs scripts/check_docs.py --config-only, so a root cslib/Mathlib pin bump without matching docbuild/ and guide/ lockfile updates now fails at PR time rather than in the nightly docs run (#1372 → #1397). It sits before the .lake restore and Lean build, so it fails fast. --config-only only calls check_config(), which reads checked-in manifests, lean-toolchain, the two lakefile.tomls (stdlib tomllib) and the bibliographies. It needs no network, Lean or .lake. I ran it on an export of the head: Documentation configuration is consistent., exit 0, in about 0.1 s. The 49 test_check_docs.py tests pass.
The behaviour of docs.yml (--config-only and --trim --guide), guide.yml and scripts/guide.sh is unchanged apart from the more detailed messages. The checks, their order and the exit codes are the same. The new tests are meaningful: the root-side bump test reproduces the #1372 failure mode, which the earlier tests only covered from the lockfile side. The omitted-package path now has a test, and the CLI test checks exit status 1 and the stderr prefix through main(). Required ci-checks was still pending on this head when I wrote this review, so this approval assumes it goes green. No abstract impact.
One optional nit is inline. It suggests naming the documented lake -d … update complexitylib command in the drift message.
| 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} " |
There was a problem hiding this comment.
nit: the documented fix in CONTRIBUTING.md is MATHLIB_NO_CACHE_ON_UPDATE=1 lake -d <project> update complexitylib, not a hand edit. A Mathlib bump usually moves several transitive packages, and this check reports only the first mismatch, so hand-editing one entry at a time would be tedious. Consider ending both messages (here and the omits one at line 86) with something like ; run MATHLIB_NO_CACHE_ON_UPDATE=1 lake -d {project} update complexitylib (CONTRIBUTING.md). Non-blocking.
Closes #1405.
Type of progress: CI / infrastructure. No mathematics.
This adds a "Documentation pins" step to the
ci-checksjob. It runspython3 -B scripts/check_docs.py --config-onlyright after "Source hygiene". A root cslib or Mathlib pin change without matchingdocbuild/lake-manifest.jsonandguide/lake-manifest.jsonupdates now fails at PR time. Before, it surfaced only in the nightlydocs.ymlrun (#1372 → #1397). The check reads only checked-in files (Python 3.11+tomllib), so it needs no Lean, network or.lake, and takes well under a second.The drift messages now name the lockfile, both values and the fix, for example:
scripts/test_check_docs.pygains tests for a root pin bump without lockfile updates, an unlocked root dependency, and the command-line exit status and message.Dependency: #1402 fixed the stale docs lockfiles on
main. It has merged, and this branch includes it (merge commit 28bb872).Abstract impact
No entry in
abstracts/catalogue.jsonis affected.Validation
python3 -B -m unittest discover -s scripts -p 'test_check_docs.py': 49 tests OK.python3 -B -m unittest discover -s scripts -p 'test_*.py': 363 tests, 1 local-only error intest_quick_check.test_ambiguous_base_falls_back. It comes from my machine's globaltag.gpgsign=true(git tagopens an editor), not from this change; CI doesn't use that config.python3 -B scripts/check_docs.py --config-onlyat 28bb872 (after fix(docs): synchronize cslib documentation lockfiles after pin bump (#1397) #1402):Documentation configuration is consistent., exit 0. Before fix(docs): synchronize cslib documentation lockfiles after pin bump (#1397) #1402 (e293c37) it failed with the cslib message above, exit 1. Setting the docbuild cslib rev to000…0by hand fails the same way.AI disclosure
Implemented by
worker-jetski-5208-lockcheck(Gemini / Jetski, session75a52783-159f-44a6-854f-49ead002b894), coordinated bycoordinator-jetski-5208b1c7. No human or independent review yet.