veric-extension

VS Code Web extension that lets users open Veric workspaces inside their existing VS Code, Cursor, or VS Code Web (vscode.dev / github.dev) install. Dual-published to the Microsoft Marketplace (veric.veric-extension) and Open VSX (veric/veric-extension).

Design doc: docs/multi-surface-uplift/surface-3-extension.md.

Targeting

This extension is web-targeted — the manifest sets browser (not main), the esbuild config sets platform: "browser", and the source must not import any Node-only API (fs, child_process, path.resolve, etc.). A web-targeted extension is the only form that runs in all three of vscode.dev, desktop VS Code, and Cursor (see design doc §2).

Scope (0.3.0)

Phases 3.1 – 3.8 are now live:

• Commands veric.hello, veric.run, veric.showResult, veric.showTransportLog, veric.importFile, veric.exportFile, veric.lsp.showCFG, veric.lsp.explainStep, veric.properties.openEditor.
• Property editor sidebar (Phase C, 2026-05-20). New veric.properties activity-bar container hosting the veric.properties.editor webview view. Authored properties persist as *.veric.json sidecars next to the source file (src/foo.ts ↔ src/foo.veric.json). Each row gets a "Run" button that fires veric.run with { sourceUri, propertyId }; verdicts surface on the Result panel.
• VericFsProvider against the in-memory bridge shim (src/fs/bridge-shim.ts). A real remote-VFS swap-in is queued for Phase 4.8.
• vscode-languageclient/browser language client for .while files, configured via the veric.lspUrl setting.
• vscode.AuthenticationProvider (id veric) + OAuth URI handler.
• Result webview panel mounting <ResultCard/> from @veric/views-react over a WebView HostBridge transport.
• Direct kernel transport (0.3.0). veric.run resolves a kernel bridge from the cross-realm Symbol.for("veric.ide.kernel-bridge") first (so the embedded /ide route stays a thin client); when no bridge is published, the extension self-constructs one against the veric.kernelUrl endpoint (default wss://kernel.veric.dev/rpc). Bearer auth is plumbed via the Sec-WebSocket-Protocol subprotocol carrier.
• Desktop local-kernel spawn (P8 / Track C). In the desktop (Node) extension host — VS Code, Cursor; not vscode.dev / github.dev — the main entry (dist/extension.node.js) spawns the real veric-server-rpc kernel on loopback before activation, then points the self-constructed bridge at it. See the launch contract below. The web entry (dist/extension.js, browser) can't spawn a process and keeps using veric.kernelUrl (hosted default, or the opt-in "mock" echo mode), unchanged.

Desktop local-kernel launch contract (P7)

The desktop entry consumes the fixed veric-server-rpc spawn contract (owned by ~/dev/veric-server; not built in this repo). Exact invocation the extension uses:

• Binary discovery. veric.kernelBinaryPath (absolute path) if set; otherwise the bare name veric-server-rpc resolved from PATH. Build it with cargo build -p veric-server-rpc in ~/dev/veric-server.
• Spawn. veric-server-rpc --port <free-loopback-port> --host 127.0.0.1 --log-level info --provider mock. The port is an OS-allocated free loopback port (bind :0, read it back); --host 127.0.0.1 keeps the kernel loopback-only (never public); --provider mock needs no Claude credential or network for WHILE / Solidity analysis.
• Endpoints. JSON-RPC over WS + HTTP at /rpc; health at /health. The launcher GETs http://127.0.0.1:<port>/health until it answers 2xx (15s budget), then connects the KernelRpcTransport to ws://127.0.0.1:<port>/rpc (Node ws constructor injected).
• Shutdown. Graceful SIGTERM on extension deactivation, SIGKILL after a 2s grace window.
• Loud failure (integrity rule, mirrors Track A's embed). Missing binary, spawn error, premature exit, or health-probe timeout each raise a visible error notification ("local kernel failed to start — no verification is available") with a Show Log action, and install no bridge override — so the run path shows no verdict. The extension never fabricates a passing result to paper over a dead kernel. (Implementation: src/run/local-kernel-launcher.ts, src/extension.node.ts.)

Step-through debugger

The extension registers a VS Code debug adapter (veric debug type) backed by an in-process inline adapter — there is no separate veric-dap-server process. The session (VericDebugSession) drives the kernel's solver trace over the same RPC transport the run path uses, so stepping is a replay of an already-computed trace, not a live execution. That replay model is the reason several DAP capabilities are degraded or unsupported, and the limits are surfaced here so the UI behaviour isn't surprising:

• stepOut degrades to a single forward step. The solver trace is flat — there is no call stack to step out of — so a "step out" request advances one trace step forward, the same as stepOver / stepInto. (veric-debug-session.ts stepOutRequest.)
• stepBack is supported. Because the whole trace is materialised up front, stepping backwards is just moving the cursor — the adapter advertises supportsStepBack: true and reverse-continue works.
• Restart / Terminate / EvaluateForHovers are supported. supportsRestartRequest, supportsTerminateRequest, and supportsEvaluateForHovers are all advertised true.
• setVariable, conditional breakpoints, and function breakpoints are not supported. The trace is a read-only replay: abstract values aren't assignable (supportsSetVariable: false), and the adapter has no evaluator to gate a breakpoint on a condition or bind one to a function symbol (supportsConditionalBreakpoints: false, supportsFunctionBreakpoints: false). Plain line breakpoints work.

Settings

Every contributed veric.* setting is listed here in one place; this table is the human-readable mirror of apps/extension/package.json contributes.configuration. A CI gate (pnpm settings-doc-check → scripts/check-settings-doc.mjs) fails any PR that adds a setting to the manifest without documenting it here, and vice-versa.

Scripts

Two test layers

The extension has two complementary test layers:

1. vitest unit tests under tests/ mock the vscode module via tests/setup.ts. They run on plain Node, cover every provider / command handler in detail, and are the workhorse for TDD iteration.
2. Mocha real-host smoke under test/host/ runs inside a real VS Code spawned by @vscode/test-electron or @vscode/test-web. It asserts that the manifest + the bundled dist/extension.js actually register the contributed commands / FS provider / auth provider against the genuine host. The CI publish workflow gates on pnpm test (the unit layer); the host suite is run locally and in nightly CI to catch manifest / bundler regressions that the mock layer can't see.

Release process (Phase 3.6)

Dual-publish is automated by .github/workflows/extension-publish.yml. The workflow fires on tags matching extension-v* (e.g. extension-v0.2.1) and on manual workflow_dispatch runs (dispatch defaults to dry_run=true — it builds + packages but skips the actual Marketplace / Open VSX uploads).

To cut a release:

1. Bump version in apps/extension/package.json to the new semver.
2. Open a PR with just the bump, get it merged to main.
3. From a clean checkout of main:

   git pull
   VERSION=$(node -p "require('./apps/extension/package.json').version")
   git tag "extension-v${VERSION}"
   git push origin "extension-v${VERSION}"
   

4. Watch the workflow under Actions → extension-publish. On green, the new version is live on the Microsoft Marketplace (veric.veric-extension) and Open VSX (veric/veric-extension) within a few minutes.

Required repo secrets (one-time setup)

Before the first release, configure the following GitHub repo secrets in Settings → Secrets and variables → Actions:

The workflow has no fallback — if either secret is unset when a tag lands, the corresponding publish step fails loudly. That's intentional: missing secrets must not silently skip publishing.