PVSCode: A VSCode Extension for PVS

PVSCode is a VS Code extension for working with PVS specifications. It combines editor-level language support with a JSON-RPC connection to a running PVS server, plus managed runtime installation, proof/TCC navigation, proof inspection, PVSio evaluation, and developer-facing diagnostics.

The extension is intentionally lightweight on the editor side: .pvs files get syntax highlighting, outline symbols, CodeLens actions, file badges, and contextual panes. PVS itself remains the source of truth for parsing, typechecking, TCCs, proofs, prover state, and PVSio execution.

Current Capabilities

• Syntax highlighting for .pvs files through syntaxes/pvs.tmLanguage.json.
• Heuristic top-level declaration discovery for CodeLens and Outline support.
• Compound declaration heads such as a, b, c: VAR nat are displayed as one outline item.
• CodeLens actions above PVS declarations and formulas:
  • formula-like declarations expose proof actions
  • other declarations expose TCC actions
  • JUDGEMENT and JUDGMENT are treated as formula declarations
• Parse and typecheck commands for the active PVS file.
• File badges and status-bar feedback for typecheck/error state.
• PVS Home webview with recent contexts, documentation links, and local release notes from the managed PVS install.
• Managed PVS runtime install, reinstall, master/dev release switching, update checks, and server startup.
• Open the managed runtime Prelude file from the command palette or default keybinding.
• Debug Console backed PVS server REPL for the managed pvs -raw process, started automatically with managed PVS.
• TCC pane with obligation body, saved proofs, status markers, and source-origin reveal from TCC comment line/column metadata.
• Existing proof pane with saved proof selection, default proof marking, deletion, rendered proof scripts, raw proof scripts, and a proof-tree diagram view.
• Interactive prover pane with transcript, command entry, saved proof listing, and safe close/save behavior.
• PVSio console panel for starting a session from the active theory and evaluating expressions.
• Getting Started walkthrough and PVS Gateway quick-pick command menu.

Development Setup

npm install
npm run compile

Open this folder in VS Code and run the extension with Run > Start Debugging.

Useful scripts:

npm run compile
npm run watch
npm run package

dist/ is the compiled extension entrypoint and is committed in this repository. Make changes in src/, then run npm run compile before testing or packaging.

Using The Extension

1. Open a .pvs file or a workspace containing PVS files.
2. Run PVS: Check Installation or PVS: Install PVS.
3. Use PVS Home to add/open recent contexts and inspect local release notes.
4. Run PVS Gateway: Parse Active PVS File or PVS Gateway: Typecheck Active PVS File.
5. Use CodeLens actions above declarations to inspect TCCs, proofs, or enter the prover.
6. Use PVS Gateway when you want one command menu for the most common workflows.

Commands

Core navigation and panes:

Editing and server actions:

Proofs, TCCs, and prover:

Runtime and tools:

Getting started:

Settings

Major Architecture

src/extension.ts

The composition root. It creates the output channel, JSON-RPC client, runtime manager, CodeLens provider, document symbol provider, PVS Home panel, PVSio panel, REPL debug adapter, status bar item, file decoration provider, and command registrations.

src/pvsParser.ts

A heuristic parser for editor features. It finds top-level theories and declarations, tracks nesting depth, strips PVS % line comments, classifies formula-like declarations, and keeps enough range information for CodeLens and Outline. It is not a replacement for the PVS parser.

src/pvsDocumentSymbolProvider.ts

Builds the Outline tree. It groups declarations under theories, uses typecheck metadata from the RPC client when available, and displays compound declaration heads with displayName.

src/pvsCodeLensProvider.ts

Owns declaration CodeLens, proof/TCC state caches, TCC panes, proof panes, interactive prover panes, saved proof actions, TCC origin reveal/highlight, proof script rendering, and proof-tree diagram rendering. This is the largest UI workflow module.

src/pvsRpcClient.ts

JSON-RPC 2.0 over WebSocket. It manages connection state, pending requests, server notifications, retry-compatible parameter shapes, normalization of varied server responses, typecheck metadata caches, TCC/proof/prover/PVSio calls, and raw RPC tracing.

src/pvsRuntimeManager.ts

