Repository navigation
Own goal operations and modal results on their declared types - #1398
Merged
Merged
Conversation
There was a problem hiding this comment.
Copilot was unable to review this pull request because the user who requested the review has insufficient remaining quota. Try requesting a review at a lower effort level.
An organization owner can choose the repository organization as the billing source for reviews requested by members with a paid Copilot license. Learn about Copilot code review billing.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
2 coherent commits, 4 production files, +39/-31. Three goal operations are declared on the connection owner; two existing default methods leave
NoAgentConnectionfor that parent; one unused modal-dismissal text result and both UIControlledExecutiontype checks are deleted. No new class, adapter, cache, codec, registry, test controller or compatibility entrypoint.Paired Core API: OpenHCSDev/agent-comms#3844, 4fa21cafc5aec01f10201c49b16d13100446530a. Land Core first. The new Toad head consumes the new execution API and must not be installed against old Core. Both changes are the same goal-control overhaul, not independent acceptance claims.
The previously retained goal-control target had three findings: missing connection history/update contracts and
_modalinferred as permanentlyNone. The current target check reports 0 errors, rc0, one file checked. This is not a whole-project zero-debt claim or a new application qualification.Connection owns its goal contract
Before:
After:
GoalIdis the existing identity type for history reads.GoalSession.writecarries its awaited result type rather than abandoning the contract inside an untyped method.EditInteraction.applyis now checked too.The shared unsupported reason has one declaration on
AgentConnection; both writes raise the existingGoalRefused, which already composes expected refusal withValueError. This retains the old unsupported reason while using the existing UI refusal mechanism. The ACP request/decode bodies are unchanged.Counterexample that shaped the fix:
tests/model/test_session_observation_cancellation.py:17defines a read-onlyReadAgent(AgentBase). Adding abstract goal stubs would make that existing fixture uninstantiable. Concrete defaults on the actual connection parent preserve the family without three fake implementations or a mock exemption. No test was rewritten to tolerate the wrong structure.Modal result follows its actual reader
GoalSessionkeeps a truthfulReferenceType[ModalScreen[None]] | None, and itsmodal/presentcontracts say the same thing. Both current modal members support this contract:GoalDetailsderivesSourceModal/DismissibleScreen[None];GoalEditnow declaresDismissibleScreen[None].Deletion certificate, bounded to the owned Toad source/tests/tools callers:
66f47e41acheckpoint, GoalEdit constructor sites aregoal_interaction.py:116andtest_goal_owner_views.py:160,221. The toggle cleanup only shifts that unchanged production call; other native/Textual references only inspect the already-open editor.GoalSession.presentusesApp.push_screen(modal)with neither callback nor dismissal wait. The two direct test pushes likewise only await mounting. Textual's actualpush_screen/dismissresult contract was traced, not guessed from its name.await self.on_save(text.strip())before dismissal. That callback, exception handling, saving guard, draft retention and allfinallywork remain unchanged.self.dismiss(text.strip())result. It becomesself.dismiss(); no saved text is removed from the real save path.There is no generic modal manager or invariant-generic cast hiding an incompatible result.
Execution owns toggle behavior (53444/53446)
Before,
ToggleInteraction.visible/applyasked twice whether an already-held GoalExecution was ControlledExecution. This was old IMPL-3/MEMB-2: fact=availability and action; at=old goal_interaction.py:84,93; derive=base-method/subclass; by=Core GoalExecution/ControlledExecution. Paper1 §1 and Theorems4.6/4.7 apply; a UI switch was maintaining a family fact outside its declaration.The paired Core change puts
can_toggleandapply_toggleon those existing owners. The default execution calls unavailable feedback only; controlled execution awaits the existing goal-change receiver with its existing action. Default Pause caption moves unchanged to GoalExecution; Retry/Resume and action properties stay with their existing leaves. This UI now asks/invokes the family without recovering its type. Its initial/fallback caption derives from Core, deleting the second Pause spelling. The existing UI read-only visibility gate stays.Both unavailable feedback sites now use existing GoalSession's concrete
unavailablemethod; there is no new manager or fixture method. No wire, state, generation, input, permission, scheduling or constructor/base change.Paired proof artifacts:
toggle-{before,after}-map.json,toggle-production-consumers.txt,toggle-source-proof-v2.jsonin the same scratch directory. The relevant Core/Toad source corpus has28modules/544raw/542canonical classes before and after, zero parse omissions, two local declarations OPEN (Responses and Client). Dynamic/foreign/mutation cases remain OPEN. Exactly3paired files changed; all existing class bases and other annotated fields match.88existing method/function bodies are unchanged; four Core methods and one shared UI method are added. The caption declaration moved AST-identically. Core rebased onto5f8c3716: all28mapped input hashes remain identical (toggle-rebased-inputs.json), so no compiler/test rerun was used as reassurance. Authored exact patches, not automatic NRA movement/effect proof.After whole-production grep, ControlledExecution occurs only in its Core declaration and three base declarations: zero Toad references, zero UI type checks. Targeted mypy against TWO explicit owned source roots passes0/rc0, one source file checked; no application source overlay/import run. The first extension checker failed before mypy on its mistaken expectation for NRA's nested-function key; that original log remains
toggle-source-proof.log. Corrected v2 uses the actualchangekey; production was unchanged.Core#3844 authors eight parameterized dispatch/default regression examples, compiled but UNRUN. No extra pytest/native/frontend/install was launched. Necessary future combined cases are that new Core execution test and the existing Toad goal-control/readonly paths. Native09 is not transferred to this new pair.
Original connection/modal source proof (66f47e4)
Retained artifacts:
/home/ts/.cache/agent-scratch/pi-shell-colleague/retry-ui/.goal-contract-before-map.json, revision2b3f6ba4440f34893713d7858730142d3a0bf1a0, 38 modules, 395 raw / 392 canonical classes.goal-contract-after-map.json, same four-file working delta plus the two newly used Core refusal declaration modules: 40 modules, 442 raw / 439 canonical classes. The extra 47 classes are expanded dependency coverage, not production class growth. Exactly four mapped inputs changed; 34 original mapped inputs are hash-identical.parse_python_module_roots,ModuleSyntaxIndex,ClassFamilyIndexandbuild_source_indexown the source map, class census, lexical scopes and declaration/write/call/import events. Exact authored patches implement this bounded change; no automatic promotion/native-effect proof is claimed.OwnerReconnecting,ControlledProvider.serving.Handler, andRetainAction. Runtime imports, mutation, foreign factories and unknown extension callers remain OPEN, not zero debt.goal-contract-proof-v2.json: all four files compile; 115 common method bodies are AST-identical. The weakref constructor annotation changes its AST but its executable bytecode/constants are identical. The empty-history body moved unchanged; the unsupported reason is identical. Among common methods, only the editor's unused dismissal argument changes executable work. Separately, the moved unsupported write now raises the existingGoalRefusedinstead of bareValueError, as documented above.--follow-imports=silent --ignore-missing-imports --no-incremental src/toad/goal_interaction.py; success, rc0, one source file checked.goal-contract-proof.log; no type-check result was produced from it. The corrected source proof is a distinct artifact.git diff --checkpasses. Current open PR files were read before editing and refreshed before publication. Errors confirmed Keep queue actions on captured sources and original recipients #1389's shared connection files have no competing goal-contract hunk; its submission/queue repair remains separate. P918: relocate current ToAD consumers to Core nominal owners #1330's broad import sorting is not a competing implementation.Scope and remaining evidence
No pytest, local NRA gate, native/provider/frontend job or install was run for this overhaul. The initial typing proof followed commander53319; the added owner/consumer cleanup follows53444/53446 and has separate paired source proof above. The prior Core14/Toad12 and brace selections were not repeated. The accepted native09 Retry/refusal/DM result remains evidence for its original installed pair, not this unmerged head. New physical editor/button/warm-history/mobile acceptance is not claimed.
At the next independently necessary integration selection, the relevant existing behavior paths are
tests/textual/test_goal_owner_views.py,tests/native/test_native_goal_objective_edit.pyand the read-only observation construction intests/model/test_session_observation_cancellation.py. This is a risk handoff, not a request for per-head reassurance runs.Assumed: owned goal-modal callers define the supported dismissal-result domain; the existing Core
GoalRefusedcontract remains the expected-refusal envelope; the integration owner retains merge/install/live qualification. No store, generation, input, permission or scheduling data changes.