fix(themes): PR #120 round 4 -- freeze sourced from the store
A session first rendering during diagnostic staleness emitted zero counts: round 3's frozen_diag_counts cache was per-session and only seeded from fresh computations, so a late joiner attaching mid-edit (or a buffer first visited between didChange and fresh diagnostics) had no entry and fell back to (0, 0), contradicting the documented "frozen counts, never zeros" contract. mark_stale (T M11.8) keeps the last published diagnostic vector -- only the positions are invalid -- so status_facts_msg now counts the retained for_uri entries even while stale: the retained entries ARE the frozen value. The per-session cache is deleted; sourcing the freeze from the store means there is no session state to lose to a snapshot reset and no history needed at attach, so the round-3 reset-survival property holds by construction and its round-trip test passes unchanged against the new mechanism. Acceptance item 33 marks a populated store stale BEFORE the SemanticRenderState exists and asserts the first frame reports the preserved counts; runtime bite vs pre-fix semantic_render.rs. Framing revision 8; the protocol doc's freeze sentence now says store knowledge, including the late-joiner case. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VoiEyuPjoBhvwACf8HAnLB
This commit is contained in:
parent
2fe6738d68
commit
3d6336a912
|
|
@ -128,9 +128,11 @@ receives authoritative re-sends even when nothing changed
|
||||||
daemon-side (the unchanged-generation A → B → A revisit). Bufferless
|
daemon-side (the unchanged-generation A → B → A revisit). Bufferless
|
||||||
facts (`ThemeFacts`, the minibuffer prompt) and per-frontend state
|
facts (`ThemeFacts`, the minibuffer prompt) and per-frontend state
|
||||||
(the gutter mode) survive snapshots on both sides, and the
|
(the gutter mode) survive snapshots on both sides, and the
|
||||||
instance's stale-store diagnostic-count freeze is daemon knowledge,
|
instance's stale-store diagnostic-count freeze is store knowledge,
|
||||||
not peer state — the re-sent `StatusFacts` after a snapshot carries
|
not session state — the re-sent `StatusFacts` after a snapshot
|
||||||
the frozen counts, never zeros.
|
carries the frozen counts, never zeros, including for a session
|
||||||
|
whose first frame lands during staleness (a late joiner attaching
|
||||||
|
mid-edit).
|
||||||
|
|
||||||
## Capability and version mechanics
|
## Capability and version mechanics
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,7 +1,25 @@
|
||||||
# Theme faces — framing (Arc 4 stage 1, themes)
|
# Theme faces — framing (Arc 4 stage 1, themes)
|
||||||
|
|
||||||
**Revision 7 — 2026-07-15. Status: implemented on branch
|
**Revision 8 — 2026-07-15. Status: implemented on branch
|
||||||
`theme-faces` (PR #120); revision 7 folds PR round 3.**
|
`theme-faces` (PR #120); revision 8 folds PR round 4.**
|
||||||
|
|
||||||
|
Revision 8 (PR #120 round 4, one finding): the diagnostic-count
|
||||||
|
freeze is sourced from the diag store itself, superseding round 3's
|
||||||
|
per-session `frozen_diag_counts` cache. That cache only seeded from
|
||||||
|
fresh computations, so a session FIRST rendering during staleness —
|
||||||
|
a late joiner attaching mid-edit, or a buffer first visited between
|
||||||
|
didChange and fresh diagnostics — had no entry and fell back to
|
||||||
|
(0, 0), contradicting the documented "frozen counts, never zeros"
|
||||||
|
contract. But `mark_stale` (T M11.8) keeps the last published
|
||||||
|
diagnostic vector — only the positions are invalid — so
|
||||||
|
`status_facts_msg` now counts the retained `for_uri` entries even
|
||||||
|
while stale: the retained entries ARE the frozen value, with no
|
||||||
|
session state to lose to a snapshot reset and no history needed at
|
||||||
|
attach. The per-session cache is deleted; the round-3 reset-survival
|
||||||
|
property holds by construction. Acceptance item 33 (a store marked
|
||||||
|
stale BEFORE the session exists still reports the preserved counts
|
||||||
|
on the first frame); item 32's round-trip claim is unchanged and
|
||||||
|
still passes against the new mechanism.
|
||||||
|
|
||||||
Revision 7 (PR #120 round 3, findings 1–2): the reset contract is
|
Revision 7 (PR #120 round 3, findings 1–2): the reset contract is
|
||||||
now symmetric on the GPU. The round-2 producer reset covered
|
now symmetric on the GPU. The round-2 producer reset covered
|
||||||
|
|
@ -649,14 +667,15 @@ pub struct ThemeFace {
|
||||||
needs no call. NOT reset: `last_face_epoch` / `last_theme_faces`
|
needs no call. NOT reset: `last_face_epoch` / `last_theme_faces`
|
||||||
(this channel is bufferless — the frontend keeps its face table
|
(this channel is bufferless — the frontend keeps its face table
|
||||||
across snapshots), the global minibuffer baseline, the
|
across snapshots), the global minibuffer baseline, the
|
||||||
per-frontend gutter mode, the revision-keyed diag line cache,
|
per-frontend gutter mode, the revision-keyed diag line cache, and
|
||||||
`frozen_diag_counts` (round 3 finding 2: the stale-store freeze
|
other buffers' baselines (each buffer's own snapshot precedes its
|
||||||
source is daemon-side knowledge about the buffer, split from the
|
revisit). The diagnostic-count freeze needs no protection here
|
||||||
`last_status` peer baseline precisely so the reset cannot zero
|
(rounds 3–4): it is sourced from the diag store's retained vector
|
||||||
mid-edit counts), and other buffers' baselines (each buffer's own
|
— `mark_stale` keeps the last published diagnostics, whose counts
|
||||||
snapshot precedes its revisit). Resetting on a failed write is
|
merely lag — never from session state, so the reset cannot zero
|
||||||
harmless — the failure mode is one redundant re-send, never
|
mid-edit counts and the freeze holds even for a session attaching
|
||||||
staleness. The GPU's `BufferSnapshot` arm mirrors the contract
|
during staleness. Resetting on a failed write is harmless — the
|
||||||
|
failure mode is one redundant re-send, never staleness. The GPU's `BufferSnapshot` arm mirrors the contract
|
||||||
(round 3 finding 1): it clears its buffer-scoped facts —
|
(round 3 finding 1): it clears its buffer-scoped facts —
|
||||||
search/menu popups (which gate key and pointer interception) and
|
search/menu popups (which gate key and pointer interception) and
|
||||||
the status band — alongside spans, decorations, adornments,
|
the status band — alongside spans, decorations, adornments,
|
||||||
|
|
@ -992,3 +1011,8 @@ Keybinding-driven tests dispatch keys, never `pmacs.command.invoke`.
|
||||||
finding 2): render nonzero counts, mark the store stale
|
finding 2): render nonzero counts, mark the store stale
|
||||||
(didChange), apply the snapshot reset — the re-sent
|
(didChange), apply the snapshot reset — the re-sent
|
||||||
`StatusFacts` carries the frozen nonzero counts, never (0, 0).
|
`StatusFacts` carries the frozen nonzero counts, never (0, 0).
|
||||||
|
33. **The freeze holds without session history** (PR round 4): mark
|
||||||
|
a populated store stale BEFORE constructing the
|
||||||
|
`SemanticRenderState` — the session's first frame reports the
|
||||||
|
store's preserved counts, because the freeze is the retained
|
||||||
|
diagnostic vector itself, not a per-session cache.
|
||||||
|
|
|
||||||
|
|
@ -175,18 +175,13 @@ pub struct SemanticRenderState {
|
||||||
last_summary: HashMap<BufferId, SummaryCache>,
|
last_summary: HashMap<BufferId, SummaryCache>,
|
||||||
/// `(name, modified, diag_errors, diag_warnings, message)` last
|
/// `(name, modified, diag_errors, diag_warnings, message)` last
|
||||||
/// emitted as `StatusFacts` (Q#S1; `message` since v15) —
|
/// emitted as `StatusFacts` (Q#S1; `message` since v15) —
|
||||||
/// cached-compare suppression.
|
/// cached-compare suppression. A peer emission baseline ONLY:
|
||||||
|
/// the diagnostic-count freeze deliberately holds no session
|
||||||
|
/// state (rounds 3–4) — it is sourced from the diag store's
|
||||||
|
/// retained vector, so it needs nothing here to survive the
|
||||||
|
/// `on_buffer_snapshot_sent` reset and it holds for sessions
|
||||||
|
/// with no history (a late joiner attaching mid-edit).
|
||||||
last_status: HashMap<BufferId, (String, bool, u32, u32, Option<String>)>,
|
last_status: HashMap<BufferId, (String, bool, u32, u32, Option<String>)>,
|
||||||
/// Last *fresh* whole-file diagnostic counts per buffer — the
|
|
||||||
/// freeze source while the diag store is stale (mid-edit counts
|
|
||||||
/// merely lag; flickering to zero per keystroke would be worse).
|
|
||||||
/// Split from `last_status` (PR #120 round 3 finding 2): that map
|
|
||||||
/// is a PEER emission baseline and dies with a `BufferSnapshot`
|
|
||||||
/// (`on_buffer_snapshot_sent`), while this is daemon-side
|
|
||||||
/// knowledge about the buffer and must survive the reset — or a
|
|
||||||
/// buffer switch between didChange and fresh diagnostics would
|
|
||||||
/// re-ship `StatusFacts` with zeroed counts.
|
|
||||||
frozen_diag_counts: HashMap<BufferId, (u32, u32)>,
|
|
||||||
/// Last-emitted line-number gutter mode (UX gutter arc, protocol v14) —
|
/// Last-emitted line-number gutter mode (UX gutter arc, protocol v14) —
|
||||||
/// cached-compare suppression. Seeded to `Some(Off)` (the frontend's
|
/// cached-compare suppression. Seeded to `Some(Off)` (the frontend's
|
||||||
/// default) so an off gutter never emits. Per-frontend (one value),
|
/// default) so an off gutter never emits. Per-frontend (one value),
|
||||||
|
|
@ -362,7 +357,6 @@ impl SemanticRenderState {
|
||||||
last_completion_popup: HashMap::new(),
|
last_completion_popup: HashMap::new(),
|
||||||
last_summary: HashMap::new(),
|
last_summary: HashMap::new(),
|
||||||
last_status: HashMap::new(),
|
last_status: HashMap::new(),
|
||||||
frozen_diag_counts: HashMap::new(),
|
|
||||||
// Seed to the frontend's default (gutter off): a plain default
|
// Seed to the frontend's default (gutter off): a plain default
|
||||||
// window never emits `LineNumbers`, so the common case adds no
|
// window never emits `LineNumbers`, so the common case adds no
|
||||||
// traffic and the first frame is unchanged. Only an actual
|
// traffic and the first frame is unchanged. Only an actual
|
||||||
|
|
@ -414,14 +408,14 @@ impl SemanticRenderState {
|
||||||
/// table across snapshots), `last_minibuffer` (one global core
|
/// table across snapshots), `last_minibuffer` (one global core
|
||||||
/// instance, not buffer-scoped), `last_line_numbers`
|
/// instance, not buffer-scoped), `last_line_numbers`
|
||||||
/// (per-frontend gutter mode, kept by the frontend across the
|
/// (per-frontend gutter mode, kept by the frontend across the
|
||||||
/// switch), `diag_line_cache` (a revision-keyed compute cache,
|
/// switch), and `diag_line_cache` (a revision-keyed compute
|
||||||
/// not a peer-state baseline), and `frozen_diag_counts` (the
|
/// cache, not a peer-state baseline). The diagnostic-count
|
||||||
/// stale-store freeze source — daemon-side knowledge about the
|
/// freeze survives by construction (rounds 3–4): it is sourced
|
||||||
/// buffer, not about the peer; deleting it would zero the counts
|
/// from the diag store's retained vector, never from session
|
||||||
/// on a mid-edit revisit, round 3 finding 2). Baselines for OTHER
|
/// state, so this reset cannot zero mid-edit counts. Baselines
|
||||||
/// buffers also survive — the snapshot names one buffer, and any
|
/// for OTHER buffers also survive — the snapshot names one
|
||||||
/// buffer the frontend navigates to receives its own snapshot
|
/// buffer, and any buffer the frontend navigates to receives its
|
||||||
/// first.
|
/// own snapshot first.
|
||||||
pub fn on_buffer_snapshot_sent(&mut self, buffer_id: BufferId) {
|
pub fn on_buffer_snapshot_sent(&mut self, buffer_id: BufferId) {
|
||||||
self.last_sent.remove(&buffer_id);
|
self.last_sent.remove(&buffer_id);
|
||||||
self.last_style_gate.remove(&buffer_id);
|
self.last_style_gate.remove(&buffer_id);
|
||||||
|
|
@ -892,10 +886,15 @@ impl SemanticRenderState {
|
||||||
/// nothing changed. Carries the facts a semantic frontend cannot
|
/// nothing changed. Carries the facts a semantic frontend cannot
|
||||||
/// derive locally: buffer name, modified flag, whole-file
|
/// derive locally: buffer name, modified flag, whole-file
|
||||||
/// diagnostic counts (errors / warnings). Counts freeze at their
|
/// diagnostic counts (errors / warnings). Counts freeze at their
|
||||||
/// last value while the diag store is stale — mid-edit positions
|
/// last published value while the diag store is stale — mid-edit
|
||||||
/// are wrong but *counts* merely lag, and flickering to zero on
|
/// positions are wrong but *counts* merely lag, and flickering
|
||||||
/// every keystroke would be worse. The daemon's write loop keeps
|
/// to zero on every keystroke would be worse. The freeze IS the
|
||||||
/// the variant off wires negotiated `< 8`.
|
/// store's retained vector (rounds 3–4): `mark_stale` keeps the
|
||||||
|
/// last published diagnostics, so counting them while stale
|
||||||
|
/// yields the frozen value with no session state to lose — not
|
||||||
|
/// to a snapshot reset, and not by attaching mid-edit. The
|
||||||
|
/// daemon's write loop keeps the variant off wires negotiated
|
||||||
|
/// `< 8`.
|
||||||
fn status_facts_msg(
|
fn status_facts_msg(
|
||||||
&mut self,
|
&mut self,
|
||||||
state: &EditorState,
|
state: &EditorState,
|
||||||
|
|
@ -913,43 +912,33 @@ impl SemanticRenderState {
|
||||||
let buf = reg.get(buffer_id).ok()?;
|
let buf = reg.get(buffer_id).ok()?;
|
||||||
(buf.name().to_owned(), buf.is_modified(), message)
|
(buf.name().to_owned(), buf.is_modified(), message)
|
||||||
};
|
};
|
||||||
let counts = {
|
let (diag_errors, diag_warnings) = {
|
||||||
let core = state.core.borrow();
|
let core = state.core.borrow();
|
||||||
buffer_file_uri(&core, buffer_id).and_then(|uri| {
|
buffer_file_uri(&core, buffer_id).map_or((0, 0), |uri| {
|
||||||
let store = state.lsp_manager.borrow().diag_store();
|
let store = state.lsp_manager.borrow().diag_store();
|
||||||
let guard = store.lock().expect("diag store mutex poisoned");
|
let guard = store.lock().expect("diag store mutex poisoned");
|
||||||
if guard.is_stale(&uri) {
|
// Counted even while the store is STALE (round 4):
|
||||||
None // keep the cached counts
|
// `mark_stale` keeps the last published vector (T
|
||||||
} else {
|
// M11.8) — positions are invalid mid-edit, but counts
|
||||||
let mut errors = 0u32;
|
// merely lag, so the retained entries ARE the frozen
|
||||||
let mut warnings = 0u32;
|
// value. Sourcing the freeze from the store rather
|
||||||
for d in guard.for_uri(&uri) {
|
// than any per-session cache means a session first
|
||||||
match d.severity {
|
// rendering during staleness — a late joiner, or a
|
||||||
crate::diag::DiagnosticSeverity::Error => errors += 1,
|
// buffer first visited mid-edit — reports the
|
||||||
crate::diag::DiagnosticSeverity::Warning => warnings += 1,
|
// preserved counts instead of zeros, and the snapshot
|
||||||
_ => {}
|
// reset has nothing count-related to preserve.
|
||||||
}
|
let mut errors = 0u32;
|
||||||
|
let mut warnings = 0u32;
|
||||||
|
for d in guard.for_uri(&uri) {
|
||||||
|
match d.severity {
|
||||||
|
crate::diag::DiagnosticSeverity::Error => errors += 1,
|
||||||
|
crate::diag::DiagnosticSeverity::Warning => warnings += 1,
|
||||||
|
_ => {}
|
||||||
}
|
}
|
||||||
Some((errors, warnings))
|
|
||||||
}
|
}
|
||||||
|
(errors, warnings)
|
||||||
})
|
})
|
||||||
};
|
};
|
||||||
// Fresh counts advance the freeze source; a stale store reads
|
|
||||||
// it back. Never `last_status` — that is the peer emission
|
|
||||||
// baseline and dies with a `BufferSnapshot`, while the frozen
|
|
||||||
// counts are daemon-side knowledge that must survive the
|
|
||||||
// reset (round 3 finding 2).
|
|
||||||
let (diag_errors, diag_warnings) = match counts {
|
|
||||||
Some(fresh) => {
|
|
||||||
self.frozen_diag_counts.insert(buffer_id, fresh);
|
|
||||||
fresh
|
|
||||||
}
|
|
||||||
None => self
|
|
||||||
.frozen_diag_counts
|
|
||||||
.get(&buffer_id)
|
|
||||||
.copied()
|
|
||||||
.unwrap_or((0, 0)),
|
|
||||||
};
|
|
||||||
let facts = (name, modified, diag_errors, diag_warnings, message);
|
let facts = (name, modified, diag_errors, diag_warnings, message);
|
||||||
if self.last_status.get(&buffer_id) == Some(&facts) {
|
if self.last_status.get(&buffer_id) == Some(&facts) {
|
||||||
return None;
|
return None;
|
||||||
|
|
|
||||||
|
|
@ -1,7 +1,7 @@
|
||||||
// theme_faces_acceptance.rs --- Themes Arc 4 stage 1 acceptance
|
// theme_faces_acceptance.rs --- Themes Arc 4 stage 1 acceptance
|
||||||
// (docs/theme-faces-framing.md, acceptance items 1–19, 24–26, 28–29,
|
// (docs/theme-faces-framing.md, acceptance items 1–19, 24–26, 28–29,
|
||||||
// and 32; the GPU routes — 20–23, 27, and 30–31 — live in pmacs-gpu's
|
// and 32–33; the GPU routes — 20–23, 27, and 30–31 — live in
|
||||||
// headless suite).
|
// pmacs-gpu's headless suite).
|
||||||
|
|
||||||
//! Named UI faces (`ui` / `ui.*` theme entries) + the `ThemeFacts`
|
//! Named UI faces (`ui` / `ui.*` theme entries) + the `ThemeFacts`
|
||||||
//! wire channel (protocol v16).
|
//! wire channel (protocol v16).
|
||||||
|
|
@ -1084,9 +1084,10 @@ fn snapshot_reset_keeps_frozen_diag_counts_while_the_store_is_stale() {
|
||||||
// `last_status` was both the peer emission baseline AND the
|
// `last_status` was both the peer emission baseline AND the
|
||||||
// stale-store freeze source, so the round-2 reset zeroed the
|
// stale-store freeze source, so the round-2 reset zeroed the
|
||||||
// counts: a buffer switch between didChange and fresh
|
// counts: a buffer switch between didChange and fresh
|
||||||
// diagnostics re-shipped StatusFacts with (0, 0). The freeze
|
// diagnostics re-shipped StatusFacts with (0, 0). The freeze is
|
||||||
// source now lives apart (`frozen_diag_counts`) and survives
|
// now the diag store's own retained vector (round 4 superseded
|
||||||
// `on_buffer_snapshot_sent`.
|
// round 3's per-session cache), so the reset has nothing
|
||||||
|
// count-related to lose.
|
||||||
use pmacs::diag::DiagnosticSeverity;
|
use pmacs::diag::DiagnosticSeverity;
|
||||||
|
|
||||||
let mut state = editor();
|
let mut state = editor();
|
||||||
|
|
@ -1146,6 +1147,56 @@ fn snapshot_reset_keeps_frozen_diag_counts_while_the_store_is_stale() {
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
// ---------------------------------------------------------------------------
|
||||||
|
// 33 — the freeze holds without session history (PR #120 round 4)
|
||||||
|
// ---------------------------------------------------------------------------
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn a_session_first_rendering_during_staleness_reports_preserved_counts() {
|
||||||
|
// `mark_stale` keeps the last published diagnostic vector — only
|
||||||
|
// the positions are invalid — so the freeze must hold for a
|
||||||
|
// session with NO per-session history. Pre-fix, the producer
|
||||||
|
// skipped the retained entries while stale and a late joiner (or
|
||||||
|
// a buffer first visited mid-edit) fell back to (0, 0), against
|
||||||
|
// the documented "frozen counts, never zeros" contract.
|
||||||
|
use pmacs::diag::DiagnosticSeverity;
|
||||||
|
|
||||||
|
let mut state = editor();
|
||||||
|
type_str(&mut state, "boom\nfine\n");
|
||||||
|
let uri = attach_diags(
|
||||||
|
&state,
|
||||||
|
vec![
|
||||||
|
diag(DiagnosticSeverity::Error),
|
||||||
|
diag(DiagnosticSeverity::Warning),
|
||||||
|
],
|
||||||
|
);
|
||||||
|
|
||||||
|
// didChange BEFORE any session exists for this buffer.
|
||||||
|
{
|
||||||
|
let store = state.lsp_manager.borrow().diag_store();
|
||||||
|
store
|
||||||
|
.lock()
|
||||||
|
.expect("diag store lock")
|
||||||
|
.mark_stale(uri.clone());
|
||||||
|
}
|
||||||
|
|
||||||
|
let mut sem = semantic(&state);
|
||||||
|
let first = sem.render_frame(&state);
|
||||||
|
let counts = first.iter().find_map(|m| match m {
|
||||||
|
InstanceMessage::StatusFacts {
|
||||||
|
diag_errors,
|
||||||
|
diag_warnings,
|
||||||
|
..
|
||||||
|
} => Some((*diag_errors, *diag_warnings)),
|
||||||
|
_ => None,
|
||||||
|
});
|
||||||
|
assert_eq!(
|
||||||
|
counts,
|
||||||
|
Some((1, 1)),
|
||||||
|
"a late joiner's first frame reports the store's preserved counts"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
// ---------------------------------------------------------------------------
|
// ---------------------------------------------------------------------------
|
||||||
// 12 + 16 + 19 — ThemeFacts emission discipline; late join; set wipes
|
// 12 + 16 + 19 — ThemeFacts emission discipline; late join; set wipes
|
||||||
// ---------------------------------------------------------------------------
|
// ---------------------------------------------------------------------------
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue