Repository navigation
Conversation
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict. [Critical impact] The repository-side removals appear safe to merge. SummaryRemoves the public version-bump implementation and documents its ownership by the private
Reviews (2) · Last reviewed commit: "Move version-bump implementation and tes..." · Reviewed by Greptile |
|
Source review at exact head This head materially changes the earlier proposal. The final diff has six paths: a short operator pointer, deletion of the two hosted workflows, and removal of the old bump helper, its dedicated tests and CI summary renderer. The proposed public VM controller, its tests and systemd units are absent. My earlier controller analysis therefore does not become a change request against this head, or acceptance of its private replacement. The complete public deletion diff and a bounded reference audit of all 17 retained workflows, both bump skills, package initialization/configuration, Python README and Makefile found no remaining executable invocation of the removed helper or renderer. The dedicated test and its removed helper form the same retired dependency chain; normal Python test discovery remains intact. A small documentation follow-up remains: the version-bump-project skill's description still says it is used by the retired workflow. The private replacement's reported test results, draft-publication behavior and live service/checkpoint continuity remain owner evidence. They were not independently certified here, and I made no service, account, controller or branch changes. Removing the two workflows still needs the separate direct authorization required by current CONTRIBUTING.md. This review assignment supplies no exception to its workflow-change rule. The current main |
Retire the public version-bump implementation in favor of the private Lean VM controller in Vilin97/lean-pool-automation#4.
Remove the GitHub-hosted Mathlib Bump workflow, its obsolete Claude-auth canary, the old release/pin helper and CI report renderer, and their moved tests. Keep only a short operator pointer in
.github/BUMP_AUTOMATION.md. The runner, release tools, repair prompt, tests, installer and systemd units live inlean-pool-automation; no new VM code remains in the final public diff.The private controller uses full Git ancestry to fix branch resumption, selects cx accounts by most remaining quota, preserves repairs across failover/restarts, and runs the existing build and quality gates before publishing a draft content PR. Public proof sources and quality rules are unchanged.
Validation: 32 migration tests and 55 existing automation tests pass locally and on the Lean VM; the private package starts with system Python without a public engine. Ruff, shell syntax and systemd verification pass. The previous live cx model/tool smoke test exercised a failed first account followed by a successful second account.
Deployment retains the same VM service/timer, checkout, caches and pending v4.35.0 checkpoint. Both retired GitHub workflows remain administratively disabled to prevent duplicate controllers while this cleanup is reviewed.