test(journey): pin the destination commit, and land the doc updates
Completes Journey Stage 1a: the `commit_to` acceptance suite (framing §6 N4, N6, N6b, N6c, P1, P2, P3) plus the documentation updates COHERENCE §25 requires the PR to carry. Bite-testing the new pins found a real gap. Deleting the `ScopedFrontend` arm from `acting_frontend` left N4 green, because `ScopedFrontend::enter` also swaps `core.active_frontend` and the ambient fallback then answers correctly on its own. The arm is load-bearing in exactly one case — a commit reached from inside an interactive command, where the origin sits between the override and the ambient value — and nothing pinned it. N4b is added, driven through `dispatch_key` because that is the only thing that establishes an interactive origin, and the mutation now bites it. Two smaller corrections found the same way: * `commit_to`'s forged-destination message was unreachable. Typed as `AnyUserData`, mlua rejected a table during argument conversion, so a caller got "error converting Lua table to userdata" — true, but naming neither the rule nor the remedy. The parameter is now `mlua::Value` and the pointed message fires. * P1 and P2 also fail on full revert, since `commit_to` does not exist on the pre-image, so §6.0's "legitimately green on the pre-image" does not describe them. They stay in the P list because their discriminating falsifier is the named mutation — a revert-only check cannot distinguish "validates" from "validates in time" — and each pin now says so at its own site rather than being silently mislabelled. Bite results, each run against the whole suite: scope stops swapping `core.active_frontend` -> N6a, P3 fail; nothing else preflight moved after the callback -> P1, P2 fail; nothing else drop the `ScopedFrontend` arm -> N4b fails; nothing else Docs: COHERENCE §2 grade + step-3 verdict row, §20 Priority 1 and the arc list; the GPU initial-target framing's Q#GT6 and acceptance 10, whose directory case this stage deliberately supersedes; handoff §1; the active-work ledger; framing rev 7. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This commit is contained in:
parent
25b07be97b
commit
d9d1c0b423
57
COHERENCE.md
57
COHERENCE.md
|
|
@ -339,7 +339,8 @@ the journey.
|
||||||
|
|
||||||
### Ground truth: the journey today
|
### Ground truth: the journey today
|
||||||
|
|
||||||
**Grade: broken at step 3.** Verified empirically at audit time:
|
**Grade: reaches step 5; thin from step 6 on.** Was **broken at step 3**
|
||||||
|
at audit time:
|
||||||
|
|
||||||
```
|
```
|
||||||
$ ./target/release/pmacs .
|
$ ./target/release/pmacs .
|
||||||
|
|
@ -347,15 +348,23 @@ pmacs: Is a directory (os error 21)
|
||||||
EXIT=1
|
EXIT=1
|
||||||
```
|
```
|
||||||
|
|
||||||
The literal first arrow of the diagram above fails. `load_file`
|
The literal first arrow of the diagram above failed. `load_file`
|
||||||
(`src/file_io.rs:81-87`) does `File::open` (succeeds on a directory)
|
(`src/file_io.rs:81-87`) does `File::open` (succeeds on a directory)
|
||||||
then `read_to_end` → EISDIR, which is not `NotFound`, so
|
then `read_to_end` → EISDIR, which is not `NotFound`, so
|
||||||
`EditorState::open` returns `Err` and `main` prints and exits
|
`EditorState::open` returned `Err` and `main` printed and exited.
|
||||||
(`src/main.rs:411-414`). Multiple file arguments are also rejected
|
|
||||||
(`"multiple files not yet supported"`, `src/main.rs:227`). Everything
|
**Journey Stage 1a fixed that arrow** (`docs/journey-stage1a-framing.md`).
|
||||||
from step 6 onward is gated on a file being open, and the only
|
`resolve_target_buffer` now answers `ResolvedTarget::Directory` *ahead*
|
||||||
zero-config way to open one is naming it on the command line — which
|
of the load, `pmacs .` lists the directory in dired, `RET` visits a
|
||||||
requires already knowing the path.
|
file, and a self-insert lands in it — steps 3 and 5 run end to end,
|
||||||
|
pinned by `tests/journey_acceptance.rs`. Which surface opens a directory
|
||||||
|
is a `path.open-directory` chain with dired as a replaceable fallback,
|
||||||
|
so this did not grow a second directory surface.
|
||||||
|
|
||||||
|
Still true: multiple file arguments are rejected (`"multiple files not
|
||||||
|
yet supported"`, `src/main.rs:227`), and everything from step 6 onward
|
||||||
|
is gated on a file being open — but the zero-config way to open one is
|
||||||
|
no longer "already know the path".
|
||||||
|
|
||||||
Full verdict table:
|
Full verdict table:
|
||||||
|
|
||||||
|
|
@ -363,7 +372,7 @@ Full verdict table:
|
||||||
|---|---|---|---|
|
|---|---|---|---|
|
||||||
| 1 | Install | **Partial** | Source build only: `cargo build --release --workspace --features pmacs/crdt` (`README.md`). No binaries, no packaging. Runtime deps (`/bin/sh`, git, tar, coreutils) documented, never checked at runtime |
|
| 1 | Install | **Partial** | Source build only: `cargo build --release --workspace --features pmacs/crdt` (`README.md`). No binaries, no packaging. Runtime deps (`/bin/sh`, git, tar, coreutils) documented, never checked at runtime |
|
||||||
| 2 | Launch unconfigured | **Works** | `EditorState::new()` → empty `*scratch*`; missing config is not an error (`src/config.rs:7-9`); recentf/saveplace/autosave default-on |
|
| 2 | Launch unconfigured | **Works** | `EditorState::new()` → empty `*scratch*`; missing config is not an error (`src/config.rs:7-9`); recentf/saveplace/autosave default-on |
|
||||||
| 3 | Open real project | **Missing at the CLI** | `pmacs .` still exits 1 (above): `load_file` does `File::open` (which succeeds on a directory) then `read_to_end` → EISDIR, which is not `NotFound`, so `resolve_target_buffer`'s create-a-`[new file]` arm never fires. Dired Stage 1 (merged #165) supplies the buffer a directory should resolve *to*; routing `pmacs .` into it is Journey Stage 1's work, which must not invent a second directory surface |
|
| 3 | Open real project | **Works at the CLI** | Journey Stage 1a: `resolve_target_buffer` answers `ResolvedTarget::Directory` before the EISDIR-producing load, and `EditorState::open` / the daemon bootstrap dispatch the `path.open-directory` chain, whose fallback is dired (#165's buffer, reached rather than duplicated). Startup no longer fails: an unreadable directory, a crashed resolver, and a cleared handler all report on the status line and leave the session running. Because the listing is async and the bootstrap is synchronous, the commit runs against a destination captured at request time (`pmacs.window.commit_to`) rather than against the ambient frontend |
|
||||||
| 4 | Understand interface | **Partial** | Mode line gives name/modified/L:C/scroll + mode/LSP/terminal segments; but no welcome text (`EditorCore::new` sets `status: String::new()`), no cheat sheet, and `C-h` deletes a word (§18) |
|
| 4 | Understand interface | **Partial** | Mode line gives name/modified/L:C/scroll + mode/LSP/terminal segments; but no welcome text (`EditorCore::new` sets `status: String::new()`), no cheat sheet, and `C-h` deletes a word (§18) |
|
||||||
| 5 | Edit | **Works** | Full CUA + Emacs keymap in 161 lines (`builtin/keymaps/default.lua`); isearch, query-replace, kill ring, undo/redo, auto-indent/pair/comment, atomic save. Genuinely excellent zero-config |
|
| 5 | Edit | **Works** | Full CUA + Emacs keymap in 161 lines (`builtin/keymaps/default.lua`); isearch, query-replace, kill ring, undo/redo, auto-indent/pair/comment, atomic save. Genuinely excellent zero-config |
|
||||||
| 6 | Language intelligence | **Partial** | Rust grammar bundled and auto-attaches; rust-analyzer preconfigured (`builtin/runtime/lsp.lua:44-52`) — but a missing binary fails silently (§1.2) and highlighting masks it. No LSP status command exists to diagnose |
|
| 6 | Language intelligence | **Partial** | Rust grammar bundled and auto-attaches; rust-analyzer preconfigured (`builtin/runtime/lsp.lua:44-52`) — but a missing binary fails silently (§1.2) and highlighting masks it. No LSP status command exists to diagnose |
|
||||||
|
|
@ -1474,14 +1483,18 @@ missing runtime entity — a real arc).
|
||||||
### Priority 1: Protect the golden product journey
|
### Priority 1: Protect the golden product journey
|
||||||
|
|
||||||
Establish the end-to-end workflow; treat regressions as release
|
Establish the end-to-end workflow; treat regressions as release
|
||||||
blockers. **State: broken at step 3 (§2). Mostly wiring, and unusually
|
blockers. **State: runs to step 5; thin from step 6 (§2). Mostly wiring,
|
||||||
cheap:** directory-argument handling (the remaining half of step 3 —
|
and unusually cheap:** directory-argument handling (**done**: Journey
|
||||||
dired Stage 1 landed the buffer it should resolve to); a find-file
|
Stage 1a); a find-file surface (**done**: #162 open-by-path, #165
|
||||||
surface (**done**: #162 open-by-path, #165 browsing); surfacing the
|
browsing); surfacing the LSP spawn failure with guidance (§1.2); a
|
||||||
LSP spawn failure with guidance (§1.2); a
|
|
||||||
compile keybinding + `cargo build`/`test` default from the existing
|
compile keybinding + `cargo build`/`test` default from the existing
|
||||||
`ProjectKind::Cargo`; a terminal keybinding; a welcome buffer. The
|
`ProjectKind::Cargo`; a terminal keybinding (**done**: `C-c t`, #173); a
|
||||||
journey acceptance suite (§19) is the ratchet that keeps it fixed.
|
welcome buffer. The journey acceptance suite (§19) is the ratchet that
|
||||||
|
keeps it fixed — it **exists now** (`tests/journey_acceptance.rs`,
|
||||||
|
Stage 1a), seeded with steps 2, 3, and 5.
|
||||||
|
|
||||||
|
Journey Stage 1b is the named remainder: the compile binding + Cargo
|
||||||
|
defaults, LSP spawn guidance, and the welcome buffer.
|
||||||
|
|
||||||
### Priority 2: Make workspace and location explicit
|
### Priority 2: Make workspace and location explicit
|
||||||
|
|
||||||
|
|
@ -1545,11 +1558,13 @@ Candidate arc cuts, honoring one-feature-one-branch-one-PR and the
|
||||||
framing workflow (each needs its own scout + framing before any
|
framing workflow (each needs its own scout + framing before any
|
||||||
implementation — this list is direction, not commitment):
|
implementation — this list is direction, not commitment):
|
||||||
|
|
||||||
1. **Journey Stage 1** (P1): directory open + compile defaults +
|
1. **Journey Stage 1** (P1): split at the new-Rust-primitive line.
|
||||||
LSP-failure surfacing + bindings + welcome buffer + the first
|
**Stage 1a — landed**: directory open, the `EditorState::open` →
|
||||||
journey acceptance suite. Dired Stage 1 has landed (#165), so the
|
`resolve_target_buffer` unification, the destination-scope substrate,
|
||||||
buffer a directory resolves *to* already exists; this arc routes
|
and the first journey acceptance suite. It routes `pmacs .` into
|
||||||
`pmacs .` into it rather than growing a second directory surface.
|
#165's dired buffer rather than growing a second directory surface.
|
||||||
|
**Stage 1b — remaining**: compile defaults, LSP-failure surfacing,
|
||||||
|
bindings, welcome buffer.
|
||||||
2. **Discovery surface** (P4): the describe/list/where-is command
|
2. **Discovery surface** (P4): the describe/list/where-is command
|
||||||
family, M-x rich rows, help unification, help prefix.
|
family, M-x rich rows, help unification, help prefix.
|
||||||
3. **Transient keymap layer** (§6): the overlay scope + lifetime
|
3. **Transient keymap layer** (§6): the overlay scope + lifetime
|
||||||
|
|
|
||||||
|
|
@ -331,24 +331,41 @@ If it does not, stop and repair the remote/fetch configuration.
|
||||||
--check` clean.
|
--check` clean.
|
||||||
- Stage 4b (the input method) is NOT in this PR and not started.
|
- Stage 4b (the input method) is NOT in this PR and not started.
|
||||||
|
|
||||||
## Journey Stage 1a — framing rev 5 APPROVED; branch cut, implementing
|
## Journey Stage 1a — IMPLEMENTED on branch, gates run, PR pending
|
||||||
|
|
||||||
- Approved framing: `docs/journey-stage1a-framing.md` **rev 5** (four
|
- Framing `docs/journey-stage1a-framing.md` **rev 7** (four review
|
||||||
review rounds). Branch `journey-stage1a-directory-open`, framing
|
rounds, then two correction revisions found during implementation).
|
||||||
committed as its first commit. No PR yet.
|
Branch `journey-stage1a-directory-open`, rebased onto `githubsucks/main`
|
||||||
|
@ `74301d1`.
|
||||||
- Recovery: `git fetch githubsucks && git checkout
|
- Recovery: `git fetch githubsucks && git checkout
|
||||||
journey-stage1a-directory-open`. The framing now travels; the
|
journey-stage1a-directory-open`. Everything below is committed and
|
||||||
implementation does not until it is committed and pushed.
|
pushed; nothing depends on a worktree or `/tmp`.
|
||||||
- Ordering: PR #177 MERGED (2026-07-26), so 1a is unblocked. 1a lands
|
- **Ships:** the directory arm on `resolve_target_buffer`,
|
||||||
|
`EditorState::open` rewritten as a caller of it (the unification), the
|
||||||
|
`path.open-directory` chain + `pmacs.path.directory_handler` fallback
|
||||||
|
slot, `pmacs.window.commit_to` with its scoped frontend and preflight,
|
||||||
|
the nonconstructible destination userdata, the daemon bootstrap arm,
|
||||||
|
and `tests/journey_acceptance.rs` (23 pins). No protocol change —
|
||||||
|
still v20.
|
||||||
|
- **Doc updates ride the PR** per COHERENCE §25: §2 grade + step-3
|
||||||
|
verdict row, §20 Priority 1 + the arc list, the GPU initial-target
|
||||||
|
framing's Q#GT6 / acceptance 10 supersession, handoff §1.
|
||||||
|
- **Bite results** (each mutation run against the full suite): scope
|
||||||
|
stops swapping `core.active_frontend` → N6a + P3 fail, nothing else;
|
||||||
|
preflight moved after the callback → P1 + P2 fail, nothing else; drop
|
||||||
|
the `ScopedFrontend` arm from `acting_frontend` → N4b fails, nothing
|
||||||
|
else. That last mutation is why N4b exists — it left N4 green.
|
||||||
|
- Ordering: PR #177 MERGED (2026-07-26), so 1a was unblocked. 1a lands
|
||||||
before dired Stage 2. When 1a lands, Stage 2 must re-scout and revise
|
before dired Stage 2. When 1a lands, Stage 2 must re-scout and revise
|
||||||
its framing around the scoped `pmacs.window.commit_to` boundary before
|
its framing around the scoped `pmacs.window.commit_to` boundary before
|
||||||
its implementation branch is cut. That revision is a prerequisite, not
|
its implementation branch is cut. That revision is a prerequisite, not
|
||||||
a review-time discovery.
|
a review-time discovery.
|
||||||
- Implementation order inside the branch (framing §12): scoped frontend
|
- **Named deferrals carried out of this stage:** dired's *interactive*
|
||||||
override + shared eligibility predicate first (separable, testable
|
paths (`C-x d`, tree descent, refresh) still rely on the ambient
|
||||||
without dired), then `commit_to` and the opaque destination, then the
|
frontend a tick later and are not migrated onto captured destinations;
|
||||||
directory arm and resolver chain, then the journey suite, then the
|
the stale startup scratch buffer is still not removed (only the false
|
||||||
doc updates COHERENCE §25 requires.
|
doc comment is corrected); `resolve_target_buffer`'s directory arm has
|
||||||
|
no picker, only the chain that leaves room for one.
|
||||||
|
|
||||||
## The CRDT half of the test corpus is dark in CI — NEEDS A LANE
|
## The CRDT half of the test corpus is dark in CI — NEEDS A LANE
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -54,8 +54,51 @@ commands, read `docs/active-work.md` immediately after this file.
|
||||||
standard new work is evaluated against. Per `CLAUDE.md`, **every new
|
standard new work is evaluated against. Per `CLAUDE.md`, **every new
|
||||||
framing doc must state its coherence impact** — journey steps touched,
|
framing doc must state its coherence impact** — journey steps touched,
|
||||||
interaction islands added, config-registry adoption, background-work
|
interaction islands added, config-registry adoption, background-work
|
||||||
attribution. Its §2 grades the golden journey **broken at step 3**
|
attribution. Its §2 grades the golden journey; **Journey Stage 1a
|
||||||
(`pmacs .` exits 1).
|
moved that grade off "broken at step 3"** — see the arc bullet below.
|
||||||
|
- **Journey arc (P1) — Stage 1a LANDED**
|
||||||
|
(`docs/journey-stage1a-framing.md`). `pmacs .` opens a directory
|
||||||
|
instead of exiting 1, on **one** path: `resolve_target_buffer` gained a
|
||||||
|
`ResolvedTarget::Directory` arm *ahead* of the load, `EditorState::open`
|
||||||
|
became a caller of it rather than a parallel implementation, and the
|
||||||
|
daemon/GPU bootstrap shares the same arm. Which surface handles a
|
||||||
|
directory is the `path.open-directory` chain with dired as a
|
||||||
|
replaceable fallback slot. `tests/journey_acceptance.rs` is the new
|
||||||
|
cross-subsystem ratchet (steps 2, 3, 5 seeded; **stages add rows, none
|
||||||
|
removes them**). No protocol change.
|
||||||
|
- **A hook a builtin subscribes to can never be first-claimant-wins
|
||||||
|
for users.** `HookRegistry::add` only appends and builtins load
|
||||||
|
before `init.lua`, so a dired subscription would always claim before
|
||||||
|
any user listener. That is why dired is a *slot*
|
||||||
|
(`pmacs.path.directory_handler`) and not a subscriber — and why
|
||||||
|
clearing the slot has to leave startup succeeding with a status,
|
||||||
|
not exiting 1.
|
||||||
|
- **A raise and a `false` are indistinguishable in `proceed`.**
|
||||||
|
`run_short_circuit` returns `proceed = false` for both; only
|
||||||
|
`HookOutcome.errors` separates them, and it decides whether to
|
||||||
|
*report*, not whether to fall back. Getting this backwards produces a
|
||||||
|
fallback that runs after a user's resolver crashed mid-handling.
|
||||||
|
- **The listing is async; the bootstrap is synchronous.** The whole
|
||||||
|
post-await commit therefore runs against a destination captured at
|
||||||
|
request time (`pmacs.window.commit_to`), which preflights every
|
||||||
|
precondition *before* invoking the callback — dired mutates handle
|
||||||
|
state, `prev`, and paint long before it reaches anything that could
|
||||||
|
refuse, so validating at display time is four mutations too late.
|
||||||
|
Awaiting inside a commit is refused: a yield would restore the scope
|
||||||
|
while the coroutine is still parked.
|
||||||
|
- **The scope swaps `core.active_frontend`, not just an override** —
|
||||||
|
`pmacs.window.buffer()`'s no-arg arm reads the ambient active buffer
|
||||||
|
directly, so dired's `prev` capture would otherwise follow whatever
|
||||||
|
frontend happened to be dispatching. The override *also* exists, and
|
||||||
|
is load-bearing in exactly one case: a commit reached from inside an
|
||||||
|
interactive command, where the origin would otherwise outrank the
|
||||||
|
ambient value. Bite-testing found N4 green without it.
|
||||||
|
- **`replace_active_buffer` does not drop the startup scratch buffer**,
|
||||||
|
despite its doc comment having claimed so for as long as it has
|
||||||
|
existed. Its body is one `switch_active_buffer` call. The comment is
|
||||||
|
corrected here; changing the lifetime is separate work.
|
||||||
|
- Stage 1b is the named remainder: compile binding + Cargo defaults,
|
||||||
|
LSP spawn guidance, welcome buffer.
|
||||||
- **Lean 4 arc (Arc 8) — stages 1, 2, 3a, 3b LANDED**
|
- **Lean 4 arc (Arc 8) — stages 1, 2, 3a, 3b LANDED**
|
||||||
(`docs/lean4-mode-framing.md`; #160, #161, #167, #170; merge
|
(`docs/lean4-mode-framing.md`; #160, #161, #167, #170; merge
|
||||||
`d400f30`). pmacs edits Lean 4: `arborium-lean` highlighting, a
|
`d400f30`). pmacs edits Lean 4: `arborium-lean` highlighting, a
|
||||||
|
|
|
||||||
|
|
@ -282,8 +282,17 @@ observers; they are not the transport implementation.
|
||||||
- Any `NotFound` from the initial load creates an empty path-backed buffer,
|
- Any `NotFound` from the initial load creates an empty path-backed buffer,
|
||||||
including when a parent is currently absent; save-time errors remain
|
including when a parent is currently absent; save-time errors remain
|
||||||
save-time errors, matching local `pmacs FILE`.
|
save-time errors, matching local `pmacs FILE`.
|
||||||
- `PermissionDenied`, `IsADirectory`, invalid path bytes at the OS boundary,
|
- `PermissionDenied`, invalid path bytes at the OS boundary, and other
|
||||||
and other non-`NotFound` errors fail startup.
|
non-`NotFound` errors fail startup.
|
||||||
|
- **`IsADirectory` is superseded by Journey Stage 1a**
|
||||||
|
(`docs/journey-stage1a-framing.md`). A directory no longer reaches the
|
||||||
|
load at all: `resolve_target_buffer` answers `ResolvedTarget::Directory`
|
||||||
|
ahead of it, so a directory target now *succeeds*, dispatching the
|
||||||
|
`path.open-directory` chain and replying `Opened`. Deliberate
|
||||||
|
supersession, not drift — the whole point of that stage is that
|
||||||
|
`pmacs .` must not exit 1, and a daemon/GPU bootstrap that still failed
|
||||||
|
would leave the two entry points disagreeing about the same argument.
|
||||||
|
Non-directory failures are unchanged.
|
||||||
- The buffer display name may use `Path::display()` and therefore replacement
|
- The buffer display name may use `Path::display()` and therefore replacement
|
||||||
characters; this must never replace the raw backing path used for dedup,
|
characters; this must never replace the raw backing path used for dedup,
|
||||||
load, or save.
|
load, or save.
|
||||||
|
|
@ -550,12 +559,17 @@ process behavior.
|
||||||
9. **New file:** a nonexistent target produces an empty snapshot, `[new file]`
|
9. **New file:** a nonexistent target produces an empty snapshot, `[new file]`
|
||||||
status/path identity, accepts an edit/save through the real session, and
|
status/path identity, accepts an edit/save through the real session, and
|
||||||
creates the requested file under the launcher cwd—not the daemon cwd.
|
creates the requested file under the launcher cwd—not the daemon cwd.
|
||||||
10. **Open error:** a directory/permission-denied target returns a specific
|
10. **Open error:** a permission-denied target returns a specific
|
||||||
failure before ready/window creation and makes root fail. The daemon shuts
|
failure before ready/window creation and makes root fail. The daemon shuts
|
||||||
down that failed session's socket; a client that lingers or sends another
|
down that failed session's socket; a client that lingers or sends another
|
||||||
event cannot reach uninstalled session state. An existing daemon remains
|
event cannot reach uninstalled session state. An existing daemon remains
|
||||||
connectable; a pre-existing frontend's active buffer and contents remain
|
connectable; a pre-existing frontend's active buffer and contents remain
|
||||||
unchanged.
|
unchanged.
|
||||||
|
**Amended by Journey Stage 1a:** the *directory* case is deliberately
|
||||||
|
superseded and moved to the success path — see Q#GT6. A directory
|
||||||
|
target now reaches ready and the document window shows dired, pinned
|
||||||
|
by `initial_target_directory_reaches_ready` and its two siblings in
|
||||||
|
`src/daemon.rs`. Permission-denied is unchanged and still fails.
|
||||||
11. **Dedup preserves unsaved edits:** frontend A opens and modifies a file
|
11. **Dedup preserves unsaved edits:** frontend A opens and modifies a file
|
||||||
without saving; target-launch frontend B opens the same normalized path and
|
without saving; target-launch frontend B opens the same normalized path and
|
||||||
receives A's authoritative unsaved text with the same `BufferId`, not disk
|
receives A's authoritative unsaved text with the same `BufferId`, not disk
|
||||||
|
|
|
||||||
|
|
@ -114,6 +114,39 @@ acceptance tests), §20 Priority 1.**
|
||||||
it asserted nothing about `run`. Q#JR12 is downgraded to an
|
it asserted nothing about `run`. Q#JR12 is downgraded to an
|
||||||
observation.
|
observation.
|
||||||
|
|
||||||
|
- rev 7 (2026-07-26) — **found while writing the `commit_to` suite and
|
||||||
|
bite-testing it.** Three, all confirmed:
|
||||||
|
- **N4 did not pin what its comment claimed.** Deleting the
|
||||||
|
`ScopedFrontend` arm from `acting_frontend` left N4 green, because
|
||||||
|
`ScopedFrontend::enter` *also* swaps `core.active_frontend` and the
|
||||||
|
ambient fallback then answers correctly on its own. The arm is
|
||||||
|
load-bearing in exactly one situation — a commit reached from inside
|
||||||
|
an interactive command, where the origin sits between the override
|
||||||
|
and the ambient value and would otherwise win. **N4b** is added,
|
||||||
|
driven through `dispatch_key` (the only thing that establishes an
|
||||||
|
interactive origin), and the mutation now bites it. The general
|
||||||
|
lesson is the §6.0 one again from a new angle: two mechanisms that
|
||||||
|
agree on the common path make either one look load-bearing.
|
||||||
|
- **`commit_to`'s forged-destination message was unreachable.** With
|
||||||
|
the parameter typed `mlua::AnyUserData`, mlua rejected a table during
|
||||||
|
argument conversion, so a caller who fabricated one got "error
|
||||||
|
converting Lua table to userdata" — true, but naming neither the rule
|
||||||
|
nor how to obtain a real destination. The parameter is now
|
||||||
|
`mlua::Value` and the pointed message actually fires. The refusal is
|
||||||
|
unchanged; only its legibility is.
|
||||||
|
- **P1 and P2 also fail on full revert**, since `commit_to` does not
|
||||||
|
exist on the pre-image. §6.0's "legitimately green on the pre-image"
|
||||||
|
does not describe them. They stay in the P list because their
|
||||||
|
*discriminating* falsifier is the named mutation, not the revert: a
|
||||||
|
revert-only check cannot distinguish "validates" from "validates in
|
||||||
|
time", which is the entire claim. Noted at each pin rather than
|
||||||
|
silently mislabelled.
|
||||||
|
- Bite results recorded: mutation A (scope stops swapping
|
||||||
|
`core.active_frontend`) fails N6a and P3 and nothing else; mutation B
|
||||||
|
(preflight moved after the callback) fails P1 and P2 and nothing
|
||||||
|
else; mutation C (drop the `ScopedFrontend` arm) fails N4b and
|
||||||
|
nothing else.
|
||||||
|
|
||||||
---
|
---
|
||||||
|
|
||||||
## 0.5. Coherence impact (`COHERENCE.md` §20, required since #163)
|
## 0.5. Coherence impact (`COHERENCE.md` §20, required since #163)
|
||||||
|
|
@ -697,6 +730,14 @@ is **removed rather than recast**: it proved nothing N1 does not.
|
||||||
in **A's** captured window, and B's active buffer and window are
|
in **A's** captured window, and B's active buffer and window are
|
||||||
unchanged. Falsified by reverting `commit_to` to the ambient
|
unchanged. Falsified by reverting `commit_to` to the ambient
|
||||||
`switch_buffer`.
|
`switch_buffer`.
|
||||||
|
- **N4b — the scope outranks an *interactive origin*, added rev 7.** N4
|
||||||
|
alone does not pin `acting_frontend`'s ordering claim: with the
|
||||||
|
`ScopedFrontend` arm deleted, N4 still passes, because `enter` also
|
||||||
|
swaps `core.active_frontend`. The arm matters only when an interactive
|
||||||
|
origin is set, which sits between the override and the ambient value.
|
||||||
|
A command dispatched by frontend B calls `commit_to` with A's
|
||||||
|
destination; the commit must still land in A's window. Falsified by
|
||||||
|
deleting the arm, or by ordering it after the interactive origin.
|
||||||
- **N5** Bootstrap with a deliberately **non-scratch** LOCAL primary
|
- **N5** Bootstrap with a deliberately **non-scratch** LOCAL primary
|
||||||
document buffer: the reply's `buffer_id` is that buffer, and after
|
document buffer: the reply's `buffer_id` is that buffer, and after
|
||||||
quiescence the window shows dired (Q#JR9, §4.5).
|
quiescence the window shows dired (Q#JR9, §4.5).
|
||||||
|
|
@ -711,7 +752,11 @@ is **removed rather than recast**: it proved nothing N1 does not.
|
||||||
- **N6b — `commit_to` refuses a forged destination.** A Lua-constructed
|
- **N6b — `commit_to` refuses a forged destination.** A Lua-constructed
|
||||||
table with plausible `frontend`/`window`/`buffer` fields is rejected as
|
table with plausible `frontend`/`window`/`buffer` fields is rejected as
|
||||||
a type error, and userdata cannot be constructed from Lua (Q#JR14d).
|
a type error, and userdata cannot be constructed from Lua (Q#JR14d).
|
||||||
Falsified by accepting a table.
|
Falsified by accepting a table. *Rev 7:* the parameter is typed
|
||||||
|
`mlua::Value` and `commit_to` performs the check itself, so the refusal
|
||||||
|
names the rule — typed as `AnyUserData`, mlua rejected the table during
|
||||||
|
argument conversion with a message naming neither the rule nor the
|
||||||
|
remedy, leaving the pointed one unreachable.
|
||||||
- **N6c — a declining listener cannot redirect the destination.** Two
|
- **N6c — a declining listener cannot redirect the destination.** Two
|
||||||
listeners: the first receives `dest`, attempts mutation inside `pcall`,
|
listeners: the first receives `dest`, attempts mutation inside `pcall`,
|
||||||
observes the read-only rejection, and declines; the second verifies
|
observes the read-only rejection, and declines; the second verifies
|
||||||
|
|
@ -746,6 +791,13 @@ is **removed rather than recast**: it proved nothing N1 does not.
|
||||||
|
|
||||||
### 6.2 Preservation pins (P), each with its falsifying mutation
|
### 6.2 Preservation pins (P), each with its falsifying mutation
|
||||||
|
|
||||||
|
*Rev 7 correction:* **P1 and P2 also fail on full revert** — `commit_to`
|
||||||
|
does not exist on the pre-image, so §6.0's "legitimately green on the
|
||||||
|
pre-image" does not describe them. They stay here because their
|
||||||
|
*discriminating* falsifier is the named mutation: a revert-only check
|
||||||
|
cannot distinguish "validates" from "validates in time", which is their
|
||||||
|
entire claim. P3–P8 are preservation pins in the strict sense.
|
||||||
|
|
||||||
- **P1 — precondition failure is atomic (the blocker's negative half).**
|
- **P1 — precondition failure is atomic (the blocker's negative half).**
|
||||||
**Three** destination failures, each asserted the same way — after
|
**Three** destination failures, each asserted the same way — after
|
||||||
quiescence the buffer count is unchanged, **no dired buffer or handle
|
quiescence the buffer count is unchanged, **no dired buffer or handle
|
||||||
|
|
|
||||||
|
|
@ -370,7 +370,7 @@ pub(crate) fn install(lua: &Lua, core: &SharedCore, win: &Table) -> mlua::Result
|
||||||
"commit_to",
|
"commit_to",
|
||||||
lua.create_function(
|
lua.create_function(
|
||||||
move |lua,
|
move |lua,
|
||||||
(dest, body): (mlua::AnyUserData, mlua::Function)|
|
(dest, body): (mlua::Value, mlua::Function)|
|
||||||
-> mlua::Result<mlua::MultiValue> {
|
-> mlua::Result<mlua::MultiValue> {
|
||||||
// Journey Stage 1a (Q#JR14). Preflight FIRST, then
|
// Journey Stage 1a (Q#JR14). Preflight FIRST, then
|
||||||
// scope, then run. The ordering is the whole point:
|
// scope, then run. The ordering is the whole point:
|
||||||
|
|
@ -381,9 +381,21 @@ pub(crate) fn install(lua: &Lua, core: &SharedCore, win: &Table) -> mlua::Result
|
||||||
// mutations too late and leaves a hidden buffer
|
// mutations too late and leaves a hidden buffer
|
||||||
// behind, so every destination precondition is
|
// behind, so every destination precondition is
|
||||||
// checked before the callback is invoked at all.
|
// checked before the callback is invoked at all.
|
||||||
|
//
|
||||||
|
// Typed as `Value` rather than `AnyUserData` so this
|
||||||
|
// message is REACHABLE: with the narrower type mlua
|
||||||
|
// rejects a table during argument conversion, and a
|
||||||
|
// caller who fabricated one got "error converting Lua
|
||||||
|
// table to userdata" — true, but it names neither the
|
||||||
|
// rule nor how to get a real destination.
|
||||||
|
let dest = match &dest {
|
||||||
|
mlua::Value::UserData(userdata) => {
|
||||||
|
userdata.borrow::<super::DirectoryDestinationLua>().ok()
|
||||||
|
}
|
||||||
|
_ => None,
|
||||||
|
};
|
||||||
let dest = dest
|
let dest = dest
|
||||||
.borrow::<super::DirectoryDestinationLua>()
|
.ok_or_else(|| {
|
||||||
.map_err(|_| {
|
|
||||||
mlua::Error::runtime(
|
mlua::Error::runtime(
|
||||||
"pmacs.window.commit_to: expected a destination captured by \
|
"pmacs.window.commit_to: expected a destination captured by \
|
||||||
the editor (it cannot be constructed from Lua)",
|
the editor (it cannot be constructed from Lua)",
|
||||||
|
|
|
||||||
|
|
@ -27,14 +27,22 @@
|
||||||
//! distinction is load-bearing: an equivalence assertion between two
|
//! distinction is load-bearing: an equivalence assertion between two
|
||||||
//! implementations that already agree proves nothing about structural
|
//! implementations that already agree proves nothing about structural
|
||||||
//! reuse.
|
//! reuse.
|
||||||
|
//!
|
||||||
|
//! Two P pins here — P1 and P2 — *also* fail on full revert, since
|
||||||
|
//! `commit_to` does not exist on the pre-image. They are labelled P
|
||||||
|
//! because their discriminating falsifier is the named mutation: a
|
||||||
|
//! revert-only check cannot distinguish "validates" from "validates in
|
||||||
|
//! time", which is their entire claim. Each says so at its own site.
|
||||||
|
|
||||||
use std::path::Path;
|
use std::path::Path;
|
||||||
use std::time::{Duration, Instant};
|
use std::time::{Duration, Instant};
|
||||||
|
|
||||||
use crossterm::event::{KeyCode, KeyEvent, KeyEventKind, KeyEventState, KeyModifiers};
|
use crossterm::event::{KeyCode, KeyEvent, KeyEventKind, KeyEventState, KeyModifiers};
|
||||||
|
use pmacs::buffer::BufferId;
|
||||||
use pmacs::editor::EditorState;
|
use pmacs::editor::EditorState;
|
||||||
use pmacs::editor_core::normalize_buffer_path;
|
use pmacs::editor_core::normalize_buffer_path;
|
||||||
use pmacs::protocol::FrontendId;
|
use pmacs::protocol::FrontendId;
|
||||||
|
use pmacs::window::{FrontendView, Layout, Window, WindowId};
|
||||||
use tempfile::TempDir;
|
use tempfile::TempDir;
|
||||||
|
|
||||||
// ---------------------------------------------------------------------------
|
// ---------------------------------------------------------------------------
|
||||||
|
|
@ -129,6 +137,70 @@ fn buffer_count(s: &EditorState) -> usize {
|
||||||
s.core.borrow().registry.borrow().ids().len()
|
s.core.borrow().registry.borrow().ids().len()
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// The buffer a window currently shows, or `None` if it is not live.
|
||||||
|
fn buffer_in(s: &EditorState, window: WindowId) -> Option<BufferId> {
|
||||||
|
s.core.borrow().windows.get(&window).map(|w| w.buffer_id)
|
||||||
|
}
|
||||||
|
|
||||||
|
/// The window `LOCAL` currently has selected.
|
||||||
|
fn local_window(s: &EditorState) -> WindowId {
|
||||||
|
s.core
|
||||||
|
.borrow()
|
||||||
|
.views
|
||||||
|
.get(&FrontendId::LOCAL)
|
||||||
|
.expect("LOCAL view")
|
||||||
|
.active
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Register a second frontend with its own single-window layout,
|
||||||
|
/// mirroring `build_fresh_frontend_view` (the same helper shape
|
||||||
|
/// `bottom_panel_stage1_acceptance` uses).
|
||||||
|
fn attach_frontend(s: &EditorState, fid: FrontendId) -> WindowId {
|
||||||
|
let mut core = s.core.borrow_mut();
|
||||||
|
let buffer_id = core.active_buffer_id();
|
||||||
|
let text_view = {
|
||||||
|
let reg = core.registry.borrow();
|
||||||
|
pmacs::text_view::TextView::new(reg.get(buffer_id).expect("buffer"))
|
||||||
|
};
|
||||||
|
let win = WindowId::next();
|
||||||
|
core.windows
|
||||||
|
.insert(win, Window::new(win, buffer_id, text_view));
|
||||||
|
core.register_frontend_view(
|
||||||
|
fid,
|
||||||
|
FrontendView {
|
||||||
|
layout: Layout::single(win),
|
||||||
|
active: win,
|
||||||
|
fold_projection: true,
|
||||||
|
panel_capable: true,
|
||||||
|
frame_geometry: None,
|
||||||
|
panel_hidden: false,
|
||||||
|
},
|
||||||
|
);
|
||||||
|
win
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Drive the **real** chain far enough to obtain a genuine destination
|
||||||
|
/// and leave it in the Lua global `dest`.
|
||||||
|
///
|
||||||
|
/// The listener claims (returns `false`), so nothing is committed and no
|
||||||
|
/// fallback runs: what lands in `dest` is exactly the userdata dired
|
||||||
|
/// would have received, produced by the production capture rather than
|
||||||
|
/// fabricated. Nothing in the test suite can construct one — that is
|
||||||
|
/// N6b's whole subject.
|
||||||
|
fn capture_dest(s: &mut EditorState, dir: &Path) {
|
||||||
|
exec(
|
||||||
|
s,
|
||||||
|
"dest = nil
|
||||||
|
pmacs.hook.add('path.open-directory', function(_, d) dest = d return false end)",
|
||||||
|
);
|
||||||
|
s.open_directory_target(dir);
|
||||||
|
pump(s);
|
||||||
|
assert!(
|
||||||
|
eval::<bool>(s, "return dest ~= nil"),
|
||||||
|
"the chain must hand listeners a destination"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
/// Open through the **real** startup entry point, as `pmacs PATH` does.
|
/// Open through the **real** startup entry point, as `pmacs PATH` does.
|
||||||
fn launch(path: &Path) -> EditorState {
|
fn launch(path: &Path) -> EditorState {
|
||||||
let mut s = EditorState::open(path.to_path_buf()).expect("startup must not fail");
|
let mut s = EditorState::open(path.to_path_buf()).expect("startup must not fail");
|
||||||
|
|
@ -360,6 +432,597 @@ fn journey_a_raising_resolver_suppresses_the_fallback_and_reports() {
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
// ---------------------------------------------------------------------------
|
||||||
|
// The destination commit (`pmacs.window.commit_to`)
|
||||||
|
// ---------------------------------------------------------------------------
|
||||||
|
//
|
||||||
|
// The substrate half of Stage 1a. A directory listing settles a tick or
|
||||||
|
// more after the request, by which time the ambient frontend, selected
|
||||||
|
// window, and active buffer may all name something else — so the whole
|
||||||
|
// post-await commit runs against a destination captured at request time.
|
||||||
|
//
|
||||||
|
// `LOCAL` is the requesting frontend throughout, because
|
||||||
|
// `open_directory_target` is the local-startup seam; the daemon's
|
||||||
|
// non-`LOCAL` capture is pinned in `src/daemon.rs`, where the production
|
||||||
|
// caller lives. What varies here is what the *ambient* frontend is doing
|
||||||
|
// while the commit runs, which is exactly the misrouting the scope
|
||||||
|
// exists to prevent.
|
||||||
|
|
||||||
|
/// The frontend that competes for ambient authority in these tests.
|
||||||
|
const COMPETITOR: FrontendId = FrontendId(7);
|
||||||
|
|
||||||
|
/// **N4** — the commit lands in the *requesting* frontend's window even
|
||||||
|
/// though another frontend is the one dispatching.
|
||||||
|
///
|
||||||
|
/// The blocker's positive half. Falsified by reverting `commit_to` to an
|
||||||
|
/// ambient display: the file then appears in the competitor's window.
|
||||||
|
#[test]
|
||||||
|
fn commit_to_delivers_to_the_requesting_frontend_not_the_ambient_one() {
|
||||||
|
let td = project();
|
||||||
|
let mut s = EditorState::new();
|
||||||
|
exec(&s, "pmacs.lsp.config = {}");
|
||||||
|
capture_dest(&mut s, td.path());
|
||||||
|
|
||||||
|
let local_win = local_window(&s);
|
||||||
|
let other_win = attach_frontend(&s, COMPETITOR);
|
||||||
|
let other_before = buffer_in(&s, other_win);
|
||||||
|
|
||||||
|
// The competitor becomes the dispatching frontend while the work is
|
||||||
|
// "in flight" — the state a worker completion actually returns to.
|
||||||
|
s.core.borrow_mut().active_frontend = COMPETITOR;
|
||||||
|
|
||||||
|
let alpha = td.path().join("alpha.txt").display().to_string();
|
||||||
|
exec(
|
||||||
|
&s,
|
||||||
|
&format!(
|
||||||
|
"assert(pmacs.window.commit_to(dest, function()
|
||||||
|
pmacs.window.display_file({alpha:?})
|
||||||
|
end))"
|
||||||
|
),
|
||||||
|
);
|
||||||
|
|
||||||
|
assert_eq!(
|
||||||
|
buffer_in(&s, other_win),
|
||||||
|
other_before,
|
||||||
|
"the competing frontend's window must be untouched"
|
||||||
|
);
|
||||||
|
s.core.borrow_mut().active_frontend = FrontendId::LOCAL;
|
||||||
|
assert_eq!(
|
||||||
|
active_name(&s),
|
||||||
|
alpha,
|
||||||
|
"the commit must land in the requesting frontend's captured window"
|
||||||
|
);
|
||||||
|
assert_eq!(
|
||||||
|
local_window(&s),
|
||||||
|
local_win,
|
||||||
|
"and in that window, not a new one"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
/// **N4b** — the scope beats an *interactive origin*, not merely the
|
||||||
|
/// ambient frontend.
|
||||||
|
///
|
||||||
|
/// Found by bite-testing N4: with the `ScopedFrontend` arm deleted from
|
||||||
|
/// `acting_frontend`, N4 still passed, because `ScopedFrontend::enter`
|
||||||
|
/// also swaps `core.active_frontend` and the ambient fallback then
|
||||||
|
/// answers correctly on its own. The arm is load-bearing in exactly one
|
||||||
|
/// situation — a commit reached from inside an interactive command,
|
||||||
|
/// where the origin sits *between* the override and the ambient value
|
||||||
|
/// and would otherwise win. `acting_frontend`'s comment claims that
|
||||||
|
/// ordering; nothing pinned it.
|
||||||
|
///
|
||||||
|
/// Driven through `dispatch_key`, because the interactive origin is
|
||||||
|
/// established by dispatch and by nothing else — `invoke_interactive`
|
||||||
|
/// requires a context rather than creating one.
|
||||||
|
///
|
||||||
|
/// Falsified by deleting the `ScopedFrontend` arm from
|
||||||
|
/// `acting_frontend`, or by reordering it after the interactive origin.
|
||||||
|
#[test]
|
||||||
|
fn commit_to_outranks_an_interactive_origin() {
|
||||||
|
let td = project();
|
||||||
|
let mut s = EditorState::new();
|
||||||
|
exec(&s, "pmacs.lsp.config = {}");
|
||||||
|
capture_dest(&mut s, td.path());
|
||||||
|
|
||||||
|
let local_win = local_window(&s);
|
||||||
|
let other_win = attach_frontend(&s, COMPETITOR);
|
||||||
|
let other_before = buffer_in(&s, other_win);
|
||||||
|
|
||||||
|
let alpha = td.path().join("alpha.txt").display().to_string();
|
||||||
|
exec(
|
||||||
|
&s,
|
||||||
|
&format!(
|
||||||
|
"pmacs.command.define {{
|
||||||
|
name = 'test.journey-commit',
|
||||||
|
description = 'commit to a captured destination from inside a command',
|
||||||
|
fn = function()
|
||||||
|
committed = pmacs.window.commit_to(dest, function()
|
||||||
|
pmacs.window.display_file({alpha:?})
|
||||||
|
end)
|
||||||
|
end,
|
||||||
|
}}
|
||||||
|
pmacs.keymap.bind {{ scope = 'global', sequence = 'C-c j',
|
||||||
|
command = 'test.journey-commit' }}"
|
||||||
|
),
|
||||||
|
);
|
||||||
|
|
||||||
|
// The COMPETITOR runs the command, so ITS id is the interactive
|
||||||
|
// origin for the whole invocation.
|
||||||
|
s.dispatch_key(COMPETITOR, key(KeyCode::Char('c'), KeyModifiers::CONTROL));
|
||||||
|
s.dispatch_key(COMPETITOR, key(KeyCode::Char('j'), KeyModifiers::NONE));
|
||||||
|
|
||||||
|
assert!(
|
||||||
|
eval::<bool>(&s, "return committed"),
|
||||||
|
"the commit must be accepted"
|
||||||
|
);
|
||||||
|
assert_eq!(
|
||||||
|
buffer_in(&s, other_win),
|
||||||
|
other_before,
|
||||||
|
"the invoking frontend's own window must be untouched"
|
||||||
|
);
|
||||||
|
s.core.borrow_mut().active_frontend = FrontendId::LOCAL;
|
||||||
|
assert_eq!(
|
||||||
|
active_name(&s),
|
||||||
|
alpha,
|
||||||
|
"the commit must land in the captured destination, not the \
|
||||||
|
interactive origin's window"
|
||||||
|
);
|
||||||
|
assert_eq!(local_window(&s), local_win);
|
||||||
|
}
|
||||||
|
|
||||||
|
/// **N6a** — the scope is restored when the callback returns normally.
|
||||||
|
///
|
||||||
|
/// Falsified by dropping the guard's restore, or by never swapping
|
||||||
|
/// `core.active_frontend` in the first place (then `inside` reads the
|
||||||
|
/// competitor and the assertion fails from the other direction).
|
||||||
|
#[test]
|
||||||
|
fn commit_to_scopes_and_restores_on_a_normal_return() {
|
||||||
|
let td = project();
|
||||||
|
let mut s = EditorState::new();
|
||||||
|
exec(&s, "pmacs.lsp.config = {}");
|
||||||
|
capture_dest(&mut s, td.path());
|
||||||
|
attach_frontend(&s, COMPETITOR);
|
||||||
|
s.core.borrow_mut().active_frontend = COMPETITOR;
|
||||||
|
|
||||||
|
exec(
|
||||||
|
&s,
|
||||||
|
"inside, scoped = nil, nil
|
||||||
|
assert(pmacs.window.commit_to(dest, function()
|
||||||
|
inside = pmacs.frontend.id()
|
||||||
|
scoped = pmacs._async._in_commit_scope()
|
||||||
|
end))",
|
||||||
|
);
|
||||||
|
|
||||||
|
assert_eq!(
|
||||||
|
eval::<i64>(&s, "return inside"),
|
||||||
|
i64::try_from(FrontendId::LOCAL.0).expect("frontend id"),
|
||||||
|
"inside the commit the acting frontend is the requesting one"
|
||||||
|
);
|
||||||
|
assert!(
|
||||||
|
eval::<bool>(&s, "return scoped"),
|
||||||
|
"and the commit-scope flag is set while the callback runs"
|
||||||
|
);
|
||||||
|
assert_eq!(
|
||||||
|
s.core.borrow().active_frontend,
|
||||||
|
COMPETITOR,
|
||||||
|
"the ambient frontend must be restored on return"
|
||||||
|
);
|
||||||
|
assert!(
|
||||||
|
!eval::<bool>(&s, "return pmacs._async._in_commit_scope()"),
|
||||||
|
"and the commit-scope flag cleared"
|
||||||
|
);
|
||||||
|
assert_eq!(
|
||||||
|
eval::<i64>(&s, "return pmacs.frontend.id()"),
|
||||||
|
i64::try_from(COMPETITOR.0).expect("frontend id"),
|
||||||
|
"the Lua-visible frontend must be restored too"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
/// **N6b (part of N6)** — a raising callback still restores.
|
||||||
|
///
|
||||||
|
/// The path that makes the guard RAII rather than a pair of statements:
|
||||||
|
/// `commit_to` captures the call's result and lets the guard drop before
|
||||||
|
/// propagating it. Falsified by `?`-propagating the callback's error
|
||||||
|
/// through the scope, or by restoring on the success path only.
|
||||||
|
#[test]
|
||||||
|
fn commit_to_restores_when_the_callback_raises() {
|
||||||
|
let td = project();
|
||||||
|
let mut s = EditorState::new();
|
||||||
|
exec(&s, "pmacs.lsp.config = {}");
|
||||||
|
capture_dest(&mut s, td.path());
|
||||||
|
attach_frontend(&s, COMPETITOR);
|
||||||
|
s.core.borrow_mut().active_frontend = COMPETITOR;
|
||||||
|
|
||||||
|
exec(
|
||||||
|
&s,
|
||||||
|
"local ok, err = pcall(pmacs.window.commit_to, dest, function()
|
||||||
|
error('commit exploded')
|
||||||
|
end)
|
||||||
|
raised = (not ok) and tostring(err) or '<no raise>'",
|
||||||
|
);
|
||||||
|
|
||||||
|
assert!(
|
||||||
|
eval::<String>(&s, "return raised").contains("commit exploded"),
|
||||||
|
"the callback's error must propagate"
|
||||||
|
);
|
||||||
|
assert_eq!(
|
||||||
|
s.core.borrow().active_frontend,
|
||||||
|
COMPETITOR,
|
||||||
|
"a raising callback must still restore the ambient frontend"
|
||||||
|
);
|
||||||
|
assert!(
|
||||||
|
!eval::<bool>(&s, "return pmacs._async._in_commit_scope()"),
|
||||||
|
"and must still clear the commit-scope flag"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
/// **N6c (part of N6)** — awaiting inside a commit is refused, the
|
||||||
|
/// refusal names the rule, and the scope is restored anyway.
|
||||||
|
///
|
||||||
|
/// A yield would restore the scope while the coroutine is still parked,
|
||||||
|
/// so the rest of the commit would resume ambient — silently
|
||||||
|
/// reintroducing exactly the misrouting N4 pins against. Driven inside
|
||||||
|
/// `pmacs.async`, which is where a real await lives.
|
||||||
|
///
|
||||||
|
/// Falsified by dropping the `_in_commit_scope` check from
|
||||||
|
/// `Handle:await`: the await then succeeds and `refusal` reads
|
||||||
|
/// `<no raise>`.
|
||||||
|
#[test]
|
||||||
|
fn commit_to_refuses_an_await_and_restores() {
|
||||||
|
let td = project();
|
||||||
|
let mut s = EditorState::new();
|
||||||
|
exec(&s, "pmacs.lsp.config = {}");
|
||||||
|
capture_dest(&mut s, td.path());
|
||||||
|
attach_frontend(&s, COMPETITOR);
|
||||||
|
s.core.borrow_mut().active_frontend = COMPETITOR;
|
||||||
|
|
||||||
|
exec(
|
||||||
|
&s,
|
||||||
|
&format!(
|
||||||
|
"refusal = nil
|
||||||
|
pmacs.async(function()
|
||||||
|
local handle = pmacs.fs.read_dir({:?})
|
||||||
|
local ok, err = pcall(pmacs.window.commit_to, dest, function()
|
||||||
|
return handle:await()
|
||||||
|
end)
|
||||||
|
refusal = (not ok) and tostring(err) or '<no raise>'
|
||||||
|
-- Drain it OUTSIDE the commit, which is where the refusal
|
||||||
|
-- says the await belongs -- and which also settles the job
|
||||||
|
-- so the pump can reach quiescence.
|
||||||
|
handle:await()
|
||||||
|
end)",
|
||||||
|
td.path().display().to_string()
|
||||||
|
),
|
||||||
|
);
|
||||||
|
pump(&mut s);
|
||||||
|
|
||||||
|
let refusal: String = eval(&s, "return refusal");
|
||||||
|
assert!(
|
||||||
|
refusal.contains("cannot await inside") && refusal.contains("commit_to"),
|
||||||
|
"the refusal must name the rule it enforces; got {refusal:?}"
|
||||||
|
);
|
||||||
|
assert_eq!(
|
||||||
|
s.core.borrow().active_frontend,
|
||||||
|
COMPETITOR,
|
||||||
|
"a refused await must still restore the ambient frontend"
|
||||||
|
);
|
||||||
|
assert!(
|
||||||
|
!eval::<bool>(&s, "return pmacs._async._in_commit_scope()"),
|
||||||
|
"and must still clear the commit-scope flag"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
/// **N6b** — a forged destination is rejected, and the callback never
|
||||||
|
/// runs.
|
||||||
|
///
|
||||||
|
/// A plausible `{frontend, window, buffer}` table is what any Lua could
|
||||||
|
/// fabricate. Falsified by accepting a table, or by borrowing the
|
||||||
|
/// userdata after invoking the callback.
|
||||||
|
#[test]
|
||||||
|
fn commit_to_refuses_a_forged_destination() {
|
||||||
|
let td = project();
|
||||||
|
let mut s = EditorState::new();
|
||||||
|
exec(&s, "pmacs.lsp.config = {}");
|
||||||
|
capture_dest(&mut s, td.path());
|
||||||
|
|
||||||
|
let win = eval::<i64>(&s, "return dest:window()");
|
||||||
|
exec(
|
||||||
|
&s,
|
||||||
|
&format!(
|
||||||
|
"ran = false
|
||||||
|
local ok, err = pcall(pmacs.window.commit_to,
|
||||||
|
{{ frontend = 0, window = {win}, buffer = 0 }},
|
||||||
|
function() ran = true end)
|
||||||
|
rejected = (not ok) and tostring(err) or '<accepted>'"
|
||||||
|
),
|
||||||
|
);
|
||||||
|
|
||||||
|
let rejected: String = eval(&s, "return rejected");
|
||||||
|
assert!(
|
||||||
|
rejected.contains("cannot be constructed from Lua"),
|
||||||
|
"a forged table must be rejected by type, not merely fail later; got {rejected:?}"
|
||||||
|
);
|
||||||
|
assert!(
|
||||||
|
!eval::<bool>(&s, "return ran"),
|
||||||
|
"a rejected destination must not reach the callback"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
/// **N6c** — a declining listener cannot redirect the destination.
|
||||||
|
///
|
||||||
|
/// The same userdata is handed to every listener in turn. As a table, an
|
||||||
|
/// earlier listener could rewrite the window and then decline, sending
|
||||||
|
/// the fallback somewhere the user never asked for. Falsified by passing
|
||||||
|
/// a shared mutable table.
|
||||||
|
#[test]
|
||||||
|
fn a_declining_listener_cannot_redirect_the_destination() {
|
||||||
|
let td = project();
|
||||||
|
let mut s = EditorState::new();
|
||||||
|
exec(&s, "pmacs.lsp.config = {}");
|
||||||
|
let target = local_window(&s);
|
||||||
|
|
||||||
|
exec(
|
||||||
|
&s,
|
||||||
|
"seen_first, seen_second, mutation = nil, nil, nil
|
||||||
|
pmacs.hook.add('path.open-directory', function(_, d)
|
||||||
|
seen_first = d:window()
|
||||||
|
-- Try to redirect, then decline. Both halves matter: a
|
||||||
|
-- successful mutation with a decline is the attack.
|
||||||
|
local ok, err = pcall(function() d.window = 999 end)
|
||||||
|
mutation = (not ok) and tostring(err) or '<mutated>'
|
||||||
|
end)
|
||||||
|
pmacs.hook.add('path.open-directory', function(_, d)
|
||||||
|
seen_second = d:window()
|
||||||
|
end)",
|
||||||
|
);
|
||||||
|
|
||||||
|
s.open_directory_target(td.path());
|
||||||
|
pump(&mut s);
|
||||||
|
|
||||||
|
let mutation: String = eval(&s, "return mutation");
|
||||||
|
assert!(
|
||||||
|
!mutation.contains("<mutated>"),
|
||||||
|
"the destination must be read-only; got {mutation:?}"
|
||||||
|
);
|
||||||
|
let first = eval::<i64>(&s, "return seen_first");
|
||||||
|
let second = eval::<i64>(&s, "return seen_second");
|
||||||
|
assert_eq!(
|
||||||
|
first, second,
|
||||||
|
"every listener must see the same, unaltered destination"
|
||||||
|
);
|
||||||
|
assert_eq!(
|
||||||
|
u64::try_from(second).expect("window id"),
|
||||||
|
target.raw(),
|
||||||
|
"and it must still name the window the editor captured"
|
||||||
|
);
|
||||||
|
// And the fallback commits THERE, not to whatever the first listener
|
||||||
|
// wanted -- the observable the attack was aiming at.
|
||||||
|
assert!(
|
||||||
|
active_name(&s).starts_with("*dired:"),
|
||||||
|
"the declined chain must still fall back to dired"
|
||||||
|
);
|
||||||
|
assert_eq!(
|
||||||
|
buffer_in(&s, target),
|
||||||
|
Some(eval::<pmacs::lua_bindings::BufferIdLua>(&s, "return pmacs.window.buffer()").0),
|
||||||
|
"in the captured window"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
// --- the commit's preservation pins ---------------------------------------
|
||||||
|
|
||||||
|
/// **P1** — every destination precondition is checked *before* the
|
||||||
|
/// callback runs, so a failure mutates nothing.
|
||||||
|
///
|
||||||
|
/// Four refusals, each asserted the same way: `commit_to` returns
|
||||||
|
/// `(false, reason)`, the callback never ran, and no buffer was created.
|
||||||
|
/// Table-driven deliberately — the failure message names which
|
||||||
|
/// precondition regressed, which four separate near-identical tests
|
||||||
|
/// would give up in exchange for nothing.
|
||||||
|
///
|
||||||
|
/// *Mutation:* move the preflight from before the callback to after it
|
||||||
|
/// (rev 2's design, which validated at display time). All four fail.
|
||||||
|
/// *Second mutation, for the dedicated case:* pass `Some(dest.buffer)`
|
||||||
|
/// instead of `None` to `window_accepts_buffer`. Only that case fails —
|
||||||
|
/// which is why it is listed separately from the stale-buffer case it
|
||||||
|
/// otherwise resembles.
|
||||||
|
///
|
||||||
|
/// **Also fails on full revert**, since `commit_to` does not exist on the
|
||||||
|
/// pre-image. It is listed as a P because the discriminating falsifier is
|
||||||
|
/// the named mutation, not the revert: a revert-only check would not
|
||||||
|
/// distinguish "validates" from "validates in time".
|
||||||
|
#[test]
|
||||||
|
fn preservation_a_failed_precondition_never_reaches_the_callback() {
|
||||||
|
// (label, Lua that breaks the precondition, expected reason fragment)
|
||||||
|
let cases: [(&str, &str, &str); 4] = [
|
||||||
|
(
|
||||||
|
"frontend gone",
|
||||||
|
// Handled in Rust below: unregistering a view has no Lua surface.
|
||||||
|
"",
|
||||||
|
"requesting frontend is gone",
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"window gone",
|
||||||
|
"local doomed = dest:window()
|
||||||
|
pmacs.window.split_horizontal()
|
||||||
|
while pmacs.window.current() == doomed do pmacs.window.focus_next() end
|
||||||
|
pmacs.window.close_others()",
|
||||||
|
"is gone",
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"stale buffer",
|
||||||
|
"pmacs.window.switch_buffer(pmacs.buffer.create('*usurper*'))",
|
||||||
|
"now shows another buffer",
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"dedicated",
|
||||||
|
"pmacs.window.set_params(dest:window(), { dedicated = true })",
|
||||||
|
"is dedicated",
|
||||||
|
),
|
||||||
|
];
|
||||||
|
|
||||||
|
for (label, break_it, expected) in cases {
|
||||||
|
let td = project();
|
||||||
|
let mut s = EditorState::new();
|
||||||
|
exec(&s, "pmacs.lsp.config = {}");
|
||||||
|
capture_dest(&mut s, td.path());
|
||||||
|
|
||||||
|
if label == "frontend gone" {
|
||||||
|
s.core
|
||||||
|
.borrow_mut()
|
||||||
|
.unregister_frontend_view(FrontendId::LOCAL);
|
||||||
|
} else {
|
||||||
|
exec(&s, break_it);
|
||||||
|
}
|
||||||
|
let before = buffer_count(&s);
|
||||||
|
|
||||||
|
exec(
|
||||||
|
&s,
|
||||||
|
"ran = false
|
||||||
|
ok, reason = pmacs.window.commit_to(dest, function() ran = true end)",
|
||||||
|
);
|
||||||
|
|
||||||
|
assert!(
|
||||||
|
!eval::<bool>(&s, "return ok"),
|
||||||
|
"{label}: commit_to must refuse"
|
||||||
|
);
|
||||||
|
let reason: String = eval(&s, "return tostring(reason)");
|
||||||
|
assert!(
|
||||||
|
reason.contains(expected),
|
||||||
|
"{label}: reason must say why; wanted {expected:?}, got {reason:?}"
|
||||||
|
);
|
||||||
|
assert!(
|
||||||
|
!eval::<bool>(&s, "return ran"),
|
||||||
|
"{label}: the callback must not run at all -- validating after it \
|
||||||
|
is four mutations too late"
|
||||||
|
);
|
||||||
|
assert_eq!(
|
||||||
|
buffer_count(&s),
|
||||||
|
before,
|
||||||
|
"{label}: a refused commit must create no buffer"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// **P2 — stale intent loses**, through dired's real commit path.
|
||||||
|
///
|
||||||
|
/// The user replaced the destination window's buffer while the listing
|
||||||
|
/// was in flight. Their action is newer information than the request, so
|
||||||
|
/// the request loses: dired refuses, their buffer survives, and no dired
|
||||||
|
/// buffer or handle is left behind for that path.
|
||||||
|
///
|
||||||
|
/// P1 pins the preflight in isolation; this drives `pmacs.dired.open`
|
||||||
|
/// with a captured destination — the same call the handler makes — so
|
||||||
|
/// the atomicity claim is asserted where the four mutations actually
|
||||||
|
/// live.
|
||||||
|
///
|
||||||
|
/// *Mutation:* drop the `dest.buffer` comparison from the preflight
|
||||||
|
/// (window-only validation). The dired buffer then replaces the user's.
|
||||||
|
#[test]
|
||||||
|
fn preservation_a_stale_destination_loses_to_the_users_newer_buffer() {
|
||||||
|
let td = project();
|
||||||
|
let mut s = EditorState::new();
|
||||||
|
exec(&s, "pmacs.lsp.config = {}");
|
||||||
|
capture_dest(&mut s, td.path());
|
||||||
|
let target = local_window(&s);
|
||||||
|
|
||||||
|
// The user switches the destination window while the work is in flight.
|
||||||
|
exec(
|
||||||
|
&s,
|
||||||
|
"usurper = pmacs.buffer.create('*usurper*')
|
||||||
|
pmacs.window.switch_buffer(usurper)",
|
||||||
|
);
|
||||||
|
let usurper = buffer_in(&s, target);
|
||||||
|
let before = buffer_count(&s);
|
||||||
|
|
||||||
|
exec(
|
||||||
|
&s,
|
||||||
|
&format!(
|
||||||
|
"failure = nil
|
||||||
|
pmacs.async(function()
|
||||||
|
local ok, err = pcall(pmacs.dired.open, {:?}, {{ dest = dest }})
|
||||||
|
failure = (not ok) and tostring(err) or '<committed>'
|
||||||
|
end)",
|
||||||
|
canon(td.path())
|
||||||
|
),
|
||||||
|
);
|
||||||
|
pump(&mut s);
|
||||||
|
|
||||||
|
let failure: String = eval(&s, "return failure");
|
||||||
|
assert!(
|
||||||
|
failure.contains("destination is gone"),
|
||||||
|
"dired must report the refusal rather than commit; got {failure:?}"
|
||||||
|
);
|
||||||
|
assert_eq!(
|
||||||
|
buffer_in(&s, target),
|
||||||
|
usurper,
|
||||||
|
"the user's newer buffer must survive"
|
||||||
|
);
|
||||||
|
assert_eq!(
|
||||||
|
buffer_count(&s),
|
||||||
|
before,
|
||||||
|
"and no dired buffer may be left behind"
|
||||||
|
);
|
||||||
|
assert_eq!(
|
||||||
|
active_name(&s),
|
||||||
|
"*usurper*",
|
||||||
|
"nor may the refusal change what is displayed"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
/// **P3** — dired reads its `prev` inside the scope, so `q` returns to
|
||||||
|
/// the *destination* window's buffer, not the ambient frontend's.
|
||||||
|
///
|
||||||
|
/// `handle.prev` is captured with `pmacs.window.buffer()`, whose no-arg
|
||||||
|
/// arm reads the core's ambient `active_buffer_id()`. That is precisely
|
||||||
|
/// why the scope swaps `core.active_frontend` and not only the override:
|
||||||
|
/// a scope that swapped the override alone would leave this one line
|
||||||
|
/// reading the competitor's buffer, and `q` would drop the user into a
|
||||||
|
/// buffer from another frontend's window.
|
||||||
|
///
|
||||||
|
/// Asserted through `q` rather than by reaching into dired's handle
|
||||||
|
/// table — `prev`'s entire meaning is where `q` lands.
|
||||||
|
///
|
||||||
|
/// *Mutation:* stop swapping `core.active_frontend` in
|
||||||
|
/// `ScopedFrontend::enter` (keep the override). `q` then lands in
|
||||||
|
/// `*competitor*`.
|
||||||
|
#[test]
|
||||||
|
fn preservation_dired_captures_prev_from_the_destination_not_the_ambient_frontend() {
|
||||||
|
let td = project();
|
||||||
|
let mut s = EditorState::new();
|
||||||
|
exec(&s, "pmacs.lsp.config = {}");
|
||||||
|
|
||||||
|
let target = local_window(&s);
|
||||||
|
let origin = buffer_in(&s, target).expect("the startup buffer");
|
||||||
|
|
||||||
|
// A competitor whose window shows a buffer of its own, ambient while
|
||||||
|
// the listing settles.
|
||||||
|
let other_win = attach_frontend(&s, COMPETITOR);
|
||||||
|
let competitor_buffer =
|
||||||
|
eval::<pmacs::lua_bindings::BufferIdLua>(&s, "return pmacs.buffer.create('*competitor*')")
|
||||||
|
.0;
|
||||||
|
s.core
|
||||||
|
.borrow_mut()
|
||||||
|
.install_buffer_in_window(other_win, competitor_buffer)
|
||||||
|
.expect("install");
|
||||||
|
s.core.borrow_mut().active_frontend = COMPETITOR;
|
||||||
|
|
||||||
|
s.open_directory_target(td.path());
|
||||||
|
pump(&mut s);
|
||||||
|
s.core.borrow_mut().active_frontend = FrontendId::LOCAL;
|
||||||
|
assert!(
|
||||||
|
active_name(&s).starts_with("*dired:"),
|
||||||
|
"the listing must have committed"
|
||||||
|
);
|
||||||
|
|
||||||
|
type_char(&mut s, 'q');
|
||||||
|
assert_eq!(
|
||||||
|
buffer_in(&s, target),
|
||||||
|
Some(origin),
|
||||||
|
"`q` must return to the buffer the DESTINATION window showed, not \
|
||||||
|
the ambient frontend's"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
// ---------------------------------------------------------------------------
|
// ---------------------------------------------------------------------------
|
||||||
// Step 5 — edit immediately
|
// Step 5 — edit immediately
|
||||||
// ---------------------------------------------------------------------------
|
// ---------------------------------------------------------------------------
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue