vscode: prove a file and manage proof jobs from the editor

[0xGeorgii]

Why

The journey from Inference source to a reviewed proof result should work from VS Code: compile locally, submit, then watch, review and manage proof jobs. Until now that took a terminal, the web portal, and a separate unpublished extension in the proof server's repository.

What users get

• Inference: Prove This File (editor title and Explorer menus on .inf, or the command palette):
  1. Finds the infc that infs build will spawn (from the doctor's Resolved infc).
  2. Compares its --commit-hash and --abi-version with the compiler the proof server accepts (GET /api/v1/meta → acceptedToolchain). A mismatch is refused before anything is uploaded, with an offer to install the accepted release when there is one.
  3. Runs infs build <file>.inf -v in the file's folder, with INFC_PATH pinned to the checked binary. The output is out/<file>.v.
  4. Checks the .v for proof holes and the upload limit, then submits it under the portal's content-derived idempotency key.
  5. Opens the job panel and selects the job in the jobs view.
• Inference: Submit Rocq File for Proof: submits an existing .v.
• Proof Jobs view in the Inference sidebar: newest first, status filter, "Load more…", and per-job Cancel, Run Again, Delete, Copy ID, Compare and Open Certificate.
• Job panel, following the run live over SSE (with a polling fallback):
  • phase ribbon, obligations (including refuted), time budget and deadline;
  • the prover's activity as readable lines scoped to theorem and attempt (previously truncated JSON);
  • the independent verifier's verdict and kernel-reported assumptions, with the existing fail-closed claim banners;
  • artifacts that open read-only after a SHA-256 check, a diff of the completed proof against its input, and Open certificate in portal. The portal keeps the single implementation of the certificate's claim rules.
• Setup: an API key per server, stored in secret storage and checked against /api/v1/me when set. A Proof Server group appears in the Configuration view. The new setting inference.prover.serverUrl must be HTTPS; plain HTTP is accepted only for localhost. Before the first upload to a server, the extension shows a notice once.

Where the code comes from

• The API client, SSE client, detail renderer and their 85 tests move here from Inferara/inference-ai-prover/editors/vscode. That extension was never published and will be retired once this ships.
• New calls: meta, me, paging/filtering, delete, artifact listing, and a 64 MiB artifact cap.
• The prove flow (src/prover/proveFlow.ts) injects every effect, so each gate is unit-tested.
• The server side is Inferara/inference-ai-prover#267, which adds acceptedToolchain to /meta. Against an older server, Prove asks before compiling unchecked.

Release

• New .github/workflows/vscode_extension_publish.yml publishes from a vscode-v<version> tag. It builds through vscode_extension.yml, which is now also workflow_call and uploads the checked .vsix, so the published bytes are the bytes those checks passed.
• It publishes to the Marketplace (VSCE_PAT) and Open VSX (OVSX_PAT) from the marketplace environment, then attaches the .vsix to a GitHub release.
• Maintainer setup before the first release:
  • create the marketplace environment with required reviewers;
  • add VSCE_PAT (Marketplace > Manage for the inference-lang publisher);
  • claim the inference-lang namespace on Open VSX and add OVSX_PAT;
  • bump version in package.json.
• The packaged file list is unchanged: the same 11 files, with a production bundle.

Risk and limits

• Nothing changes for users who never set a key: no proof-server traffic, and the toolchain features are untouched.
• Until the proof server accepts a released compiler, "Prove This File" correctly refuses a release infc. The server currently pins d71a9c3e (ABI 1.3), and adopting v0.0.6 is planned after the TAITRONICS booth. Submitting a .v works today.
• License: the moved client code was Inferara-owned and is now GPL-3.0 with the rest of the extension.

Verification

All of these ran in a node:24 container.

• npx tsc --noEmit -p .: clean.
• npm test: 433 passed: 298 existing, 79 moved (the moved suite's 6 manifest tests are replaced by new ones for this package), and 56 new. The new tests cover:
  • the identity check;
  • preflight, and an idempotency key matching an independently computed reference;
  • server-URL rules;
  • list paging and merging;
  • spawn timeout and abort;
  • the API endpoints;
  • agent-activity formatting;
  • detail actions and the phase ribbon;
  • every prove-flow gate, plus an end-to-end run with fake infs/infc scripts and a local HTTP server;
  • manifest wiring, which checks each job action's when clause against the context value for all 15 statuses. That test caught a /\.proof/ regex matching every job.
• npm run "test syntax": 93 passed.
• npm run package: the 11 expected files and no source map.
• rhysd/actionlint: clean on both workflows.
• Real toolchain: in a Linux arm64 container with the accepted infs/infc (d71a9c3e) against a stub server, the flow resolved infc through infs doctor, matched it, built fixtures/aerospace/telemetry_limit.inf and uploaded a .v whose SHA-256 is 7796bcb9…. That is exactly the canonical output recorded in the prover's contracts/infc.lock.json. The same binary was refused against a v0.0.6/ABI 1.8 server.
• Not yet done: a manual pass in the Extension Development Host against the hosted server (QA_GUIDE §14). It needs a service key.

🤖 Generated with Claude Code

Confidence Score: 5/5

The change since the last review appears safe to merge.

Diagram

%%{init: {'theme': 'neutral'}}%%
flowchart LR
    Source["Inference file"] --> Check["Check compiler identity"]
    Check --> Build["Compile locally"]
    Build --> Upload["Check and upload Rocq file"]
    Rocq["Existing Rocq file"] --> Upload
    Upload --> Job["Proof job"]
    Job --> Watch["Follow events and status"]
    Watch --> Review["Review verdict and artifacts"]
    Review --> Again["Run again with original filename"]
    Again --> Job

Loading

_{Reviews (5) · Last reviewed commit: "vscode: keep the job's filename when run..." · Reviewed by Greptile}

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!