Commit Graph

890 Commits

Author SHA1 Message Date
Levi Neuwirth 8b457de878 docs: record the post-integration gate run
Separates the pre-integration numbers, which described a tree 28 commits
behind, from the ones that describe what the PR now proposes.

The GPU test count is the integration proof rather than merely a pass: it
went 199 to 202, and e547a90 added exactly three tests to pmacs-gpu,
which is the entire delta on main since the merge base. Both sides' tests
are therefore present and running, and neither was dropped by the
auto-merge. Confirmed structurally as well -- main's fix survives as the
deferred closure form rather than the eager one that panicked, with its
regression test, alongside this lane's math work in the same file.
2026-07-25 14:37:15 -04:00
Levi Neuwirth f3e065dc78 Merge canonical main (8c86d34) into the inline-math slice
The lane was 28 commits behind. Merged rather than rebased, per the
#135/#137 precedent: the PR is awaiting review rounds and a rebase would
break every review anchor.

The only conflict was docs/active-work.md, where both sides add lanes.
Kept both: main's lanes verbatim, with this lane leading since it is the
one in flight. The conflict was pre-existing rather than introduced by
the dired or Lean 4 ledger commits -- it already conflicted against main
at e745068.

The integration surface, derived from git diff merge-base..main rather
than from another PR's file list, is pmacs-gpu/src/main.rs: main gained
72 lines there from e547a90, the minimap all-blank-slab divide-by-zero
fix, and this lane rewrites large parts of the same file. Git auto-merged
it textually. A clean auto-merge is not evidence the tree compiles, so
the full gate suite is what discharges it; the ledger records the
post-integration numbers separately from the pre-integration ones, which
described a tree 28 commits behind.
2026-07-25 14:32:48 -04:00
Levi Neuwirth b5bea3b2f5 docs(coherence): record the dead reporting channel and #161's slice
Rides this PR per COHERENCE.md §25 ("when a PR changes any audited claim
here, updating this file rides that PR").

§0 and §7: multi-root LSP affinity moves from in-flight-branch to PR
#161, and §7 gains the rule the slice actually establishes — a
*fallback* root is deliberately NOT an identity, so markerless files
keep sharing one server per language. That is the part a reader would
otherwise assume went the other way.

§1.2 gains the finding this PR turned up, which sharpens the audit
rather than restating it. The section recorded that background failures
produce "no `*errors*` entry"; the sharper fact is that **the channel
does not exist**. Fifteen call sites — `async.lua` (5), `syntax.lua`
(4), and one each in `lsp.lua`, `mcp.lua`, `fs.lua`, `editops.lua`,
`autosave.lua`, `commands/default.lua` — report through `pmacs.error`,
each guarded `if pmacs.error then ...`. It is defined nowhere in
production; the only assignment in the tree is a test stub
(`src/editor.rs:9881`), and `type(pmacs.error)` is nil in a fresh
`EditorState` (probed, not inferred). `pmacs.errors` plural in
compile.lua is an unrelated namespace. All fifteen are dead, and the
guard is what kept it unnoticed — it makes the silence read as
deliberate.

Hence the corollary now recorded beside the rule: report through a
channel with a **test that observes it**, or the guard is
indistinguishable from the silence it was meant to fix.

Also a frequency note: per-root affinity makes the
preconfigured-but-missing-server failure fire once per project root
rather than once per language per session. Unchanged in kind, strictly
more frequent. Surfacing it stays Priority 1 work needing its own
framing — it is user-visible product behavior (what message, where,
with what guidance), not a substrate fix to smuggle into an affinity PR.

Line-number citations in the touched sections re-verified per §25;
symbols are authoritative where they drifted.
2026-07-25 14:28:56 -04:00
Levi Neuwirth 3952db9657 Merge remote-tracking branch 'githubsucks/main' into HEAD 2026-07-25 14:26:21 -04:00
Levi Neuwirth ebcd2c4f6f fix(lsp): attribute a failing root resolver (COHERENCE §1.2)
COHERENCE.md §1.2 makes "a `pcall` around background wiring must log
attributed failure, never discard it" a standing rule, and names
`ensure_server`'s swallowed spawn failure as its canonical case — the
exact function this branch modifies. Round 1 deferred the resolver's
silent `pcall` as a Stage 3 concern. Under that rule it is not a
deferral, it is a fresh instance of the named anti-pattern added by a PR
touching the cited function, made worse by the memo: a raised error is
buried permanently for that directory and never observed again.

A resolver that raises, or returns a non-string non-nil, now leaves an
attributed trace naming the language and the directory. Returning nil
remains the documented decline and stays silent — pinned, so "report
failures" cannot be satisfied by reporting every resolution.

The report goes through `pmacs.editor.set_status`, NOT `pmacs.error`,
and that choice is the finding:

**`pmacs.error` does not exist.** Fifteen call sites across `async.lua`
(5), `syntax.lua` (4), `lsp.lua`, `mcp.lua`, `fs.lua`, `editops.lua`,
`autosave.lua`, and `commands/default.lua` report background failures
through it, each guarded `if pmacs.error then ...`. It is defined
nowhere in production; the only assignment in the tree is a test stub at
`src/editor.rs:9881`, and `type(pmacs.error)` is nil in a fresh
`EditorState` (probed, not inferred). `pmacs.errors` (plural) in
compile.lua is an unrelated namespace. So all fifteen reports are dead,
and the guard makes the silence look deliberate — which is why nobody
noticed. Writing the test is what caught it: the first version of this
fix used `pmacs.error` and its pin failed against a working
implementation.

Both bites recorded: dropping the report entirely fails the pin, and so
does reporting ONLY through `pmacs.error` — the dead-channel variant
this nearly shipped.

Not fixed here, deliberately: defining `pmacs.error`, the fifteen dead
sites, and surfacing the spawn failure itself. That last is Priority 1
work and a user-visible product behavior — what message, where, with
what guidance — so it needs its own framing rather than being smuggled
into an affinity PR.
2026-07-25 14:24:59 -04:00
Levi Neuwirth 8c86d344c3
Merge pull request #164 from levineuwirth/dired-framing
docs: dired arc framing (revision 5) + post-merge doc refresh
2026-07-25 18:21:03 +00:00
Levi Neuwirth 7c01c93226 docs: dired arc framing (revision 5) + post-merge doc refresh
Lands the approved dired framing on main as its own docs PR, and brings
the two required docs current after find-file merged as #162.

The framing was approved after two review rounds (seven findings, then
six) and revised twice more since: revision 4 recorded what implementing
Stage 0 falsified in the approved text, and revision 5 adds the coherence
impact statement that #163 made mandatory for every framing.

The coherence statement is new work, not a restatement. COHERENCE.md
section 20 Priority 1 already names this arc -- a find-file surface and
directory-argument handling -- so the framing now states which journey
steps it touches (7, and partially 3), that it adds no interaction island
because its keys are a mode-scoped keymap through the ordinary registry
and wdired is a mode swap rather than a modal layer, that it adopts the
config registry for dired.kill-when-opening, and that it inherits the
worker-attribution gap for its read_dir jobs without worsening it. It
also draws the boundary against the adjacent Journey Stage 1 arc: CLI
directory handling belongs there, the two meet at resolve_target_buffer,
and dired supplies the buffer a directory should resolve to rather than
growing a second directory surface.

One convergence worth recording: section 2 grades the golden journey
broken at step 3 because pmacs on a directory exits 1, and the mechanism
it cites -- File::open succeeding on a directory, then read_to_end
returning EISDIR -- is the same one Stage 0 pinned in its
accepting-a-directory test, where the pcall turns it into a status
message instead.

The handoff snapshot was stale through eight merges. It now anchors on
main at 2af1ab3, records COHERENCE.md as required reading and a required
framing input, and carries the two minibuffer facts find-file
established: a custom completion source cannot descend directories, and
a selected candidate shadows typed text -- both of which apply to M-x and
switch-buffer, not just find-file.

The ledger gains the dired lane with Stage 1's scope, the reason its one
Rust change cannot be done in Lua, and the rebase note for the dired
branch, whose framing commits become redundant when this lands.
2026-07-25 14:09:49 -04:00
Levi Neuwirth 2af1ab34a6
Merge pull request #162 from levineuwirth/find-file
feat(find-file): open a file by path with C-x C-f (dired arc Stage 0)
2026-07-25 18:03:18 +00:00
Levi Neuwirth 90ccda0c29
Merge pull request #163 from levineuwirth/coherence-doc
docs: add COHERENCE.md as a required doc
2026-07-25 15:38:02 +00:00
Levi Neuwirth 066b8652b8 docs: add COHERENCE.md as a required doc, audited against the codebase
COHERENCE.md states the product-coherence thesis (pmacs should be
immediately excellent, progressively understandable, completely
inspectable, and ultimately replaceable) and, per-section, the audited
ground truth of how the codebase measures against it: a scorecard
across 19 concerns, the golden-journey verdict table (breaks at "open a
real project" -- `pmacs .` exits 1), the six hardcoded key-interception
shadows with no transient-keymap mechanism to migrate them to, the
discoverability substrate-without-surface gap, the package/worker
identity gap, and three cross-cutting patterns (substrate without
surface, the silence asymmetry, per-arc coherence debt) that explain
most of the individual findings.

CLAUDE.md and AGENTS.md now list it as required reading alongside
agent-handoff.md and active-work.md, and ask new framing docs to state
their coherence impact. No runtime code changes.
2026-07-25 11:37:21 -04:00
Levi Neuwirth 0b0d5acd81 fix(find-file): review round 1 -- name the real test, pin two gaps
Three of the five review findings land here; the other two are recorded
as named deferrals in the framing on the dired branch.

Finding 1: the command comment cited "acc4", a name from a draft scheme
that no test carries. It now names the real test, and the comment splits
the shadowing consequence into the two cases that actually exist -- a new
bare name that matches an entry (shadowed) versus one that matches
nothing (creates normally) -- each pointing at its test.

Finding 2: the everyday new-file flow had no test. Typing a bare name
that is not a subsequence of any entry is the path users hit first, and
the only route combining free text with a relative join; every existing
new-file test used a name containing a separator.
find_file_bare_new_name_creates_in_the_root covers it, asserting the
parent is the prompt's root so the join itself is pinned.

Finding 3: the failure arm was never exercised, and as the review noted,
deleting the pcall would have passed the whole suite. Accepting a
directory candidate reaches display_file, whose load fails because
File::open on a directory succeeds and the read returns EISDIR;
find_file_accepting_a_directory_reports_instead_of_raising pins that this
surfaces as the command's status message, leaves the active buffer alone,
and closes the prompt. Verified by manual revert: with the pcall replaced
by a direct call, that test and only that test fails. scripts/bite could
not isolate it, since the guard and its test have no separating commit.

Finding 4 is documented at the command rather than left implicit:
accepting on empty input opens the first-sorted candidate, because
fuzzy_score returns Some(0) for an empty needle and filter_and_sort
breaks the tie lexicographically, so dotfiles lead and a directory can
lead. M-x and switch-buffer share the mechanism, so it is inherited
rather than introduced, and it is listed in the framing beside the
accept-semantics change that would close it.
2026-07-25 11:33:46 -04:00
Levi Neuwirth 35085b54d1 fix: rustfmt the acceptance suite and pin two untested arms (round 1)
The blocker was process, not design. The test file was committed before
`cargo fmt` ran, so the reflow of five over-width assertions sat
uncommitted in the working tree while the branch as pushed failed the
first gate in CLAUDE.md. The "fmt clean" reported on the PR described
the worktree, not the branch. Gate results are only meaningful run
against the pushed tree, so this commit lands the formatting first and
the gates are re-run against it.

Two pins review asked for, each covering a branch the nine acceptance
tests left untested:

- A **string** `config.root` as an affinity key. acc17 covers only the
  function form, so `return configured, "config"` had no test. The bite
  puts both files in their own marked project: drop the config arm and
  they key on their own detected roots and spawn two servers, so one
  server on the configured root is only reachable if the override wins.
- `root = false` reads as unset. Defended by a truthiness check rather
  than `~= nil`, previously by comment alone. Under `~= nil` the config
  arm returns `false, "config"` and `file_uri_for(false)` returns nil, so
  the file lands on a rootless server instead of its detected project.

Each was falsified against exactly the mutation it targets and neither
against the other.

Also documents an asymmetry review caught: `project_root_for`'s
"detected" arm is canonicalized for free because `pmacs.project.detect`
canonicalizes before walking, but a **configured** root — string or
resolver return — is fed to `file_uri_for` exactly as written, and the
affinity key is that URI. On macOS a resolver returning `/var/…` and a
detected `/private/var/…` are therefore different keys for one
directory, silently yielding two servers for one project. There is no
Lua-side canonicalizer to normalize it, and Stage 3's Lean resolver is
the first real consumer, so the obligation is stated in the
`config.root` doc comment where that resolver's author will read it.
2026-07-25 11:19:43 -04:00
Levi Neuwirth 4a2aa92510 style: rustfmt the find-file acceptance harness 2026-07-25 11:13:57 -04:00
Levi Neuwirth 92f57d8894 docs: record Stage 1's landing and the Stage 2 affinity lane
Stage 1 merged as #160 (`main` @ `0827dd1`); the Lean lane header and
branch line now say so, and Stage 2 gets its own subsection.

Edits stay inside the Lean lane. PR #156 is still open against both this
file and `docs/agent-handoff.md`, and it rewrites the snapshot header,
the canonical-base line, and the whole bottom-panel lane — so those are
left alone rather than merged twice. `agent-handoff.md` is untouched for
the same reason plus its own: §1 describes what is on `main`, so it
updates at merge, not during review.

Records the one finding this stage turned up but did not fix:
`ensure_server` never forwards `cfg.restart` to `pmacs.lsp.spawn`, so a
`restart` in `pmacs.lsp.config[lang]` is silently dropped on the
auto-attach path. Pre-existing, and out of scope for a PR whose
acceptance 16 pins existing attach behavior as unchanged.
2026-07-25 11:03:54 -04:00
Levi Neuwirth 2a0884b377 feat(find-file): open a file by path with C-x C-f
Dired arc Stage 0 (docs/dired-framing.md section 10, Q#DR11). Until now
pmacs had no discoverable way to open a file by path: no find-file
command and no C-x C-f binding, so a file entered a session only from
the CLI, an LSP jump, a project-search visit, or C-x C-r, whose prompt
does pass free text through but completes only over the recent list.

The command prompts with completion rooted at the active buffer's
directory, or the process cwd when the buffer has no backing path, and
opens the result through pmacs.window.display_file. A path that does not
exist yet creates a buffer bound to it with the "[new file]" status,
which is Emacs parity and comes from resolve_target_buffer rather than
anything added here. Nothing is written to disk until the user saves.

Two substrate facts shape the design and are documented at the command
rather than left to be rediscovered.

Completion is flat: the files source lists one directory and yields bare
basenames, and a custom function source could not do better, because
sources are called with no arguments and run synchronously outside any
coroutine, so a callback can neither see the input to re-root on nor
await a directory listing. Hierarchical completion is a named Rust
change in the framing.

A selected candidate shadows typed text: recompute_candidates selects
index 0 whenever the candidate list is non-empty, and
resolve_accepted_value returns the candidate over the typed contents. So
typed text reaches the accept handler exactly when the input filters
every candidate away, which for basename candidates under a subsequence
filter means when it contains a separator. That makes the deeper-path
case work verbatim and leaves one hole: a new bare name that is a
subsequence of an existing entry opens the existing file. The acceptance
pins that as a decision rather than an accident; closing it needs a Rust
change to accept semantics that Stage 0 deliberately does not make.

A leading tilde is expanded before the path reaches the core, because
get_or_load_buffer normalizes the path it stores but loads from the raw
one -- so an unexpanded tilde path deduplicates against an already-open
buffer yet fails to load a file that is not open yet.

The prompt field starts empty and names its root in the prompt string
instead: any prefill would contain a separator and silently disable
completion.

Acceptance is dispatch-driven throughout -- a real C-x C-f, real typing,
a real RET -- so a dead binding cannot pass vacuously and the Lua
lifecycle accept(), which bypasses the path interactive input takes, is
not used.
2026-07-25 10:45:50 -04:00
Levi Neuwirth 1ae5963e9d feat(lsp): one server per detected project root (Q#LN15)
`ensure_server` reused any live server whose `language_id` matched,
regardless of project root — its own comment documented this as a known
post-v0.1 limitation. For project-model-strict servers that is a
correctness failure, not a rough edge: `lake serve` is bound to one Lake
package, rust-analyzer and gopls to one workspace, so the second project
a user opens gets a server that cannot resolve its imports.

Server affinity is now keyed on the project root, with one rule that
keeps the change from regressing every other language:

  The affinity key is the root only when a root was actually FOUND.

`project_root_for` never returns nil for a file that has a path — its
last resort is the file's own directory — so a naive `(language_id,
root)` key would give every directory of loose scratch files its own
server, for every language: two stray .py files in different directories
would spawn two pyrights where today they share one. It now returns
`root, source` with source one of "config" / "detected" / "fallback",
and only the first two become an affinity key.

Matching is on the spawned spec's `root_uri`, nil matching nil, so the
fallback spawn passes `root_uri = nil` for the key and the stored spec to
agree. `cwd` still carries the directory, and `build_initialize`
(src/lsp.rs) derives the identical `rootUri` from `cwd` when the field is
None — using a percent-encoder with the same allowed set as Lua's
`file_uri_for`. The initialize payload for that case is therefore
byte-identical to before; only what the reuse loop matches on changes.
`build_initialize` is the only reader of `spec.root_uri` in the tree.

Two consequences, both deliberate and both asserted rather than
discovered:

- A server hand-spawned from init.lua with only `cwd` set also reads
  back nil, so a root-bearing attach will not adopt it. We cannot know
  which root it was meant to serve, and guessing wrongly routes a
  project's files to the wrong server.
- Opening files across N project roots spawns N servers. rust-analyzer
  has the same property and no editor caps it by default; `pmacs.lsp.stop`
  is the manual escape and an LRU reaping policy stays deferred.

`config[language].root` may now be a `function(path) -> string|nil` as
well as a string, for languages whose root rule the shared marker walk
cannot express — an innermost-wins walk cannot find an *outermost*
marker. A resolver returning nil declines and falls through to the marker
walk. Results are memoized per directory because hoisting the root
computation above the reuse loop puts it on every attach rather than
every spawn; the memo is keyed weakly by the resolver function itself, so
replacing `config[lang].root` cannot serve a root the old one computed.

`pmacs.lsp.list()` rows gain `root_uri` and `cwd`. `root_uri` is the spec
field verbatim, deliberately not the URI the server was initialized with.

No protocol change. No Lean content: this is the shared affinity function
for every LSP language, so it ships as its own PR and is exercised
through rust, python, go and typescript against `pmacs_fake_lsp`.

tests/lsp_multi_root_acceptance.rs covers acceptance 13-21. Every fixture
sets `pmacs.project.set_search_boundary` at its own tempdir root:
without it the marker walk climbs to the filesystem root, and a stray
`.git` above the temp directory would turn the markerless cases into
detected ones — the assertions would still pass while testing nothing.

Refs docs/lean4-mode-framing.md Q#LN15, acceptance 13-21.
2026-07-25 10:36:11 -04:00
Levi Neuwirth 0827dd1416
Merge pull request #160 from levineuwirth/lean4-stage1
feat(lean4): Arc 8 Stage 1 — grammar, major mode, and the editing table stakes
2026-07-25 14:27:09 +00:00
Levi Neuwirth 1a5805366a docs: record the Lean 4 lane in the active-work ledger
Review round 1 flagged that neither ledger knew about this branch, and
`docs/active-work.md`'s stated job is exactly the volatile open lanes.
Records the branch, base, framing revision, what Stage 1 ships, the
discharged Q#LN1 obligation, the Q#LN4 blast radius, and the four
implementation findings that are not in the framing (the `warning`
colour collision with `number`, `Some(1)` resolving to `@function`
rather than `@constructor`, the `module > declaration > def` nesting,
and `injection_aliases` being a write-only proxy). Also carries forward
the two Stage 2 corrections the framing already holds, since that lane
starts next.

Deliberately ADDITIVE ONLY -- one new section, zero deleted lines. PR
#156 is open against both this file and `docs/agent-handoff.md` and owns
the snapshot header, the canonical-base line, and the bottom-panel
lane's status. Touching those here would collide with a PR already in
review, which is the "frozen reviewed PRs do not absorb moving
overlapping work" lesson from #135/#137.

`docs/agent-handoff.md` is deliberately untouched: its §1 snapshot
describes what is ON `main`, so it gets updated when this merges, not
while it is in review.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-25 10:18:38 -04:00
Levi Neuwirth 34767d332d fix(test): make acc12 pin the claim it names (review round 1)
Review finding: acc12's server-list assertion could not fail for the
regression class it was written to catch. The shared `editor()` helper
runs `pmacs.lsp.config = {}` before any buffer opens, so
`#pmacs.lsp.list() == 0` holds for every language regardless of what
Stage 1 ships -- a Stage-3 front-run that added
`pmacs.lsp.config.lean4` in a builtin runtime file would have slipped
straight past it. The same vacuous-assertion shape as #155 R2.

acc12 now asserts the actual claim against a PRISTINE `EditorState`,
before any config wipe: no builtin runtime file defines
`pmacs.lsp.config.lean4`. A non-vacuity check pins that the same lookup
finds `pmacs.lsp.config.rust`, so this cannot pass merely because the
table is empty or absent.

Bite-verified: adding `pmacs.lsp.config.lean4 = ... { command = "lake",
args = { "serve" } }` to `builtin/runtime/lsp.lua` fails the test; the
stub was reverted.

The process-list half is kept and its comment now says why it survives
the wipe: a direct probe spawn from a future `lean.lua` shows up there
whatever `pmacs.lsp.config` contains.

Also fixes a stale column in a `highlight.rs` comment -- the Lua table
brace in `local t = {}` is at col 10, which is what the code already
used.

Gates rerun: fmt and strict workspace clippy clean; 1,826 default +
2,003 CRDT library tests; lean4 Stage 1 9/9; M4 121; required GPU 152;
isolated-config workspace sweep 3,150 across 90 suites; diff check clean.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-25 10:18:27 -04:00
Levi Neuwirth 0c922682c0 feat(lean4): editing surface + Stage 1 acceptance (Q#LN5, LN6, LN17)
Completes Arc 8 Stage 1: the Lua-side tables that turn a recognized
grammar into a usable mode, plus the acceptance suite for all twelve
framing criteria.

comment.lua -- `lean4 = "--"` (Q#LN5). Line comments only; Lean's block
comment `/- -/` and docstring `/-- -/` belong to the comment arc's own
named deferral and this lane does not front-run it.

pair.lua -- `⟨⟩`, `⦃⦄`, `⟮⟯` alongside the ASCII brackets (Q#LN6). The
anonymous constructor is among the most-typed constructs in Lean;
omitting it would make the pair set feel broken. The other two ride along
because the Stage 4 input method can produce them, and a bracket the pair
set does not understand is worse than one it does. All three sit outside
the nine built-in pair chars, so per Q#AP1 their undo is
cross-peer-degraded -- the documented, pre-existing limitation of
user-extended pairs. No `''`: Lean uses the prime as an identifier suffix
(`h'`, `foo'`), the same reason Rust excludes it.

syntax.lua -- the `lean` -> `lean4` modeline alias (Q#LN2), so an Emacs
`-*- mode: lean -*-` or a Vim `ft=lean` line is not stranded by the entry
being named `lean4`.

syntax.rs -- the `lean` -> `lean4` injection alias (Q#LN17), so both
```lean and ```lean4 fences highlight. The Lean 3 spelling is mapped
forward deliberately: a ```lean fence is overwhelmingly Lean 4 in
practice.

highlight.rs -- `warning` moves from bold red to bold BRIGHT red. Writing
the test found the collision: `number` is plain `fg(1)`, so `sorry` and
the literal `42` beside it were the same colour, differing only in the
bold flag. `sorry` means "admitted, not proved" and is the one token in a
proof file a reader must never skim past, so it now gets the loudest
entry in the table and the test asserts the full style rather than the
colour.

Twelve criteria, seventeen tests. Notes on the ones that could have been
vacuous:

  * acc4 uses a `.txt` fixture, not `.lean` -- on a `.lean` path the
    extension alone yields `lean4` and the assertion would pass with the
    alias table empty. acc4b removes the alias and pins that the raw name
    survives, so acc4 cannot silently stop testing anything.
  * acc11 goes through the real `_parse_now` injection path and asserts a
    `lean4` CHILD LAYER appears. `pmacs.parse.injection_aliases` is a
    documented write-only proxy, so an alias-table read would have proven
    nothing about the parser; acc11b pins that a misspelled fence still
    resolves to nothing.
  * acc12 asserts through the process supervisor and the server list that
    opening a Lean buffer spawns nothing. This is not decorative: the
    machine this arc was scouted on has elan installed with no default
    toolchain, where `lake --version` itself fails, and Stage 1 must be
    unaffected by that.

Gates: fmt and strict workspace clippy clean; 1,826 default + 2,003 CRDT
library tests; lean4 Stage 1 9, comment toggle 14, auto-pair 45,
injection 4; M4 121; required GPU 152; isolated-config workspace sweep
3,150 across 90 suites; `git diff --check` clean.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-25 09:59:48 -04:00
Levi Neuwirth 60714ee46b
Merge pull request #159 from levineuwirth/minimap-blank-slab-panic 2026-07-25 13:53:56 +00:00
Levi Neuwirth 5207d40caf feat(theme): add the four Lean 4 capture entries (Arc 8 Stage 1, Q#LN4)
`constructor`, `character`, `keyword.conditional`, and `warning` are the
captures the Lean query uses that the global theme table lacked. Three of
them are not Lean-only, so this is a deliberate retro-paint of already
shipped languages -- the #146 lesson applied on purpose rather than
discovered afterwards.

The blast radius, measured rather than assumed:

  * `constructor` reaches SEVEN language entries, not four. The emitting
    crates are rust, lua, python and javascript, but
    `tree_sitter_javascript::HIGHLIGHT_QUERY` is concatenated base-first
    into javascriptreact, typescript and typescriptreact as well.
  * Its shape is not "constructors". rust/python/javascript tag every
    capitalized identifier (`#match? "^[A-Z]"`); lua tags every
    table-constructor brace. So this recolors `None`, every class-cased
    name, and every Lua `{}` -- all of which rendered as unstyled default
    text before.
  * `character` reaches zig only; `keyword.conditional` reaches cmake and
    zig, which previously flattened it to `keyword`; `warning` reaches no
    other grammar and exists for Lean's `sorry`.

The alternative was an in-repo overlay renaming the captures (the #144
LaTeX pattern), which forks a 213-line query we would then own and
hand-merge on every crate bump. There is no middle option: styling Lean's
constructors without touching the other seven entries requires renaming
the capture, which requires the overlay.

Pinned in both directions, per #146:

  * the positive breadth pin asserts all seven entries emit
    `@constructor` at the QUERY level -- chosen over per-fixture checks
    because the base-query composition is the fragile part; if someone
    stops concatenating the JS base into `typescript`, this fails while
    any single-language fixture still passes;
  * two grid pins prove the theme entry reaches painted cells, and a
    third records that a variant in CALL position keeps `@function` --
    the difference between "capitalized identifiers recolor" and "enum
    variants recolor", only the first of which is true;
  * the negative pin asserts ten languages (markdown, json, yaml, html,
    css, c, cpp, go, toml, bash) emit none of the four names, with a
    non-vacuity check that the same predicate finds each name where it
    does occur.

Rev 1 of the framing named Lua and Python in that negative pin, which was
a self-contradiction -- both are retro-painted by `constructor`, so the
assertion would have been vacuous in the #155 R2 shape. Review round 1
caught it.

Full lib suite (1,824) and the required-GPU gate (152) pass unchanged, so
no existing assertion depended on these captures being unstyled.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-25 09:51:27 -04:00
Levi Neuwirth 6ea8d2756e feat(syntax): bundle the Lean 4 grammar (Arc 8 Stage 1, Q#LN1-3)
Adds `arborium-lean` 2.18 and one `BUILTIN_LANGUAGES` entry, closing the
framing's open verification obligation on the crate choice.

Why this crate and not `tree-sitter-lean4` (Q#LN1): the latter depends on
`tree-sitter = "0.25"` directly rather than the shared
`tree-sitter-language` ABI crate, and `^0.25` excludes our 0.26, so it
would fork the graph exactly as the dead `tree-sitter-dockerfile` does.
It also exports only `pub fn language()` while its README advertises a
`LANGUAGE` const that does not exist, and its package `include` omits
`queries/` so it ships no highlights at all. `arborium-lean` uses
`tree-sitter-language 0.1` as its sole runtime dep, ships a pre-generated
ABI-15 parser plus scanner, and exports real query constants.
`cargo tree -d` reports no duplicate `tree-sitter`.

The entry is named `lean4`, not `lean` (Q#LN2): `ensure_server` passes
`LanguageEntry.name` through as the `didOpen` language_id, and the Lean
ecosystem's id is `lean4` -- `lean` is Lean 3, which is end-of-life. It
claims `.lean` only; `.olean` is a compiled binary and `.ilean` is JSON
metadata (Q#LN3).

Four tests. The load-bearing one is `lean4_grammar_loads_and_parses`,
which discharges the half of Q#LN1 that could not be settled by reading:
`arborium-lean` exports `const fn language() -> LanguageFn` rather than
the `LANGUAGE` const every other entry uses, and its README demonstrates
usage against a patched tree-sitter core. Neither is supposed to matter,
but "supposed to" is not evidence. The fixture parses without error, and
-- the part that actually guards a misbuild -- its Unicode operators
produce structure rather than degrading silently: the grammar must see a
`(arrow)` for the arrow, a `(forall)` for the universal quantifier, and a
`(comparison)` for the inequality.

The error-free claim is deliberately scoped to the committed fixture.
Lean's syntax is user-extensible via macros, so a static grammar
mis-parses some legal input by construction; the framing scores that as
bet 3 rather than the doc overselling it.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-25 09:49:01 -04:00
Levi Neuwirth a38296583b docs: frame Lean 4 mode (Arc 8)
The approved framing for Arc 8, revision 4, after three review rounds.
Seven stages: grammar/mode, multi-root LSP affinity, the Lean language
server, the Unicode input method, the goal view, the #eval output
channel, and module hierarchy. 19 decisions, 64 acceptance criteria.

Committed as this branch first commit per the house workflow; the
implementation of Stage 1 follows.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-25 09:44:53 -04:00
Levi Neuwirth e547a90e37 fix(gpu): stop the minimap dividing by zero on an all-blank slab
`dominant_line_shape` averages only the lines in a bucket that have
content, then guarded the result with `bool::then_some`. `then_some`
takes its argument by value, so the `MinimapLineShape` literal --- and
with it `indent_sum / count` --- is evaluated before the `count > 0`
guard is ever consulted. When a bucket holds no contentful lines the
division panics and takes the GPU frontend down.

This is reachable in ordinary use, not at an edge: the bucketing branch
runs whenever a file has more lines than the minimap has pixel rows, and
it is exactly then that a run of blank lines can fill a whole downsampled
row. A whitespace-only line counts as blank too --- `minimap_line_shape`
subtracts the indent from the total, so `content_cols` is zero.

Switch to `bool::then`, which defers the body into a closure so the zero
case short-circuits to `None`. The call site already treats `None` as
"draw no stroke for this row", so no other change is needed.

Three tests, two of which fail against the previous line:

  * a 10,000-line all-blank file driven through `minimap_rects`, which
    reproduces the original panic through the real downsampling path;
  * `dominant_line_shape` on an empty bucket;
  * a mixed bucket, asserting the average still ignores blank lines ---
    a companion guard so the fix cannot regress into counting the whole
    slice.

A comment records why this must not be "simplified" back: clippy's
`unnecessary_lazy_evaluations` pushes in precisely the wrong direction
here, and does not fire on a body that can panic.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-25 09:42:25 -04:00
Levi Neuwirth 14c1c01043 feat(math): caret-driven suppression, the draw pass, and the slice acceptance
The two halves that touch live rendering, landed together because the
acceptance criteria that make either honest need both.

Suppression (Q#MS3/MS4/MS5/MS11). Detection runs in the per-line chunk
builder — the chunk-build path, never the edit path — and substitutes
each suppressed span's source bytes with ONE spacer chunk BEFORE tab
expansion, so a literal tab inside a span vanishes with it while tabs
outside keep their SourceTab provenance. The gate reads the EFFECTIVE
caret (own_cursor, which optimistic edits predict forward — F4's
no-flap requirement holds by construction) plus both own-selection
endpoints. Three motion paths can flip a gate without a content
change, and each now re-runs the per-line chunk compare, gated on a
one-scan "does the visible slice hold a $" check: the CursorByte arm,
finish_optimistic_edit (the text re-chunks under the OLD caret there;
without the hook a typed char rendered one keystroke stale), and the
Decorations arm — whose "no decoration change needs a reshape" premise
acquires exactly one exception, the Selection endpoints Q#MS11 made
suppression inputs.

The line-reuse predicate (acceptance 11, the #120 edge). Per-line
math state is cached in lockstep with line_chunk_cache: every detected
span with the gate bit it was built under. The scroll-reuse path
refuses a retained line whose cached bits disagree with the CURRENT
caret/selection — content is unchanged on every reuse path, so the
cached span set is authoritative and the gate bits are the only
variable. The acceptance test drives the stale-gate case through
rebuild_lines_reusing_scroll directly and fails if the gate is removed
from the predicate.

The hit map (B1'). hit_test_source_byte rebuilds its runs from a
whole-slice chunk walk, so it now reads the substitutions BACK from
the per-line caches — never re-planned under a possibly-newer caret —
keeping the map and the shaped glyphs one source of truth.

The draw pass (Q#MS6/MS7). Every MathItem::Glyph draws from its own
mini-buffer with Attrs pinned to the bundled math family (F8b), placed
at layout's exact x and the shaped line's REAL baseline; the
mini-buffer itself is positioned by the line_y cosmic-text actually
produced for it, so no font-metric rederivation can drift. Fraction
rules ride the bg quad batch after the decoration washes and under the
glyphs. Wash geometry gains Q#MS11's intersection rule: a wash
touching a suppressed span widens to the box's whole reserved
rectangle (a match strictly inside the span produced a zero-width
interval before), while the round-3 exclusive-end fix keeps a
non-intersecting wash off the box.

Acceptance (framing §5). Criteria 5-11 and 14-16 run on real pixels
through render_to_view: drawn ink where a literal-spacer control
renders none, with the before-region pixel-identical; the fraction
rule as a full-width run with operand ink both sides; caret-inside
rendering EXACTLY as math-disabled (driven through the real
CursorByte arm, which owns the refresh — a direct helper call would
not have pinned the wiring); every failure mode (unbalanced, unknown
command, $$, uncoverable glyph) pixel-equal to disabled; box clicks
snapping to the span start with the trailing edge landing after the
span; the scroll-reuse stale-gate bite; reflow confined to the
affected line with the after-text shifted by exactly the quantized
projection difference; selection gating and the whole-rectangle wash;
and the licence provenance pair. Criterion 17 is discharged
differentially: cargo tree -e features output for ttf-parser is
byte-identical with and without this crate's dependency line.

Also folded in, per the round-3 close-out: the F6 documenting test
($a$$b$ is eaten by the $$-opaque rule; one separating character
restores both spans), the depth-search bound raised 6 -> 8 so a
metric shift cannot make the "floor is dead code" expect fire with a
misleading message, the MathBox { end, .. } pattern nit, and the
active-work.md lane entry.

Named v0 approximations, deliberate: the peer-caret half of
acceptance 14 is pinned at the mapping level (unit tests), not
pixels; a soft-wrapped spacer draws its box whole at the first run's
origin (the one-rectangle model); the fit budget reads the bundled
code face even under a custom set_font family — the draw anchors to
the real shaped baseline either way, so only the fit margin is
approximate.

Clippy is CLEAN across the workspace at -D warnings for the first
time on this branch: the draw pass consumed every formerly-dead item,
and the three lints it could not fix (a test-only accessor, one doc
string, one manual midpoint) are fixed here.

Gates: cargo fmt --check; cargo clippy --workspace --all-targets
-- -D warnings; 1,815 default + 1,992 CRDT library tests; M4 121
(basedpyright skipped); 199 pmacs-gpu tests under PMACS_REQUIRE_GPU=1;
workspace sweep 3,131 across 88 suites (isolated XDG_CONFIG_HOME);
git diff --check.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-24 22:04:35 -04:00
Levi Neuwirth 870209cca9 test(buffer): capture the CRDT undo no-op-with-op case
Found during #155's sweep and recorded there as one line of prose with an
uncommitted proptest seed. This turns it into something that cannot be
lost and that states what is actually known.

Reproduced on main @ e745068 with PROPTEST_CASES=2000 against
rope_matches_crdt_projection_after_arbitrary_edits, then reduced by hand
to five lines: replacing a byte range with IDENTICAL bytes is a textual
no-op but a real CRDT operation, so undoing it advances the CRDT version
while leaving the materialized text unchanged. `undo_crdt_mode` derives
an empty replacement edit and still attaches the op `crdt.undo()`
produced, which trips the proptest's "a no-op edit must have crdt_op =
None" invariant.

The test is `#[ignore]`d rather than asserted-as-correct or left as a
seed, because the resolution is a judgement call I should not make
silently:

- the raw proptest seed is NOT committed, since it would fail the suite
  on every run for a case whose correct outcome is undecided;
- the deterministic reduction reproduces without any seed, so nothing is
  lost by leaving the seed out.

What the doc comment records, so the next reader need not redo it:
content stays correct (rope and CRDT projection agree either side); both
`crdt_op` consumers read the field unconditionally and do not
short-circuit on an empty range, so replicas still converge; and
`EditorCore::undo` never seeks `edit.range.start`, so no cursor jumps.
The open question is whether the invariant is simply mis-scoped — it was
written for the forward `apply_edit` short-circuit, which returns before
producing an op, and CRDT-mode undo/redo never reach that path. One
artifact is arbitrary either way: `derive_replacement_edit` reports the
empty range at the buffer END rather than at the edit site.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-24 21:34:08 -04:00
Levi Neuwirth 7f7ad1934c docs: record bottom-panel Stage 1 (#155) landing
Handoff §1 gains the arc entry: the window-parameter substrate, the two
production `Layout::compute` callers, the recursive minima, hiding as a
durable transition, per-window input gating, the per-frontend jump
origins, and the shared initial-target load seam. §5 gains four durable
lessons, three of them the same class:

- a guard with no production caller passes every direct-call test;
- a geometric readout (`at_bottom`) is not a state predicate;
- a PTY does not translate LF to CRLF, so text equality over clipped
  output is vacuous;
- widening an ambient resolver into a scoped one can make a total
  function partial — which is what took CI red on all four Test jobs.

The roadmap position, the arc's named deferrals, and DAP's unblocking
are recorded too.

active-work closes the lane, refreshes the canonical base to `e745068`,
and keeps Stage 2's named obligations plus the two gating facts found on
the way (the sweep needs an isolated XDG_CONFIG_HOME; compile_mode
acceptance is load-sensitive, verified pre-existing).

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-24 20:33:32 -04:00
Levi Neuwirth e74506879f
Merge pull request #155 from levineuwirth/bottom-panel
Bottom panel Stage 1: window placement + TUI side windows
2026-07-25 00:21:07 +00:00
Levi Neuwirth cbf7782726 fix(math): review round 3 — mapping bug, whitespace defect, real MATH gaps
F1 was a real bug pinned by my own committed test. `end` in
ChunkSource::MathBox is EXCLUSIVE, so source position `end` is the first byte
AFTER the span — but the arm claimed it for the box's left edge, and the test
asserted that wrong value while calling the byte "interior". Consequences it
would have caused once overlays land: a search match starting just after a
span washes the whole box it does not intersect, violating Q#MS11; a peer
caret after the span draws at the box's left edge; caret geometry jumps
backwards. The same class existed in projected_to_source for a line-FINAL box,
where `within` clamps to the run length and the arm returned `start`
unconditionally, so a click past end-of-line landed on the span start. Both
committed hit tests put a chunk after the box, so that edge was never
exercised; there is now a test with the box last.

F2: parse_scripts peeked for the next marker without skipping whitespace, so
`x^2 _i` built a NESTED script — drawing the subscript displaced right by the
superscript's width — and `x^2 ^3` parsed where TeX errors, contradicting the
module's own "whitespace is insignificant" rule.

F3: layout is now fallible. A character the math font cannot draw used to
yield zero metrics and still emit a Glyph item, rendering tofu at zero advance
over its neighbour. Q#MS8's rule is "failure is always show the source", and
the draw pass needs a refusal signal — changed now, before that pass consumes
the API.

F4: the fraction gap was a hardcoded `thickness * 2.0` while the MATH table's
FractionNumeratorGapMin / FractionDenominatorGapMin went unread. Reading them
moved the flagship \frac{a}{b} from 0.732 to 0.867 and the fallback boundary
from depth 3 to depth 5. The round-2 review's hand-arithmetic estimate of
~0.85 was right; my 0.732 was inflated by the guess. The depth-SEARCHING test
absorbed the change without edits, which is the property it was written for.

F5: TeX's \epsilon and \phi are the lunate/symbol forms (U+03F5, U+03D5), not
U+03B5/U+03C6. Their italic mappings had to land with the seed change, since
both sit outside math_italic's U+03B1..03C9 run and would otherwise render
upright beside italic neighbours.

F7: the line-box budget derivation moved out of the test into
`line_box_budget`, so the draw pass and the acceptance test cannot compute
different splits while both stay green.

F8: the live-code clippy items are cleared. The 25 that remain are all
dead-code awaiting the draw pass.

189 pmacs-gpu tests pass.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-24 20:19:40 -04:00
Levi Neuwirth 9110f9f32c fix(window): keep pmacs.window.buffer() infallible with no argument
PR #155 review round 2, self-review of the round-2 commit.

The round-2 change labelled "minor" — resolving both arms of
pmacs.window.buffer() through the acting frontend for uniformity — made
the NO-ARGUMENT arm fallible. `acting_frontend` follows the interactive
origin, which can name a frontend that has no registered view: a bare
`dispatch_key` from an unattached peer does exactly that. `selected_window`
then raises "acting frontend has no layout" instead of answering.

Nothing surfaced that error, because the runtime callers do not pcall it.
killring, syntax, autosave, pair, indent and comment all read
pmacs.window.buffer() on ordinary edits, so the raise silently dropped
the operation: kill_ring_acceptance went 30/30 to 25/5, with
frontend_detached_drops_per_frontend_state reporting only "B has kill
state". main is 30/30, and reverting this one file restored it.

The no-arg arm is back on ambient active_buffer_id() and now documents
why that is deliberate rather than an oversight: dispatch sets
active_frontend to the acting frontend before running a command, so the
two agree on every real path, while only the ambient resolver has the
fallback that makes it total. The explicit-window arm keeps its Q#BP11
layout validation, which is what the arc actually needed.

acc19c pins it through the real path — a buffer.after-edit subscriber
reading pmacs.window.buffer() during a viewless peer's dispatch_key —
rather than by calling the binding directly. Bite-verified:
scripts/bite bbe4152 src/lua_bindings/mod.rs --test
bottom_panel_stage1_acceptance -- acc19c goes red with the exact
"acting frontend has no layout" traceback.

The ledger also records two gating facts found on the way: the workspace
sweep must run with an isolated XDG_CONFIG_HOME, because the real user
init.lua installs a local package and the losing race leaks a status
message into painted-frame comparisons; and a latent pre-existing main
bug in the buffer CRDT undo path, which is not this branch's and whose
proptest seed is deliberately not committed here.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012j4omtTMn9v1UfmHQb9ap6
2026-07-24 20:05:51 -04:00
Levi Neuwirth 8e4bc00015 feat(math): ChunkSource::MathBox and spacer width quantization
The suppression mechanism F2 forced: a RichChunk's only width is its text, so
a suppressed span reserves room with SPACER SPACES the way SourceTab already
does, quantized up to whole advances. Quantizing up keeps the projection
grid-aligned with the surrounding monospace text and keeps hit runs integral,
at the cost of under one advance of slack on the right.

Adding the variant to an exhaustive enum made the compiler enumerate every
seam it must participate in, which is why it is wired through all five rather
than the two I had in mind: projected_to_source, source_to_projected, the tab
expander's source remap, and offset_chunk_source. Hits anywhere inside a box
snap to the span start — the Adornment rule, because Q#MS4 gives the box no
interior byte map — and source positions inside it collapse to the box's left
edge, so text after the span accounts for the whole reserved width.

Two details the tab expander needed: a math chunk's spacer text is generated
rather than source, so it holds no tab byte to expand, and its suppressed
range is already in slice coordinates and never split, so a within-chunk
offset does not move it.

spacer_for_width guards its inputs: a non-finite width, a non-positive
advance, or a pathological ratio reserves nothing or clamps, rather than
panicking or minting an enormous string from a cast.

184 pmacs-gpu tests pass, including the 155 that predate this branch.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-24 18:57:18 -04:00
Levi Neuwirth 8c25e0ddde feat(math): currency-guarded inline span detection
Per-line `$…$` scanning with the Pandoc guards F5 required: an opener must be
followed by a non-space, a closer must be preceded by a non-space and not
followed by a digit, and `\$` escapes. Without them "prices are $5 and $6
today" renders "5 and " as math, in exactly the grammar-less prose buffers
this scanner targets. Spans never cross a newline (Q#MS3), so callers scan one
line at a time.

`$$` is opaque, and the test that forced this is worth keeping in mind. My
first version simply refused to OPEN on `$$`, reasoning that display math
would then never match. It still did: in `$$x$$` the first `$` declines to
open, the second one opens, and the third closes it — matching the inner `$x$`,
whose interior parses perfectly well. So display math would have half-rendered
as math with a stray `$` on each side, which is precisely what acceptance 15
forbids. `$$` now neither opens nor closes and abandons any pending opener.

The test that caught it was itself nearly vacuous. It asserted "every span
found must fail to parse", which passes trivially when the matched interior is
`x`. Asserting that NO span is found is the form that actually holds the
contract; the weaker version would have shipped the bug.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-24 18:47:48 -04:00
Levi Neuwirth bbe4152048 docs: record bottom-panel review round 2
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-24 18:42:04 -04:00
Levi Neuwirth f708ccb2a4 feat(math): box layout, and measure the real height budget
MathBox/MathItem composition for the Q#MS2 subset: characters advance a pen,
scripts shift by the MATH table's superscript/subscript amounts at script
scale, and \frac stacks its operands around a rule at the math axis. Inline
\frac sets its operands one style down, which is TeX's rule and also what the
parent framing's Tier 3 specifies — and it is load-bearing for Q#MS10, since
full-size operands would not fit the line at all.

The height budget is now measured rather than assumed, and the round-2 review
was right to insist on that. Two things were wrong.

First, my own test derived the budget from the MATH font's metrics. Q#MS10
says the budget is the LINE BOX, whose baseline the CODE font places —
JetBrains Mono ascends 16.32 px and descends 4.80 px at 16 px inside the 22 px
line, against Latin Modern Math's 12.90/3.10. Using the wrong font made a
plain \frac{a}{b} score 0.485 and appear to fall below the floor, which would
have meant the flagship case never rendering.

Second, with the budget derived correctly, B6 holds — \frac{a}{b} scales to
0.732 — but rev 3's guessed fallback case does not. A doubly-nested fraction
scores 0.744 and still renders; the floor is not tripped until depth 3, at
0.580. Round 2 predicted precisely this surprise-pass. Worth keeping: depth 2
scores HIGHER than depth 1, because the binding constraint flips from descent
to ascent as nesting grows asymmetrically, so "deeper is always tighter" is
false.

The test therefore SEARCHES for the tripping depth instead of hardcoding it,
and fails if no depth trips the floor at all — which would mean the fallback
arm is unreachable and the floor is dead code. Acceptance 12 records the
measured table.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-24 18:39:26 -04:00
Levi Neuwirth 52e7598da0 test(window): press the peer's own mode line in acc30c
The round-2 peer press landed in the peer's CONTENT area, so it never
reached `arm_window_drag` — the exact path Finding 5 names — and the
case bit nothing. It now presses the peer's own mode-line row, where a
single global drag slot is overwritten (and, since that lone window owns
no boundary, cleared outright).

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-24 18:37:10 -04:00
Levi Neuwirth 4d44be5d7b fix(terminal): implement the Q#BP7 growth re-arm and pin it honestly
PR #155 review round 2.

Finding 1 (must fix): Q#BP7 item 1 — "growth reaching the live tail
re-arms follow (top -> None), only when no selection is active" — was
never implemented. `at_bottom` is the instantaneous geometric readout
`scroll_offset == 0`, which a still-anchored view satisfies whenever it
happens to be tall enough to reach the tail, so the round-1 assertion
could not see the gap: the next rows the child printed pushed the
anchored view back into history.

`rearm_follow_on_growth` now clears `top` when a viewport-size
declaration makes the view cover the tail and no selection is frozen,
and every size-declaring path (`snapshot_for_view`, `record_view_size`,
`view_status_for_size`) routes through one `declare_view_size` helper so
grid and semantic declarations cannot disagree. `scroll_view` and
`begin_selection` deliberately stay out: they write `top` themselves,
and `scroll_view` already owns the scroll-driven arm.

New acc32b is the pin the review asked for: scroll into history, grow
past the tail, then release a SECOND burst of child output through a
filesystem gate and assert the view moved with it.

Finding 2: the PTY fixtures emitted LF-only output, which staircases
rightward until every row clips to blanks past the viewport width — so
the round-1 anchor assertions compared "" with "" and could not fail.
Both fixtures now emit CRLF, and each anchor comparison is guarded by
`assert!(!top_before.is_empty())`.

Finding 3: acc33's contrast case asserted nothing, and the behavior it
claimed was false as coded. With the re-arm in place it is true and now
asserted: clearing the selection at the same geometry re-arms follow and
leaves the frozen anchor.

Finding 4: `start_run` gated the panel branch on `display == "panel" or
already_in_panel(..)`, so an explicit `display = "current"` lost to the
inference — and that value is the documented user-facing opt-out from
the Stage 3 default flip. Now gated on OMISSION. acc19b gains the
explicit-"current" case.

Finding 5: `window_drag` is a `HashMap<FrontendId, WindowDragState>`, so
a peer's mode-line press can no longer steal or clear another
frontend's in-flight gesture, and concurrent drags are legal. Cleared on
detach. acc30c gains the mode-line-press case.

Minor: `pmacs.window.buffer()` resolves both arms through the acting
frontend using the shared `lookup_window` / `selected_window` validators
rather than re-implementing them beside an ambient `active_buffer_id()`.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-24 18:32:23 -04:00
Levi Neuwirth 320bcce276 feat(math): bundle Latin Modern Math and read its MATH constants
Font, licence, and the metrics half of Tier 3.

The bundled font is Latin Modern Math under the GUST Font License, added as
fonts/GUST-FONT-LICENSE.txt — deliberately a separate file from fonts/OFL.txt,
which covers JetBrains Mono only. GFL is LPPL-derived, not the SIL OFL; the
framing's F6 corrected that error and this is the discharge. At 733,736 bytes
the font is now the largest embedded asset in the repository.

ttf-parser is declared with default-features = false and only
"opentype-layout". Verified differentially: the ttf-parser feature set from
`cargo tree -e features` is byte-identical with and without this dependency
line, so the declaration widens nothing and forces no rebuild of the font
chain.

That check also corrected acceptance 17, which asserted `std` would be absent.
It is not — fontdb already enables it via `std = ["ttf-parser/std"]`, upstream
and independent of us. As written the criterion would have failed a correct
implementation, so it is now stated as the differential property that actually
matters.

MathConstants reads only what the Q#MS2 subset needs — axis height, script
scale percent, the two script shifts, and fraction rule thickness. Reading
more would be speculative: constants for deferred constructs have no consumer
to validate them, which is the Q#LX5 discipline applied to metrics. A font
with no MATH table is a typed error rather than plausible-looking zeros, so a
bundled-font regression cannot be silent (Q#MS7).

math_italic implements TeX's convention as the framing's table states it:
ASCII letters and lowercase Greek italic, uppercase Greek upright, digits and
operators unchanged, with U+210E for `h` because the 1D4xx run has a hole
there and arithmetic would land on a reserved codepoint.

Five tests, all against the real embedded bytes rather than fixtures, since B5
is the bet that would sink Tier 3 if false. One goes beyond the framing: every
italic mapping must resolve to a glyph the bundled font actually has, because
a mapping that produced tofu would be worse than the roman fallback it
replaces.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-24 18:27:34 -04:00
Levi Neuwirth b9aed61e23 feat(math): LaTeX math parser for the slice subset (Tier 2)
pmacs-gpu/src/math_parse.rs — the Q#MS2 subset: characters, groups,
sub/superscripts in either order, and \frac, plus the Greek seed map.
Everything outside the subset is a typed error, which Q#MS8 turns into
"render the raw source".

The AST is semantic, not presentational: \alpha resolves to 'α' here, but the
math-italic mapping stays in layout, where a codepoint becomes a glyph.
Baking italics into the AST would make the tree disagree with the source and
would have to be unpicked by any later non-italic style context.

Two bugs the tests caught before they could reach layout, both from skipping
whitespace in the wrong place. `parse_atom` consumed it, but the ^/_ dispatch
happens in `parse_sequence` BEFORE atoms are read — so `x ^ 2` parsed the
caret as a literal character, and an all-whitespace span produced an empty
group instead of the Empty error. Whitespace is now skipped at the dispatch
point, which fixes both at one seam.

Interior `$` is rejected explicitly so `$$x$$` degrades through the error path
(acceptance 15) rather than half-rendering.

Clippy reports MathNode as dead code, which is correct and expected: the
parser has no consumer until Tier 3 layout lands. That is exactly the
condition Q#LX5 refused to ship, now enforced mechanically. It is not
suppressed; it clears when layout arrives in this same branch.

11 unit tests, no GPU or font required.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-24 18:14:43 -04:00
Levi Neuwirth 4b1af277e1 docs(math): slice framing rev 3 — close review round 2
Four findings, one of them a real gap.

R2-2 is the substantive one. Rev 2's math-italic fix stopped at ASCII, which
reintroduced the same defect one symbol over: the parser resolves \alpha to
U+03B1, so $\alpha x$ would have drawn an upright alpha beside an italic x —
mixed styles inside a single expression, with the Greek seed map being the
slice's second flagship case after x^2. The mapping now follows TeX's actual
convention and states it as a table: ASCII letters and lowercase Greek in math
italic (U+1D434 and U+1D6FC runs, with the U+210E hole for h), uppercase Greek
deliberately upright, digits and operators unchanged. Acceptance 13 gains
$\alpha$ and $\Gamma$ cases so the uniformity is pinned rather than assumed.

R2-1 was self-inflicted: rev 2's Q#MS3 rewrite added a corrected copy of the
tree-sitter paragraph without deleting the original, leaving the stale rev-1
text immediately below the new one. Removed.

R2-4 sharpens Q#MS11 from "covers" to "intersects". For selections the
distinction is vacuous, but a search match can genuinely half-overlap a span —
searching "2$ af" in "before $x^2$ after" matches from inside the span to
outside it — and the whole-rectangle rule must apply there too, since the box
has no interior byte map to place a partial wash against.

R2-3 moves the follow-up section after prior art; the sections now run 0
through 9 in order.

Acceptance 12 also absorbs a round-2 non-finding: the reviewer's arithmetic
puts \frac{a}{b} near 0.85 and suggests \frac{x^2}{y} also clears the 0.6
floor, so the fallback case has to be computed against the real font rather
than guessed — otherwise the fallback half of the test surprise-passes by
rendering. The criterion now says so and asks for the computed scale to be
pinned.

Framing only; no implementation, no runtime code.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-24 17:57:39 -04:00
Levi Neuwirth 67976dfc5f docs(math): slice framing rev 2 — close review round 1
Nine findings, two of them decisions the implementation could not have
proceeded without, one a compliance error. Two rev-1 claims were wrong rather
than imprecise and are withdrawn where they occur.

F1, the fraction height budget, was hidden inside "a box that would exceed the
line" without saying width or height. Lines cannot grow — metrics are uniform
at 16 px over a 22 px line — and a textstyle fraction does not fit. Q#MS10 now
picks fit-to-line scaling with a 0.6x floor and source fallback below it,
records why overdraw and line growth were rejected, and states the honest
consequence: v0 shrinks nested math uniformly where TeX would use style
levels. B6 makes the floor falsifiable against the flagship case.

F3 was a genuine contradiction: acceptance 10 demanded source-width boxes
while Q#MS4 implied layout-chosen width, and that gap IS the caret-toggle
reflow question. Resolved for layout-chosen, because pinning to source width
leaves every fraction sitting in a large permanent gap, whereas reflow is
transient and tied to a deliberate caret move. Acceptance 10 is rewritten to
bound it rather than forbid it.

F2 withdrew the zero-glyph strut: a RichChunk's only width is its text, so the
mechanism is the SourceTab precedent — projected spacer text, width quantized
to whole advances. B1 is restated against the mechanism that exists.

F5 would have bitten real prose immediately: the rev-1 rule renders "prices
are $5 and $6 today" as math. Pandoc currency guards adopted, spans confined
to one line, both in acceptance.

F6 is factual and a licence matter. Latin Modern Math is the GUST Font
License, not OFL, and is 733,736 bytes rather than ~200 KB — verified against
a local TeX Live copy. The bundled licence file must say GFL, and this becomes
the largest embedded asset in the repo. The parent framing carries the same
error; correcting it is recorded as a follow-up rather than done here, since
the parent is already merged.

F4 names the new shaping-invalidation edge as the #120 trap class, including
that suppression must read the effective caret or flap during optimistic
typing. F7 puts math italic in scope, without which the flagship case renders
a roman x. F8 clarifies that glyph IDs are still resolved internally and that
drawing must pin Attrs to the math family. F9 closes the smaller gaps: the
detection hook wording, an overlay rule for selections and washes, degradation
of deferred display syntax, and folding Char/Symbol.

Framing only; no implementation, no runtime code.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-24 16:07:03 -04:00
Levi Neuwirth 7e1bfb6dc5 test(window): pin the terminal anchor, not the tail-relative offset
`TerminalViewStatus.scroll_offset` is the retained rows between the
VIEWPORT and the live tail, so it necessarily tracks viewport height: an
assertion that it survives a panel height change unchanged is either
vacuous or wrong, and it went red once under a loaded sweep for exactly
that reason. Q#BP7's invariant is that the ANCHOR is frozen, so acc32
and acc33 now compare the first visible row's text across the change,
and additionally pin the follow behavior that distinguishes them: a
shrink never re-arms follow, growth reaching the tail does, and growth
with a frozen selection does not.

Both also wait for the child's last line before sampling, so neither
races further output.

Also records the round in docs/active-work.md.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-24 15:21:48 -04:00
Levi Neuwirth f8020320e2 docs(math): frame the first inline-math vertical slice
The obvious next unit was Tier 2 (parser) plus Tier 3 (layout). This framing
rejects that for the arc's own reason: the substrate lane's Q#LX5 refused to
land the parser ahead of layout because MathNode's shape is only validated by
a consumer, and that argument does not stop at Tier 2. MathBox is only
validated once a renderer consumes it, so Tiers 2+3 with no Tier 4 reproduce
the same objection one layer up.

The unit is therefore thin and vertical: characters, sub/superscript and
fractions, detected, parsed, laid out against a real OpenType MATH table, and
drawn — with breadth deferred to follow-on work against an API that has been
exercised rather than only designed.

The scout also found a load-bearing error in the parent's integration table.
It places math_parse.rs and math_layout.rs in the core crate, which cannot
work: pmacs-gpu depends only on pmacs-protocol and never on pmacs, so a
core-crate parser is unreachable from the frontend that renders it, and
ttf-parser reaches only pmacs-gpu. Both also contradict the parent's own
"instance never learns a pixel" contract and its "pure frontend
responsibility in v0" protocol section. Q#MS1 moves both modules into
pmacs-gpu.

Two decisions buy the slice most of its simplicity. Rendering is suppressed
whenever the caret is inside a span, which makes editing-shows-source and
moving-away-renders mutually exclusive states and removes the
caret-inside-math problem rather than approximating it. And layout positions
characters rather than glyph IDs, which is sufficient for this subset and
explicitly does not generalise: glyph variants are what stretchy fences and
big operators need, and both are deferred.

Acceptance puts every claim that something reaches the screen on real pixels
through the existing headless render seam, because a layout engine wired to
nothing would pass any weaker test.

Framing only; no implementation, no runtime code.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-24 15:15:36 -04:00
Levi Neuwirth 352bf0b2ab
Merge pull request #154 from levineuwirth/inline-math-rescout
docs(math): re-scout inline-math framing against landed state (rev 2)
2026-07-24 19:08:27 +00:00
Levi Neuwirth 90fc7a913e fix(window): wire the side-window split guard and scope the divider drag
PR #155 review round 1.

Finding 1 (must fix): `try_split_active` had no production caller —
`pmacs.window.split_horizontal` / `split_vertical`, and therefore
`C-x 2` / `C-x 3`, still went through plain `split_active`. Splitting a
focused panel made the root wrapper's final child a split rather than
`Leaf(side)`, which both `Layout::compute`'s fixed pass and
`document_subtree` key on: the panel band reverted to 1:1 weight
division and an ordinary window ended up living inside it. Both bindings
now route through the guard, and acc26 asserts through the real Lua
path — a direct core call passes with the guard unwired, which is how it
survived the first round.

Finding 2: the armed-drag early return now checks the arming frontend,
so one frontend's in-flight gesture cannot cancel or swallow another's
mouse events. New acc30c.

Finding 3: `paint_mode_line_graphemes`'s doc block was left heading
`paint_divider_segment`; moved back.

Finding 4: a recompile carries no `display`, so it took the raw switch
and duplicated a panel-placed `*compilation*` into the document window.
`start_run` now detects that the buffer already owns the panel slot.
`pmacs.window.buffer` gained an optional window argument so an adopter
can ask without selecting the panel first. New acc19b.

Stage-2 hazard pins the review asked for, both in `src/daemon.rs`:
a fresh attach while LOCAL is focused in a panel inherits LOCAL's
document buffer, and an initial-target bootstrap whose `after-load`
hook creates and selects a panel still reasserts into a document window.

Minor: dropped listview's dead `p.side`; documented `focus_window`'s
caller-validates contract; `jump_back` restores through `focus_window`
so the "every focus change" contract holds; `params` / `resize` default
to the acting frontend's selected window rather than the ambient one;
widened the flexible-division math to u64 intermediates.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-24 15:07:35 -04:00
Levi Neuwirth dd414d4d2d docs(math): name the ttf-parser feature set the MATH table needs
Review finding, verified: rev 2's "no new build cost" was true only under
an unstated condition. ttf-parser re-exports `math` behind
`#[cfg(feature = "opentype-layout")]`, and it is compiled today only
because fontdb requests that feature — with `default-features = false` and
a set that is NOT ttf-parser's own default (fontdb's adds no-std-float and
omits std). A plain `ttf-parser = "0.25"` therefore unions std in and
forces a one-time rebuild of ttf-parser, fontdb, cosmic-text and glyphon.

Record the zero-rebuild spelling, `default-features = false, features =
["opentype-layout"]`, in Tier 3 §A and in the component table, so the
Tier 3 implementer declares it deliberately rather than tripping over it.
The C1 row points at the detail rather than repeating it.

Also note in the header that every anchor was re-checked at f07b75b. The
scout pin stays at ddaa80d because that is when the scouting happened;
#153 landed between the two and is test-only, moving no anchor cited here.

Framing only; no implementation, no runtime code.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-24 14:59:21 -04:00
Levi Neuwirth f07b75b4a3
Merge pull request #153 from levineuwirth/vterm-pty-flake
test(vterm): match host output past the differ's cell-skipping
2026-07-24 18:37:23 +00:00
Levi Neuwirth 85a07f378c test(vterm): gate terminal readiness on a file, not on host bytes
Both earlier attempts in this branch were wrong, and the diagnostic they
added is what proved it: the macOS failure reported a stable
`rendered prefix: 6/15 ("VTERM_")` BEFORE and AFTER the CRLF change, with an
identical cursor, across two completely different child layouts. Identical
truncation under different layouts cannot be a layout problem.

The real mechanism is pinned by the repository's own unit test,
`cell::tests::diff_split_by_unchanged_cell_is_two_spans`: `cell::diff` splits
a run at any cell where `prev == next` and never transmits that cell. So when
a character of the marker already happens to sit at its destination, the host
receives the marker with that byte MISSING, not merely escaped around. The
constant 6 is the distance to the first such hole.

That makes escape-stripped matching unsound in kind rather than merely
insufficient: no matching strategy recovers a byte that was never sent. It is
removed, and `wait_for_output` is strict again. What remains asserted through
host bytes are protocol escapes pmacs writes directly — the OSC 52 clipboard
reply, the alternate-screen and bracketed-paste resets — which are not painted
cells and which the differ never touches.

Readiness now gates on a file the child publishes, the pattern the reliable
sibling test in this file already uses. That the child's output reaches the
SCREEN stays asserted in-process over `snapshot_text`, at the layer that can
actually see it; this test keeps what it uniquely owns, the host lifecycle.

`strip_ansi` and `longest_rendered_prefix` are kept as failure diagnostics
only, and now carry a case pinning the dropped-cell shape so the wrong remedy
is not reached for again. The new readiness wait reports startup breadcrumbs
on timeout; the plain helper reports only the missing path, which is the least
useful thing to know at exactly that moment.

Both the readiness gate and its timeout diagnostic were falsified by pointing
the child at a path the test does not watch.

Test-only; no runtime code.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-24 14:27:21 -04:00
Levi Neuwirth 2a9c11461c docs: record the bottom-panel Stage 1 lane
Adds the lane to docs/active-work.md: branch, base, what Stage 1
implemented, the verification run, and the two known local-only test
caveats (the parallel-load GPU flake and compile_mode_acceptance's
single-thread requirement).

The durable handoff snapshot stays untouched until the PR merges, per
its own update protocol.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-24 14:20:16 -04:00
Levi Neuwirth 5dcc7d70a0 docs(math): re-scout inline-math framing against landed state
Revision 1 was written against protocol v18, before LaTeX Stage 1 (#144),
web grammars (#146), folding Stages 1-2 (#142/#149) and the GPU initial
target (#148) landed. Revision 2 changes no design decision; it corrects
the ground truth those merges invalidated and records the staging decision
the sibling substrate framing already took. A new section 0 lists every
correction so a reader who knows revision 1 can read it alone.

Two corrections change implementation choices rather than line numbers:

- The MATH-table dependency story was wrong in both directions. Revision 1
  said a crate must be added and that "neither is in the tree today";
  ttf-parser 0.25.1 already reaches pmacs-gpu non-optionally through
  fontdb -> cosmic-text -> glyphon, the same fontdb the frontend already
  calls. And the choice is not "one of ttf-parser or read-fonts": only
  ttf-parser exposes the MATH table, supplying exactly the constants Tier
  3 names. read-fonts 0.37.0 is present but has none, so selecting it
  would be a dead end.

- Tier 2's staging was already decided elsewhere and this note did not say
  so. The sibling framing's Q#LX5 puts the parser beside its Tier 3
  consumer, never ahead of it, because MathNode's shape is only validated
  by a layout consumer. That makes Tier 2 not independently shippable,
  which is worth stating explicitly: it is pure and conflict-free, so
  landing it alone while other lanes hold the render path is exactly the
  tempting move Q#LX5 refused.

Tier 1 is materially de-risked: the LaTeX grammar already exposes
math_environment and math_delimiter, and the in-repo query overlay this
tier proposed already exists and captures both, so the mechanism is proven
rather than speculative. The guessed node name (math_expression) is
corrected to the grammar's own. Markdown still needs the overlay
treatment.

Tier 4 gains a contention note. Revision 1 described the GPU render path
as though math were its only claimant; folding Stage 3 and the
bottom-panel arc's Stage 2 now converge on it, so whichever lands second
re-scouts against the first.

Framing only; no implementation, no runtime code.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-24 14:10:46 -04:00