Repository navigation
chore(deps): advance CSLib and Mathlib after rc2 migration #1684
Description
Upstream CSLib main advanced from #1653's reviewed 8a8ad7489cdccb007ad7279bfb9d03bbda2229ad to 254e30e6d4299c51323aaeaf5f51a4763b375d4a (comparison). The single upstream commit, CSLib #1175, moves Mathlib from 9d581dfff2e41de989072ea63abf3daf69311520 to 69552756cd8a2d2d48763cf7279fd814d6a1224d and repairs two proofs after a Nat recursor-argument rename. Lean remains v4.36.0-rc2.
Prepare a separate follow-up on the frozen #1653 head 0d38523e96f8b431aeadc86c548c9994714f9b00, then restack after that migration actually lands. Keep #1653's queued source unchanged. Advance CSLib to upstream main, synchronize root/docbuild/guide dependency lockfiles, and repair compatibility while preserving public theorem/definition meanings, encodings and independent time/space bounds. Preserve source credit. This is a dependency/API-compatibility update, not new mathematics.
The 23:37 UTC upstream-sync audit reports the pin difference and the same fourteen crei/tidy-universal MOVED lines already dispositioned in UPSTREAM.md: published 7f7c0696 is older than our intentional 9cce4cc7 adaptations. All submitted copies remain CURRENT. Preserve those adaptations; act on any genuinely new drift. Recheck upstream and rerun the audit before final publication.
Completion: all six default gates and relevant hygiene/changed-file/tidy/documentation-pin checks pass at the final head; root, API docs and guide use matching dependencies. Build API documentation and the guide, assess selected abstracts against final sources, and inspect affected rendered pages/source links when output changes. Obtain independent review of the actual pin/proof delta and any affected artifacts before integration. Keep the original rc2 migration evidence in #1653 and link it rather than duplicating it.
Owner to be claimed by worker /root/review_1646_expected under coordinator codex-coord-20261029-1732. Use isolated package source/control files and mutable build outputs; do not alter the primary checkout or the queued branch. This records the new current-upstream gap beyond #1648's frozen snapshot.
AI assistance: Codex checked the upstream commit/comparison, reran the copied-module audit and scoped this follow-up.
Activity
SamuelSchlesinger commentedon Oct 29, 2026
active — worker
codex-upstream-1684-20261029(/root/review_1646_expected) claims this bounded follow-up. Branch:work/cslib-mathlib-sync-1684-codex, based on frozen #1653 head0d38523e; I will reuse my terminal, isolated--copy-packagesworktree.worktrees/cslib-rc2-sync-1648-codexafter archiving its completed API/guide output. Scope is the upstream CSLib/Mathlib pins, matching documentation manifests and minimal compatibility repairs with unchanged public meanings, followed by all required validation and independent review. The queued #1653 branch and build remain unchanged.SamuelSchlesinger commentedon Oct 30, 2026
active — worker
codex-upstream-1684-20261029: synchronized pins/manifests and the 14 proof-label repairs pass focused strict checks, the full strict library build and import aggregation. The full test suite is still running. #1653 has now landed; next are restackingwork/cslib-mathlib-sync-1684-codexonto actual main and final source/API/guide validation. The reviewed original documentation artifacts remain archived unchanged.SamuelSchlesinger commentedon Oct 30, 2026
active — worker
codex-upstream-1684-20261029: source validation and the dependency audit are recorded in draft PR #1694, rebased onto the landed parent. All six gates and static checks pass. API/guide builds and final rendered-page/source-link checks continue while the coordinator arranges independent source review.SamuelSchlesinger commentedon Oct 30, 2026
Active —
codex-upstream-1684-20261029, author of #1694. Source stays frozen atec19e875: all six local gates/statics and outside source review pass; final-head Guide and abstract PDF builds pass. API generation is finishing without errors. Next: completed-site coverage/link/blob-provenance checks and changed-page browser inspection, then the coordinator's affected-render review.SamuelSchlesinger commentedon Oct 30, 2026
Awaiting review —
codex-upstream-1684-20261029. #1694 is frozen atec19e875; the PR now records completed local six-gate, API/guide, source-link and author rendering checks. Outside source review is FINAL. Stable generated output and captures are handed to the coordinator for independent affected-render/provenance review; hosted source CI is still running. No remaining author source changes are known.SamuelSchlesinger commentedon Oct 30, 2026
Active — non-authoring coordinator
codex-coord-1694-20261030claims only the integration of #1694 at reviewed headec19e875b8fe86d9309da5c1ca3b2af85834b9d1, under the maintainer's delegation. Source ownership and the existing source/API reviews stay unchanged. I will wait for #1697 to land with its new-policy pack/restore evidence, then enqueue #1694 at the tail and monitor it through landing. Broader #1648 remains open.SamuelSchlesinger commentedon Oct 30, 2026
Active — integration coordinator
codex-coord-1694-20261030: #1694 stays frozen while the small #1680 tooling fix lands ahead of it and #1697's final consumer restore provenance is confirmed. The fresh upstream check still reports CSLib254e30e6as current, with only the 14 documented tidy-branch exceptions. I will recheck the resulting main and monitor the pin through landing; broader #1648 stays open.SamuelSchlesinger commentedon Oct 30, 2026
Coordinator
codex-coord-20261029-1732: bounded supplemental review is assigned to non-authoring reviewer/root/review_kernel_list_1651: inspect the downloadable artifact from the existing exact-head manual API-docs run 40990419053, once complete, against the already reviewed local output. Reuse the API/Guide review; this adds hosted-artifact provenance/delta coverage, not another source review. The integration owner remains unchanged.SamuelSchlesinger commentedon Oct 30, 2026
Active — integration coordinator
codex-coord-1694-20261030: #1694 is now in merge-group CI after both ordering gates passed. The integration record links the exact combined candidate and reusable review/cache evidence. I am monitoring actual landing and cache availability; this milestone is not complete yet.SamuelSchlesinger commentedon Oct 30, 2026
Active — integration coordinator
codex-coord-1694-20261030: #1694 remains frozen in its merge-group run, currently building the library. The supplemental hosted API/Guide comparison is complete with no finding. Next are actual main landing and cache publication; broader #1648 remains open.SamuelSchlesinger commentedon Oct 30, 2026
Completed — integration coordinator
codex-coord-1694-20261030: #1694 landed with CSLib254e30e6and Mathlib69552756on rc2. Merge-group and main validation pass, and the new-pin remote-cache mapping is published and publicly available. The terminal integration record owns the revision, review and cache evidence. Broader #1648 remains open.