菜单
VSCode extension architecture and LSP server details
用 Codex 或 Claude 帮你安装 复制这段 Prompt，粘贴到 Codex、Claude 或其他助手里，让它检查 Skill 页面并帮你完成安装。
基于 SOC 职业分类
Catalogue of every covalence-* crate — what each one wraps/provides and which layer it lives in. Consult when deciding which crate to use, where new code belongs, or how the workspace is structured.
Performance of the Metamath → HOL import (covalence-metamath + covalence-hol metalogic) — pipeline, hotspots, the bench, and the history of super-linearity fixes
How to profile and optimize covalence — flamegraphs, callgrind/cachegrind, and the scaling-first methodology for finding super-linear work
Covalence repo layout, dependency graph, and key architectural rules
Performance of the Metamath → HOL import (covalence-metamath + covalence-hol metalogic) — pipeline, hotspots, the bench, and the history of super-linearity fixes
How to profile and optimize covalence — flamegraphs, callgrind/cachegrind, and the scaling-first methodology for finding super-linear work
| name | vscode-extension |
| description | VSCode extension architecture and LSP server details |
| disable-model-invocation | true |
cov lsp)Supports two file categories:
.smt, .smt2, .alethe, .cov) — diagnostics for unclosed/unmatched parens via covalence-sexp, formatting via covalence_sexp::prettyprint().wat) — diagnostics via covalence_wasm::compile_wat() (reports compile errors with line/col)Also provides textDocument/formatting for sexp files. WAT formatting is not yet implemented.
The extension supports two LSP transport modes, selected automatically by src/server.ts:
Native mode (Linux desktop, when cov is available):
VSCode ← LanguageClient ← stdio ← cov lsp (native binary)
WASM mode (browser, or native not available):
VSCode ← LanguageClient ← @vscode/wasm-wasi-lsp ← WASI Process (cov.wasm) ← lsp-server
Detection order: covalence.server.path setting → cov on PATH (Linux only) → WASM fallback.
The same src/extension.ts serves both desktop and web bundles. esbuild aliases vscode-languageclient/node → vscode-languageclient/browser for the web build.
Supported languages: SMT (.smt, .smt2), Alethe (.alethe), Cov (.cov), WAT (.wat).
The target triple is set at build time via crates/app/cov/build.rs (COV_TARGET env var) and passed into covalence_lsp::run_lsp() via LspConfig. The LSP server reports it in serverInfo.version during the initialize handshake.