vscode: calmer prove flow, compile errors in Problems, replay notices

[0xGeorgii]

Stacked on the Proof Jobs view and status bar PR; this is PR 3 of 3. Review this diff alone.

Why

From the #519 test:

• A first prove could show up to three modal dialogs, one of them on top of a progress notification, and the unchecked-compiler question came back on every prove.
• Compile errors went only to the Output channel.
• clamp.inf with fn clamp was uploaded and failed on the server.
• Re-proving an unchanged file silently opened a two-day-old portal job.
• The toolchain-switch toast read "switching to to".

Change

• Fewer interruptions.
  • Prove This File and Submit save the file instead of asking.
  • The progress notification closes before a question and reopens afterwards.
  • The upload notice comes after a successful compile and the local checks, so a doomed upload never asks.
  • "This proof server doesn't say which compiler it accepts" is asked once per server.
• Problems panel. Compile errors from infs build are added to Problems with the source infc (proof build). This covers parse errors, multi-error Type checking failed: …; … lines, analysis codes and submodule files; the formats were checked against the accepted compiler d71a9c3e. A toast summarises the errors and offers Show Problems, and the entries clear when you edit the file.
• Duplicate names. A generated file that defines a name twice is blocked locally. The message explains that the module is named after the file and points at the function to rename.
• Replays. When the server answers with an existing job, a notice says so: "already being proved", or "already proved 2d ago — " with Run Again. It uses the Idempotent-Replayed header from Inferara/inference-ai-prover#270 when present; otherwise it falls back to the job's status and age, which works on the deployed server today.
• Compiler mismatch. The dialog offers Install X and Prove, which proves again after the switch; a non-release compiler gets Copy Commit instead. performVersionChange now reports whether it succeeded and says "Inference toolchain vX is now the default.", which also fixes the message for Select Version and Update.
• Wording. Consistent terms throughout: proof server, API key, Run Again, Cancel Job.
  • Clear API Key now asks for confirmation.
  • "Save Anyway" for an unverified key is now a modal.
  • The Cancel dialog explains the wait of up to about 90 seconds while a worker starts.
• Docs. The README covers the Proving flow, commands, sidebar, status bar and privacy timing. QA_GUIDE §3, §3a and §14 have new cases for replay, diagnostics, duplicate names, reload restore, themes and finish notices.

Verification

In node:24: typecheck; npm test (502 pass); grammar tests (93 pass); npm run package, with the same 11 .vsix entries.

New tests:

• the diagnostics parser, using real compiler output;
• duplicateDefinitions and the preflight block;
• classifyReplay;
• the Idempotent-Replayed header, read from a local HTTP server;
• prove-flow ordering: the upload is asked only after the build and never for a doomed file.

Risk

Saving before Prove changes existing behaviour; it is documented and matches how a debug run saves. Problems entries can duplicate the language server's, and they clear when the file is edited.

🤖 Generated with Claude Code

Confidence Score: 5/5

The PR appears safe to merge; no new blocking issue was found.

_{Reviews (12) · Last reviewed commit: "vscode: place compile errors on the righ..." · Reviewed by Greptile}

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!