Redeliver an interrupted review comment, and close the issue on completion #76

2026-09-29T20:30:32Z

dev-agent commented

2026-09-29 20:30:32 +00:00

Fixes counterexamples 6 and 7, the last two from the Quint model (#73).

6: a crash mid-review lost the comment. The comment's cursor is saved before the work starts, so it's taken at most once. A restart in PR_OPEN then resumed quietly, and the comment was never answered.

pr.reviewing marks the comment from the moment the executor starts on it, and is cleared on every way the executor returns: pushed, stopped, escalated, or an exception reported to the operator.
It is deliberately not cleared in a finally: if the process dies, the mark must survive.
On boot in PR_OPEN with the mark set, the watch resumes just before that comment, and the operator is told: "restarted while answering review comment N on PR #M; answering it again".
The mark stays until the comment is answered, so a second crash can't lose it either.
So each comment is now taken at most once and answered at least once.

7: project complete left the plan issue open. It now closes the issue with "completed by ". As with abandon, the move to IDLE is saved first and a Gitea failure is reported, not fatal. The close logic is now a helper shared with abandon; the PR stays the operator's to merge.

Model:

it marks and redelivers, and project complete closes the issue;
review_comments_answered now means answered, being answered, or marked for redelivery, i.e. never silently dropped;
scenarios 6 and 7 flipped, and scenario 6 continues through the redelivery to the answer;
a mutant model without redelivery fails scenario 6;
all eight properties together held over 300,000 random traces and under Apalache's exhaustive check to depth 8.

Tests:

all seven counterexample reproductions now pass as regular tests; no xfail remains;
test 6 now requires both the notice and the redelivered answer;
new cases: a second crash while answering again still redelivers; an executor error counts as answered and isn't redelivered (a guard that passes on main too); project complete with Gitea down still completes and reports it.

499 unit tests and the integration suite (19 passed, 7 skipped) pass; lint and format clean.

🤖 Generated with Claude Code

https://claude.ai/code/session_01PPQ14L3LikyefCMFBqEbKE

Fixes counterexamples 6 and 7, the last two from the Quint model (#73). **6: a crash mid-review lost the comment.** The comment's cursor is saved before the work starts, so it's taken at most once. A restart in `PR_OPEN` then resumed quietly, and the comment was never answered. - `pr.reviewing` marks the comment from the moment the executor starts on it, and is cleared on **every way the executor returns**: pushed, stopped, escalated, or an exception reported to the operator. - It is deliberately **not** cleared in a `finally`: if the process dies, the mark must survive. - On boot in `PR_OPEN` with the mark set, the watch resumes just before that comment, and the operator is told: "restarted while answering review comment N on PR #M; answering it again". - The mark stays until the comment is answered, so a second crash can't lose it either. - So each comment is now taken at most once and answered at least once. **7: `project complete` left the plan issue open.** It now closes the issue with "completed by <operator>". As with `abandon`, the move to `IDLE` is saved first and a Gitea failure is reported, not fatal. The close logic is now a helper shared with `abandon`; the PR stays the operator's to merge. **Model:** - it marks and redelivers, and `project complete` closes the issue; - `review_comments_answered` now means answered, being answered, or marked for redelivery, i.e. never silently dropped; - scenarios 6 and 7 flipped, and scenario 6 continues through the redelivery to the answer; - a mutant model without redelivery fails scenario 6; - **all eight properties together** held over 300,000 random traces and under Apalache's exhaustive check to depth 8. **Tests:** - all seven counterexample reproductions now pass as regular tests; **no `xfail` remains**; - test 6 now requires both the notice and the redelivered answer; - new cases: a second crash while answering again still redelivers; an executor error counts as answered and isn't redelivered (a guard that passes on `main` too); `project complete` with Gitea down still completes and reports it. 499 unit tests and the integration suite (19 passed, 7 skipped) pass; lint and format clean. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01PPQ14L3LikyefCMFBqEbKE

dev-agent added 1 commit 2026-09-29 20:30:33 +00:00

Redeliver an interrupted review comment, and close the issue on completion

CI / checks (push) Skipped

CI / checks (pull_request) Successful in 1m16s

Details

848bd9f122

Fixes counterexamples 6 and 7 from specs/orchestrator.qnt, the last two.

6. A crash while the executor answered a review comment lost it: its
   cursor is saved before the work (at most once), and a restart in
   PR_OPEN resumed quietly. Now pr.reviewing marks the comment until
   the executor returns (every way it returns, but not a crash), and
   boot resumes the watch just before it, with a notice. The mark stays
   until it is answered, so a second crash cannot lose it either.
7. 'project complete' left the plan issue open. It now closes it with a
   note, after IDLE is saved, as abandon does (shared helper).

The model marks and redelivers, and closes the issue; scenarios 6 and 7
now expect their properties to hold. A mutant without redelivery fails
scenario 6. All eight properties held together over 300,000 traces.
No xfail reproductions remain.

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:37:01 +00:00

dongar merged commit d302d337d6 into main

2026-09-29 20:37:04 +00:00

dongar deleted branch redeliver-review-and-close-issue

2026-09-29 20:37:04 +00:00

Sign in to join this conversation.

2 Participants

Notifications

Due Date

No due date set.

Dependencies

No dependencies set.

Reference: dev/nisse#76