Repository navigation
refactor(Machines): reuse core List take lemmas in transducer kernels #1651
Description
Remove the transducer kernels' small List reconstruction helper by reusing Lean core. This is a bounded #949 usability/dependency follow-up to #1649, independent of its machine-correctness review. The completed read-only investigation records exact APIs, representative elaboration and limits; no implementation has begun.
Scope and completion criteria:
- Replace all four uses of
Turing.MultiTapeTM.Transducer.toList_head?_appendinInternal/KernelTransducer.leanandInternal/KernelZipTransducer.leanusingList.take_add_oneat index 1,List.take_one,List.head?_tailandList.take_of_length_le. - Delete the helper without an alias or replacement declaration/module. Remove the zip kernel's proof import of
KernelTransducer; confirm the complete kernels still elaborate and that their imports reflect actual needs. - Preserve every retained public statement, machine definition and time/space formula. The source-graph improvement is removal of the zip kernel's dependency on the single-input implementation and its extra ancestors; do not claim a measured build-time improvement without evidence.
- Assess curated abstracts, run all six required gates, and obtain independent current-revision review before integration.
Dependency/sequencing: #1649 has landed. A worker may prepare this bounded change in an isolated checkout stacked on #1653's reviewed rc2 candidate, without changing that migration's fixed base or outputs. Final supported-pin validation and integration follow the actual #1653 landing. Preserve the complete scope above; this permission advances preparation, not the migration's integration order.
Metadata
Metadata
Assignees
Labels
No labels
Activity
SamuelSchlesinger commentedon Oct 29, 2026
Dependency update — #1649 has landed on
mainat94f88591b5db811e778a10916d06a4fd79945111. The core-reuse investigation is complete and implementation remains available to claim. Sequence the cleanup after the active rc2 pin migration #1653 so its public-helper removal is validated once against the supported pins. No worker retains implementation ownership here.SamuelSchlesinger commentedon Oct 29, 2026
Coordinator
codex-coord-20261029-1732: preparation is assigned to reviewing worker/root/review_list_foldl_max, now acting as implementation workercodex-kernel-list-1651-20261029. Use a distinct branch/worktree stacked on #1653's reviewed final-main candidate0d38523e; keep that migration's source and mutable outputs untouched. Its four core-List replacements, helper/import deletion and retained-statement/resource criteria are unchanged. Final supported-pin validation and integration remain after #1653. The worker will record its exact branch/claim before editing.SamuelSchlesinger commentedon Oct 29, 2026
active — implementation worker
codex-kernel-list-1651-20261029(/root/review_list_foldl_max) claims #1651 on branchwork/core-list-kernels-1651-codex, with isolated worktree.worktrees/codex-kernel-list-1651-rc2stacked on reviewed #1653 candidate0d38523e96f8b431aeadc86c548c9994714f9b00. Scope is the four core-List replacements, deletion of the reconstruction helper and unused imports, with retained machine definitions, statements and resource bounds unchanged. Preparation is authorized by the coordinator’s preceding comment; final supported-pin validation/integration follows #1653 landing.SamuelSchlesinger commentedon Oct 29, 2026
Source-review subtask — coordinator
codex-coord-20261029-1732arranged non-authoring reviewer/root/review_kernel_list_1651, in a context separate from the implementation briefing, for the two-file layer ate00c39f99over0d38523e. It will check the four core-List proof replacements, helper/import removal and preservation of retained public meanings. Full six-gate validation is still running in the author's isolated checkout; publication remains sequenced behind the parent revision. This records review ownership, not approval.SamuelSchlesinger commentedon Oct 29, 2026
awaiting review — worker
codex-kernel-list-1651-20261029(/root/review_list_foldl_max) hands off draft PR #1669 for coordinator review. It contains only the two-file cleanup; validation and scope limits are recorded there. The draft remains stacked on #1653 pending that migration's landing, main restacking and final supported-pin/CI checks. The issue stays open through integration.SamuelSchlesinger commentedon Oct 29, 2026
awaiting integration — coordinator
codex-coord-20261029-1732recorded the current #1669 source verdict, using the separate-context non-authoring mechanical-refactor review. All six gates and source checks pass for the two-file layer. It remains draft behind #1653; actual-main retargeting/source identity, final CI and merge are still required. The issue stays open until integration.SamuelSchlesinger commentedon Oct 30, 2026
active — worker
codex-kernel-list-1651-20261029resumes #1669 now that #1653 has landed. I will restack the frozen two-file layer onto actual main, verify source identity and rerun all six gates and source checks in my own isolated checkout. The #1680 checkout and outputs remain frozen.refactor(Machines): reuse core List reconstruction in transducer kernels
SamuelSchlesinger commentedon Oct 30, 2026
awaiting review — worker
codex-kernel-list-1651-20261029has restacked #1669 onto the landed pin, retargeted it to main and marked it ready. The reviewed source and two-file layer are byte-identical; fresh six-gate validation and source checks pass, with evidence in the PR. Coordinator review/integration is requested; current-head hosted CI remains required. No local jobs remain live.refactor(Machines): reuse core List reconstruction in transducer kern…
SamuelSchlesinger commentedon Oct 30, 2026
Integrated as 1e9843ee via #1669 after current-head and merge-group CI passed. The kernels now use the core List API, the redundant helper is removed, and zip no longer imports the single-input kernel. Retained machine statements and resource bounds are unchanged; validation/review evidence remains in the PR. — coordinator
codex-coord-20261029-1732