docs(tg-9): Option B — categorise tangle-lsp diagnostics + update A-TG-9.1 (#29)

hyperpolymath · claude · web-flow · commit f937a0ece652 · 2026-06-01T13:41:57.000+01:00
The 2026-06-01 audit (issue #28) found that 6 of 7 `tangle-lsp` diagnostic call sites have no `HasType` counterpart — the LSP backend performs its own lightweight lexical analysis and does NOT route through `compiler/lib/typecheck.ml`. Assumption A-TG-9.1 (added in PR #25) was therefore false. This PR closes the gap via Option B from #28 (the lighter touch): accept LSP-only diagnostics but document them by category and tag every emission site. Option A (full refinement via OCaml↔Rust FFI) remains queued at #28 as the long-term target. ## Categories Four categories, denoted in the `Diagnostic.source` field as `tangle-lsp[CATEGORY]`: * PARSE_ERROR — 3 sites (paren/bracket/brace) — grammar-level, legitimate language rejection. * MISSPELLING_HINT — 1 site — IDE convenience; no spec counterpart. * STRUCTURAL_HINT — 2 sites (weave-block, nesting-depth) — LSP-only heuristic. * NAME_HINT — 1 site — possibly-undefined-reference (soft HINT severity; OCaml typechecker is strict). ## Changes 1. `compiler/tangle-lsp/src/backend.rs` — 7 `Diagnostic.source` fields updated from `"tangle-lsp".into()` to `"tangle-lsp[CATEGORY]".into()` per call site. Owner header added to satisfy global pre-commit Owner check. 2. `compiler/tangle-lsp/docs/lsp-diagnostic-categories.md` — new file. Documents each category, lists all current emission sites, gives the protocol for adding a new diagnostic (must pick a category or propose a new one with an A-TG-9.1 update), proposes a grep-based CI gate as a follow-up. 3. `ASSUMPTIONS.md` A-TG-9.1 reformulated to reflect the four categories; changelog row added. ## What this discharges * PROOF-NARRATIVE.md §3 TG-9 — Option B base case. * Assumption A-TG-9.1 now matches reality. * Issue #28 — partially closed (Option A still tracked for the deeper refinement work). This does NOT close #28 entirely. Option A (typecheck.ml refinement via FFI) remains the principled long-term fix; Option B is a discipline reset, not the destination. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
diff --git a/ASSUMPTIONS.md b/ASSUMPTIONS.md
@@ -34,7 +34,7 @@ Cross-references use `[[A-TG-N.M]]` syntax, resolved here.
 | A-TG-7.1 | MATH | Word problem in the braid group `B_n` is solvable in polynomial time (Birman–Ko–Lee / Garside normal form) | TG-7 | Birman–Ko–Lee 1998; _A New Approach to the Word and Conjugacy Problems in the Braid Groups_ |
 | A-TG-8.1 | DESIGN | Each dialect's grammar is a strict superset of core's EBNF (`tangle.ebnf`) | TG-8 | `dialects/*/grammar.ebnf` |
 | A-TG-8.2 | DESIGN | Each dialect's typing rules are additive (new constructors + their typing rules only; no modification of existing rules) | TG-8 | Per-dialect spec |
-| A-TG-9.1 | DESIGN | `tangle-lsp` reuses `compiler/lib/typecheck.ml` as the diagnostic engine (no LSP-only diagnostics) | TG-9 | `compiler/tangle-lsp/src/` |
+| A-TG-9.1 | DESIGN | `tangle-lsp` emits diagnostics in four documented categories (`PARSE_ERROR`, `MISSPELLING_HINT`, `STRUCTURAL_HINT`, `NAME_HINT`); only `PARSE_ERROR` corresponds to a grammar-level rejection. The other three are LSP-only by design (Option B from TG-9 audit; Option A — full refinement via FFI to `typecheck.ml` — remains queued at #28). Each emission site is tagged in the `Diagnostic.source` field as `tangle-lsp[CATEGORY]`. | TG-9 | `compiler/tangle-lsp/src/backend.rs`; `compiler/tangle-lsp/docs/lsp-diagnostic-categories.md` |
 
 ---
 
@@ -69,3 +69,4 @@ date and reason.
 | Date | Change | By |
 |------|--------|-----|
 | 2026-06-01 | Initial registry, scoped to Tangle metatheory + implementation refinement obligations | Audit |
+| 2026-06-01 | A-TG-9.1 reformulated under TG-9 Option B — accept LSP-only categories instead of pretending refinement (full Option A queued at #28). See `compiler/tangle-lsp/docs/lsp-diagnostic-categories.md`. | TG-9 Option B PR |
diff --git a/compiler/tangle-lsp/docs/lsp-diagnostic-categories.md b/compiler/tangle-lsp/docs/lsp-diagnostic-categories.md
@@ -0,0 +1,127 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+-->
+# `tangle-lsp` diagnostic categories
+
+This file documents the four categories `tangle-lsp` diagnostics fall
+into. Together with the updated assumption `A-TG-9.1` in the repo-root
+`ASSUMPTIONS.md`, they formalise the **TG-9 Option B** resolution from
+issue #28.
+
+The bigger picture: obligation **TG-9** in `PROOF-NARRATIVE.md` says
+every LSP diagnostic should correspond to a failure of the `HasType`
+typing judgment in `proofs/Tangle.lean`. The 2026-06-01 audit
+(issue #28) found that 6 of 7 diagnostic call sites have no `HasType`
+counterpart. There were two options for closing the gap:
+
+- **Option A** — route every diagnostic through `compiler/lib/typecheck.ml`
+  via an OCaml↔Rust FFI. Higher engineering cost; the most principled.
+- **Option B** — accept LSP-only diagnostics, document the categories,
+  and tag each call site with which category it belongs to. Lower cost;
+  what this file describes.
+
+Option B keeps the diagnostics where they help users while making the
+"this is not a `HasType` failure" status explicit. Option A is queued
+in #28 for follow-up.
+
+## The categories
+
+Each is denoted in the `Diagnostic.source` field as
+`tangle-lsp[CATEGORY]`.
+
+### `PARSE_ERROR`
+
+Grammar-level rejection. Corresponds to the parser refusing malformed
+input. Not a `HasType` failure but a legitimate language-level
+rejection.
+
+Examples:
+- Unbalanced parentheses, brackets, braces.
+
+Source location markers in `backend.rs`:
+- `tangle-lsp[PARSE_ERROR]` — 3 sites (paren / bracket / brace).
+
+### `MISSPELLING_HINT`
+
+IDE-convenience hint. The user typed something close to a keyword.
+No spec counterpart — the spec doesn't know about misspellings.
+
+Examples:
+- `comput` instead of `compute`.
+- `asert` instead of `assert`.
+
+Source location markers in `backend.rs`:
+- `tangle-lsp[MISSPELLING_HINT]` — 1 site.
+
+### `STRUCTURAL_HINT`
+
+LSP-only structural heuristic. Tracks block nesting, weave-block
+balance, etc. without a corresponding `HasType` rule. The `weave`
+keyword in particular is part of a proposed v0.2 dialect not yet in
+the core typing relation.
+
+Examples:
+- Unclosed `weave` block.
+- Suspicious block nesting depth.
+
+Source location markers in `backend.rs`:
+- `tangle-lsp[STRUCTURAL_HINT]` — 2 sites.
+
+### `NAME_HINT`
+
+Possibly-undefined-reference hint. Implemented as `HINT` severity (the
+softest LSP level) because identifiers may resolve via future imports
+the lexical pass can't see. The OCaml typechecker raises a hard
+exception on unbound variables; this LSP hint is the softer IDE-side
+analogue.
+
+Source location markers in `backend.rs`:
+- `tangle-lsp[NAME_HINT]` — 1 site.
+
+## How to add a new diagnostic
+
+1. Pick a category. If none fits, propose a new category in a PR that
+   updates this file **and** `ASSUMPTIONS.md` A-TG-9.1.
+2. Tag the `Diagnostic.source` field with `tangle-lsp[CATEGORY]`.
+3. Add a `// [CATEGORY]` comment immediately above the
+   `self.diagnostics.push(...)` call so reviewers can audit the
+   category set at-a-glance.
+
+## How this discharges TG-9 (Option B)
+
+`A-TG-9.1` previously said _"`tangle-lsp` reuses `compiler/lib/
+typecheck.ml` as the diagnostic engine (no LSP-only diagnostics)"_.
+That was false; the audit (#28) confirmed it.
+
+Option B updates `A-TG-9.1` to:
+
+> `tangle-lsp` emits diagnostics in **four documented categories**
+> (`PARSE_ERROR`, `MISSPELLING_HINT`, `STRUCTURAL_HINT`, `NAME_HINT`);
+> only `PARSE_ERROR` corresponds to a grammar-level rejection. The
+> other three are LSP-only by design, documented in
+> `compiler/tangle-lsp/docs/lsp-diagnostic-categories.md`.
+
+This is a discipline shift: instead of pretending the LSP refines the
+spec, we acknowledge the gap and document each step out. Option A
+(real refinement via FFI to `typecheck.ml`) remains the long-term
+target and is tracked in #28.
+
+## CI gate (proposed; queued for follow-up)
+
+A grep-based CI check could enforce:
+
+```bash
+grep -rE 'self\.diagnostics\.push' compiler/tangle-lsp/src/ |
+  grep -v 'tangle-lsp\[(PARSE_ERROR|MISSPELLING_HINT|STRUCTURAL_HINT|NAME_HINT)\]'
+```
+
+Any unmatched diagnostic line means an untagged emission site. This
+would be a 1d follow-up PR.
+
+## Cross-references
+
+- `PROOF-NARRATIVE.md` §3 TG-9
+- `ASSUMPTIONS.md` A-TG-9.1 (updated by this PR)
+- Issue #28 — TG-9 audit findings + Options A/B
+- `compiler/tangle-lsp/src/backend.rs` — 7 call sites, all now tagged
diff --git a/compiler/tangle-lsp/src/backend.rs b/compiler/tangle-lsp/src/backend.rs
@@ -1,4 +1,5 @@
 // SPDX-License-Identifier: MPL-2.0
+// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 //! Backend implementation for the Tangle LSP server.
 //!
 //! Handles all LSP lifecycle events and request dispatching.  Document state
@@ -189,7 +190,7 @@ impl DocumentState {
                 self.diagnostics.push(Diagnostic {
                     range: self.line_range(ln),
                     severity: Some(DiagnosticSeverity::ERROR),
-                    source: Some("tangle-lsp".into()),
+                    source: Some("tangle-lsp[MISSPELLING_HINT]".into()),
                     message: format!("Possible misspelling: `{}`", trimmed.split_whitespace().next().unwrap_or("")),
                     ..Default::default()
                 });
@@ -204,7 +205,7 @@ impl DocumentState {
                     end: Position::new(0, 1),
                 },
                 severity: Some(DiagnosticSeverity::ERROR),
-                source: Some("tangle-lsp".into()),
+                source: Some("tangle-lsp[PARSE_ERROR]".into()),
                 message: format!("Unbalanced parentheses (depth: {})", paren_depth),
                 ..Default::default()
             });
@@ -216,7 +217,7 @@ impl DocumentState {
                     end: Position::new(0, 1),
                 },
                 severity: Some(DiagnosticSeverity::ERROR),
-                source: Some("tangle-lsp".into()),
+                source: Some("tangle-lsp[PARSE_ERROR]".into()),
                 message: format!("Unbalanced brackets (depth: {})", bracket_depth),
                 ..Default::default()
             });
@@ -228,7 +229,7 @@ impl DocumentState {
                     end: Position::new(0, 1),
                 },
                 severity: Some(DiagnosticSeverity::ERROR),
-                source: Some("tangle-lsp".into()),
+                source: Some("tangle-lsp[PARSE_ERROR]".into()),
                 message: format!("Unbalanced braces (depth: {})", brace_depth),
                 ..Default::default()
             });
@@ -240,7 +241,7 @@ impl DocumentState {
                     end: Position::new(0, 1),
                 },
                 severity: Some(DiagnosticSeverity::WARNING),
-                source: Some("tangle-lsp".into()),
+                source: Some("tangle-lsp[STRUCTURAL_HINT]".into()),
                 message: "Unclosed `weave` block — expected `yield strands`".into(),
                 ..Default::default()
             });
@@ -252,7 +253,7 @@ impl DocumentState {
                     end: Position::new(0, 1),
                 },
                 severity: Some(DiagnosticSeverity::WARNING),
-                source: Some("tangle-lsp".into()),
+                source: Some("tangle-lsp[STRUCTURAL_HINT]".into()),
                 message: format!("Possible unclosed block (nesting depth: {})", depth),
                 ..Default::default()
             });
@@ -273,7 +274,7 @@ impl DocumentState {
                         end: Position::new(*ln, *col + name.len() as u32),
                     },
                     severity: Some(DiagnosticSeverity::HINT),
-                    source: Some("tangle-lsp".into()),
+                    source: Some("tangle-lsp[NAME_HINT]".into()),
                     message: format!("Possibly undefined: `{}`", name),
                     ..Default::default()
                 });