Managed PVS runtime lifecycle. It resolves GitHub releases, downloads release assets, checks existing installations, prompts before reinstalling, manages the configured source/install directory, starts/stops pvs -raw -port <port>, mirrors server output to the REPL debug adapter, and handles update/release-channel workflows.

src/pvsStartupPanel.ts

PVS Home webview. It records recent contexts in VS Code global state, renders logos and Home sections, opens links in VS Code Simple Browser, renders release notes from the managed PVS install, and provides Home actions for context management and installation checks.

src/pvsIoConsolePanel.ts

PVSio webview console. It changes context, typechecks the active theory, starts a PVSio session, sends evaluations, and renders a transcript of commands/results/errors.

src/pvsReplDebugSession.ts

Inline debug adapter for the managed PVS REPL. It lets the VS Code Debug Console act as stdin/stdout/stderr for the managed pvs subprocess.

src/webviewTheme.ts

Shared CSS tokens and base styles for extension webviews.

src/pvsTypes.ts

Shared type definitions for declarations, proofs, TCCs, prover snapshots, and CodeLens state.

Other important folders:

• syntaxes/ contains the TextMate grammar.
• media/walkthrough/ contains Getting Started artwork.
• media/vendor/ contains vendored browser libraries used by webviews, such as the proof-tree layout helper.
• dist/ contains compiled JavaScript and source maps.

JSON-RPC Server Contract

The extension connects to pvscode.serverUrl and sends JSON-RPC 2.0 requests over WebSocket. Some requests intentionally try multiple parameter shapes to tolerate small server-side contract differences.

Core file/context methods:

TCC/proof/prover methods:

PVSio methods:

Server notifications with a method and message-like payload are logged, shown in the status bar, and used opportunistically to update typecheck state.

Proof Script Rendering

Saved proof scripts are consumed in the JSON shape returned by JSON-RPC when that is the script payload:

[
  "label",
  ["cmd1"],
  ["cmd2"],
  ...
  [
    ["branch label", ["cmd1"], ...],
    ["sibling branch", ["cmd1"], ...]
  ]
]

The proof pane exposes:

• Blocks: readable nested proof commands.
• Tree: explorable branch diagram with pan, zoom, expand, fit, selected-branch Goal details, and command listing.
• Script: the original text when provided, or the JSON proof script serialized as JSON.

When the server provides canonical proof text (proof-script, or rawText/proofText on saved proofs), Blocks and Tree render from that text so command names stay exactly as printed by PVS.

Command heads are clickable when they look like prover commands; the pane asks the server for proof-help.

Home Page Data Hooks

PVS Home currently gathers:

• recent contexts from VS Code global state
• documentation links from DOC_LINKS in src/pvsStartupPanel.ts
• release notes from doc/release-notes/*.texi in the active/configured managed PVS runtime

The preferred release-notes path is version-specific, such as doc/release-notes/pvs8.1-release-notes.texi; if that file is not present, the Home pane uses the newest .texi file in doc/release-notes.

Managed Runtime Notes

The runtime manager installs into pvscode.pvsSourceDirectory or ~/PVS by default. It stores release metadata in VS Code global state under pvscode.managedRuntimeMetadata, checks whether the configured channel is already installed, asks before reinstalling, and starts the installed runtime when reinstall is declined.

Before potentially disruptive runtime actions, it checks for dirty documents and active prover/PVSio sessions.

Parser Limitations

The editor parser is deliberately heuristic. It is designed to provide responsive editor affordances before or alongside server data. It does not implement full PVS grammar or typechecking. When exact information matters, prefer the JSON-RPC server results.

Debugging And Troubleshooting

• Run PVS: Show Output to reveal logs and enable verbose RPC logging for the session.
• Set pvscode.traceRpc for persistent raw JSON-RPC logging.
• Run PVS: Check Server Status to test the current pvscode.serverUrl.
• Run PVS: Reconnect Server after changing runtime/server state.
• If CodeLens or Outline looks stale after major edits, save/typecheck the file or reload the window.
• If managed startup is affected by local init files, keep pvscode.loadUserInitForManagedServer disabled.

Packaging

npm run compile
npm run package

The package script uses vsce package. Ensure dist/ is up to date before packaging.