Repository navigation
chore(deps): track CSLib main and Lean v4.36.0-rc2 #1648
Description
The 2026-10-29 upstream audit of main@d6ccb24f finds our CSLib pin f4a472560f78c59bbedd795fe041ec507f7d0582 is an ancestor of upstream main@8a8ad7489cdccb007ad7279bfb9d03bbda2229ad, three commits behind (comparison). The new pin uses Lean v4.36.0-rc2 rather than v4.36.0-rc1 and updates Mathlib/dependency pins. The upstream source changes are small proof repairs in CCS, query sorting, circuits and perfect secrecy.
Move the base pin forward to upstream main, update the matching root/documentation/guide toolchains, dependency lockfiles, and doc-gen4/Verso tags, and repair compatibility without weakening any public theorem, model, encoding or independent resource bound. Both documentation projects already publish v4.36.0-rc2 tags. Keep the base on leanprover/cslib main, never a fork.
Audit disposition: scripts/upstream_sync.py reports all submitted copies CURRENT. Its 14 MOVED lines all record the @9cce4cc7 unpublished machine rewrite while the published crei/tidy-universal branch remains 7f7c0696; this is the exception already explained in UPSTREAM.md. Preserve those local adaptations instead of replacing them with the older published branch. Re-run the audit on the final pin and act on any genuinely new drift.
Completion criteria:
- Synchronize all root/docbuild/guide pins and toolchains; use isolated dependency sources/control files (
--copy-packages) so updates cannot modify another checkout. - Preserve source credit and public mathematical/resource meanings; document any necessary compatibility repair and update every affected client.
- Pass the six default validation gates, hygiene/changed-file/tidy checks, documentation configuration checks and the required API documentation/guide builds. Assess selected abstracts against final sources and renderer/toolchain effects; inspect affected rendered artifacts/links if rendering changes.
- Publish a reviewable PR with final validation and an independent outside-fleet review before integration. Sequence this broad toolchain migration after the smaller in-flight changes, keeping their queue moving.
No competing open pin/toolchain/upstream task was found in the issue search. Coordinator: codex-coord-20261029-1732; a dedicated worker will claim the implementation. This records a dependency migration, not new mathematics.
AI assistance: Codex ran the upstream audit, checked ancestry and documentation tags, and prepared this task.
Activity
SamuelSchlesinger commentedon Oct 29, 2026
active — worker
codex-rc2-1648-20261029(/root/review_1646_expected) claims the complete CSLib/main and Lean rc2 migration. Branch:work/cslib-rc2-sync-1648-codex; isolated worktree:.worktrees/cslib-rc2-sync-1648-codex, created with--copy-packages. Scope includes root/docs/guide pins and manifests, compatibility repairs preserving public meanings, full validation, documentation builds and abstract/rendering assessment. The coordinator will sequence integration after smaller in-flight changes.SamuelSchlesinger commentedon Oct 29, 2026
active — coordinator
codex-coord-20261029-1732reporting for workercodex-rc2-1648-20261029. Pins and the mechanical deprecated-name migration are separated from proof repairs. Ten repaired modules pass strict focused builds, and landed #1644/#1650 are incorporated. The full-gate attempt has exposed further elaboration/automation failures in Karger, determinant and expander proofs; these are being repaired with unchanged statements and resource bounds before final validation. Worker/root/review_list_foldl_maxhas a read-only subtask on ExplicitExpanders heartbeat diagnostics; edit/build ownership remains with the migration worker. CSLib main remains8a8ad748. Documentation builds, final gates and outside review remain required; this is not a completed migration.SamuelSchlesinger commentedon Oct 29, 2026
active — worker
codex-rc2-1648-20261029: root, API-doc and guide pins are synchronized with CSLib main and Lean rc2 inwork/cslib-rc2-sync-1648-codex. The dependency audit and focused compatibility checks preserve public mathematical/resource meanings. Full validation is identifying a few remaining proof-automation client adjustments; next are focused repairs, a fresh six-gate run, and API-doc/guide builds and rendering checks. Landed helper cleanups are incorporated; the coordinator is sequencing the remaining smaller PRs before this migration.SamuelSchlesinger commentedon Oct 29, 2026
active — worker
codex-rc2-1648-20261029: the source checkpoint, dependency audit and passing six-gate/static validation are recorded in draft PR #1653. API-doc/guide builds, rendered-page checks, hosted CI and final-main integration remain pending there; implementation and validation continue while the coordinator arranges outside source review.SamuelSchlesinger commentedon Oct 29, 2026
active — worker
codex-rc2-1648-20261029: source validation and the successful guide artifact/render checks are recorded in draft PR #1653. API documentation generation continues; next are its link/size checks and the final integration of the pre-pin queue. The raw folded-automation restoration remains a separate, reviewable layer in #1654 / #1657.SamuelSchlesinger commentedon Oct 29, 2026
active — coordinator
codex-coord-20261029-1732reporting for workercodex-rc2-1648-20261029. Draft #1653 now publishes the final merge of fixed pre-pinmain@96fd02a8; all six local gates and refreshed checks pass, with the reviewed migration payload unchanged. The PR owns validation and existing source/API evidence. Final outside delta review, hosted checks and API/guide rendering/link/provenance inspection remain active there. Later arithmetic, placement and kernel-cleanup PRs follow this pin migration; the issue stays open until actual integration.SamuelSchlesinger commentedon Oct 29, 2026
active — worker
codex-rc2-1648-20261029: draft #1653 now incorporates the fixed pre-pin main and passes all six gates plus static checks, with the reviewed migration patch unchanged. Final API/guide generation, rendered-link/provenance checks, hosted CI and integration-delta review remain pending in the PR; no later queued work is included.SamuelSchlesinger commentedon Oct 29, 2026
awaiting review — worker
codex-rc2-1648-20261029: final source, all six local gates, static/dependency audits and API/guide/PDF validation are consolidated in #1653. Outside source/integration review covers the frozen head. The draft remains pending final hosted source CI and the coordinator's integration checks; the issue stays open. Local generated artifacts are stable and no worker build is running.SamuelSchlesinger commentedon Oct 29, 2026
queued — coordinator
codex-coord-20261029-1732marked #1653 ready and enqueued the frozen reviewed head after final hosted CI passed. Current source/API/render reviews, all six local gates and final artifacts are recorded in the PR. Merge-group validation and actual landing remain required; this issue stays open until main integration. The later stacks remain sequenced behind it.SamuelSchlesinger commentedon Oct 29, 2026
Current-upstream gap — coordinator
codex-coord-20261029-1732checked CSLib main at 23:36 UTC: it advanced one commit to254e30e6, moving Mathlib to69552756and repairing two Nat-recursion proofs. The copied-module audit has no new drift beyond that pin difference and the fourteen already documented local machine adaptations.#1653 remains the reviewed initial rc2 milestone at
0d38523e; its active merge-group source stays frozen. New child #1684 is assigned to/root/review_1646_expectedfor the current pin/lockfile and compatibility follow-up in isolated outputs. The PR now identifies that remaining gap and no longer auto-closes this issue. Record the first landing as a milestone; keep #1648 open until the current-upstream update is integrated.SamuelSchlesinger commentedon Oct 30, 2026
Milestone completed — #1653 landed on main as
0ba8b2e59d4d7009c814096d8bbb4a9823d06963at 00:23 UTC, following successful merge-group validation. The landed tree is exactly the independently reviewed0d38523esource: initial CSLib8a8/Lean rc2 migration, compatible proof repairs and checked API/guide output.This issue remains open. #1684 owns the newer CSLib254e30e6/Mathlib69552756 update; its initial full validation passed and final main-based validation/documentation work is in progress. Ready small follow-ons are being restacked onto the landed milestone. No new mathematics is claimed by the dependency migration.