docs: 1-pre implemented --- framing revision 10, the lane, and a hazard

Three documents, one finding each.

**`docs/gui-stage1-input-framing.md` -> revision 10.** Revision 9 is the
approved design and revision 10 changes none of it. It records ONE scope
correction that could not be seen from the design: P1 has a second
structural exception, for the keyboard family alone, and it is winit's
rather than this seam's. `KeyEvent` carries a `pub(crate)
platform_specific` field, so no `WindowEvent::KeyboardInput` can be
constructed outside winit. Bounded three ways rather than accepted
whole --- it does not reach the pointer families (`DeviceId::dummy()`
exists for exactly this, checked BEFORE writing the exception down), the
family's only decision is factored into `route_key_action` and witnessed
directly, and what stays uncovered is one pattern arm with no logic.

Also records that P3 is now MEASURED: deleting the whole delegation
leaves all 256 `pmacs-gpu` tests green, not merely the 13 new rows.

**`docs/active-work.md`** --- the lane moves to IMPLEMENTED with the
four commits, the shape, the verbatim-move method, and the gate result.

**`docs/agent-handoff.md`** --- the stray-marker hazard gains what this
run earned: `scripts/gate` DOES NOT ISOLATE `TMPDIR`. It isolates the
target directory and five ambient roots, so `tempfile::tempdir()` still
lands under whatever `/tmp` happens to contain, and the hazard therefore
reproduces INSIDE a gate run --- which is how it surfaced here, on a
lane that touches only `pmacs-gpu/src/main.rs`. The bullet now carries
the discriminating command pair (`TMPDIR=/tmp` 0/2 versus a marker-free
root 2/2) rather than only the narrative, because a rerun establishes
nothing about this and the pair establishes everything. Isolating
`TMPDIR` is assigned to the gate lane, not to whichever feature PR trips
over it next.

One code change rides along: `EventOutcome`'s doc comment said
`event_loop.exit()` is called in "exactly one place", which is true of
the function and false of the call sites --- there are two, both inside
`window_event`. Stated precisely now, since the whole point of the
sentence is that a reader can check it by grep.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016bqGA6s9tTUFzYpbeW3tai
This commit is contained in:
Levi Neuwirth 2026-08-11 23:55:57 +02:00
parent e95564567e
commit 41a08b8237
No known key found for this signature in database
4 changed files with 155 additions and 26 deletions

View File

@ -250,7 +250,7 @@ hazard in a shape that looks committed. **A documented error message
that never appears is worse than no documentation**, because the reader that never appears is worse than no documentation**, because the reader
waits for a signal that is not coming. waits for a signal that is not coming.
## GUI arc Stage 1 — 1-pre branch OPEN, framing APPROVED, no PR yet ## GUI arc Stage 1 — 1-pre IMPLEMENTED, no PR yet
**Written at the branch's first commit**, with the framing, as the arc's **Written at the branch's first commit**, with the framing, as the arc's
§5 requires of every PR in it. §5 requires of every PR in it.
@ -259,25 +259,57 @@ waits for a signal that is not coming.
Stage 0 merge, #236). **`githubsucks/gui-stage1-pre` is the Stage 0 merge, #236). **`githubsucks/gui-stage1-pre` is the
authoritative tip** — the ref, not a SHA. Recover with authoritative tip** — the ref, not a SHA. Recover with
`git fetch githubsucks && git checkout gui-stage1-pre`. `git fetch githubsucks && git checkout gui-stage1-pre`.
- **Framing `docs/gui-stage1-input-framing.md`, revision 9, APPROVED** - **Framing `docs/gui-stage1-input-framing.md`, revision 10, APPROVED**
after **eight rejected revisions**. It is Stage 1's framing for **all** after **eight rejected revisions**. Revision 9 is the approved design;
slices and governs the later branches; only Stage 0 was framed by the **revision 10 changes none of it** and records one scope correction
arc document itself. found against this implementation (below). It is Stage 1's framing for
**all** slices and governs the later branches; only Stage 0 was framed
by the arc document itself.
- **Scope of THIS branch: 1-pre only — the input seam. No behaviour - **Scope of THIS branch: 1-pre only — the input seam. No behaviour
change.** `App::window_event` is **655 lines** (`main.rs:2734`) and change.** `App::window_event` was **655 lines** and is now **33**: one
nothing below it can be witnessed without a display, which is why the `route_event` call and one arm per route. Nothing below it could be
seam precedes every other slice. witnessed without a display, which is why the seam precedes every
- **The evidence contract, because "no behaviour change" is not one:** a other slice.
**headless routing harness** records, per event family, the routing - **IMPLEMENTED in four commits, one per event family**, so each lands
decision, the **outbound protocol events, and the LOCAL effects** — with its own witnesses and mutations rather than as one 600-line
exit, redraw, resize, state mutation. Production `window_event` diff: `014110f` lifecycle (close / modifiers / resize), `7f0f9db`
becomes a **thin call-through**. Mutation evidence: bypassing an arm, redraw, `0705564` keyboard, `e955645` the four pointer arms.
or misrouting one family to another, must fail. - **The shape.** Deciding is `route_event(&WindowEvent) -> Route`, a
- **P3 is an ACCEPTED STRUCTURAL EXCEPTION.** A headless test cannot free function composing one decision function per family
construct `ActiveEventLoop` or invoke the real callback, so the (`route_lifecycle`, `route_keyboard` + `route_key_action`,
`window_event → router` delegation is a **code-review invariant, not a `route_pointer`). Performing stays on `App` in seven `apply_*`
tested one**. Recorded rather than papered over: mutation evidence methods. **A route names its LOCAL EFFECT**, not merely the family
covers every router arm and **not** the delegation. that claims it, and the harness records routes — because
`CloseRequested` and `RedrawRequested` send the daemon nothing, so a
transcript of protocol traffic could not tell a handled arm from a
dropped one.
- **Every moved body verified as the original, mechanically.** The
keyboard body is byte-identical modulo two named conversions; the four
pointer bodies were checked by re-running rustfmt on the pre-move text
at the new indent level and diffing, since de-indenting by 8 columns
lets rustfmt rejoin lines. **13 witnesses, 17 mutations.**
- **P3 IS NOW MEASURED, NOT ASSUMED.** Replacing `window_event`'s whole
body with `let _ = (event_loop, event);` — a GUI that responds to no
input at all — leaves **all 256 `pmacs-gpu` tests green**. That is the
exception's true extent: `ActiveEventLoop` cannot exist outside a live
event loop, so **no** headless test in the crate observes the
delegation, not merely none of the new ones.
- **A SECOND ACCEPTED STRUCTURAL EXCEPTION, found here and winit's
rather than ours.** `KeyEvent` carries a `pub(crate)
platform_specific` field, so **no `WindowEvent::KeyboardInput` can be
constructed outside winit** and the keyboard family's routing arm
cannot be fed by a test. Bounded three ways: it does **not** extend to
the pointer families (`DeviceId::dummy()` exists for exactly this, and
all three pointer events are constructible — checked before writing
the exception down); the family's only real decision is factored into
`route_key_action(ElementState)` and witnessed directly; and what
stays unwitnessed is one pattern arm containing a match and a call.
- **`event_loop.exit()` now appears in exactly two places, both inside
`window_event`.** The keyboard body was its second caller (the idle
Escape), so `apply_keyboard` returns an `EventOutcome` rather than
taking an `&ActiveEventLoop` — which is what keeps the bodies
reachable in principle. **Stage 1a's A4 deletes that branch**, at
which point `EventOutcome` has one variant and should go.
- **Slice order (each its own branch and PR):** `1-pre` → `1a`\* → `1b` - **Slice order (each its own branch and PR):** `1-pre` → `1a`\* → `1b`
→ `1c` → `1d` → `1e`\*. **`1a` and `1e` are protocol-bearing (v24 → `1c` → `1d` → `1e`\*. **`1a` and `1e` are protocol-bearing (v24
`TextInput`, v25 `OpenTarget`/`OpenTargetResult`) and are `TextInput`, v25 `OpenTarget`/`OpenTargetResult`) and are
@ -286,9 +318,33 @@ waits for a signal that is not coming.
Stage 2, so the arc framing's §2.5 and the standing backlog are Stage 2, so the arc framing's §2.5 and the standing backlog are
amended here. Stage 1 keeps the deliberate OS reservation and adds no amended here. Stage 1 keeps the deliberate OS reservation and adds no
island. island.
- **Gates:** `./scripts/gate --acceptance gpu_invocation_acceptance` - **Gates:** `./scripts/gate --acceptance gpu_invocation_acceptance`.
plus touched input suites, and `PMACS_REQUIRE_GPU=1 cargo test -p That one invocation already runs `PMACS_REQUIRE_GPU=1 cargo test -p
pmacs-gpu`. **No `--protocol`** — 1-pre changes no wire. pmacs-gpu` (step `gpu`) and the full `--workspace --no-fail-fast`
sweep in both feature configurations, so the framing §11 phrase "plus
touched input suites" is satisfied by the sweep rather than by a
hand-picked list. **No `--protocol`** — 1-pre changes no wire.
- **THE FIRST GATE RUN WENT RED ON A STRAY `/tmp/.git`, NOT ON THIS
BRANCH.** `m4` and the sweep failed
`m4_24_bare_string_glob_stays_relative` and
`m4_24_d3_fallback_base_is_the_smallest_attachment_dir` — two LSP
file-watcher tests — with every other target green. Established as
environmental three ways, in increasing strength:
- **Structurally impossible for this branch to cause.** The diff
touches only `pmacs-gpu/src/main.rs`; `pmacs-gpu` is a workspace
**member but not a dependency** of the root package, so the
`m4_acceptance` binary never links it.
- **The marker is older than the session.** `/tmp/.git` is empty and
was created at 20:14 CEST, **3.5 h before** the gate run at 23:45;
`/tmp` held 8,920 entries. That is handoff §1's recorded hazard
exactly.
- **A discriminating pair, same binary and commit, one variable:**
`TMPDIR=/tmp` → **0/2**, `TMPDIR=<marker-free>` → **2/2**. A rerun
would have established nothing; this establishes the cause.
**`scripts/gate` isolates the target dir and five ambient roots but
NOT `TMPDIR`** — recorded in handoff §1, where the standing fix is
assigned to the gate lane rather than to this PR.
## The GUI arc — Stage 0 MERGED as #236 (`f8ad3e7`) ## The GUI arc — Stage 0 MERGED as #236 (`f8ad3e7`)

View File

@ -210,6 +210,30 @@ commands, read `docs/active-work.md` immediately after this file.
server-rooted watcher then faithfully watched. A server-rooted watcher then faithfully watched. A
markerless-fixture red that looks like a watcher bug may be an markerless-fixture red that looks like a watcher bug may be an
ancestor marker, on any machine. ancestor marker, on any machine.
**SEEN AGAIN 2026-08-11, and `scripts/gate` DOES NOT PROTECT YOU
FROM IT.** The gate isolates the target directory and five ambient
roots but **not `TMPDIR`**, so `tempfile::tempdir()` still lands
under a `/tmp` that may carry a marker. It surfaced inside a gate
run on an unrelated lane (GUI 1-pre, which touches only
`pmacs-gpu/src/main.rs`) as **`m4_24_bare_string_glob_stays_relative`
and `m4_24_d3_fallback_base_is_the_smallest_attachment_dir`**, in
both the `m4` step and the `--workspace` sweep, with every other
target in the corpus green.
**Diagnose it with the discriminating pair, not a rerun** — same
binary, same commit, one variable:
```sh
TMPDIR=/tmp cargo test --test m4_acceptance -- m4_24_ # 0/2
TMPDIR=<marker-free dir> cargo test --test m4_acceptance -- m4_24_ # 2/2
```
Check the ancestors of the temp root for `.git`, `Cargo.toml` and
friends before believing any markerless-fixture red. **Isolating
`TMPDIR` inside `scripts/gate` is the standing fix and belongs to
the gate lane**, not to whichever feature PR happens to trip over
it.
- **Deliberately unbuilt**: kernel notification (framing option E) — - **Deliberately unbuilt**: kernel notification (framing option E) —
a framed option, not residue; its trigger is the 4 s worst-case a framed option, not residue; its trigger is the 4 s worst-case
external-change latency mattering in practice. external-change latency mattering in practice.

View File

@ -1,8 +1,10 @@
# GUI arc, Stage 1 — input foundation (framing) # GUI arc, Stage 1 — input foundation (framing)
**Status: revision 9 — APPROVED.** Revisions 1–8 rejected. **Status: revision 10 — APPROVED.** Revisions 1–8 rejected; revision 9
**Q#S1-8, Q#S1-9 and Q#S1-10 are RULED.** Implementation may begin is the approved design and **revision 10 changes none of it** — it
from this document. records one scope correction found against the 1-pre implementation
(§6, "Revision 10"). **Q#S1-8, Q#S1-9 and Q#S1-10 are RULED.**
**1-pre is IMPLEMENTED**; 1a onward may begin from this document.
**Verification base:** checked in the `gui-arc-stage0` worktree at **Verification base:** checked in the `gui-arc-stage0` worktree at
`a994f37`, whose tree for these files is what `f8ad3e7` merged. `a994f37`, whose tree for these files is what `f8ad3e7` merged.
@ -117,6 +119,52 @@ P3 remains an accepted structural exception: not headlessly testable.
| P2 | Harness records outbound events **and local effects** (exit, redraw, resize, state mutation) | no harness | record outbound only → exit/redraw rows | | P2 | Harness records outbound events **and local effects** (exit, redraw, resize, state mutation) | no harness | record outbound only → exit/redraw rows |
| P3 | `window_event` is a thin call-through | — | **structural/code-review invariant; not testable headlessly** (no `ActiveEventLoop`) | | P3 | `window_event` is a thin call-through | — | **structural/code-review invariant; not testable headlessly** (no `ActiveEventLoop`) |
**Revision 10 — one finding against the implementation, not the
design.** The 1-pre seam is built and the table above holds, with one
scope correction that could not be seen from the design.
**P1 has a SECOND structural exception, and it is winit's rather than
this seam's.** `KeyEvent` carries a `pub(crate) platform_specific`
field (`winit-0.30.13/src/event.rs:655`), so **no
`WindowEvent::KeyboardInput` can be constructed outside winit** and no
headless test can feed one to the router. P1's mutation — misroute a
family, fail that family's row — is therefore unavailable for the
**keyboard** family alone.
Three things bound it, so it is a measured exception rather than a
blanket one:
- **The exception does not extend to the pointer families.** Winit
provides `DeviceId::dummy()` for exactly this purpose, and
`CursorMoved` / `MouseInput` / `MouseWheel` are constructible. Checked
before the exception was written down; all three are witnessed.
- **What stays unwitnessed is one pattern arm with no logic in it.** The
family's only decision — a press is acted on, a release is claimed and
discarded — is factored into `route_key_action(ElementState) ->
KeyAction`, which takes a constructible argument and is witnessed
directly, with both misroute mutations failing that row alone.
- **P3 is now measured, not assumed.** Replacing `window_event`'s entire
body with `let _ = (event_loop, event);` — a GUI that responds to no
input at all — leaves **all 256 `pmacs-gpu` tests green**, not merely
the 13 routing rows. That is the exception's true extent: no headless
test anywhere in the crate observes the delegation.
**P2's harness records ROUTES, and that is the mechanism rather than a
narrowing.** A route names its local effect — `Exit`, `Redraw`,
`Resize { width, height }`, `Modifiers(state)` — so one transcript
covers both halves of P2's contract. The transcript row is deliberately
the **sole** owner of P2 (the per-variant rows call `route_event`
directly), which is what keeps "record outbound only" failing exactly
one row instead of every row.
**One design consequence worth carrying into 1a.** The keyboard arm was
the second caller of `event_loop.exit()` — the idle-Escape local quit —
so its body returns an `EventOutcome` rather than taking an
`&ActiveEventLoop`. `event_loop.exit()` now appears in exactly two
places, both inside `window_event`, and nowhere else in the crate.
**A4 deletes the Escape branch, at which point `EventOutcome` has one
variant and should go with it.**
### 1a — `TextInput` (v24) ### 1a — `TextInput` (v24)
| # | Contract | Witness (fails today because) | Mutation | | # | Contract | Witness (fails today because) | Mutation |

View File

@ -3371,7 +3371,8 @@ enum Route<'a> {
/// keyboard family produces anything but `Continue` today: an idle /// keyboard family produces anything but `Continue` today: an idle
/// Escape is a local quit. Returning the decision rather than taking an /// Escape is a local quit. Returning the decision rather than taking an
/// `&ActiveEventLoop` is what keeps every body reachable from a test — /// `&ActiveEventLoop` is what keeps every body reachable from a test —
/// `event_loop.exit()` is called in exactly one place, `window_event`. /// the crate's two `event_loop.exit()` call sites, this one and
/// `LifecycleRoute::Exit`, both sit in `window_event` and nowhere else.
/// ///
/// Stage 1a's A4 deletes that branch (an idle Escape must reach the /// Stage 1a's A4 deletes that branch (an idle Escape must reach the
/// daemon and never exit), at which point this type has one variant and /// daemon and never exit), at which point this type has one variant and