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>

builtin/runtime/comment.lua

@@ -39,6 +39,10 @@ pmacs.comment.strings = {
   sh = "#",
   toml = "#",
   yaml = "#",
+  -- Lean 4 (framing Q#LN5). `--` only: Lean's block comment is `/- -/` and
+  -- its docstring `/-- -/`, but block-comment toggling is the comment arc's
+  -- own named deferral and this lane does not front-run it.
+  lean4 = "--",
 }
 
 -- Start of the line containing `pos`: chunked backward scan for the

builtin/runtime/pair.lua

@@ -62,6 +62,22 @@ pmacs.pair.sets = {
   markdown = { "()", "[]", "{}", '""', "``" },
   sh = { "()", "[]", "{}", '""', "''" },
   bash = { "()", "[]", "{}", '""', "''" },
+  -- Lean 4 (framing Q#LN6). `⟨⟩` (anonymous constructor) is among the
+  -- most-typed constructs in Lean and omitting it would make the pair set
+  -- feel broken; `⦃⦄` (strict implicit binder) and `⟮⟯` 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 are OUTSIDE the nine built-in pair chars, so per Q#AP1 their
+  -- opener is a source-peer op and their closer a daemon-peer op: their undo
+  -- is cross-peer-degraded. That is the documented, pre-existing limitation
+  -- of user-extended pairs, whose general fix is chronological cross-peer
+  -- undo arbitration (named substrate work).
+  --
+  -- No `''`: Lean uses `'` as a primed-identifier suffix (`h'`, `foo'`), so
+  -- pairing it would fight the user constantly. Same reasoning that excludes
+  -- it for Rust.
+  lean4 = { "()", "[]", "{}", "⟨⟩", "⦃⦄", "⟮⟯", '""' },
 }
 
 -- Length of the well-formed UTF-8 sequence starting at `s[i]`, or nil

builtin/runtime/syntax.lua

@@ -227,6 +227,11 @@ local default_modeline_aliases = {
   yml = "yaml",
   makefile = "make",
   docker = "dockerfile",
+  -- Lean 4 (framing Q#LN2). The grammar entry is named `lean4` because that
+  -- name becomes the `didOpen` language_id, but an Emacs `-*- mode: lean -*-`
+  -- or a Vim `ft=lean` line is what people actually write, so neither
+  -- spelling strands a file.
+  lean = "lean4",
 }
 for name, language in pairs(default_modeline_aliases) do
   if pmacs.parse.modeline_aliases[name] == nil then

src/highlight.rs

@@ -208,7 +208,12 @@ impl Theme {
             ("constructor", fg(11)),
             ("character", fg(2)),
             ("keyword.conditional", fg_bold(13)),
-            ("warning", fg_bold(1)),
+            // Bold BRIGHT red, deliberately the loudest entry in the table
+            // and deliberately distinct from `number`'s plain `fg(1)`: in a
+            // proof file `sorry` means "this is admitted, not proved", which
+            // is the one thing a reader must never skim past. Plain `fg(1)`
+            // would have collided with every numeric literal on colour alone.
+            ("warning", fg_bold(9)),
         ];
         let by_capture = entries
             .iter()
@@ -1527,6 +1532,17 @@ mod tests {
         src: &str,
         col: u32,
     ) -> pmacs_protocol::cell::Color {
+        painted_style_at(language_name, file, src, col).fg
+    }
+
+    /// As [`painted_fg_at`], but returns the whole style — needed where a
+    /// colour alone does not discriminate (Lean's `warning` vs `number`).
+    fn painted_style_at(
+        language_name: &str,
+        file: &str,
+        src: &str,
+        col: u32,
+    ) -> pmacs_protocol::cell::Style {
         use crate::buffer::{Buffer, BufferId, EditOp};
         use crate::cell::{Cell, CellSize};
         use crate::syntax::{ParseView, SyntaxRegistry};
@@ -1564,7 +1580,7 @@ mod tests {
             folds: None,
         };
         hv.render(&buf, viewport, &mut grid);
-        grid.get(CellCoord::new(0, col)).style.fg
+        grid.get(CellCoord::new(0, col)).style
     }
 
     /// Does `language`'s compiled highlight query use `capture`?
@@ -1576,6 +1592,92 @@ mod tests {
         query.capture_names().contains(&capture)
     }
 
+    #[test]
+    fn lean4_grid_paints_comment_keyword_name_operator_and_number() {
+        // Framing acceptance 5: the grammar plus the crate query plus the
+        // theme table actually produce distinct styles on a painted grid.
+        // Asserted end-to-end rather than at the query level because a
+        // capture that resolves to `Style::default()` is indistinguishable
+        // from no capture at all to a reader.
+        use pmacs_protocol::cell::Color;
+
+        // `-- c` — the whole comment run.
+        assert_eq!(
+            painted_fg_at("lean4", "a.lean", "-- c\n", 0),
+            Color::Indexed(8),
+            "a Lean line comment paints the comment style"
+        );
+
+        // `def foo : Nat := 42`
+        let src = "def foo : Nat := 42\n";
+        assert_eq!(
+            painted_fg_at("lean4", "a.lean", src, 0),
+            Color::Indexed(5),
+            "`def` paints the keyword style"
+        );
+        assert_eq!(
+            painted_fg_at("lean4", "a.lean", src, 4),
+            Color::Indexed(4),
+            "the definition's name paints the function style"
+        );
+        assert_eq!(
+            painted_fg_at("lean4", "a.lean", src, 14),
+            Color::Indexed(6),
+            "`:=` paints the operator style"
+        );
+        assert_eq!(
+            painted_fg_at("lean4", "a.lean", src, 17),
+            Color::Indexed(1),
+            "a numeric literal paints the number style"
+        );
+
+        // A string literal, and `theorem` as a second declaration keyword.
+        assert_eq!(
+            painted_fg_at("lean4", "a.lean", "def s := \"hi\"\n", 9),
+            Color::Indexed(2),
+            "a string literal paints the string style"
+        );
+        assert_eq!(
+            painted_fg_at("lean4", "a.lean", "theorem t : True := trivial\n", 0),
+            Color::Indexed(5),
+            "`theorem` paints the keyword style"
+        );
+        assert_eq!(
+            painted_fg_at("lean4", "a.lean", "theorem t : True := trivial\n", 8),
+            Color::Indexed(4),
+            "the theorem's name paints the function style"
+        );
+    }
+
+    #[test]
+    fn lean4_sorry_paints_the_warning_style_distinctly_from_a_number() {
+        // Framing acceptance 6. `sorry` admits a goal without proving it —
+        // in a proof file it is the single most important token to notice,
+        // and it is why Q#LN4 adds a `warning` entry at all.
+        //
+        // The style is asserted in FULL, not by colour: `number` and the
+        // first-choice `warning` colour were both indexed red, so a
+        // colour-only assertion would have passed with `sorry` painted
+        // exactly like the literal `42` beside it. That is the whole failure
+        // this test exists to prevent.
+        use pmacs_protocol::cell::Color;
+
+        let sorry = painted_style_at("lean4", "a.lean", "theorem t : True := sorry\n", 20);
+        assert_eq!(
+            sorry.fg,
+            Color::Indexed(9),
+            "`sorry` paints the warning colour"
+        );
+        assert!(sorry.bold, "`sorry` is bold");
+
+        let number = painted_style_at("lean4", "a.lean", "def n := 42\n", 9);
+        assert_ne!(
+            (sorry.fg, sorry.bold),
+            (number.fg, number.bold),
+            "`sorry` must be visually distinct from a numeric literal"
+        );
+    }
+
     #[test]
     fn lean4_constructor_capture_retro_paints_the_whole_javascript_family() {
         // Framing acceptance 7 (Q#LN4), the breadth half. `constructor` was

src/syntax.rs

@@ -251,6 +251,12 @@ pub fn default_injection_aliases() -> HashMap<String, String> {
         ("golang", "go"),
         ("yml", "yaml"),
         ("md", "markdown"),
+        // Lean 4 (framing Q#LN17). A ```lean fence is overwhelmingly Lean 4
+        // in practice, so the Lean 3 spelling is deliberately mapped forward
+        // rather than left unresolved. `lean4` needs no alias — it is the
+        // entry name. `lean4-mode` does the equivalent through
+        // `markdown-code-lang-modes`.
+        ("lean", "lean4"),
     ]
     .into_iter()
     .map(|(a, b)| (a.to_owned(), b.to_owned()))

tests/lean4_stage1_acceptance.rs

@@ -0,0 +1,320 @@
+//! Lean 4 mode, Stage 1 acceptance (Arc 8, `docs/lean4-mode-framing.md`).
+//!
+//! Covers the framing's Stage 1 criteria that live above the Rust
+//! substrate — major mode, modeline aliasing, comment toggle, the pair
+//! set, and markdown fence injection. Criteria 1, 2, and the Q#LN4
+//! retro-paint pins (7, 8) are unit tests in `src/syntax.rs` and
+//! `src/highlight.rs`, where the theme table and grammar registry live.
+//!
+//! Dispatch-driven, following `comment_toggle_acceptance`: `M-;` and
+//! typed characters go through `dispatch_key` so the real command
+//! boundary and typed-edit provenance are exercised. Buffers are
+//! file-backed (language detection needs a path); each editor gets a
+//! private tempdir `StateDir` and an emptied `pmacs.lsp.config` so
+//! nothing spawns a language server — Stage 1 has no LSP at all.
+//!
+//! Criterion 12 is the reason this suite touches no process: it must
+//! pass on a machine with no `lean`, no `lake`, and no configured elan
+//! toolchain. That is not hypothetical — the machine this arc was
+//! scouted on has elan installed with no default toolchain, where
+//! `lake --version` itself fails.
+
+use crossterm::event::{KeyCode, KeyEvent, KeyEventKind, KeyEventState, KeyModifiers};
+use pmacs::editor::EditorState;
+use pmacs::lua_bindings::StateDir;
+use pmacs::protocol::FrontendId;
+use std::path::PathBuf;
+use std::sync::atomic::{AtomicUsize, Ordering};
+
+fn fresh_state_dir() -> PathBuf {
+    static SEQ: AtomicUsize = AtomicUsize::new(0);
+    let dir = std::env::temp_dir().join(format!(
+        "pmacs-lean4-{}-{}",
+        std::process::id(),
+        SEQ.fetch_add(1, Ordering::Relaxed)
+    ));
+    std::fs::create_dir_all(&dir).unwrap();
+    dir
+}
+
+fn editor(state_dir: &std::path::Path) -> EditorState {
+    let s = EditorState::new();
+    s.lua_host.lua().remove_app_data::<StateDir>();
+    s.lua_host
+        .lua()
+        .set_app_data(StateDir(state_dir.to_path_buf()));
+    exec(&s, "pmacs.lsp.config = {}");
+    s
+}
+
+fn write_file(dir: &std::path::Path, name: &str, body: &str) -> String {
+    let p = dir.join(name);
+    std::fs::write(&p, body).unwrap();
+    p.display().to_string()
+}
+
+fn key(code: KeyCode, mods: KeyModifiers) -> KeyEvent {
+    KeyEvent {
+        code,
+        modifiers: mods,
+        kind: KeyEventKind::Press,
+        state: KeyEventState::NONE,
+    }
+}
+
+fn alt(s: &mut EditorState, c: char) {
+    s.dispatch_key(FrontendId::LOCAL, key(KeyCode::Char(c), KeyModifiers::ALT));
+}
+
+fn type_str(s: &mut EditorState, text: &str) {
+    for ch in text.chars() {
+        s.dispatch_key(
+            FrontendId::LOCAL,
+            key(KeyCode::Char(ch), KeyModifiers::NONE),
+        );
+    }
+}
+
+fn exec(s: &EditorState, src: &str) {
+    s.lua_host.lua().load(src.to_string()).exec().unwrap();
+}
+
+fn eval<T: mlua::FromLuaMulti>(s: &EditorState, src: &str) -> T {
+    s.lua_host.lua().load(src.to_string()).eval().unwrap()
+}
+
+fn buffer_text(s: &EditorState) -> String {
+    let b: mlua::String = eval(
+        s,
+        "local b = pmacs.window.buffer(); return b:slice(0, b:len())",
+    );
+    String::from_utf8_lossy(&b.as_bytes()).into_owned()
+}
+
+fn cursor(s: &EditorState) -> i64 {
+    eval(s, "return pmacs.editor.cursor()")
+}
+
+/// Fresh editor visiting `name` (created in the state tempdir) with
+/// `body` on disk, cursor at 0.
+fn editor_visiting(name: &str, body: &str) -> EditorState {
+    let dir = fresh_state_dir();
+    let s = editor(&dir);
+    let f = write_file(&dir, name, body);
+    exec(&s, &format!("pmacs.buffer.find_or_open({f:?})"));
+    exec(&s, "pmacs.editor.goto_byte(0)");
+    s
+}
+
+fn major_mode(s: &EditorState) -> Option<String> {
+    eval(s, "return pmacs.buffer.major_mode(pmacs.window.buffer())")
+}
+
+// ---------------------------------------------------------------------------
+// Criterion 3 — major mode
+// ---------------------------------------------------------------------------
+
+#[test]
+fn acc3_opening_a_lean_file_sets_the_lean4_major_mode() {
+    let s = editor_visiting("Basic.lean", "def x : Nat := 1\n");
+    assert_eq!(
+        major_mode(&s).as_deref(),
+        Some("lean4"),
+        "a .lean file carries the lean4 major mode"
+    );
+}
+
+// ---------------------------------------------------------------------------
+// Criterion 4 — modeline aliasing (Q#LN2)
+// ---------------------------------------------------------------------------
+
+#[test]
+fn acc4_emacs_and_vim_modelines_spelling_lean_resolve_to_lean4() {
+    // The grammar entry is `lean4`, but `-*- mode: lean -*-` and `ft=lean`
+    // are what people write. Both must land on the same mode, or a file
+    // with an explicit modeline is stranded with no grammar.
+    //
+    // Deliberately on a `.txt` path: if the fixture were `.lean`, the
+    // extension alone would produce `lean4` and the assertion would pass
+    // with the alias table empty — the vacuous shape.
+    for body in [
+        "-- -*- mode: lean -*-\ndef x : Nat := 1\n",
+        "-- vim: ft=lean\ndef x : Nat := 1\n",
+    ] {
+        let s = editor_visiting("modeline.txt", body);
+        assert_eq!(
+            major_mode(&s).as_deref(),
+            Some("lean4"),
+            "modeline {body:?} resolves through the alias to lean4"
+        );
+    }
+}
+
+#[test]
+fn acc4b_the_lean_alias_is_load_bearing() {
+    // Non-vacuity guard for acc4: with the alias removed, the same
+    // fixture resolves to the raw `lean` name instead. If this ever
+    // reports `lean4`, acc4 is proving nothing.
+    let s = editor_visiting("modeline.txt", "x\n");
+    exec(&s, "pmacs.parse.modeline_aliases.lean = nil");
+    let dir = fresh_state_dir();
+    let f = write_file(&dir, "other.txt", "-- -*- mode: lean -*-\ndef x := 1\n");
+    exec(&s, &format!("pmacs.buffer.find_or_open({f:?})"));
+    assert_eq!(
+        major_mode(&s).as_deref(),
+        Some("lean"),
+        "without the alias the modeline name is not normalized"
+    );
+}
+
+// ---------------------------------------------------------------------------
+// Criterion 9 — comment toggle (Q#LN5)
+// ---------------------------------------------------------------------------
+
+#[test]
+fn acc9_comment_toggle_round_trips_with_the_dash_dash_prefix() {
+    let mut s = editor_visiting("Basic.lean", "def x : Nat := 1\ndef y : Nat := 2\n");
+    exec(&s, "pmacs.editor.goto_byte(0)");
+    alt(&mut s, ';');
+    assert_eq!(
+        buffer_text(&s),
+        "-- def x : Nat := 1\ndef y : Nat := 2\n",
+        "M-; comments a Lean line with `-- `"
+    );
+    // Round trip, including the padding space.
+    exec(&s, "pmacs.editor.goto_byte(0)");
+    alt(&mut s, ';');
+    assert_eq!(
+        buffer_text(&s),
+        "def x : Nat := 1\ndef y : Nat := 2\n",
+        "M-; uncomments it exactly"
+    );
+}
+
+// ---------------------------------------------------------------------------
+// Criterion 10 — pairs (Q#LN6)
+// ---------------------------------------------------------------------------
+
+#[test]
+fn acc10_lean_bracket_pairs_close_and_the_prime_does_not() {
+    // The three Unicode brackets are the reason this decision exists: all
+    // are outside the nine built-in pair chars, so they exercise the
+    // user-extended pair path rather than the frontends' optimistic
+    // classifier.
+    for (opener, expected) in [("⟨", "⟨⟩"), ("⦃", "⦃⦄"), ("⟮", "⟮⟯")] {
+        let mut s = editor_visiting("Basic.lean", "");
+        exec(&s, "pmacs.editor.goto_byte(0)");
+        type_str(&mut s, opener);
+        assert_eq!(
+            buffer_text(&s),
+            expected,
+            "typing {opener} inserts the closing half"
+        );
+        assert_eq!(
+            cursor(&s),
+            i64::try_from(opener.len()).expect("opener length fits"),
+            "the point sits between the pair"
+        );
+    }
+}
+
+#[test]
+fn acc10b_the_prime_suffix_does_not_pair_in_lean() {
+    // Lean uses `'` as a primed-identifier suffix (`h'`, `foo'`), so
+    // pairing it would fight the user on nearly every proof.
+    let mut s = editor_visiting("Basic.lean", "");
+    exec(&s, "pmacs.editor.goto_byte(0)");
+    type_str(&mut s, "h'");
+    assert_eq!(
+        buffer_text(&s),
+        "h'",
+        "the prime is a suffix in Lean, not an opener"
+    );
+}
+
+// ---------------------------------------------------------------------------
+// Criterion 11 — markdown fences (Q#LN17)
+// ---------------------------------------------------------------------------
+
+/// Parse `src` as markdown and return the child layer language names.
+///
+/// Goes through the real `_parse_now` injection path rather than reading
+/// the alias table: `pmacs.parse.injection_aliases` is a documented
+/// WRITE-ONLY proxy (the canonical map lives Rust-side), so an
+/// alias-table read would prove nothing about what the parser does.
+fn markdown_layer_languages(src: &[u8]) -> Vec<String> {
+    let state = EditorState::new();
+    let buf_id = state
+        .lua_host
+        .registry()
+        .borrow_mut()
+        .create_from_bytes("doc.md".to_owned(), src);
+    state
+        .lua_host
+        .lua()
+        .globals()
+        .set("BUF", pmacs::lua_bindings::BufferIdLua(buf_id))
+        .expect("bind BUF");
+    state
+        .lua_host
+        .lua()
+        .load("pmacs.parse._parse_now(BUF, 'markdown')")
+        .exec()
+        .expect("synchronous parse");
+    let bundle = state
+        .syntax_registry
+        .view(buf_id)
+        .and_then(|h| h.current())
+        .expect("installed bundle");
+    bundle
+        .layers
+        .iter()
+        .map(|l| l.language_name.clone())
+        .collect()
+}
+
+#[test]
+fn acc11_lean_and_lean4_markdown_fences_both_inject_the_lean_grammar() {
+    // Both spellings must resolve to the same grammar: `lean4` is the entry
+    // name and `lean` goes through the injection alias. A ```lean fence is
+    // overwhelmingly Lean 4 in practice, which is why the Lean 3 spelling
+    // is mapped forward rather than left unresolved (Q#LN17).
+    for fence in ["lean", "lean4"] {
+        let src = format!("# Doc\n\n```{fence}\ndef x : Nat := 1\n```\n");
+        let langs = markdown_layer_languages(src.as_bytes());
+        assert!(
+            langs.iter().any(|l| l == "lean4"),
+            "```{fence} injects a lean4 child layer; got {langs:?}"
+        );
+    }
+}
+
+#[test]
+fn acc11b_an_unknown_fence_name_still_injects_nothing() {
+    // Non-vacuity guard for acc11: the alias must be what resolves `lean`,
+    // not some catch-all that would light up any fence name.
+    let langs = markdown_layer_languages(b"# Doc\n\n```leen\ndef x := 1\n```\n");
+    assert!(
+        !langs.iter().any(|l| l == "lean4"),
+        "a misspelled fence must not reach the lean4 grammar; got {langs:?}"
+    );
+}
+
+// ---------------------------------------------------------------------------
+// Criterion 12 — no toolchain required
+// ---------------------------------------------------------------------------
+
+#[test]
+fn acc12_stage1_spawns_no_process_and_needs_no_lean_toolchain() {
+    // Stage 1 is grammar + Lua tables only. Opening a Lean file must not
+    // reach for `lake`, `lean`, or `elan` — the LSP arrives in Stage 3, and
+    // even then it is fallible by design (Q#LN7).
+    //
+    // Asserted through the process supervisor rather than by inspection:
+    // opening the file leaves the child-process list exactly as it was.
+    let s = editor_visiting("Basic.lean", "def x : Nat := 1\n");
+    let procs: i64 = eval(&s, "return #pmacs.process.list()");
+    assert_eq!(procs, 0, "opening a Lean buffer spawns no child process");
+    let servers: i64 = eval(&s, "return #pmacs.lsp.list()");
+    assert_eq!(servers, 0, "Stage 1 attaches no language server");
+}