vscode: clearer Proof Jobs view, proving status bar item, finish notices

editors/vscode/package.json

@@ -167,6 +167,11 @@
         "title": "Inference: Filter Proof Jobs by Status",
         "icon": "$(filter)"
       },
+      {
+        "command": "inference.clearProofJobsFilter",
+        "title": "Inference: Show All Proof Jobs",
+        "icon": "$(clear-filter)"
+      },
       {
         "command": "inference.openProofJob",
         "title": "Open Proof Job"
@@ -197,7 +202,7 @@
       },
       {
         "command": "inference.openProofJobInPortal",
-        "title": "Open Certificate in Portal",
+        "title": "Open in Portal",
         "icon": "$(link-external)"
       }
     ],
@@ -209,8 +214,18 @@
           "group": "navigation"
         },
         {
-          "command": "inference.filterProofJobs",
+          "command": "inference.proveFile",
           "when": "view == inference.proofJobsView",
+          "group": "navigation@0"
+        },
+        {
+          "command": "inference.filterProofJobs",
+          "when": "view == inference.proofJobsView && !inference.prover.filtered",
+          "group": "navigation@1"
+        },
+        {
+          "command": "inference.clearProofJobsFilter",
+          "when": "view == inference.proofJobsView && inference.prover.filtered",
           "group": "navigation@1"
         },
         {
@@ -221,7 +236,22 @@
         {
           "command": "inference.submitProof",
           "when": "view == inference.proofJobsView",
-          "group": "1_submit"
+          "group": "1_submit@1"
+        },
+        {
+          "command": "inference.filterProofJobs",
+          "when": "view == inference.proofJobsView && inference.prover.filtered",
+          "group": "1_submit@2"
+        },
+        {
+          "command": "inference.setProverApiKey",
+          "when": "view == inference.proofJobsView",
+          "group": "2_key@1"
+        },
+        {
+          "command": "inference.clearProverApiKey",
+          "when": "view == inference.proofJobsView && inference.prover.configured",
+          "group": "2_key@2"
         }
       ],
       "view/item/context": [
@@ -246,7 +276,7 @@
         },
         {
           "command": "inference.openProofJobInPortal",
-          "when": "view == inference.proofJobsView && viewItem =~ /\\.terminal/",
+          "when": "view == inference.proofJobsView && viewItem =~ /^inference\\.proofJob\\./",
           "group": "1_review@2"
         },
         {
@@ -266,7 +296,7 @@
         },
         {
           "command": "inference.deleteProofJob",
-          "when": "view == inference.proofJobsView && viewItem =~ /\\.terminal/",
+          "when": "view == inference.proofJobsView && viewItem =~ /\\.(terminal|lost)/",
           "group": "2_manage@3"
         }
       ],
@@ -334,6 +364,10 @@
         {
           "command": "inference.openProofJobInPortal",
           "when": "false"
+        },
+        {
+          "command": "inference.clearProofJobsFilter",
+          "when": "inference.prover.filtered"
         }
       ]
     },

editors/vscode/src/extension.ts

@@ -10,6 +10,7 @@ import { registerDoctorCommand } from './commands/doctor';
 import { registerSelectVersionCommand } from './commands/selectVersion';
 import { registerUpdateCommand, checkForUpdates } from './commands/update';
 import { createStatusBar, updateStatusBar } from './ui/statusBar';
+import { failingChecks, toolchainHealth, toolchainHealthLabel } from './ui/statusBarState';
 import { InferenceConfigProvider, ConfigItem } from './ui/configTree';
 import { runDoctor } from './toolchain/doctor';
 import { registerProver } from './prover';
