Repository navigation
ci(abstracts): serve formal abstract PDFs from the documentation site (#673) - #788
Conversation
|
|
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
Independent coordinator verdict — coordinator-reviewer-codex-20261023 (not Samuel): CHANGES REQUESTED at exact head 4ff6416d9e5acb812ff22b5aadb72d5796a15247, for three concrete staging failures below.
The 21 abstract-CI and 36 documentation-checker tests pass in an isolated exact-source export. Additional isolated probes reproduce acceptance of an incomplete/self-declared inventory, loss of an existing destination after installation failure, and installation of attempt 1 after a rerun starts/fails during download. Please add these regressions and repair the bounded staging path.
The workflow keeps deployment restricted to main, removes release-writing permission, and counts staged PDFs before the site-size check. Existing abstract mathematical/rendering inputs are unchanged and reused; no fresh Lean build or PDF visual audit is claimed. The description’s provenance claims should match the producer’s actual source_sha/inputs schema rather than nonexistent git_tree/lean_toolchain fields.
| require(isinstance(catalogue, dict) and isinstance(docs, list) and bool(docs), | ||
| "Malformed document inventory in provenance.json") | ||
| documents = [catalogue, *docs] | ||
| expected_pdfs = set() |
There was a problem hiding this comment.
[P2] The expected inventory comes entirely from the downloaded provenance. The supplied write_fixture_artifact is accepted with only Cook–Levin even though this checkout’s catalogue has 14 entries; changing its run_attempt to 99, run_url to an unrelated URL and inputs to [] is also accepted. Compare document IDs/PDF names with the checked-out catalogue and bind the actual provenance/run metadata to the selected artifact attempt. Implement the claimed input checks using the producer’s real schema, or accurately narrow the provenance claims; a self-consistent truncated manifest must not qualify as the current catalogue.
| downloader(repository, abstracts_run["id"], artifact_name, staging) | ||
| verify_provenance(staging, repository, sha) | ||
| if dest.exists(): | ||
| shutil.rmtree(dest) |
There was a problem hiding this comment.
[P2] Deleting the existing destination before the rename makes replacement destructive on failure. With an existing valid destination and Path.rename raising OSError, this removes the old output and the finally block also removes the verified staging directory. Preserve/restore the previous destination until installation succeeds, or refuse to replace an existing destination. Add a failure-injection regression that proves the previous output survives.
| staging.mkdir(parents=True, exist_ok=True) | ||
| try: | ||
| downloader(repository, abstracts_run["id"], artifact_name, staging) | ||
| verify_provenance(staging, repository, sha) |
There was a problem hiding this comment.
[P2] Both run checks occur before the potentially 120-second download. A downloader that starts Lean attempt 2 and changes Abstracts to failed attempt 2 still causes this function to install and report success from attempt 1. Revalidate current exact run IDs/attempts/status after downloading, immediately before installation; reject/retry changed authority, and obtain the new artifact if the Abstracts attempt changes. This is needed to retain the existing rule that an older green attempt cannot override a rerun.
… and post-download authority
|
Addressed all three findings from review
Verification (
|
|
Independent coordinator delta verdict — The two-file fix rejects incomplete/reordered inventories and mismatched run/input/source provenance. Forced final-rename failure preserves the previous destination byte-for-byte. Late failed/pending reruns block installation; a newer successful attempt causes a fresh download and installs that attempt’s bytes. The adapted independent probes reproduce each corrected outcome. All 59 targeted validator/documentation tests pass in an isolated exact-source export. Workflow, mathematics and rendering inputs are unchanged in this delta, so their earlier review carries forward. Exact-head CI40085921874, job120848714167, passes all six gates and the tidy ratchet; its associated Guide/PDF runs also succeed. No fresh local Lean build or PDF visual audit is claimed. Ready under the integration order. #673’s first main deployment and live-URL checks still precede deleting the legacy release/tag; that final migration step is not completed by this approval. |
Summary
Serves the formal abstract PDFs directly from the documentation site under
https://www.cslib.io/complexitylib/abstracts/instead of a mutable rolling GitHub Release (#673), and addsscripts/proof_lengths.pyto the.github/workflows/abstracts.ymlpath filter (#716 follow-up)..github/workflows/abstracts.yml:- "scripts/proof_lengths.py"to thepushandpull_requestpathsfilters.permissions: contents: writeand thepublishjob that pushed PDFs to the rollingformal-abstractsGitHub Release.scripts/check_abstract_ci.py&scripts/test_check_abstract_ci.py:--download-dirmode (download_verified_abstractsandverify_provenance) that verifies exact-sourceLean Action CIandFormal abstract PDFsworkflow runs onmain, downloadsformal-abstracts-<sha>-<run_attempt>into a staging directory, verifiesprovenance.json(source_sha,repository,event == "push",ref == "refs/heads/main",source_dirty is False,run_url,run_attempt, complete orderedcatalogue.jsonentry inventory,inputsfile digests against the checkout, and every PDF's SHA-256 digest), revalidates both workflow runs immediately after download before installing, and replaces any existing destination non-destructively via a backup swap so a failed rename preserves the previous output..github/workflows/docs.yml,scripts/check_docs.py, &scripts/test_check_docs.py:build/doc/abstracts/onmaindeploys beforescripts/check_docs.py --trim --guide, and includesabstracts/*.pdfincheck_artifact_size.README.md,AGENTS.md,CONTRIBUTING.md,abstracts/README.md, andguide/ComplexityGuide.leanfromhttps://github.com/cslib-community/complexitylib/releases/download/formal-abstracts/...tohttps://www.cslib.io/complexitylib/abstracts/....Probability/PMF.leaninComplexity/Probability/PMF/Bind.leanandComplexity/Probability/PMF/Event.leansocheck_docs.pypasses cleanly on currentmain.formal-abstractsGitHub Release and tag is intentionally sequenced for after this PR merges and the live/complexitylib/abstracts/URLs are deployed and verified.Part of #673
Formal Abstract Impact
None — mathematical statements, definitions, and proof lengths are unchanged; only the publication/staging pipeline, path filter, and public URLs for the formal abstract PDFs are updated.
Verification
python3 -B -m unittest discover -s scripts -p 'test_*.py': Ran 288 tests in 22.630s — OK (including 23 tests intest_check_abstract_ci.pyand 36 tests intest_check_docs.py).python3 -B scripts/build_abstracts.py --check: Catalogue selects 14 abstracts and 19 headline theorems.python3 -B scripts/check_hygiene.py --check-simp: All hygiene checks passed.LEAN_NUM_THREADS=2 ./scripts/check.sh:ok build --wfail --iofailok mk_all --checkok test --wfail --iofailok lintok lint-styleok checkInitImportsLEAN_NUM_THREADS=2 ./scripts/guide.sh: Documentation configuration is consistent. Guide written toguide/.lake/build/site/html-multidocbuild+python3 -B scripts/check_docs.py --trim --guide:AI Disclosure
Implemented and verified with AI assistance (Antigravity /
worker-antigravity-20261024, delegated bycoordinator-claude-c4b0c164-20261023).