Skip to content

fix: keep watch progress during reconstructed admission - #58

Merged
nybarius merged 4 commits into
mainfrom
work/predecessor-reland-check-20260930
Oct 20, 2026
Merged

nybarius merged 4 commits into
mainfrom
work/predecessor-reland-check-20260930

Conversation

@nybarius

Copy link
Copy Markdown
Owner

What this changes and why

A bounded daemon tick can receive a re-land refusal and then run the rebuilt head's admission synchronously on the controller. That second read bypasses the existing in-flight scheduling path: an unrelated admission may already have completed, yet its merge waits for the reconstructed read. The reproduction holds that read open and shows the ready head waiting beyond a 50 ms tick budget.

Keep tree/history reconstruction and the original tree and history checks on the controller. Submit only the rebuilt admission through the same admission executor, memory guard and PR slot. Later ticks retain the actual candidate head and base together with the original PR row, class, tree, ref and inputs. The controller receives its result through the original acceptance, error and watched-hold logic. Draining retains both source identities and performs no publication.

Before publishing an accepted deferred result, reread the original PR and require the same head SHA/ref, the configured base, open state, draft: false, and an observed label list without the hold label. Missing, malformed, changed or opted-out sources are retried. A stopped train blocks later publication in that round. An unrelated main advance does not discard the accepted successor: the resulting PR still needs ordinary admission and the current merge gate.

The unbounded one-shot path keeps its original synchronous behavior. Admission capacity, worker ceilings, the shared memory guard, gate rules and original test assertions remain unchanged. RealGitHub.pull adds only the observed base ref, leaving missing data unknown.

Tests

  • RED controls executed against the exact original production source. The ready head waited behind the rebuilt read, and stale or unread original PRs could still be superseded. All ten original rebuilt-admission checks remained green. Additional controls cover pending-slot identity, repeated discovery, drain, original watched holds, main-only advancement, source ref changes, malformed readiness, raw unread API objects and a real stopped Train result.
  • Full original make test: 452 tests passed in 20.576 s on Python 3.12.14, including the denylist, proof-map checks and local end-to-end demo. All source bytes were unchanged after execution. Independent code review checked source/candidate separation, preserved acceptance logic, original memory/slot use and drain behavior.
  • Original rules.py, reconstruction code and Lean statements reviewed unchanged. reland_tree and reland_gate retain their tree-value meaning; they do not substitute for the rebuilt head's original admission or prove executor scheduling.
  • Full make check / required CI: the original make proofs and make docker targets were attempted and stopped immediately because lake and docker are absent. Local lean/elan and a container runtime are also unavailable; no toolchain or image downloads were attempted. The existing Python 3.11/3.12/3.13, Lean build/axiom and container jobs still need to pass.

Anything reviewers should look at closely

The candidate must stay out of the generic original-PR admission path. The in-flight row names the rebuilt commit, while publication checks and held memory name the original PR. Discovery's seen key uses that original head, avoiding a second read of the same source when a deferred slot refills. The fresh PR read adds no new external command or command interpolation.

The local result establishes the code and test behavior. Installation on a live owner, native receipts and sustained merge throughput remain separate observations.

Source

Continues the existing owner branch of merged #22 for this newly demonstrated scheduling defect. No equivalent open pull request exists. Verified head 2123846f6448a3a6d431fdf4c9662f9282c42192, tree 6e601c88ef9e27d727c1796d381ed5a5d85a85bd, based on d5ef9cbd81b5d85763f010b63a86c6704eb47c0f. Test-only commits precede the production change.

Use the original daemon, repository and gate fakes with event-controlled reads. Keep a reconstructed admission pending while a separate original admission has completed successfully, and require the ready head to reach the existing merge path without waiting for that reconstruction.

Against the current daemon the ten original re-land admission checks pass and the new progress assertion fails. No rebuilt branch or pull request is published before its original acceptance. The standard-library runner reproduces the failure without extra dependencies.
A rebuilt admission can finish after its original head moves, closes, becomes draft or held, changes its target branch, or cannot be read. Exercise each case with the original daemon and an event-controlled admission and require no branch or pull-request publication from the obsolete result.

All six new cases fail against the unchanged original daemon. The ten original admission checks still pass, and the pending-rebuild progress regression still fails.
Reproduce controller blocking, stopped-round effects, original-source changes,
and unread readiness while retaining the original re-land acceptance checks.
Scope the new progress observation to the rebuilt pull request so an
independent accepted merge remains permitted.

Original-source RED: 19 methods with 20 expected failures; the original
10 re-land checks and main-only advance and held-watch controls pass.
Corrected RED receipt SHA256: 68982ad7401c67860af98656d1ea9062b1fb7dc6108462654a657a009db5f8a3
Run bounded re-land admission through the existing owned slot and executor.
Retain both the original pull request and reconstructed checked source in
continuation and drain receipts. Finish on the controller, preserving the
original acceptance checks and requiring fresh original-source readiness
before publishing. Leave one-shot reads and resource ceilings unchanged.

Verified: original make test, 452 tests passed in 20.576s; source unchanged.
Focused original and lifecycle checks: 86 tests passed.
Tests-only RED precedes this change in ecdf06c.
@nybarius
nybarius merged commit a043fcd into main Oct 20, 2026
12 of 13 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant