feat(rust): provekit-lsp implementation (spec already in v1.3.0 catalog)#26
Conversation
Lands the Rust peer of the LSP protocol spec at protocol/specs/2026-04-30-lsp-protocol.md (already in v1.3.0 catalog). A language-agnostic LSP coordinator. Reads .provekit/config.toml to discover language plugins. Routes each source file to the correct parser (built-in Rust, or external NDJSON-over-stdio RPC plugin per provekit-lsp-plugin/1). Delegates verification to a configurable JSON-RPC backend. Surface (matches spec + plugin protocol described in examples/lsp-plugins/README.md, landing in PR D): - src/main.rs: tower-lsp server, initialize/textDocument/* handlers, per-document annotation cache, contract-binding diagnostics - src/config.rs: TOML loader for .provekit/config.toml (server backend, per-language plugin or builtin parser) - src/parser.rs: built-in Rust parser using syn for #[provekit::*] attrs - src/plugin.rs: JSON-RPC plugin host (initialize/parse/shutdown) - src/backend.rs: JSON-RPC verifier client Workspace registration: adds "provekit-lsp" to implementations/rust/Cargo.toml [workspace] members; Cargo.lock updated to lock the new transitive deps (tower-lsp 0.20, lsp-types 0.94, tokio 1.43, dashmap 5, etc). Status doc: docs/per-language-status.md gains an LSP Plugin column across all rows, marks Rust LSP as shipping (`+`), and adds a Zig row plus Java status uplift. The matrix change is genuinely cross-PR so the entire diff lands here; PRs B/C/D for Java, Zig, and the example plugins reference this matrix. Sanity: - cargo not installed locally; cannot verify cargo build -p provekit-lsp in this branch. Lockfile copied verbatim from author's working tree (where the impl already built); CI's Rust job will be the canonical build check. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Warning Rate limit exceeded
To keep reviews running without waiting, you can enable usage-based add-on for your organization. This allows additional reviews beyond the hourly cap. Account admins can enable it under billing. ⌛ How to resolve this issue?After the wait time has elapsed, a review can be triggered using the We recommend that you space out your commits to avoid hitting the rate limit. 🚦 How do rate limits work?CodeRabbit enforces hourly rate limits for each developer per organization. Our paid plans have higher rate limits than the trial, open-source and free plans. In all cases, we re-allow further reviews after a brief timeout. Please see our FAQ for further information. ℹ️ Review info⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Pro Run ID: ⛔ Files ignored due to path filters (1)
📒 Files selected for processing (8)
✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Review rate limit: 0/1 reviews remaining, refill in 11 minutes and 45 seconds.Comment |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: d06a286753
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| full_cmd.push("--rpc".to_string()); | ||
| full_cmd.extend_from_slice(args); |
There was a problem hiding this comment.
spawn_direct manually appends --rpc to full_cmd, but spawn() also unconditionally appends --rpc, so direct-path plugin launches receive the flag twice. Many plugin CLIs treat unexpected extra args as errors, so this can prevent external language plugins from starting in real projects that configure plugin as a path.
Useful? React with 👍 / 👎.
| if !plugin_name.contains('/') && !plugin_name.contains("\\") { | ||
| LanguagePlugin::spawn_by_name(project_root, plugin_name) | ||
| } else { |
There was a problem hiding this comment.
load_plugin sends every slash-free plugin name to spawn_by_name, which only resolves .provekit/.../manifest.toml; it never falls back to executing the binary name directly. This breaks the documented/configured flow where plugin = "provekit-lsp-go" should work via PATH, causing plugin loading failures unless users create manifests for every language plugin.
Useful? React with 👍 / 👎.
| let diagnostics = build_diagnostics(&result, range); | ||
| client | ||
| .publish_diagnostics(uri_clone, diagnostics, None) | ||
| .await; |
There was a problem hiding this comment.
The verification loop publishes diagnostics once per annotation, and each notification contains only that annotation’s result. Under LSP semantics, clients treat publishDiagnostics as the current diagnostic set for the document, so later annotation results overwrite earlier ones and users only see a subset of errors/hints when multiple annotated functions exist in one file.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Pull request overview
This PR introduces a new Rust provekit-lsp workspace member that acts as a language-agnostic Provekit LSP server: it parses source annotations (built-in for Rust, plugin-based for other languages) and delegates verification to a JSON-RPC backend. It fits into the codebase as the IDE-facing layer for the protocol/spec work already present in the catalog.
Changes:
- Adds a new Rust LSP crate with config loading, Rust annotation parsing, plugin hosting, backend RPC transport, and the main tower-lsp server.
- Wires the new crate into the Rust workspace and updates the lockfile for its dependencies.
- Updates the per-language status matrix to add LSP plugin status and companion language status changes.
Reviewed changes
Copilot reviewed 8 out of 9 changed files in this pull request and generated 14 comments.
Show a summary per file
| File | Description |
|---|---|
implementations/rust/provekit-lsp/src/plugin.rs |
Adds plugin manifest lookup, process spawning, RPC handshake, and plugin annotation decoding. |
implementations/rust/provekit-lsp/src/parser.rs |
Adds the built-in Rust parser for #[provekit::*] annotations using syn. |
implementations/rust/provekit-lsp/src/main.rs |
Adds the tower-lsp server, document cache, hover/code action/code lens logic, and verification dispatch. |
implementations/rust/provekit-lsp/src/config.rs |
Adds .provekit/config.toml deserialization and language/backend config helpers. |
implementations/rust/provekit-lsp/src/backend.rs |
Adds JSON-RPC transport for the verification backend. |
implementations/rust/provekit-lsp/Cargo.toml |
Defines the new provekit-lsp crate and its dependencies. |
implementations/rust/Cargo.toml |
Registers provekit-lsp as a workspace member. |
implementations/rust/Cargo.lock |
Records dependency updates required by the new crate. |
docs/per-language-status.md |
Updates the public status matrix for LSP plugin coverage and companion language work. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| tokio::spawn(async move { | ||
| let mut backend = backend.lock().await; | ||
| match backend.verify(&function_name, &cid).await { | ||
| Ok(result) => { | ||
| let diagnostics = build_diagnostics(&result, range); | ||
| client | ||
| .publish_diagnostics(uri_clone, diagnostics, None) | ||
| .await; |
| tokio::spawn(async move { | ||
| let mut backend = backend.lock().await; | ||
| match backend.verify(&function_name, &cid).await { | ||
| Ok(result) => { | ||
| let diagnostics = build_diagnostics(&result, range); | ||
| client | ||
| .publish_diagnostics(uri_clone, diagnostics, None) | ||
| .await; |
| command: Some(Command { | ||
| title: "Re-verify".to_string(), | ||
| command: "provekit.reverify".to_string(), | ||
| arguments: Some(vec![ | ||
| serde_json::json!(ann.function_name), | ||
| serde_json::json!(cid), | ||
| ]), | ||
| }), |
| .map(|u| PathBuf::from(u.path())) | ||
| .or_else(|| { | ||
| params.workspace_folders.as_ref().and_then(|folders| { | ||
| folders.first().map(|f| PathBuf::from(f.uri.path())) |
| #[serde(default = "default_timeout")] | ||
| pub timeout_ms: u64, | ||
| #[serde(default = "default_cache_dir")] | ||
| pub cache_dir: String, |
|
|
||
| async fn update_document(&self, uri: Url, text: String, _lang_id: String) { | ||
| // Determine language from file extension | ||
| let path = PathBuf::from(uri.path()); |
| /// External plugin binary path or name (looked up in PATH) | ||
| pub plugin: Option<String>, |
| // Try manifest lookup first | ||
| if !plugin_name.contains('/') && !plugin_name.contains("\\") { | ||
| LanguagePlugin::spawn_by_name(project_root, plugin_name) | ||
| } else { | ||
| // Direct path or binary name |
| "params": { | ||
| "function": function, | ||
| "target_cid": target_cid, | ||
| } |
| let plugin = Self::spawn(manifest, project_root)?; | ||
| // Append extra args | ||
| // (spawn already appended --rpc; these are additional) | ||
| // We don't have a way to send args post-spawn, so we need to rebuild. | ||
| // Actually spawn_manifest handles this. Let me refactor. | ||
| // For now direct spawn uses the command as-is. | ||
| drop(plugin); | ||
| // Re-spawn with extra args | ||
| let mut full_cmd = command.to_vec(); | ||
| full_cmd.push("--rpc".to_string()); | ||
| full_cmd.extend_from_slice(args); | ||
| let manifest = PluginManifest { | ||
| name: command.first().cloned().unwrap_or_default(), | ||
| command: full_cmd, | ||
| working_dir: None, | ||
| }; | ||
| Self::spawn(manifest, project_root) |
Summary
protocol/specs/2026-04-30-lsp-protocol.md, in v1.3.0 catalog).provekit-lsp-plugin/1.What landed
implementations/rust/provekit-lsp/src/main.rsimplementations/rust/provekit-lsp/src/config.rs.provekit/config.tomlloaderimplementations/rust/provekit-lsp/src/parser.rssyn-based) for#[provekit::*]attrsimplementations/rust/provekit-lsp/src/plugin.rsinitialize/parse/shutdown)implementations/rust/provekit-lsp/src/backend.rsimplementations/rust/Cargo.tomlprovekit-lspto[workspace] members(single-line append)implementations/rust/Cargo.lockCompanion PRs
This PR is part of a four-way drop. The status matrix (
docs/per-language-status.md) gained an LSP Plugin column across every row plus a new Zig row plus a Java uplift. Splitting that diff cleanly across the four PRs is busywork, so the entire matrix change lands here. Companion PRs reference it:feat/java-kitfeat/zig-kitexamples/lsp-pluginsSanity
cargonot installed on the cutter machine; CI's Rust job will be the canonical compile gate. Lockfile is copied verbatim from the author's working tree (the impl built locally there).main.rsmatches the plugin-protocol description inexamples/lsp-plugins/README.md(PR D):initialize/parse/shutdown, annotation kindsimplement/contract/verify.Cargo.tomldiff is exactly one line, theprovekit-lspworkspace member entry. No version bumps, no dep changes elsewhere.Test plan
cargo build --release -p provekit-lspsucceeds.cargo test -p provekit-lsppasses.