dongarandClaude Opus 5.5
a921b73d34
M4.3's block, with new triggers and a way out. A VM out of reach at the check before a run, in a run (which ends there: the driver, a toolchain step and a requested step), or while preparing the workspace blocks every project on it; the item stays ready, waiting on no one. On the intake round it is tried again every tuning.build_vm.retry_s (300), and once it answers it must still answer settle_s (180) later; then the work a lost run left there is parked (pushed), the VM unblocked, and that said once. A changed host key, at the check or on a retry, blocks the VM too, until the operator's `vm ready`, which trusts the new key: `trust new host key` is retired, and the message says it's a key problem that may be an impersonation. Questions are answered while a VM is blocked, without it. Starting the agent with a VM down no longer fails. The walk breaks the VM's SSH, now or partway through a run, and checks that no model works on a VM that is down; loop.qnt models the VM going and coming back (unblocked_only_when_up). Together they found: a lost run's work set aside by the next item there; a question left behind a block; a lost VM swallowed while the toolchain step checked or recorded it; and a remark waiting to be answered that outlived its PR's merge. All fixed. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J5Utyfzw7gF7UhjRDEtjTk
101 lines
4.4 KiB
Plaintext
101 lines
4.4 KiB
Plaintext
// Counterexamples found in loop.qnt, written out as short traces. Each was a
|
|
// gap in docs/Architecture.md; the model now has the proposed fix (marked
|
|
// FIX n in loop.qnt), and each trace checks the fixed behaviour.
|
|
//
|
|
// Run: quint test specs/loop_scenarios.qnt (runs every *Test)
|
|
module loop_scenarios {
|
|
import loop.* from "./loop"
|
|
|
|
// An assigned issue, restated, a go-ahead, milestone 1 under way.
|
|
action toWorking = init
|
|
.then(assignIssue(1)).then(intake(1, "A", false))
|
|
.then(activate(1)).then(restate(false))
|
|
.then(say(1, "go")).then(handleMsg)
|
|
.then(startMilestone)
|
|
|
|
// ...and published: its PR is open and the item waits for the merge.
|
|
action toPrOpen = toWorking
|
|
.then(finishMilestone)
|
|
.then(publishStep(false)).then(publishStep(false)).then(publishStep(false))
|
|
|
|
// 1. Abandoning an item left its open PR open: L2 closed the record and
|
|
// aborted intents, but said nothing about PRs. Fixed: abandon closes
|
|
// the item's open PRs with a note.
|
|
run abandonClosesTheOpenPrTest =
|
|
toPrOpen
|
|
.then(park)
|
|
.then(say(1, "abandon")).then(handleMsg)
|
|
.expect(closed_items_leave_nothing and s.prs.get(prKey(1, 1, 0)) == "closed")
|
|
|
|
// 2. Gitea opened the PR but the response was lost, so the agent never
|
|
// knew. The operator closed that PR; the agent's retry only adopted
|
|
// *open* PRs, so it opened a second one over the operator's close.
|
|
// Fixed: a closed PR on the branch is an answer: report it and ask.
|
|
run retryNeverReopensAClosedPrTest =
|
|
toWorking
|
|
.then(finishMilestone)
|
|
.then(publishStep(false))
|
|
.then(publishStep(true)) // opened, response lost
|
|
.then(prAct(1, "closed")) // the operator closes it
|
|
.then(finishMilestone) // the agent retries
|
|
.then(publishStep(false)).then(publishStep(false))
|
|
.expect(one_pr_per_milestone and itm(s, 1).waitFor == "answer")
|
|
|
|
// 3. A review comment made the item ready; the operator merged the PR
|
|
// before the fix was pushed, so the fix went to a merged branch and
|
|
// never reached main. Fixed: a fix for a PR that merged meanwhile goes
|
|
// out as a new PR (and one for a closed PR is reported).
|
|
run reviewFixAfterMergeGetsANewPrTest =
|
|
toPrOpen
|
|
.then(prAct(1, "comment")).then(observe(1))
|
|
.then(prAct(1, "merged"))
|
|
.then(answerReview)
|
|
.expect(review_fixes_land and itm(s, 1).stage == "working" and itm(s, 1).attempt == 1)
|
|
|
|
// 4. After a PR closed unmerged and the operator answered, the next
|
|
// milestone could start with the closed one never merged. Fixed: a
|
|
// redo is the same milestone on a new branch and PR.
|
|
run closedPrRedoesTheSameMilestoneTest =
|
|
toPrOpen
|
|
.then(prAct(1, "closed")).then(observe(1))
|
|
.then(say(1, "answer")).then(handleMsg)
|
|
.then(startMilestone)
|
|
.expect(milestone_after_merge and itm(s, 1).ms == 1 and itm(s, 1).attempt == 1)
|
|
|
|
// 5. Work begun in conversation gets a record issue, assigned to the
|
|
// agent. Opening it and storing the link were two steps, and intake
|
|
// could take the assigned, unlinked issue for new work in between.
|
|
// Fixed: the issue carries its work item's ID from creation.
|
|
run recordIssueIsNeverTakenForNewWorkTest =
|
|
init
|
|
.then(converse("A")).then(activate(1)).then(restate(false))
|
|
.then(say(1, "go")).then(handleMsg)
|
|
.then(createRecord)
|
|
.expect(s.issues.get(99).linked == 1)
|
|
.then(linkRecord)
|
|
.expect(one_item_per_issue and itm(s, 1).issue == 99)
|
|
|
|
// M4.3: a build VM the driver finds broken blocks its project; nothing is
|
|
// taken up on it until the operator says `vm ready`, then work goes on.
|
|
run aBrokenVmBlocksUntilReadyTest =
|
|
init
|
|
.then(assignIssue(1)).then(intake(1, "A", false))
|
|
.then(activate(1)).then(requestReimage)
|
|
.expect(s.vmBlocked.contains("A") and s.active == 0)
|
|
.then(vmReady("A"))
|
|
.then(activate(1))
|
|
.expect(blocked_vm_runs_nothing and s.active == 1)
|
|
|
|
// #137: an out-of-reach VM found at the check blocks its project; a probe
|
|
// can't unblock it while it's down, and does once it's back.
|
|
run anUnreachableVmBlocksUntilItAnswersTest =
|
|
init
|
|
.then(assignIssue(1)).then(intake(1, "A", false))
|
|
.then(goDown("A"))
|
|
.then(activate(1))
|
|
.expect(s.vmUnreachable.contains("A") and s.active == 0)
|
|
.then(comeBack("A")).then(probe("A"))
|
|
.then(activate(1))
|
|
.expect(all_properties and s.active == 1)
|
|
}
|