docs: LSP_SERVER.md, VS Code LSP client, and post-#222 documentation sweep - #726
Merged
Conversation
…222 sweep New LSP_SERVER.md: what the language server is, install/editor wiring, the standard feature surface, the warm incremental verification core, and full wire shapes for the four agent-facing custom methods with the speculate -> inspect -> propose loop. Served on-domain at veralang.dev/LSP_SERVER.md (same build_site.py treatment as SKILL.md), sitemapped, indexed in llms.txt, embedded in llms-full.txt. VS Code extension 0.2.0: starts vera lsp automatically for .vera files (vscode-languageclient, settings vera.lsp.enabled/path, restart command), degrading gracefully to grammar-only when the binary or npm install is absent. Requires VS Code 1.82+. veralang.dev overhaul: section 06 Get Started (VS Code row starts the server; [lsp] install path) and section 07 for machines reframed around read-vs-interrogate with a fourth agent-card and a speculativeEdit proof-delta sample; section 04 feature box; status sentence. Sweep: vera lsp joins the command lists in README/CLAUDE/AGENTS/SKILL; README editor-support/features/install/tree updated; AGENTS.md gains the agent-facing custom-methods section; KNOWN_ISSUES drops the stale LSP-server row and gains three real LSP limitations (#724 single-file model, #181 parameter-only slot goto, #725 handler-unaware addEffect); module-map lsp/ line count corrected (a v0.0.168 update silently failed); release-count figures corrected to the actual tag count (v0.0.24.1 made releases = version + 1, uncounted since). Allowlist re-keyed after SKILL.md edits. Release prep for v0.0.169. Co-Authored-By: Claude <noreply@anthropic.invalid>
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #726 +/- ##
=======================================
Coverage 90.90% 90.90%
=======================================
Files 70 70
Lines 24854 24854
Branches 292 292
=======================================
Hits 22594 22594
Misses 2253 2253
Partials 7 7
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
|
Note Reviews pausedIt looks like this branch is under active development. To avoid overwhelming you with review comments due to an influx of new commits, CodeRabbit has automatically paused this review. You can configure this behavior by changing the Use the following commands to manage reviews:
Use the checkboxes below for quick actions:
📝 WalkthroughWalkthroughAdds v0.0.169: LSP server user manual and LSP contract, VS Code language-client wiring and manifest, typed-hole grammar support across editors, site indexing and SKILL allowlist updates, and coordinated release/version metadata changes. ChangesLSP documentation and VS Code integration
Sequence Diagram(s)sequenceDiagram
participant Client
participant VeraLSP
participant Z3Core
Client->>VeraLSP: didOpen / didChange
VeraLSP->>Z3Core: incremental verification
VeraLSP-->>Client: publish diagnostics + tier hints
Client->>VeraLSP: vera/speculativeEdit
VeraLSP->>Z3Core: verify speculative delta
VeraLSP-->>Client: proof-delta result
Client->>VeraLSP: vera/proposeEdit
VeraLSP->>Z3Core: apply edit and re-verify
VeraLSP-->>Client: updated diagnostics/state
Estimated code review effort🎯 3 (Moderate) | ⏱️ ~25 minutes Possibly related PRs
Suggested labels
🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (4 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches🧪 Generate unit tests (beta)
Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 2
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
scripts/build_site.py (1)
204-206:⚠️ Potential issue | 🟡 Minor | ⚡ Quick winFix absolute-link rewriting for directory targets.
_abs_links()always emits.../blob/main/..., which breaks repo-directory links (e.g.editors/vscode/) onceLSP_SERVER.mdis published todocs/LSP_SERVER.md.Suggested fix
- parts_inner.append(link_re.sub( - lambda m: f"[{m.group(1)}]({REPO}/blob/main/{m.group(2)})", line - )) + def _to_abs(match: re.Match[str]) -> str: + label = match.group(1) + rel = match.group(2) + rel_path = rel.split("#", 1)[0] + anchor = f"#{rel.split('#', 1)[1]}" if "#" in rel else "" + kind = "tree" if rel_path.endswith("/") else "blob" + return f"[{label}]({REPO}/{kind}/main/{rel_path}{anchor})" + + parts_inner.append(link_re.sub(_to_abs, line))As per coding guidelines, Markdown documentation should avoid broken links; this generator currently creates broken directory URLs in published docs.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@scripts/build_site.py` around lines 204 - 206, The _abs_links() replacement always injects "/blob/main/" which breaks links that should point to repository directories; update the link_re substitution (the lambda that builds f"[{m.group(1)}]({REPO}/blob/main/{m.group(2)})") to detect directory targets (e.g., m.group(2) ends with '/' or has no file extension) and use "/tree/main/" for those, keeping "/blob/main/" for file targets; ensure the logic is applied where parts_inner.append(...) is called and that REPO is still used as the base.Source: Coding guidelines
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@editors/textmate/README.md`:
- Line 21: Update the README line that reads "The grammar covers the full Vera
language as of v0.0.168." to reference the current release by changing v0.0.168
to v0.0.169 so the editor docs reflect the v0.0.169 release; locate and edit
that exact sentence in the README.md (the line mentioning "The grammar covers
the full Vera language as of ...") and replace the version token.
In `@HISTORY.md`:
- Line 357: Update the tagged-release count in the summary line that currently
reads "Total: **810+ commits, 170 tagged releases, 62 active development
days.**" to "169 tagged releases" (change 170 → 169) and then ensure the same
summary in README.md is updated the same way so both files stay synchronized;
locate the "Total:" summary line in HISTORY.md and the corresponding summary
line in README.md and make the numeric change.
---
Outside diff comments:
In `@scripts/build_site.py`:
- Around line 204-206: The _abs_links() replacement always injects "/blob/main/"
which breaks links that should point to repository directories; update the
link_re substitution (the lambda that builds
f"[{m.group(1)}]({REPO}/blob/main/{m.group(2)})") to detect directory targets
(e.g., m.group(2) ends with '/' or has no file extension) and use "/tree/main/"
for those, keeping "/blob/main/" for file targets; ensure the logic is applied
where parts_inner.append(...) is called and that REPO is still used as the base.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: 784cb4d1-1d98-4e9f-89c0-dbabc3cccb6e
⛔ Files ignored due to path filters (9)
docs/LSP_SERVER.mdis excluded by!docs/**docs/SKILL.mdis excluded by!docs/**docs/index.htmlis excluded by!docs/**docs/index.mdis excluded by!docs/**docs/llms-full.txtis excluded by!docs/**docs/llms.txtis excluded by!docs/**docs/sitemap.xmlis excluded by!docs/**editors/vscode/package-lock.jsonis excluded by!**/package-lock.jsonuv.lockis excluded by!**/*.lock,!uv.lock
📒 Files selected for processing (20)
AGENTS.mdCHANGELOG.mdCLAUDE.mdHISTORY.mdKNOWN_ISSUES.mdLSP_SERVER.mdREADME.mdSKILL.mdeditors/README.mdeditors/textmate/README.mdeditors/vscode/CHANGELOG.mdeditors/vscode/README.mdeditors/vscode/extension.jseditors/vscode/package.jsonpyproject.tomlscripts/build_site.pyscripts/check_site_assets.pyscripts/check_skill_examples.pyvera/README.mdvera/__init__.py
CodeRabbit asked for the textmate coverage marker to say v0.0.169; auditing that claim found the one grammar addition since v0.0.100 — typed holes (?) — was unhighlighted in both grammars. Both now scope it as constant.language.hole.vera (lookarounds avoid accidental matches), the marker is bumped honestly, and the VS Code README/ CHANGELOG document the scope. Skip-changelog: editor-grammar amendment within this PR's unreleased v0.0.169 section
There was a problem hiding this comment.
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
editors/textmate/README.md (1)
50-65:⚠️ Potential issue | 🟡 Minor | ⚡ Quick winAdd the typed hole scope to the TextMate README scope reference table.
Line 21 now claims the grammar "covers the full Vera language as of v0.0.169", but the scope reference table (lines 50–65) does not include an entry for
?(typed hole), despite the grammar file now supporting it with scopeconstant.language.hole.vera. The VS Code README includes this entry in its scope table (line 123).For consistency with the grammar and the VS Code documentation, add a row to the TextMate scope table:
| `?` (typed hole) | `constant.language.hole.vera` |Place it after the
true,false,purerow and before the->row.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@editors/textmate/README.md` around lines 50 - 65, The README's TextMate scope reference table is missing the typed-hole entry; add a new table row containing "`?` (typed hole)" mapped to "constant.language.hole.vera" and insert it immediately after the "`true`, `false`, `pure` | `constant.language.vera`" row and before the "`->` | `keyword.operator.arrow.vera`" row so the table matches the grammar and VS Code README.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Outside diff comments:
In `@editors/textmate/README.md`:
- Around line 50-65: The README's TextMate scope reference table is missing the
typed-hole entry; add a new table row containing "`?` (typed hole)" mapped to
"constant.language.hole.vera" and insert it immediately after the "`true`,
`false`, `pure` | `constant.language.vera`" row and before the "`->` |
`keyword.operator.arrow.vera`" row so the table matches the grammar and VS Code
README.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: 62383e06-65a7-44c2-b0e1-d796bc4c62ce
📒 Files selected for processing (5)
editors/textmate/README.mdeditors/textmate/Vera.tmbundle/Syntaxes/Vera.tmLanguageeditors/vscode/CHANGELOG.mdeditors/vscode/README.mdeditors/vscode/syntaxes/vera.tmLanguage.json
Key-features grid flows as masonry columns (columns: 3 260px) instead of stretch-to-tallest grid rows, killing the whitespace gaps; the Language server box text tightened to neighbour length. The VS Code editor row breaks into two left-justified lines (colon dropped). The section-07 agent cards become one bordered list panel: mono filename column at a fixed 9.5rem, descriptions aligned to a common edge, stacking vertically under 780px. Skip-changelog: hand-written landing-page styling within this PR's unreleased v0.0.169 section
In the stacked sub-780px layout the agent-list filename kept its 9.5rem flex-basis, which becomes HEIGHT in a column flex container — a 152px void under every filename. The media query now resets it (flex:none): 21px filenames, uniform rows. The section-06 language- server paragraph drops its 62ch cap and spans the full column width, matching the install code block above it. Skip-changelog: hand-written landing-page styling within this PR's unreleased v0.0.169 section
#726) The features-grid and install-section links now match the sibling DE_BRUIJN.md convention (GitHub blob URL, rendered markdown for human readers); the for-machines section keeps the on-domain /LSP_SERVER.md alternates by design, paired with /SKILL.md. Skip-changelog: hand-written landing-page link targets within this PR's unreleased v0.0.169 section
The veralang.dev/SKILL.md copy exists to give THE agent entrypoint a definitive URL — a deliberate singleton, not a pattern. LSP_SERVER.md now follows the same convention as every other doc: GitHub links everywhere (including the for-machines cards, matching AGENTS.md and CLAUDE.md), indexed in llms.txt via the raw URL, embedded in full in llms-full.txt. The generated docs/LSP_SERVER.md copy, its sitemap entry, and the build/check wiring are removed. Skip-changelog: amends this PR's own unreleased v0.0.169 entry, which is corrected in the same commit
The TextMate/VS Code rows in Get Started are grouped under the same 2px flame-tinted left border + 1rem padding as the code-sample asides in section 02, so the annotation device reads consistently across sections. Skip-changelog: hand-written landing-page styling within this PR's unreleased v0.0.169 section
The hole pattern was added to both grammars but the scope-reference row only to the VS Code README; the TextMate table now matches. Skip-changelog: editor-doc amendment within this PR's unreleased v0.0.169 section
rgba(255,176,128,.3) was tuned for the dark section-02 band and washed out on cream; the line now uses solid var(--flame-300), matching the section-01 thesis blockquote — the established vertical-line treatment for light sections. Skip-changelog: hand-written landing-page styling within this PR's unreleased v0.0.169 section
The section-07 speculativeEdit response is now properly indented (one key per line) and syntax-highlighted with the page's existing palette: keys in .sl, string values in .str, literals in .num, comment in .cm. Skip-changelog: hand-written landing-page styling within this PR's unreleased v0.0.169 section
Owner
Author
|
@coderabbitai The outside-diff finding on editors/textmate/README.md is fixed in 0b3abec — the scope-reference table now carries the |
|
Tip For best results, initiate chat on the files or code changes.
|
GUI-launched VS Code does not inherit a shell PATH, so the default 'vera' resolution failed (or hit a stale shim) for every from-source install — the exact quiet failure the user diagnosed. Resolution order is now: explicit vera.lsp.path setting, then a workspace-local venv (.venv/bin/vera, .venv\Scripts\vera.exe), then PATH; a standard clone needs zero configuration. Spawn failure now surfaces ONE warning with an Open Settings action instead of only an output-channel line. Resolution order documented in the setting description, extension README, LSP_SERVER.md, and both CHANGELOGs. Also files #727 (duplicate E501 diagnostics for a violating call site, surfaced while screenshotting the hover) and restores the KNOWN_ISSUES Bugs table to track it. Skip-changelog: amends this PR's own unreleased v0.0.169 entry in the same commit
…SSUES (#726) Skip-changelog: tracking-table row for a newly filed bug
#726) The extension-fix commit edited LSP_SERVER.md (a build_site source as of this PR) without regenerating its llms-full.txt embed — caught by CI's unconditional check but not locally, because the pre-commit site-assets hook's files filter predates LSP_SERVER.md becoming a source. The filter now includes it. Skip-changelog: regenerated artefact + hook-filter amendment within this PR
There was a problem hiding this comment.
Actionable comments posted: 2
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@editors/vscode/extension.js`:
- Around line 42-64: resolveServerCommand currently picks the first .venv binary
it finds across all workspaceFolders which can pick the wrong project's
toolchain in multi-root workspaces; change the lookup to prefer the workspace
folder associated with the active editor (use
vscode.window.activeTextEditor?.document and
vscode.workspace.getWorkspaceFolder) and only fall back to scanning other
workspaceFolders if no active-folder candidate is found, so resolveServerCommand
first searches the active editor's folder for the .venv paths before scanning
the rest.
In `@LSP_SERVER.md`:
- Around line 45-49: Update the VS Code auto-start documentation paragraph that
currently lists `.venv/bin/vera` to also mention the Windows workspace-venv
probe `.venv\Scripts\vera.exe` so readers know the extension auto-detects a
Windows virtualenv executable; edit the sentence that references
`.venv/bin/vera` in LSP_SERVER.md (the VS Code / bundled extension description)
to include the Windows path and a short parenthetical note about Windows
support.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: e7293bd1-9cc0-4149-a77a-40bbe902c6d9
📒 Files selected for processing (7)
CHANGELOG.mdKNOWN_ISSUES.mdLSP_SERVER.mdeditors/vscode/CHANGELOG.mdeditors/vscode/README.mdeditors/vscode/extension.jseditors/vscode/package.json
…und) In a multi-root workspace the first workspaceFolder's .venv could belong to a different project; resolveServerCommand now probes the folder owning the active document first, then the remaining folders. LSP_SERVER.md documents the Windows probe path (.venv\Scripts\ vera.exe) alongside the POSIX one; llms-full embed regenerated. Skip-changelog: extension amendment within this PR's unreleased v0.0.169 entry
Owner
Author
|
@coderabbitai The re-surfaced outside-diff finding on editors/textmate/README.md was already addressed in 0b3abec — the scope table carries |
|
Tip For best results, initiate chat on the files or code changes.
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Documentation sweep following the issue 222 LSP arc (v0.0.161–v0.0.168), plus the VS Code extension's LSP client. Three parallel audits (limitations tables, capability coverage, cross-doc consistency) drove the work list; everything below was verified against the repo before changing.
New: LSP_SERVER.md
The language server's user manual: what an LSP server is (briefly), install (
pip install -e ".[lsp]") and editor wiring (VS Code extension or any generic LSP client), the standard feature surface (tier-annotated diagnostics, per-function verification-tier hints, hover, slot go-to-definition, typed-hole completion), what makes ours different — the warm incremental verification core and the four agent-facing custom methods with full request/response shapes (vera/speculativeEdit,vera/proposeEdit,vera/strengthenContract,vera/addEffect) — the typical speculate → inspect → propose agent loop, current limitations, and architecture pointers. No Vera code blocks, so no new example-checker script is needed (JSON/bash only).Indexed in
llms.txt(build_site.py) and linked from README's editor-support and install sections.VS Code extension 0.2.0 — LSP client
extension.js: startsvera lspfor.verafiles viavscode-languageclient^9.0.1 (hence engines 1.75 → 1.82+); settingsvera.lsp.enabled/vera.lsp.path; command Vera: Restart Language Server.npm install(the client library lazilyrequired in try/catch), a missingverabinary, orvera.lsp.enabled: falseall degrade to syntax-highlighting-only with an explanatory line in the output channel, never an error storm.package-lock.jsoncommitted for reproducible from-source installs; verified bynpm install+ module resolution (the only unresolvable import isvscodeitself, which exists only inside the extension host) andnode --check.veralang.dev overhaul (docs/index.html + generated assets)
The landing page's two audience-addressed sections both gain the server, by design rather than as another feature box:
vera lspautomatically", and a closing paragraph covers what the server provides, the standalone[lsp]install, and the generic-LSP-client path.LSP_SERVER.md, a paragraph naming the four custom methods, and a compactspeculativeEditproof-delta sample (JSON — shape-checked against the real response; the HTML example gate ignores non-Vera blocks).Surfacing for agents:
llms.txtindexesLSP_SERVER.md(GitHub raw URL, matching AGENTS.md/FAQ), andllms-full.txtembeds the full text so single-file agent readers see the server manual without a second fetch. Theveralang.dev/SKILL.mdon-domain copy remains a deliberate singleton — the one definitive agent-entrypoint URL — so no second on-domain copy is created; all LSP_SERVER.md links (landing page included) follow the GitHub convention used by every other doc.Landing-page review rounds (from manual review)
Masonry columns for the Key-features grid (kills stretch-to-tallest-row gaps), the VS Code editor row as two left-justified lines, the §07 agent docs as one aligned list panel instead of 3+1 orphaned cards (with the sub-780px flex-basis-becomes-height bug fixed), the §06 server paragraph spanning the full column, and typed-hole grammar coverage in both editors (surfaced by auditing the textmate coverage-marker claim — the one syntax addition since the grammars were written).
Sweep findings fixed
vera lspwas absent from every command list (README, CLAUDE.md, AGENTS.md, SKILL.md) while every sibling command was present — added everywhere, with the[lsp]extra documented in each install section.vera/obligations/+vera/lsp/and LSP_SERVER.md.vera/addEffectpropagation (filed as 725). Both new issues carry full context and are tracked here per the new-issue rule.vera/obligations/+vera/lsp/; feature list gains the language server; install section notes the lighter[lsp]-only path.lsp/line count still said 1203 — the v0.0.168 update ran a sed whose pattern never matched and nothing gates module-map counts; corrected to the measured 1389.v0.0.24.1hotfix broke the releases-equals-version assumption long ago and every bump since inherited the off-by-one. Both locations now carry the measured count (170 including this release).editors/README.mdupdated for the extension's new scope.scripts/fix_allowlists.py --fix(61 entries, duplicate-key audit clean).Audit results that needed no change
Spec-chapter limitation tables (ch. 6, 8, 9, 11, 12) all verified current; FAQ/EXAMPLES/CONTRIBUTING/DESIGN/ENVIRONMENT have no stale LSP claims; CITATION.cff carries no version field (nothing to drift); TESTING.md already documents the LSP test surface thoroughly.
Release prep (v0.0.169)
Version across all 6 tracked sites, CHANGELOG section + compare links, HISTORY row, site assets regenerated; doc-count, version-sync, site-asset, README/SKILL example-checker gates all green; full suite 4,281 passed.
🤖 Generated with Claude Code
Summary by CodeRabbit
New Features
Documentation
Chores