docs: destination-capture revision 2 --- full matrix, preservation suite, coherence
Three review findings. Q#DC-2 parameterization was incomplete. Revision 1 said only "skip the stale-buffer check for a non-replacing continuation", but a panel result does not depend on the captured document window at all: it does not replace that window buffer (check 3), does not occupy it (check 4), and does not need that specific window to exist (check 2). Retaining any of the three can reject git.status for an unrelated document-window change; dropping them without an explicit profile risks weakening document replacement. The question now carries a four-row matrix with two profiles, and check 1 --- the requesting frontend still has a layout --- is the entire panel profile. That has a consequence the framing now states rather than leaving to be discovered: if the panel profile needs only the frontend, a frontend with no document window can still host a panel, so Q#DC-4 return-nil rule is right for the document profile and possibly wrong for the panel one. Settled as part of answering Q#DC-2, not after it. tests/journey_acceptance.rs joins dired as a named preservation suite and stop signal. It carries 27 commit_to references across nine named pins --- forged destination, scope-and-restore on normal return and on raise, await refusal, delivery to the requesting frontend, the declining-listener redirect guard, and two already named preservation_* --- and Journey Stage 1a own framing treats it as a required gate. A lane that generalizes its substrate does not get to relax that. The stop signal now covers both suites: a suite edited to accommodate the change under test has stopped being evidence. The coherence-impact section was missing entirely. CLAUDE.md and COHERENCE.md section 25 both require one for coherence-affecting work, and this lane qualifies twice over --- new Lua API surface, and a generalization of a Journey substrate. Section 16 is the section it serves. Journey steps: none added, one protected. Islands, config registry: none. Section 9: neutral, and stated precisely, because knowing which frontend a result belongs to is NOT knowing who asked for it --- that is the worker-identity arc and the two should not be conflated just because both concern async continuations. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016bqGA6s9tTUFzYpbeW3tai
This commit is contained in:
parent
71ef951535
commit
91e4e514a1
|
|
@ -275,8 +275,15 @@ from #171 and #215.
|
||||||
authoritative tip** — the ref, not a SHA. Recover with
|
authoritative tip** — the ref, not a SHA. Recover with
|
||||||
`git fetch githubsucks && git checkout destination-capture`.
|
`git fetch githubsucks && git checkout destination-capture`.
|
||||||
|
|
||||||
- **Framing `docs/destination-capture-framing.md`, revision 1**, in
|
- **Framing `docs/destination-capture-framing.md`, revision 2**, in
|
||||||
review.
|
review. Revision 2 took three findings: Q#DC-2's parameterization was
|
||||||
|
incomplete (a panel depends on **none** of checks 2–4, not just check
|
||||||
|
3, so the question now carries a full preflight matrix with every
|
||||||
|
omission testable); `tests/journey_acceptance.rs` joins dired as a
|
||||||
|
**preservation suite and stop signal**, since it holds the
|
||||||
|
`commit_to` scope, forged-userdata, preflight and restoration pins
|
||||||
|
this lane generalizes; and the **coherence-impact section was missing
|
||||||
|
entirely**, which `CLAUDE.md` and `COHERENCE.md` §25 both require.
|
||||||
- **A PREREQUISITE LANE. PR #227 (git Stage 1) blocks on it.** #227's
|
- **A PREREQUISITE LANE. PR #227 (git Stage 1) blocks on it.** #227's
|
||||||
P1a review finding is why it exists: git's async completions mutate
|
P1a review finding is why it exists: git's async completions mutate
|
||||||
and display UI without capturing the initiating frontend
|
and display UI without capturing the initiating frontend
|
||||||
|
|
|
||||||
|
|
@ -1,8 +1,21 @@
|
||||||
# A destination capture any async continuation can use
|
# A destination capture any async continuation can use
|
||||||
|
|
||||||
**Status: framing pass, revision 1. Pre-implementation. Awaiting
|
**Status: framing pass, revision 2. Pre-implementation. Awaiting
|
||||||
approval.**
|
approval.**
|
||||||
|
|
||||||
|
**Revision 2 takes three review findings.** Q#DC-2's parameterization
|
||||||
|
was **incomplete** — a panel result does not depend on the captured
|
||||||
|
document window being live or non-dedicated either, not just on its
|
||||||
|
buffer, so the question now carries a full **preflight matrix** with
|
||||||
|
every omission testable. `tests/journey_acceptance.rs` joins dired as a
|
||||||
|
named **preservation suite and stop signal**; it carries the
|
||||||
|
`commit_to` scope, forged-userdata, preflight and restoration pins this
|
||||||
|
lane generalizes, and Journey Stage 1a's framing treats it as a
|
||||||
|
required gate. And **§5 (coherence impact) was missing entirely**,
|
||||||
|
which `CLAUDE.md` and `COHERENCE.md` §25 both require of
|
||||||
|
coherence-affecting work — this lane adds Lua API surface and
|
||||||
|
generalizes a Journey substrate, so it qualifies twice over.
|
||||||
|
|
||||||
**A prerequisite lane. PR #227 (git Stage 1) blocks on it**, and its
|
**A prerequisite lane. PR #227 (git Stage 1) blocks on it**, and its
|
||||||
P1a review finding is the reason this exists.
|
P1a review finding is the reason this exists.
|
||||||
|
|
||||||
|
|
@ -107,7 +120,48 @@ decided, and it is the substance of this lane.
|
||||||
lands. A prerequisite that also converts its first consumer makes the
|
lands. A prerequisite that also converts its first consumer makes the
|
||||||
two impossible to review separately.
|
two impossible to review separately.
|
||||||
|
|
||||||
## 5. Open questions
|
## 5. Coherence impact (§20)
|
||||||
|
|
||||||
|
**Revision 1 omitted this section entirely, and it is required.**
|
||||||
|
`CLAUDE.md` and `COHERENCE.md` §25 both say a framing for
|
||||||
|
coherence-affecting work must cite the section it serves and state its
|
||||||
|
impact — and this lane adds **new Lua API surface** and generalizes a
|
||||||
|
Journey-substrate mechanism, which is coherence-affecting on both
|
||||||
|
counts. Recording the impacts as neutral where they are neutral is part
|
||||||
|
of the requirement, not a way around it.
|
||||||
|
|
||||||
|
- **§16 semantic frontend — the section this serves.** The defect it
|
||||||
|
removes is a continuation resolving its target from *ambient* state a
|
||||||
|
tick after the request, which is precisely the multi-frontend
|
||||||
|
correctness §16 exists to protect. A capture makes "which frontend
|
||||||
|
asked" a value rather than a guess.
|
||||||
|
- **§14 workbench primitives — indirect, and the honest framing is
|
||||||
|
*enabling*.** This does not add a primitive. It removes the reason an
|
||||||
|
async adopter would hand-roll frontend tracking, which is the
|
||||||
|
mechanism by which primitives acquire per-consumer idiosyncrasies.
|
||||||
|
- **Journey steps touched: none directly, one PROTECTED.** The golden
|
||||||
|
journey does not gain a step. But Journey Stage 1a's Q#JR14 substrate
|
||||||
|
is what this generalizes, and §7 makes `tests/journey_acceptance.rs`
|
||||||
|
a preservation suite precisely so a generalization cannot erode the
|
||||||
|
step it came from.
|
||||||
|
- **Interaction islands (§6): none added.** No key interception, no
|
||||||
|
dispatch precedence rung. `dispatch_key` is untouched.
|
||||||
|
- **Config registry: no setting.** Where a continuation lands is a
|
||||||
|
correctness property, not a preference, and a toggle would offer to
|
||||||
|
turn correctness off.
|
||||||
|
- **Background-work attribution (§9): NEUTRAL, and worth stating
|
||||||
|
precisely rather than skipping.** This lane adds no background work
|
||||||
|
and no new unattributable surface. It also does **not** improve §9 —
|
||||||
|
knowing which frontend a result belongs to is not knowing who asked
|
||||||
|
for it or why. That is the worker-identity lane's arc, and the two
|
||||||
|
should not be confused because both concern async continuations.
|
||||||
|
- **§10 extension trust — a small positive.** The capture keeps the
|
||||||
|
Q#JR14d property that a destination is **nonconstructible from Lua**,
|
||||||
|
so generalizing the mechanism does not widen what extension code can
|
||||||
|
fabricate. §7 re-asserts the forged-destination refusal after the
|
||||||
|
rename for exactly this reason.
|
||||||
|
|
||||||
|
## 6. Open questions
|
||||||
|
|
||||||
### Q#DC-1 — what does the capture take as arguments?
|
### Q#DC-1 — what does the capture take as arguments?
|
||||||
|
|
||||||
|
|
@ -129,15 +183,49 @@ fabrication hole the userdata design closes.
|
||||||
buffer, and the stale-intent check applies only then.
|
buffer, and the stale-intent check applies only then.
|
||||||
3. **Two capture kinds**, document and panel, with different preflights.
|
3. **Two capture kinds**, document and panel, with different preflights.
|
||||||
|
|
||||||
*My vote: **(2)***. The four checks are not equally applicable, and
|
*My vote: **(2)***, with the profiles spelled out below rather than
|
||||||
which apply is a property of *what the continuation does*, which only
|
left to implementation.
|
||||||
the caller knows. (3) duplicates the liveness checks that both need;
|
|
||||||
(1) ships a refusal that will read as a bug the first time a user hits
|
|
||||||
it.
|
|
||||||
|
|
||||||
**I hold this one loosely.** It is the design decision of the lane, and
|
**Revision 1 said only "skip the stale-buffer check for a non-replacing
|
||||||
(1) has a real argument — a uniform rule is easier to reason about than
|
continuation", and that was incomplete.** Review is right: a panel
|
||||||
a parameterized one, and over-refusal is at least *safe*.
|
result does not depend on the captured **document window** at all. It
|
||||||
|
does not replace that window's buffer, so check 3 is irrelevant; it
|
||||||
|
does not occupy that window, so check 4 (dedicated) is irrelevant; and
|
||||||
|
it does not need that specific window to exist, so check 2 is
|
||||||
|
irrelevant. Retaining any of the three can reject `git.status` for a
|
||||||
|
document-window change that has nothing to do with where the panel
|
||||||
|
goes. But dropping them **without an explicit profile** is how document
|
||||||
|
replacement quietly loses its guarantees.
|
||||||
|
|
||||||
|
**The matrix, stated so every omission is deliberate and testable:**
|
||||||
|
|
||||||
|
| # | Precondition (`window_panel.rs:488-525`) | Document replacement | Frontend/panel scope |
|
||||||
|
|---|---|---|---|
|
||||||
|
| 1 | Requesting frontend still has a layout | **required** | **required** |
|
||||||
|
| 2 | Destination window still live in it | **required** | not applicable |
|
||||||
|
| 3 | Window still shows the captured buffer (Q#JR14c stale intent) | **required** | not applicable |
|
||||||
|
| 4 | Window is not dedicated (Q#JR14f) | **required** | not applicable |
|
||||||
|
|
||||||
|
**Check 1 is the entire panel profile**, and that is the honest reading
|
||||||
|
of what a panel continuation actually depends on: the frontend it was
|
||||||
|
launched from still exists. Everything else in the capture is document
|
||||||
|
state the panel never touches.
|
||||||
|
|
||||||
|
**Consequence for the capture, which follows and should not be
|
||||||
|
discovered later:** if the panel profile needs only the frontend, then
|
||||||
|
a frontend with **no document window** can still host a panel — so
|
||||||
|
Q#DC-4's "return `nil`" is right for the document profile and possibly
|
||||||
|
wrong for the panel one. That interaction is settled as part of
|
||||||
|
answering this, not after it.
|
||||||
|
|
||||||
|
**I hold the *choice* loosely, not the matrix.** (1) has a real
|
||||||
|
argument — a uniform rule is easier to reason about, and over-refusal
|
||||||
|
is safe — but it would refuse the git panel for reasons unrelated to
|
||||||
|
it, and "safe" refusals that users cannot explain are how a mechanism
|
||||||
|
gets worked around. If review prefers (1) or (3), the matrix above is
|
||||||
|
what changes, and **every cell marked "not applicable" must still be
|
||||||
|
tested as deliberately omitted** (§7) so a future reader cannot mistake
|
||||||
|
an omission for an oversight.
|
||||||
|
|
||||||
### Q#DC-3 — what is the type called?
|
### Q#DC-3 — what is the type called?
|
||||||
|
|
||||||
|
|
@ -158,7 +246,7 @@ inventing a fallback destination. A continuation with nowhere to land
|
||||||
should say so, and #227's adopter should degrade to today's ambient
|
should say so, and #227's adopter should degrade to today's ambient
|
||||||
behaviour with a status message rather than silently guessing.
|
behaviour with a status message rather than silently guessing.
|
||||||
|
|
||||||
## 6. Verification
|
## 7. Verification
|
||||||
|
|
||||||
- **A captured destination survives a frontend switch**: capture in A,
|
- **A captured destination survives a frontend switch**: capture in A,
|
||||||
make B active, commit, and assert the result lands in **A**. This is
|
make B active, commit, and assert the result lands in **A**. This is
|
||||||
|
|
@ -168,15 +256,36 @@ behaviour with a status message rather than silently guessing.
|
||||||
- **A fabricated destination is still refused** — the existing Q#JR14d
|
- **A fabricated destination is still refused** — the existing Q#JR14d
|
||||||
guarantee, re-asserted after the rename so the generalization cannot
|
guarantee, re-asserted after the rename so the generalization cannot
|
||||||
quietly open the hole it was built to close.
|
quietly open the hole it was built to close.
|
||||||
- **Each preflight refusal is witnessed by its own case**: frontend
|
- **Every preflight refusal is witnessed by its own case, in BOTH
|
||||||
gone, window gone, stale buffer, dedicated window — and, under
|
profiles** (Q#DC-2's matrix): frontend gone, window gone, stale
|
||||||
Q#DC-2's answer, that the stale-buffer refusal does **not** fire for
|
buffer, dedicated window — each asserted to **refuse** under the
|
||||||
a continuation that declared it is not replacing that buffer.
|
document profile, and each of the three marked "not applicable"
|
||||||
- **`nil` when the frontend has no document window** (Q#DC-4).
|
asserted to **NOT refuse** under the panel profile. A deliberately
|
||||||
|
omitted check that has no test is indistinguishable from a check
|
||||||
|
someone forgot, and the next reader will restore it.
|
||||||
|
- **`nil` when the frontend has no document window** (Q#DC-4) — for
|
||||||
|
the **document** profile. Whether the panel profile can capture
|
||||||
|
without one follows from Q#DC-2 and is asserted whichever way it is
|
||||||
|
answered.
|
||||||
- **The directory path is unchanged** — dired's existing acceptance
|
- **The directory path is unchanged** — dired's existing acceptance
|
||||||
coverage passes untouched. **If any dired test needs editing, the
|
coverage passes untouched.
|
||||||
generalization changed Journey Stage 1a's semantics** and that is a
|
- **`tests/journey_acceptance.rs` passes UNCHANGED**, as a named
|
||||||
stop signal, not a fixup.
|
preservation suite. It carries the established contract this lane
|
||||||
|
generalizes — 27 `commit_to` references across nine named pins
|
||||||
|
including `commit_to_refuses_a_forged_destination`,
|
||||||
|
`commit_to_scopes_and_restores_on_a_normal_return`,
|
||||||
|
`commit_to_restores_when_the_callback_raises`,
|
||||||
|
`commit_to_refuses_an_await_and_restores`,
|
||||||
|
`commit_to_delivers_to_the_requesting_frontend_not_the_ambient_one`,
|
||||||
|
`a_declining_listener_cannot_redirect_the_destination`, and two
|
||||||
|
rows already named `preservation_*`. Journey Stage 1a's own framing
|
||||||
|
treats this suite as a required gate; a lane that generalizes its
|
||||||
|
substrate does not get to relax that.
|
||||||
|
- **STOP SIGNAL, for both suites.** If any existing `dired` or
|
||||||
|
`journey_acceptance` test needs editing, the generalization changed
|
||||||
|
Journey Stage 1a's semantics. That is cause to stop and report, not
|
||||||
|
to adjust the test — a suite edited to accommodate the change under
|
||||||
|
test has stopped being evidence.
|
||||||
- **`Handle:await` still refuses inside the scope**, including through
|
- **`Handle:await` still refuses inside the scope**, including through
|
||||||
`pmacs.async.yield_to_next_tick` if the worker-identity lane's Q#W-7
|
`pmacs.async.yield_to_next_tick` if the worker-identity lane's Q#W-7
|
||||||
has landed by then; if it has not, this lane does **not** add that
|
has landed by then; if it has not, this lane does **not** add that
|
||||||
|
|
@ -187,7 +296,7 @@ behaviour with a status message rather than silently guessing.
|
||||||
that is #227's adoption, after this lands. This lane ships the
|
that is #227's adoption, after this lands. This lane ships the
|
||||||
mechanism and one set of tests for the mechanism.
|
mechanism and one set of tests for the mechanism.
|
||||||
|
|
||||||
## 7. Not in scope
|
## 8. Not in scope
|
||||||
|
|
||||||
**Adopting the capture anywhere**, including git (#227 does that) and
|
**Adopting the capture anywhere**, including git (#227 does that) and
|
||||||
including migrating other async continuations that have the same latent
|
including migrating other async continuations that have the same latent
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue