vscode: redesign the proof job panel

editors/vscode/package.json

@@ -29,7 +29,8 @@
     "workspaceContains:**/*.inf",
     "onLanguage:inference",
     "onView:inference.configView",
-    "onView:inference.proofJobsView"
+    "onView:inference.proofJobsView",
+    "onWebviewPanel:inference.proofJob"
   ],
   "contributes": {
     "viewsContainers": {

editors/vscode/src/prover/buildLog.ts

@@ -0,0 +1,98 @@
+/**
+ * The first error in a server build log (`build.log`, Rocq output). Pure — no
+ * `vscode` import.
+ *
+ * Rocq reports `File "<path>", line N, characters A-B:` followed by the
+ * message. The server compiles the uploaded file in place (only the proof
+ * terminators change), so line N is line N of the submitted `.v`.
+ */
+
+export interface BuildError {
+    /** 1-based line in the compiled file, when the log names one. */
+    line?: number;
+    /** 0-based character range on that line. */
+    startChar?: number;
+    endChar?: number;
+    /** The message without its `Error:` prefix, at most 600 characters. */
+    message: string;
+}
+
+const LOCATION = /^File "[^"]*", line (\d+), characters (\d+)-(\d+):\s*$/;
+
+function clean(lines: string[]): string {
+    const text = lines
+        .join('\n')
+        .replace(/^\s*Error:\s*/, '')
+        .trim();
+    return text.length > 600 ? `${text.slice(0, 600)}…` : text;
+}
+
+/**
+ * First located error, else the first `Error:` block, else null. Warnings use
+ * the same location header, so a located block counts only when its message
+ * is an error.
+ */
+export function firstBuildError(log: string): BuildError | null {
+    const lines = log.replace(/\r\n?/g, '\n').split('\n');
+    for (let i = 0; i < lines.length; i++) {
+        const m = LOCATION.exec(lines[i]);
+        if (!m) {
+            continue;
+        }
+        const body: string[] = [];
+        for (let j = i + 1; j < lines.length; j++) {
+            if (LOCATION.test(lines[j]) || (lines[j].trim() === '' && body.length > 0)) {
+                break;
+            }
+            body.push(lines[j]);
+        }
+        if (!/^\s*Error:/.test(body.find((l) => l.trim() !== '') ?? '')) {
+            continue;
+        }
+        const message = clean(body);
+        if (message) {
+            return {
+                line: Number(m[1]),
+                startChar: Number(m[2]),
+                endChar: Number(m[3]),
+                message,
+            };
+        }
+    }
+    const errorAt = lines.findIndex((l) => /^\s*Error:/.test(l));
+    if (errorAt >= 0) {
+        const body: string[] = [];
+        for (let j = errorAt; j < lines.length && (j === errorAt || lines[j].trim() !== ''); j++) {
+            body.push(lines[j]);
+        }
+        const message = clean(body);
+        return message ? { message } : null;
+    }
+    return null;
+}
+
+/**
+ * A hint for `<name> already exists`: the compiler names the module after the
+ * file, so a function with the file's name defines it twice.
+ */
+export function duplicateNameHint(message: string, fileStems: readonly string[]): string | null {
+    const m = /^(\S+) already exists\.?$/.exec(message.split('\n')[0].trim());
+    if (!m) {
+        return null;
+    }
+    const name = m[1];
+    if (fileStems.includes(name)) {
+        return `The compiler names the module after the file, so a function also named “${name}” defines “${name}” twice. Rename the file or the function, then prove again.`;
+    }
+    return `“${name}” is defined twice in the generated file.`;
+}
+
+/** File name without directory and final extension. */
+export function fileStem(name: string | null | undefined): string | null {
+    if (!name) {
+        return null;
+    }
+    const base = name.split(/[\\/]/).pop() ?? name;
+    const dot = base.lastIndexOf('.');
+    return dot > 0 ? base.slice(0, dot) : base;
+}

editors/vscode/src/prover/eventFormat.ts

@@ -17,7 +17,7 @@ const MAX_PAYLOAD_CHARS = 160;
 const MAX_ACTIVITY_CHARS = 240;
 
 /** Server-originated agent limits (`agent.limited.code`), as the portal words them. */
-const AGENT_LIMIT_MESSAGES: Readonly<Record<string, string>> = {
+export const AGENT_LIMIT_MESSAGES: Readonly<Record<string, string>> = {
     AGENT_REQUEST_LIMIT:
         'Agent request limit reached. No further model requests are allowed for this job.',
     AGENT_PROVIDER_RATE_LIMITED:
@@ -69,7 +69,7 @@ function clip(text: string, max: number): string {
  * One `agent.activity` payload as a readable line. The kinds mirror the
  * portal's transcript (`portal/src/lib/store.ts::applyActivity`).
  */
-function summarizeActivity(p: Record<string, unknown>): string {
+export function summarizeActivity(p: Record<string, unknown>): string {
     const kind = str(p.kind) ?? '';
     const detail = str(p.detail) ?? '';
     if (kind === 'truncated') {
@@ -110,7 +110,7 @@ function activityScope(p: Record<string, unknown>): string {
 }
 
 /** Per-type human summary of an event payload ('' = type alone suffices). */
-function summarize(env: EventEnvelope): string {
+export function summarize(env: EventEnvelope): string {
     const p = asRecord(env.payload);
     const name = str(p.name);
     const attempt = num(p.attempt);

editors/vscode/src/prover/index.ts

@@ -1,14 +1,15 @@
 import * as vscode from 'vscode';
 
-import { hasApiKey, SERVER_URL_SETTING, updateConfiguredContext } from './config';
+import { hasApiKey, resolveConfig, SERVER_URL_SETTING, updateConfiguredContext } from './config';
 import {
     cancelJobInteractive,
     compareProof,
     deleteJobInteractive,
     openInPortal,
     resubmitJob,
 } from './jobActions';
-import { JobDetailViewManager } from './jobDetailView';
+import { JOB_PANEL_VIEW_TYPE, JobDetailViewManager } from './jobDetailView';
+import { JobOrigins, type JobOrigin } from './jobOrigins';
 import { FILTER_STATUSES } from './jobList';
 import { JobTreeItem, ProofJobsProvider } from './jobsTree';
 import { ProofDocuments } from './proofDocuments';
@@ -40,21 +41,53 @@ export function registerProver(
     const jobs = new ProofJobsProvider(secrets, log);
     const view = vscode.window.createTreeView('inference.proofJobsView', { treeDataProvider: jobs });
     const documents = new ProofDocuments(secrets);
-    const panels = new JobDetailViewManager(secrets, log, documents, () => void jobs.refresh());
-    disposables.push(jobs, view, documents, panels);
+    const origins = new JobOrigins(context.workspaceState);
+    /** The local files a job was uploaded from, when this workspace knows them. */
+    const originOf = async (jobId: string): Promise<JobOrigin | undefined> => {
+        const config = await resolveConfig(secrets).catch(() => null);
+        return config ? origins.get(config.serverUrl, jobId) : undefined;
+    };
+    const runAgain = async (job: JobResponse) => {
+        const fresh = await resubmitJob(secrets, log, job);
+        if (fresh) {
+            await showJob(fresh, await originOf(job.id));
+        }
+    };
+    const panels = new JobDetailViewManager(
+        context.extensionUri,
+        secrets,
+        log,
+        documents,
+        origins,
+        () => void jobs.refresh(),
+        runAgain,
+    );
+    disposables.push(
+        jobs,
+        view,
+        documents,
+        panels,
+        vscode.window.registerWebviewPanelSerializer(JOB_PANEL_VIEW_TYPE, panels),
+    );
 
     disposables.push(view.onDidChangeVisibility((e) => jobs.setVisible(e.visible)));
     if (view.visible) {
         jobs.setVisible(true);
     }
 
-    const showJob: SubmitHooks['showJob'] = async (job, source) => {
+    const showJob: SubmitHooks['showJob'] = async (job, origin) => {
+        if (origin) {
+            const config = await resolveConfig(secrets).catch(() => null);
+            if (config) {
+                await origins.set(config.serverUrl, job.id, origin);
+            }
+        }
         await jobs.refresh();
         const node = jobs.findNode(job.id);
         if (node && view.visible) {
             await view.reveal(node, { select: true, focus: false });
         }
-        await panels.open(job, source);
+        await panels.open(job, origin);
     };
     const jobOf = (arg: unknown): JobResponse | undefined =>
         arg instanceof JobTreeItem ? arg.job : undefined;
@@ -96,9 +129,8 @@ export function registerProver(
     });
     command('inference.resubmitProofJob', async (arg) => {
         const job = jobOf(arg);
-        const fresh = job && (await resubmitJob(secrets, log, job));
-        if (fresh) {
-            await showJob(fresh);
+        if (job) {
+            await runAgain(job);
         }
     });
     command('inference.copyProofJobId', async (arg) => {

editors/vscode/src/prover/jobActions.ts

@@ -160,10 +160,11 @@ export async function compareProof(
 export async function openInPortal(
     secrets: vscode.SecretStorage,
     job: JobRef,
-    tab: 'certificate' | undefined = 'certificate',
+    page: 'certificate' | 'job' = 'certificate',
 ): Promise<void> {
     const config = await requireConfig(secrets);
     if (config) {
+        const tab = page === 'certificate' ? 'certificate' : undefined;
         await vscode.env.openExternal(vscode.Uri.parse(portalJobUrl(config.serverUrl, job.id, tab)));
     }
 }