Adopt an already-published PR instead of publishing again #75

2026-09-29T19:58:20Z

dev-agent commented

2026-09-29 19:58:20 +00:00

Fixes counterexample 5 from the Quint model (#73).

The bug: a crash after the PR was opened, but before PR_OPEN was recorded, left the agent in EXECUTING. The restart question's continue and then start published again. Gitea refused a second PR, and there was no path back to PR_OPEN. On the live run the executor model happened to notice the existing work, but recovery shouldn't depend on that (A4: structural, not advisory).

Changes

Boot adopts a published PR (A3 step 4, control.py). Restarting in EXECUTING, if Gitea shows this milestone's PR open, the agent records it, watches it from the first comment (nothing watched it before), and resumes in PR_OPEN with "restarted after milestone 1 was published: PR #N is open". If Gitea can't say, or the PR is closed, the restart question is asked as before.
Publishing is idempotent (publish.py). After pushing, an open PR for the branch is adopted (the push has updated it) instead of opening a second one. This also covers a PR that Gitea opened but whose response was lost. published_pull_request() is the shared lookup; a closed PR doesn't count, since the operator closed it.
Model:
- adoption on boot and when publishing, plus the lost-response outcome;
- scenario 5 flipped, and a new scenario 5b (response lost, then a retry adopts the PR);
- one_pr_per_milestone now counts the PRs Gitea opened per milestone. It used to be a flag the fixed model could never set, which would have made it pass trivially. A mutant model without adoption fails 5b, so the property really checks adoption.
- one_pr_per_milestone, no_stranding, await_input_has_a_question, execution_needs_approval and approval_only_of_what_was_seen each held over 200,000 traces.

Tests:

counterexample 5 loses its xfail and now also checks that boot announces the PR;
publishing again adopts the open PR, and it's updated rather than duplicated;
a closed PR isn't adopted;
boot with Gitea unreachable asks the restart question (a guard: unchanged behaviour).

The three new behaviour tests fail on main. 494 unit tests and the integration suite pass; lint and format clean. Counterexamples 6 and 7 remain xfail.

🤖 Generated with Claude Code

https://claude.ai/code/session_01PPQ14L3LikyefCMFBqEbKE

Fixes counterexample 5 from the Quint model (#73). **The bug:** a crash after the PR was opened, but before `PR_OPEN` was recorded, left the agent in `EXECUTING`. The restart question's `continue` and then `start` published again. Gitea refused a second PR, and there was no path back to `PR_OPEN`. On the live run the executor model happened to notice the existing work, but recovery shouldn't depend on that (A4: structural, not advisory). **Changes** - **Boot adopts a published PR** (A3 step 4, `control.py`). Restarting in `EXECUTING`, if Gitea shows this milestone's PR **open**, the agent records it, watches it from the first comment (nothing watched it before), and resumes in `PR_OPEN` with "restarted after milestone 1 was published: PR #N is open". If Gitea can't say, or the PR is closed, the restart question is asked as before. - **Publishing is idempotent** (`publish.py`). After pushing, an open PR for the branch is adopted (the push has updated it) instead of opening a second one. This also covers a PR that Gitea opened but whose response was lost. `published_pull_request()` is the shared lookup; a closed PR doesn't count, since the operator closed it. - **Model:** - adoption on boot and when publishing, plus the lost-response outcome; - scenario 5 flipped, and a new scenario 5b (response lost, then a retry adopts the PR); - `one_pr_per_milestone` now **counts the PRs Gitea opened** per milestone. It used to be a flag the fixed model could never set, which would have made it pass trivially. A mutant model without adoption fails 5b, so the property really checks adoption. - `one_pr_per_milestone`, `no_stranding`, `await_input_has_a_question`, `execution_needs_approval` and `approval_only_of_what_was_seen` each held over 200,000 traces. **Tests:** - counterexample 5 loses its `xfail` and now also checks that boot announces the PR; - publishing again adopts the open PR, and it's updated rather than duplicated; - a closed PR isn't adopted; - boot with Gitea unreachable asks the restart question (a guard: unchanged behaviour). The three new behaviour tests fail on `main`. 494 unit tests and the integration suite pass; lint and format clean. Counterexamples 6 and 7 remain `xfail`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01PPQ14L3LikyefCMFBqEbKE

dev-agent added 1 commit 2026-09-29 19:58:20 +00:00

Adopt an already-published PR instead of publishing again

CI / checks (push) Skipped

CI / checks (pull_request) Successful in 1m12s

Details

8bd1ac0fa2

Fixes counterexample 5 from specs/orchestrator.qnt. A crash after the
PR was opened but before PR_OPEN was recorded left the agent in
EXECUTING; the restart question's 'continue' and 'start' then published
again, Gitea refused a second PR, and there was no way back to PR_OPEN.
On the live run the executor model happened to notice the existing
work; recovery must not depend on that.

- Boot (A3 step 4): in EXECUTING, if Gitea shows the milestone's PR
  open, adopt it, watch it from the start, and resume in PR_OPEN with a
  notice. Gitea unreachable or the PR closed: the restart question, as
  before.
- MilestonePublisher.publish is idempotent: after pushing, an open PR
  for the branch is adopted (and so updated) rather than a second one
  opened. This also covers a PR opened whose response was lost.
- The model adopts too, gains the lost-response outcome, and now counts
  PRs opened per milestone (one_pr_per_milestone was a flag the fixed
  model could never set). A mutant without adoption fails the new
  scenario; the properties held over 200,000 traces each.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PPQ14L3LikyefCMFBqEbKE

dongar approved these changes

2026-09-29 20:14:42 +00:00

dongar merged commit 83a4bd72b5 into main

2026-09-29 20:14:47 +00:00

dongar deleted branch adopt-published-pr

2026-09-29 20:14:47 +00:00

Sign in to join this conversation.

2 Participants

Notifications

Due Date

No due date set.

Dependencies

No dependencies set.

Reference: dev/nisse#75