Close five gaps the loop model found
CI / checks (push) Skipped
CI / checks (pull_request) Successful in 1m18s
CI / checks (push) Skipped
CI / checks (pull_request) Successful in 1m18s
- abandon closes the item's open PRs - a PR the operator closed is an answer, never reopened by a retry - a review fix for a PR that merged meanwhile goes out as a new PR - redoing a milestone after a closed PR gets a new branch and PR - a record issue carries its work item's ID from creation Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PPQ14L3LikyefCMFBqEbKE
This commit is contained in:
1 parent
5839091d65
commit
8c38444b88
1 file changed
+16
-8
+16
-8
@@ -199,8 +199,8 @@ again after a restart), permissions (L3), and work in progress as intents (L8).
|
||||
else is a bug, which the model checker (`specs/`) guards against.
|
||||
- **`stop` works in every state:** it ends the current turn or delegation at the
|
||||
next tool boundary, unmounts elevated credentials, and asks what next.
|
||||
- **`abandon` ends a work item** from any waiting point, closing its record with a
|
||||
note and aborting its unresolved intents.
|
||||
- **`abandon` ends a work item** from any waiting point, closing its record and
|
||||
any open PRs with a note and aborting its unresolved intents.
|
||||
- **Every action passes through the three layers** (P4).
|
||||
|
||||
### L3. Authority: scope and approvals
|
||||
@@ -379,7 +379,8 @@ migration hook.
|
||||
- **Before any external side effect, record an intent;** after it, commit it.
|
||||
- **Every external effect is idempotent against external truth:** re-running an
|
||||
interrupted step detects and adopts what already happened (e.g. an open PR for
|
||||
the branch).
|
||||
the branch). What the operator has since undone is an answer, not a gap to
|
||||
fill: a PR they closed is reported, never opened again.
|
||||
- **Intake is taken at most once and answered at least once:** a durable cursor per
|
||||
external thread; an item being answered stays marked until done and is
|
||||
redelivered after a crash; comments the agent can't act on yet aren't consumed.
|
||||
@@ -397,8 +398,9 @@ migration hook.
|
||||
out and its approval hasn't expired (O2); anything else is reported with what is
|
||||
known, and the operator chooses. Never a blind resume.
|
||||
|
||||
**Verification:** these rules are checked by a formal model (`specs/`, Quint) over
|
||||
interleavings of messages, comments, outcomes and crashes. Each counterexample is
|
||||
**Verification:** these rules, and the loop's (L1, L2, D1, D4, D5), are checked by
|
||||
formal models (`specs/`, Quint) over interleavings of messages, comments, outcomes
|
||||
and crashes. Each counterexample is
|
||||
reproduced against the real code before it is fixed.
|
||||
|
||||
### L9. Models, roles and helpers
|
||||
@@ -551,8 +553,10 @@ Work arrives as Gitea issues or conversation, and leaves as reviewed PRs.
|
||||
- **Unassigned issues are backlog,** never work, though the agent will discuss them.
|
||||
- **Open Gitea dependencies make an issue blocked** (L1).
|
||||
- **Work that starts in conversation gets a record:** the agent opens an issue,
|
||||
assigned to itself and linked to the item. Intake ignores issues already linked,
|
||||
so nothing is picked up twice. This is the only time the agent assigns itself.
|
||||
assigned to itself, that carries the work item's ID from the moment it is
|
||||
created. Intake ignores any issue carrying an ID, so a record is never taken for
|
||||
new work, even before the agent has stored the link. This is the only time the
|
||||
agent assigns itself.
|
||||
|
||||
**Starting an item.** The agent reads the project's documents (D2), then
|
||||
**restates its understanding** in the item's thread: what it takes the request to
|
||||
@@ -654,7 +658,8 @@ Installing on any other host is class 3.
|
||||
branch only after the previous PR has merged (read from Gitea). Meanwhile the item
|
||||
waits on the operator and the agent does other work. A review comment makes the
|
||||
item ready (D5); a PR closed without merging makes it ready with that fact, and the
|
||||
agent asks what next.
|
||||
agent asks what next. Redoing the milestone gets a new branch and PR, and the
|
||||
merge rule still applies to it.
|
||||
- **Parking pushes the item's branch,** so another item on the same project starts
|
||||
fresh and this one resumes from its branch.
|
||||
- **Publish only the work:** what the agent changed, counted from where the
|
||||
@@ -677,6 +682,9 @@ Installing on any other host is class 3.
|
||||
- **Operator comments on a PR** (conversation and inline) are instructions; the
|
||||
agent answers with commits to the same PR, replying where the comment was made.
|
||||
Intake is as in L8.
|
||||
- **The PR may have moved on meanwhile.** After pushing a fix, the agent checks the
|
||||
PR: if it merged before the fix landed, the fix goes out as a new PR; if it was
|
||||
closed, the agent says so and asks.
|
||||
- **Merging follows the trust dial** (L3). Today the operator merges. If the dial
|
||||
lets the agent merge its own PRs once checks pass, branch protection must require
|
||||
an approval the agent's account can't give, so Gitea enforces the rule.
|
||||
|
||||
Reference in new issue
Block a user