@@ -271,14 +272,13 @@ async function checkToolchain(
     updateStatusBar(statusBarItem, doctorResult);
     configProvider.refresh(detection, doctorResult);
 
-    const status = doctorResult?.hasErrors
-        ? 'errors'
-        : doctorResult?.hasWarnings
-            ? 'warnings'
-            : 'healthy';
-    if (doctorResult?.hasErrors) {
+    const health = toolchainHealth(doctorResult);
+    const status = toolchainHealthLabel(health);
+    if (health === 'errors') {
         outputChannel.error(`Toolchain status: ${status}`);
-    } else if (doctorResult?.hasWarnings) {
+    } else if (health === 'degraded') {
+        outputChannel.warn(`Toolchain status: ${status} (${failingChecks(doctorResult).join('; ')})`);
+    } else if (health === 'warnings') {
         outputChannel.warn(`Toolchain status: ${status}`);
     } else {
         outputChannel.info(`Toolchain status: ${status}`);

editors/vscode/src/prover/index.ts

@@ -10,8 +10,9 @@ import {
 } from './jobActions';
 import { JOB_PANEL_VIEW_TYPE, JobDetailViewManager } from './jobDetailView';
 import { JobOrigins, type JobOrigin } from './jobOrigins';
-import { FILTER_STATUSES } from './jobList';
+import { FILTER_LABELS, FILTER_STATUSES, hasCertificate, isActiveJob } from './jobList';
 import { JobTreeItem, ProofJobsProvider } from './jobsTree';
+import { ProverStatus } from './proverStatusBar';
 import { ProofDocuments } from './proofDocuments';
 import { registerProverAuthCommands } from './proofAuth';
 import { registerProveFileCommand, type CompilerCheck } from './proveFile';
@@ -38,10 +39,10 @@ export function registerProver(
     const disposables: vscode.Disposable[] = [];
     let compilerCheck: CompilerCheck | undefined;
 
-    const jobs = new ProofJobsProvider(secrets, log);
-    const view = vscode.window.createTreeView('inference.proofJobsView', { treeDataProvider: jobs });
-    const documents = new ProofDocuments(secrets);
     const origins = new JobOrigins(context.workspaceState);
+    const jobs = new ProofJobsProvider(secrets, log, origins);
+    const view = vscode.window.createTreeView('inference.proofJobsView', { treeDataProvider: jobs, showCollapseAll: false });
+    const documents = new ProofDocuments(secrets);
     /** 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);
@@ -62,11 +63,19 @@ export function registerProver(
         () => void jobs.refresh(),
         runAgain,
     );
+    const status = new ProverStatus({
+        nameOf: (job) => jobs.displayName(job),
+        openJob: async (job) => panels.open(job, await originOf(job.id)),
+        runAgain,
+        isPanelActive: (jobId) => panels.isActive(jobId),
+    });
     disposables.push(
         jobs,
         view,
         documents,
         panels,
+        status,
+        jobs.onDidLoad((snapshot) => status.update(snapshot)),
         vscode.window.registerWebviewPanelSerializer(JOB_PANEL_VIEW_TYPE, panels),
     );
 
@@ -82,6 +91,10 @@ export function registerProver(
                 await origins.set(config.serverUrl, job.id, origin);
             }
         }
+        if (isActiveJob(job)) {
+            jobs.noteSubmitted();
+            status.watch(job);
+        }
         await jobs.refresh();
         const node = jobs.findNode(job.id);
         if (node && view.visible) {
@@ -96,19 +109,35 @@ export function registerProver(
 
     command('inference.refreshProofJobs', () => jobs.refresh());
     command('inference.loadMoreProofJobs', () => jobs.loadMore());
+    const setFilter = async (filter: JobStatus | undefined) => {
+        view.description = filter ? `Showing: ${FILTER_LABELS[filter]}` : undefined;
+        await jobs.setFilter(filter);
+    };
     command('inference.filterProofJobs', async () => {
-        const all = 'All statuses';
-        const picked = await vscode.window.showQuickPick([all, ...FILTER_STATUSES], {
-            title: 'Show proof jobs with status',
-            placeHolder: jobs.statusFilter ?? all,
+        type Item = vscode.QuickPickItem & { status?: JobStatus };
+        const option = (s: JobStatus): Item => ({
+            label: FILTER_LABELS[s],
+            description: s,
+            status: s,
+            picked: jobs.statusFilter === s,
+        });
+        const items: Item[] = [
+            { label: 'All jobs', description: jobs.statusFilter ? undefined : 'current' },
+            { label: 'In progress', kind: vscode.QuickPickItemKind.Separator },
+            ...FILTER_STATUSES.filter((s) => isActiveJob({ status: s }) && s !== 'Lost').map(option),
+            { label: 'Finished', kind: vscode.QuickPickItemKind.Separator },
+            ...FILTER_STATUSES.filter((s) => !isActiveJob({ status: s }) || s === 'Lost').map(option),
+        ];
+        const picked = await vscode.window.showQuickPick(items, {
+            title: 'Show proof jobs',
+            placeHolder: jobs.statusFilter ? `Showing: ${FILTER_LABELS[jobs.statusFilter]}` : 'Showing all jobs',
+            matchOnDescription: true,
         });
-        if (picked === undefined) {
-            return;
+        if (picked) {
+            await setFilter(picked.status);
         }
-        const status = picked === all ? undefined : (picked as JobStatus);
-        view.description = status ? `Status: ${status}` : undefined;
-        await jobs.setFilter(status);
     });
+    command('inference.clearProofJobsFilter', () => setFilter(undefined));
     command('inference.openProofJob', async (arg) => {
         const job = jobOf(arg);
         if (job) {
@@ -149,13 +178,14 @@ export function registerProver(
     command('inference.openProofJobInPortal', async (arg) => {
         const job = jobOf(arg);
         if (job) {
-            await openInPortal(secrets, job);
+            await openInPortal(secrets, job, hasCertificate(job) ? 'certificate' : 'job');
         }
     });
 
     // A different server or key means different jobs: drop what is loaded
     // and every open panel before loading again.
     const changed = () => {
+        status.reset();
         jobs.reset();
         panels.closeAll();
         void jobs.refresh();

editors/vscode/src/prover/jobDetailModel.ts

@@ -439,7 +439,8 @@ function verdictActions(job: JobResponse, result: JobResultResponse | null, verd
             ? { action: 'openCertificate', label: 'Certificate', icon: 'linkExternal', ariaLabel: 'Open the certificate in the portal' }
             : { action: 'openPortal', label: 'Open in portal', icon: 'linkExternal', ariaLabel: 'Open this job in the portal' });
     }
-    if (['failed', 'timed-out', 'provision-failed', 'lost', 'canceled'].includes(verdict.kind)) {
+    // Not for Lost: the server runs it again by itself.
+    if (['failed', 'timed-out', 'provision-failed', 'canceled'].includes(verdict.kind)) {
         actions.push({ action: 'resubmit', label: 'Run Again', icon: 'rerun', ariaLabel: 'Run this proof job again' });
     }
     return actions;

editors/vscode/src/prover/jobDetailView.ts

@@ -107,6 +107,11 @@ export class JobDetailViewManager implements vscode.Disposable, vscode.WebviewPa
         private readonly onRunAgain: (job: JobResponse) => Promise<void>,
     ) {}
 
+    /** The job's panel is the active editor tab. */
+    isActive(jobId: string): boolean {
+        return this.states.get(jobId)?.panel.active === true;
+    }
+
     /** Close every panel: the server or the account changed. */
     closeAll(): void {
         for (const state of [...this.states.values()]) {