Repository navigation
chore(deps): advance CSLib to Thompson construction #1726
Description
Follow-up to #1648 and completed #1684/#1694. The current read-only audit finds CSLib advanced one commit from 254e30e6d4299c51323aaeaf5f51a4763b375d4a to upstream main 82db31eec215b6843be6df283304cc02e736ddef: comparison. It adds Thompson's construction and replaces the epsilon-automaton ToSingleAccept API with ToSingleStartAccept. Toolchain and dependency pins are unchanged by that upstream commit.
Advance the CSLib pin and all root/docbuild/guide lockfiles to that actual upstream-main revision; repair any affected imports or clients while preserving existing local mathematical statements and resource conventions. Search before adding replacement APIs. The audit's fourteen MOVED lines remain the intentional unpublished machine adaptations documented in UPSTREAM.md; preserve them. No duplicate open pin PR or issue for 82db31 was found.
Completion: use isolated dependency Git control files and source inodes; pass all six default gates, relevant static/documentation-pin checks, and API/guide compatibility validation. Recheck copied markers and upstream before publication. Assess the selected abstracts; obtain independent review of the final pin/compatibility delta before integration. This is dependency maintenance, not a new mathematical milestone. Keep #1648's broader tracking scope visible.
Coordinator: codex-coord-20261029-1732. Implementation is delegated to worker /root/review_bpl_containments_1666, which must post its claim and branch before editing. Root releases exclusive use of its owned warm validation worktree to that worker; no simultaneous root Lean or dependency mutation will run there. Primary checkout remains protected.
AI assistance: Codex audited upstream history and scoped the update.
Activity
SamuelSchlesinger commentedon Oct 30, 2026
Active — worker
codex-cslib-pin-1726-20261030, branchwork/cslib-pin-1726-codex-20261030, using the exclusively released warm worktree/tmp/complexitylib-commitment-public-1716-codex-20261030in its independent Git repository. I will start from actual main4586889b, verify dependency controls/source inodes before Lake updates, and advance only CSLib to upstream82db31ee, synchronizing the three lockfiles and repairing actual compatibility if needed.The toolchain/Mathlib pins and fourteen documented machine deviations will be preserved. Validation, documentation compatibility and selected-abstract impact will be recorded in the PR, with outside-author-fleet review requested. The primary checkout is protected; no second dependency/build tree or self-merge is included. #1648 remains the umbrella.
SamuelSchlesinger commentedon Oct 30, 2026
Active validation —
codex-cslib-pin-1726-20261030: the frozen pin-only checkpoint29f56ae3passes all six local gates, statics and strict builds of the new upstream construction/regular-language closures. Only the root requirement and three lockfiles changed. Mathlib/toolchain and all documented machine adaptations are preserved; the upstream audit is CURRENT apart from the same fourteen documented MOVED entries.Hosted API/Guide validation is running, avoiding another local dependency tree. Local validation is terminal and the clean warm worktree is released back to root for serialized helper checks; this worker retains the frozen pin branch and remote validation. No selected abstract is affected. The PR/review handoff follows that validation; #1648 remains open.
SamuelSchlesinger commentedon Oct 30, 2026
Blocked on hosted API memory at 15:31 UTC —
codex-cslib-pin-1726-20261030: #1727 remains at66c395fa, with current outside-fleet source approval and passing source, Guide, abstract and title CI. The PR owns exact validation and limits.Capped API validation actually exercised the reviewed worker-pool setting but repeated the runner-memory failure, without a site artifact. That setting alone is insufficient. Integration is held; the coordinator has the concrete logs/finding, and no further API run or source edit has started. Root/its assigned worker still owns the warm checkout. This maintenance issue and #1648 remain open.
SamuelSchlesinger commentedon Oct 30, 2026
Active — worker
codex-cslib-pin-1726-20261030, resuming the coordinator-authorized documentation-memory fix on separate branchwork/cslib-pin-docs-memory-1726-codex-20261030from frozen29f56ae3. The four reviewed pin files will remain byte-identical. I will inspect the pinned Lake resource controls and add only a confirmed documentation-generation cap, preserving all validation, provenance and publishing options.Root has released exclusive ownership of the existing warm checkout back to me for serialized bootstrap/validation; no second dependency tree is involved. The current API retry remains the only live API run. The new workflow delta will receive focused outside-fleet review before the existing author branch is updated.
SamuelSchlesinger commentedon Oct 30, 2026
Active bounded follow-up — worker/session
codex-docgen-srcuri-1726-20261030owns upstream doc-gen4#434, branchwork/srcuri-job-dependency-codex-20261030, in independent source checkout/tmp/doc-gen4-srcuri-codex-20261030. This is the coordinator-delegated scheduling investigation after #1727's capped API run still exhausted memory.I found no existing upstream scheduling fix and read the README/current test conventions; there is no AGENTS.md, CONTRIBUTING.md or CODESTYLE.md in that repository. The next deliverable is a tiny Lake-only dependency-wait probe and, if warranted, the smallest nonblocking Job composition patch. No full API rerun, new large dependency tree, behind-manifest package edit or warm-checkout access is included. #1727 remains blocked; the probe must distinguish measured scheduling behavior from the unmeasured full-build root cause.
SamuelSchlesinger commentedon Oct 30, 2026
Awaiting review for the bounded upstream follow-up —
codex-docgen-srcuri-1726-20261030: draft doc-gen4#435 is frozen atcf840d8, linked to upstream issue #434. Its PR owns the patch, runnable Lake-only probe, measured thread comparison, cached-URI behavior change and validation limits. Upstream CI awaits maintainer approval of the fork contribution.This is a reviewable scheduling proposal, not proof that the full API OOM is fixed. #1727 remains blocked at its unchanged source head; no consumer pin, source behind a manifest, warm checkout or full API run was changed. All local probe processes are terminal.
Integration still needs independent review and an explicit source/provenance choice: a verified upstream matching-version tag under current documentation-pin rules, or a separately reviewed immutable snapshot and narrow policy exception. The current validator requires the generator's configured revision to match the Lean-version tag; a manifest-only repoint to this unmerged snapshot would not be an honest supported pin. The coordinator owns that choice and subsequent downstream validation.