From 4334495a09092e3d87c11e0d9b28888e724b1d79 Mon Sep 17 00:00:00 2001 From: 0xGeorgii Date: Sat, 10 Oct 2026 01:10:46 +0900 Subject: [PATCH 1/4] vscode: clearer Proof Jobs view, proving status bar item, finish notices MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Proof Jobs view: - Rows are named after the .inf they came from and read like "Verified · 15/15 · 2h ago", with coloured codicons from the same verdict wording as the job panel and a Markdown tooltip. - "In progress" and "Finished" groups while something runs (flat when filtered); reveal works through real parents. - The filter offers plain names grouped by in progress / finished, and Show All Proof Jobs (new command) clears it. - Error rows act: a rejected key opens Set API Key, a network error retries, a bad server URL opens the setting. - Menus follow the server: Open in Portal for every job (certificate tab only for runs that can carry one), Run Again not for Lost (the server re-queues it), Delete also for Lost; the view title gains Prove This File and the key commands. - Polling adapts: 5 s just after a submit, 10 s while jobs move (also when hidden), 60 s when idle and visible, off when idle and hidden, with backoff on errors. Status bar: - A proving item shows the running job and its progress (or "Proving 2"), then the last result; it opens the job or the view. - A notice when a watched job finishes, with Open (and Run Again for failures), unless its panel is already in front. - The toolchain item is no longer red when a doctor check fails but infs resolved a working infc (e.g. Platform with a custom inference.path): it shows a warning that the compiler works, and the Configuration view and the log say "works with issues". Co-Authored-By: Claude Opus 5.5 --- editors/vscode/package.json | 44 ++- editors/vscode/src/extension.ts | 14 +- editors/vscode/src/prover/index.ts | 57 +++- editors/vscode/src/prover/jobDetailView.ts | 5 + editors/vscode/src/prover/jobList.ts | 123 +++++++- editors/vscode/src/prover/jobPresentation.ts | 83 ------ editors/vscode/src/prover/jobsTree.ts | 282 ++++++++++++++---- editors/vscode/src/prover/proverStatusBar.ts | 124 ++++++++ .../vscode/src/prover/proverStatusBarState.ts | 80 +++++ .../vscode/src/test/prover-job-list.test.ts | 77 ++++- .../src/test/prover-job-presentation.test.ts | 80 ----- .../vscode/src/test/prover-manifest.test.ts | 7 +- .../vscode/src/test/prover-status-bar.test.ts | 71 +++++ .../vscode/src/test/settings-schema.test.ts | 5 +- editors/vscode/src/ui/configTree.ts | 24 +- editors/vscode/src/ui/statusBarState.ts | 46 +++ 16 files changed, 853 insertions(+), 269 deletions(-) create mode 100644 editors/vscode/src/prover/proverStatusBar.ts create mode 100644 editors/vscode/src/prover/proverStatusBarState.ts create mode 100644 editors/vscode/src/test/prover-status-bar.test.ts diff --git a/editors/vscode/package.json b/editors/vscode/package.json index eccf3f9d..c8fa6096 100644 --- a/editors/vscode/package.json +++ b/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" } ] }, diff --git a/editors/vscode/src/extension.ts b/editors/vscode/src/extension.ts index ff63f0b1..42f89814 100644 --- a/editors/vscode/src/extension.ts +++ b/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}`); diff --git a/editors/vscode/src/prover/index.ts b/editors/vscode/src/prover/index.ts index 2a1644a0..17448a15 100644 --- a/editors/vscode/src/prover/index.ts +++ b/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 => { 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,7 +178,7 @@ 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' : undefined); } }); diff --git a/editors/vscode/src/prover/jobDetailView.ts b/editors/vscode/src/prover/jobDetailView.ts index 81b9dbcf..439cb922 100644 --- a/editors/vscode/src/prover/jobDetailView.ts +++ b/editors/vscode/src/prover/jobDetailView.ts @@ -107,6 +107,11 @@ export class JobDetailViewManager implements vscode.Disposable, vscode.WebviewPa private readonly onRunAgain: (job: JobResponse) => Promise, ) {} + /** 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()]) { diff --git a/editors/vscode/src/prover/jobList.ts b/editors/vscode/src/prover/jobList.ts index e2716874..137a8eba 100644 --- a/editors/vscode/src/prover/jobList.ts +++ b/editors/vscode/src/prover/jobList.ts @@ -3,7 +3,8 @@ * under plain node. */ -import { isCancelableStatus, isTerminalStatus } from './jobDetailHtml'; +import { isCancelableStatus, isTerminalStatus } from './jobStatus'; +import { listVerdict } from './jobVerdict'; import type { JobResponse, JobStatus } from './types'; /** Jobs per page (the server allows up to 100). */ @@ -16,17 +17,51 @@ export const FILTER_STATUSES: readonly JobStatus[] = [ 'ProvisionFailed', ]; +/** Plain filter labels; the raw status is shown beside each. */ +export const FILTER_LABELS: Readonly> = { + Accepted: 'Accepted', + Queued: 'Waiting for a worker', + Provisioning: 'Starting a worker', + Booting: 'Worker booting', + Running: 'Proving', + Verifying: 'Verifying', + Canceling: 'Canceling', + Succeeded: 'Succeeded', + PartialSuccess: 'Partially proved', + CompileGoals: 'Compiled only', + Failed: 'Failed', + TimedOut: 'Timed out', + Lost: 'Worker lost', + Canceled: 'Canceled', + ProvisionFailed: "Couldn't start", +}; + +/** Jobs the server can still move (Lost is re-queued by the server). */ +export function isActiveJob(job: Pick): boolean { + return !isTerminalStatus(job.status) || job.status === 'Lost'; +} + +/** The portal opens on the certificate for runs that can carry one. */ +export function hasCertificate(job: Pick): boolean { + return job.status === 'Succeeded' || job.status === 'PartialSuccess' || job.status === 'CompileGoals'; +} + /** - * Tree `contextValue` for a job: `inference.proofJob` plus `.cancelable` or - * `.terminal`, plus `.proof` when the run can carry a completed proof. + * Tree `contextValue` for a job: `inference.proofJob` plus one of + * `.cancelable`, `.active` (Verifying/Canceling), `.lost` or `.terminal`, + * plus `.proof` when the run can carry a completed proof. * package.json menus match these with `viewItem =~ /…/`. */ export function jobContextValue(job: Pick): string { let value = 'inference.proofJob'; if (isCancelableStatus(job.status)) { value += '.cancelable'; + } else if (job.status === 'Lost') { + value += '.lost'; } else if (isTerminalStatus(job.status)) { value += '.terminal'; + } else { + value += '.active'; } if (job.status === 'Succeeded' || job.status === 'PartialSuccess') { value += '.proof'; @@ -53,3 +88,85 @@ export function mergeFirstPage(fresh: JobResponse[], loaded: JobResponse[], page ...loaded.filter((j) => !ids.has(j.id) && Date.parse(j.createdAt ?? '') < oldest), ]; } + +/** "just now", "4m ago", "2h ago", "yesterday", "3d ago", else a short date. */ +export function relativeTime(iso: string | null | undefined, now: number): string { + const t = Date.parse(iso ?? ''); + if (Number.isNaN(t)) { + return ''; + } + const s = Math.max(0, Math.round((now - t) / 1000)); + if (s < 45) return 'just now'; + const m = Math.round(s / 60); + if (m < 60) return `${m}m ago`; + const h = Math.round(m / 60); + if (h < 24) return `${h}h ago`; + const d = Math.round(h / 24); + if (d === 1) return 'yesterday'; + if (d < 7) return `${d}d ago`; + return new Date(t).toLocaleDateString(undefined, { month: 'short', day: 'numeric' }); +} + +/** Row description: `Verified · 15/15 · 2h ago`. */ +export function describeJob(job: JobResponse, now: number): string { + const parts = [listVerdict(job).badge]; + if (typeof job.holesClosed === 'number' && typeof job.holesTotal === 'number' && job.holesTotal > 0) { + parts.push(`${job.holesClosed}/${job.holesTotal}`); + } + const when = relativeTime(job.createdAt, now); + if (when) { + parts.push(when); + } + return parts.join(' · '); +} + +export interface PollState { + /** Some loaded job can still move. */ + active: boolean; + /** The Proof Jobs view is visible. */ + visible: boolean; + /** Milliseconds since this window submitted a job, or null. */ + msSinceSubmit: number | null; + /** Consecutive failed loads. */ + errors: number; +} + +/** + * When to load the job list next (ms), or null to stop: fast right after a + * submit, steady while jobs move (also hidden, for the status bar and finish + * notices), slow when idle and visible, off when idle and hidden, and backing + * off on errors. + */ +export function pollDelay(state: PollState): number | null { + if (!state.active && !state.visible) { + return null; + } + if (state.errors > 0) { + return Math.min(300_000, 10_000 * 2 ** Math.min(state.errors - 1, 5)); + } + if (state.msSinceSubmit !== null && state.msSinceSubmit < 120_000) { + return 5_000; + } + return state.active ? 10_000 : 60_000; +} + +/** + * Jobs that finished since the previous load, among those this window saw + * moving (`watched`). A job that disappears or was never seen active is not + * reported. + */ +export function finishedJobs( + previous: ReadonlyMap, + next: readonly JobResponse[], + watched: ReadonlySet, +): JobResponse[] { + return next.filter((job) => { + const before = previous.get(job.id); + return ( + watched.has(job.id) && + before !== undefined && + isActiveJob({ status: before }) && + !isActiveJob(job) + ); + }); +} diff --git a/editors/vscode/src/prover/jobPresentation.ts b/editors/vscode/src/prover/jobPresentation.ts index f407fcfc..9ac02a57 100644 --- a/editors/vscode/src/prover/jobPresentation.ts +++ b/editors/vscode/src/prover/jobPresentation.ts @@ -21,86 +21,3 @@ export function isProvedSuccess( claimClass === 'Verified' ); } - -/** Status text that does not leave an unqualified legacy Succeeded claim. */ -export function jobStatusLabel( - status: JobStatus, - mode: RunMode | null | undefined, - holesTotal: number | null | undefined, - holesClosed: number | null | undefined, - claimClass: ClaimClass | null | undefined, -): string { - if (status !== 'Succeeded') { - return status; - } - if ( - isProvedSuccess( - status, - mode, - holesTotal, - holesClosed, - claimClass, - ) - ) { - return status; - } - if (mode === 'prove') { - if ( - typeof holesTotal !== 'number' || - holesTotal <= 0 || - typeof holesClosed !== 'number' || - holesClosed !== holesTotal - ) { - return `${status} (counts invalid)`; - } - if (claimClass === 'StructuralOnly') { - return `${status} (structural only)`; - } - return `${status} (claim unverified)`; - } - return `${status} (${mode === 'compile-goals' ? mode : 'mode unknown'})`; -} - -/** Pure icon-id mapping so proof-success behavior is testable without VS Code. */ -export function jobStatusIconId( - status: JobStatus, - mode: RunMode | null | undefined, - holesTotal: number | null | undefined, - holesClosed: number | null | undefined, - claimClass: ClaimClass | null | undefined, -): string { - switch (status) { - case 'Queued': - case 'Accepted': - case 'Provisioning': - case 'Booting': - return 'clock'; - case 'Running': - return 'sync~spin'; - case 'Verifying': - return 'beaker'; - case 'Succeeded': - return isProvedSuccess( - status, - mode, - holesTotal, - holesClosed, - claimClass, - ) - ? 'check' - : 'warning'; - case 'CompileGoals': - case 'PartialSuccess': - return 'warning'; - case 'Failed': - case 'TimedOut': - case 'Lost': - case 'ProvisionFailed': - return 'x'; - case 'Canceling': - case 'Canceled': - return 'circle-slash'; - default: - return 'question'; - } -} diff --git a/editors/vscode/src/prover/jobsTree.ts b/editors/vscode/src/prover/jobsTree.ts index 1876e587..d1ba89b4 100644 --- a/editors/vscode/src/prover/jobsTree.ts +++ b/editors/vscode/src/prover/jobsTree.ts @@ -2,21 +2,57 @@ import * as vscode from 'vscode'; import { AuthError, ProverApi } from './api'; import { describeError, resolveConfig } from './config'; -import { jobContextValue, mergeFirstPage, PAGE_SIZE } from './jobList'; -import { jobStatusIconId, jobStatusLabel } from './jobPresentation'; +import { JobOrigins } from './jobOrigins'; +import { + describeJob, + FILTER_LABELS, + isActiveJob, + jobContextValue, + mergeFirstPage, + PAGE_SIZE, + pollDelay, +} from './jobList'; +import { listVerdict, type Verdict, type VerdictIcon } from './jobVerdict'; import type { JobResponse, JobStatus } from './types'; -/** Auto-refresh cadence while the view is visible (milliseconds). */ -const AUTO_REFRESH_MS = 10_000; -type NodeKind = 'job' | 'message' | 'more'; +type NodeKind = 'job' | 'group' | 'message' | 'more'; + +/** Codicon and theme colour per verdict icon (tree rows, status bar). */ +export const VERDICT_CODICONS: Readonly> = { + pass: { id: 'pass-filled', color: 'testing.iconPassed' }, + warning: { id: 'warning', color: 'list.warningForeground' }, + error: { id: 'error', color: 'testing.iconFailed' }, + refuted: { id: 'close', color: 'charts.purple' }, + running: { id: 'sync~spin', color: 'charts.blue' }, + waiting: { id: 'clock', color: 'charts.blue' }, + verifying: { id: 'workspace-trusted', color: 'charts.blue' }, + canceled: { id: 'circle-slash', color: 'descriptionForeground' }, + loading: { id: 'loading~spin' }, +}; + +export function verdictThemeIcon(verdict: Verdict): vscode.ThemeIcon { + const icon = VERDICT_CODICONS[verdict.icon]; + return new vscode.ThemeIcon(icon.id, icon.color ? new vscode.ThemeColor(icon.color) : undefined); +} + +/** What the last load ended with, for the status bar and notifications. */ +export interface JobsSnapshot { + jobs: readonly JobResponse[]; + /** A problem to show instead of jobs, or null. */ + problem: { kind: 'auth' | 'config' | 'network'; message: string } | null; + configured: boolean; + serverUrl: string | null; +} export class JobTreeItem extends vscode.TreeItem { constructor( label: string, public readonly nodeKind: NodeKind, public readonly job?: JobResponse, + public readonly parent?: JobTreeItem, + collapsible = vscode.TreeItemCollapsibleState.None, ) { - super(label, vscode.TreeItemCollapsibleState.None); + super(label, collapsible); if (nodeKind === 'job' && job) { this.id = job.id; this.contextValue = jobContextValue(job); @@ -24,51 +60,62 @@ export class JobTreeItem extends vscode.TreeItem { } } -function describeJob(job: JobResponse): string { - const parts = [jobStatusLabel(job.status, job.mode, job.holesTotal, job.holesClosed, job.claimClass)]; - if (typeof job.holesClosed === 'number' && typeof job.holesTotal === 'number') { - parts.push(`holes ${job.holesClosed}/${job.holesTotal}`); - } - return parts.join(' · '); -} - /** - * The Proof Jobs view: the caller's jobs, newest first, optionally filtered - * by status, with a "Load more" node for older pages. Refreshes every - * {@link AUTO_REFRESH_MS} ms while visible; a refresh reloads the first page - * and keeps older pages already loaded. + * The Proof Jobs view: the caller's jobs, newest first, in "In progress" and + * "Finished" groups (flat when filtered or when nothing is running), with a + * "Load more" node for older pages. Loads on a schedule from + * {@link pollDelay}; a refresh reloads the first page and keeps older pages. */ export class ProofJobsProvider implements vscode.TreeDataProvider, vscode.Disposable { private readonly changed = new vscode.EventEmitter(); readonly onDidChangeTreeData = this.changed.event; + private readonly loaded = new vscode.EventEmitter(); + /** Fires after every load (and reset). */ + readonly onDidLoad = this.loaded.event; private jobs: JobResponse[] = []; private hasMore = false; - private errorMessage: string | null = null; + private problem: JobsSnapshot['problem'] = null; private configured = false; - private timer: ReturnType | undefined; + private serverUrl: string | null = null; + private timer: ReturnType | undefined; private loading: Promise | null = null; private filter: JobStatus | undefined; + private visible = false; + private errors = 0; + private lastSubmit: number | null = null; /** Bumped on a server or account change; replies from older generations are dropped. */ private generation = 0; + private groups = new Map(); constructor( private readonly secrets: vscode.SecretStorage, private readonly log: vscode.LogOutputChannel, + private readonly origins: JobOrigins, ) {} get statusFilter(): JobStatus | undefined { return this.filter; } + get snapshot(): JobsSnapshot { + return { jobs: this.jobs, problem: this.problem, configured: this.configured, serverUrl: this.serverUrl }; + } + /** Show only `status` (undefined = all); a load in flight finishes first. */ async setFilter(status: JobStatus | undefined): Promise { this.filter = status; this.jobs = []; + await vscode.commands.executeCommand('setContext', 'inference.prover.filtered', status !== undefined); await this.loading; return this.refresh(); } + /** A job was just submitted from this window: poll quickly for a while. */ + noteSubmitted(): void { + this.lastSubmit = Date.now(); + } + /** Reload the first page; concurrent calls share one load. */ refresh(): Promise { return this.loading ?? this.track(this.load(false)); @@ -89,9 +136,11 @@ export class ProofJobsProvider implements vscode.TreeDataProvider, this.generation++; this.jobs = []; this.hasMore = false; - this.errorMessage = null; + this.problem = null; this.loading = null; + this.errors = 0; this.changed.fire(undefined); + this.loaded.fire(this.snapshot); } private track(load: Promise): Promise { @@ -99,34 +148,74 @@ export class ProofJobsProvider implements vscode.TreeDataProvider, if (this.loading === tracked) { this.loading = null; } + this.schedule(); }); this.loading = tracked; return tracked; } setVisible(visible: boolean): void { + this.visible = visible; if (visible) { void this.refresh(); - this.timer ??= setInterval(() => void this.refresh(), AUTO_REFRESH_MS); - } else if (this.timer) { - clearInterval(this.timer); + } else { + this.schedule(); + } + } + + private schedule(): void { + if (this.timer) { + clearTimeout(this.timer); this.timer = undefined; } + const delay = pollDelay({ + active: this.jobs.some(isActiveJob), + visible: this.visible, + msSinceSubmit: this.lastSubmit === null ? null : Date.now() - this.lastSubmit, + errors: this.errors, + }); + if (delay !== null && this.configured) { + this.timer = setTimeout(() => void this.refresh(), delay); + } } /** The node for a loaded job (for TreeView.reveal, which matches by id). */ findNode(jobId: string): JobTreeItem | undefined { const job = this.jobs.find((j) => j.id === jobId); - return job ? this.makeNode(job) : undefined; + if (!job) { + return undefined; + } + const grouped = this.grouped(); + const parent = grouped ? this.group(isActiveJob(job) ? 'active' : 'finished', 0) : undefined; + return this.makeNode(job, parent); } - private makeNode(job: JobResponse): JobTreeItem { - const node = new JobTreeItem(job.filename ?? job.id, 'job', job); - node.iconPath = new vscode.ThemeIcon( - jobStatusIconId(job.status, job.mode, job.holesTotal, job.holesClosed, job.claimClass), - ); - node.description = describeJob(job); - node.tooltip = `${job.id}\nstatus: ${jobStatusLabel(job.status, job.mode, job.holesTotal, job.holesClosed, job.claimClass)}\nclaim class: ${job.claimClass ?? 'unknown'}${job.createdAt ? `\nsubmitted: ${new Date(job.createdAt).toLocaleString()}` : ''}`; + /** The name a job is shown under: the `.inf` it came from, else the upload. */ + displayName(job: JobResponse): string { + const origin = this.serverUrl ? this.origins.get(this.serverUrl, job.id) : undefined; + return JobOrigins.displayName(origin) ?? job.filename ?? job.id; + } + + private makeNode(job: JobResponse, parent?: JobTreeItem): JobTreeItem { + const verdict = listVerdict(job); + const name = this.displayName(job); + const node = new JobTreeItem(name, 'job', job, parent); + node.iconPath = verdictThemeIcon(verdict); + node.description = describeJob(job, Date.now()); + const tooltip = new vscode.MarkdownString(undefined, true); + tooltip.appendMarkdown(`$(${VERDICT_CODICONS[verdict.icon].id.replace('~spin', '')}) **${escapeMd(verdict.headline)}**\n\n`); + tooltip.appendMarkdown(`${escapeMd(verdict.body)}\n\n`); + const facts = [ + name !== job.filename && job.filename ? `${escapeMd(name)} → ${code(job.filename)}` : undefined, + typeof job.holesTotal === 'number' && job.holesTotal > 0 ? `${job.holesClosed ?? 0}/${job.holesTotal} obligations` : undefined, + job.createdAt ? `submitted ${new Date(job.createdAt).toLocaleString()}` : undefined, + ].filter(Boolean); + if (facts.length) { + tooltip.appendMarkdown(`${facts.join(' · ')}\n\n`); + } + tooltip.appendMarkdown(`Job ${code(job.id)}`); + node.tooltip = tooltip; + node.accessibilityInformation = { label: `${name}, ${verdict.badge}, ${node.description}` }; node.command = { title: 'Open Proof Job', command: 'inference.openProofJob', arguments: [node] }; return node; } @@ -139,18 +228,19 @@ export class ProofJobsProvider implements vscode.TreeDataProvider, } catch (err) { this.configured = true; this.jobs = []; - this.errorMessage = describeError(err); - this.changed.fire(undefined); + this.problem = { kind: 'config', message: describeError(err) }; + this.fire(); return; } if (!config) { this.configured = false; this.jobs = []; - this.errorMessage = null; - this.changed.fire(undefined); + this.problem = null; + this.fire(); return; } this.configured = true; + this.serverUrl = config.serverUrl; try { const api = new ProverApi(config.serverUrl, config.apiKey); const before = more ? this.jobs[this.jobs.length - 1]?.createdAt ?? undefined : undefined; @@ -164,62 +254,140 @@ export class ProofJobsProvider implements vscode.TreeDataProvider, // older loaded pages keeps the answer from the last "Load more". this.hasMore = page.length === PAGE_SIZE; } - this.errorMessage = null; + this.problem = null; + this.errors = 0; } catch (err) { if (generation !== this.generation) { return; } - this.jobs = []; - this.hasMore = false; - this.errorMessage = - err instanceof AuthError && err.status === 401 - ? 'Authentication failed. Check your API key.' - : describeError(err); + this.errors++; + const auth = err instanceof AuthError && err.status === 401; + this.problem = auth + ? { kind: 'auth', message: 'The proof server rejected the API key.' } + : { kind: 'network', message: describeError(err) }; + if (auth) { + this.jobs = []; + this.hasMore = false; + } this.log.error(`Prover: listing jobs: ${err instanceof Error ? err.message : err}`); } + this.fire(); + } + + private fire(): void { + this.groups.clear(); this.changed.fire(undefined); + this.loaded.fire(this.snapshot); + } + + /** Grouped when unfiltered and something is in progress. */ + private grouped(): boolean { + return !this.filter && this.jobs.some(isActiveJob); + } + + private group(kind: 'active' | 'finished', count: number): JobTreeItem { + const existing = this.groups.get(kind); + if (existing) { + return existing; + } + const label = kind === 'active' ? 'In progress' : 'Finished'; + const node = new JobTreeItem(label, 'group', undefined, undefined, vscode.TreeItemCollapsibleState.Expanded); + node.id = `group:${kind}`; + node.description = count > 0 ? String(count) : undefined; + node.contextValue = `inference.proofJobGroup.${kind}`; + this.groups.set(kind, node); + return node; } getTreeItem(element: JobTreeItem): vscode.TreeItem { return element; } - getParent(): undefined { - return undefined; + getParent(element: JobTreeItem): JobTreeItem | undefined { + return element.parent; + } + + private problemNode(): JobTreeItem { + const problem = this.problem!; + const node = new JobTreeItem( + problem.kind === 'auth' + ? 'API key rejected — set a new key' + : problem.kind === 'config' + ? problem.message + : "Can't reach the proof server — retry", + 'message', + ); + node.iconPath = new vscode.ThemeIcon(problem.kind === 'auth' ? 'key' : 'error', new vscode.ThemeColor('list.errorForeground')); + node.tooltip = problem.message; + node.command = problem.kind === 'auth' + ? { title: 'Set API Key', command: 'inference.setProverApiKey' } + : problem.kind === 'config' + ? { title: 'Open Setting', command: 'workbench.action.openSettings', arguments: ['inference.prover.serverUrl'] } + : { title: 'Retry', command: 'inference.refreshProofJobs' }; + return node; } getChildren(element?: JobTreeItem): JobTreeItem[] { + if (element?.nodeKind === 'group') { + const kind = element.id === 'group:active' ? 'active' : 'finished'; + const jobs = this.jobs.filter((j) => isActiveJob(j) === (kind === 'active')); + const items = jobs.map((job) => this.makeNode(job, element)); + if (kind === 'finished' && this.hasMore) { + items.push(this.moreNode(element)); + } + return items; + } if (element || !this.configured) { return []; // unconfigured → the welcome view shows instead } - if (this.errorMessage) { - const node = new JobTreeItem(this.errorMessage, 'message'); - node.iconPath = new vscode.ThemeIcon('error'); - node.tooltip = this.errorMessage; - return [node]; + if (this.problem && (this.problem.kind !== 'network' || this.jobs.length === 0)) { + return [this.problemNode()]; } + const problem = this.problem ? [this.problemNode()] : []; if (this.jobs.length === 0) { const node = new JobTreeItem( - this.filter ? `No ${this.filter} jobs.` : 'No proof jobs yet.', + this.filter ? `No “${FILTER_LABELS[this.filter]}” jobs.` : 'No proof jobs yet. Prove an .inf file to start.', 'message', ); node.iconPath = new vscode.ThemeIcon('info'); + if (this.filter) { + node.command = { title: 'Show All Jobs', command: 'inference.clearProofJobsFilter' }; + node.tooltip = 'Click to show all jobs'; + } return [node]; } + if (this.grouped()) { + const active = this.jobs.filter(isActiveJob).length; + return [...problem, this.group('active', active), this.group('finished', this.jobs.length - active)]; + } const items = this.jobs.map((job) => this.makeNode(job)); if (this.hasMore) { - const more = new JobTreeItem('Load more…', 'more'); - more.iconPath = new vscode.ThemeIcon('ellipsis'); - more.command = { title: 'Load More', command: 'inference.loadMoreProofJobs' }; - items.push(more); + items.push(this.moreNode()); } - return items; + return [...problem, ...items]; + } + + private moreNode(parent?: JobTreeItem): JobTreeItem { + const more = new JobTreeItem('Load more…', 'more', undefined, parent); + more.iconPath = new vscode.ThemeIcon('ellipsis'); + more.command = { title: 'Load More', command: 'inference.loadMoreProofJobs' }; + return more; } dispose(): void { if (this.timer) { - clearInterval(this.timer); + clearTimeout(this.timer); } this.changed.dispose(); + this.loaded.dispose(); } } + +function escapeMd(text: string): string { + return text.replace(/[\\`*_{}[\]()#+\-.!|<>]/g, (c) => `\\${c}`); +} + +/** An inline code span (backticks inside are replaced; code spans take no escapes). */ +function code(text: string): string { + return `\`${text.replace(/`/g, "'")}\``; +} diff --git a/editors/vscode/src/prover/proverStatusBar.ts b/editors/vscode/src/prover/proverStatusBar.ts new file mode 100644 index 00000000..3086d0a5 --- /dev/null +++ b/editors/vscode/src/prover/proverStatusBar.ts @@ -0,0 +1,124 @@ +import * as vscode from 'vscode'; + +import { finishedJobs, isActiveJob } from './jobList'; +import { listVerdict } from './jobVerdict'; +import { VERDICT_CODICONS, type JobsSnapshot } from './jobsTree'; +import { proverStatusState } from './proverStatusBarState'; +import type { JobResponse, JobStatus } from './types'; + +/** Internal command behind the status bar item. */ +export const SHOW_PROVER_STATUS_COMMAND = 'inference.showProverStatus'; + +export interface ProverStatusHooks { + nameOf(job: JobResponse): string; + openJob(job: JobResponse): Promise; + runAgain(job: JobResponse): Promise; + /** The job's panel is the active editor tab (no notice needed). */ + isPanelActive(jobId: string): boolean; +} + +/** + * The proving status bar item and the "job finished" notices. Both follow the + * Proof Jobs loads ({@link JobsSnapshot}); the job list keeps loading while + * jobs move, even when its view is hidden. + */ +export class ProverStatus implements vscode.Disposable { + private readonly item = vscode.window.createStatusBarItem(vscode.StatusBarAlignment.Left, -1); + private readonly command: vscode.Disposable; + private previous = new Map(); + private readonly watched = new Set(); + private lastFinished: JobResponse | null = null; + private target: string | null = null; + private snapshot: JobsSnapshot | null = null; + + constructor(private readonly hooks: ProverStatusHooks) { + this.item.name = 'Inference Proof Jobs'; + this.item.command = SHOW_PROVER_STATUS_COMMAND; + this.command = vscode.commands.registerCommand(SHOW_PROVER_STATUS_COMMAND, () => this.onClick()); + } + + /** A job was just submitted here: watch it and stop showing the last result. */ + watch(job: JobResponse): void { + this.watched.add(job.id); + this.lastFinished = null; + if (this.snapshot) { + this.update(this.snapshot); + } + } + + update(snapshot: JobsSnapshot): void { + this.snapshot = snapshot; + for (const job of snapshot.jobs) { + if (isActiveJob(job)) { + this.watched.add(job.id); + } + } + const finished = finishedJobs(this.previous, snapshot.jobs, this.watched); + this.previous = new Map(snapshot.jobs.map((j) => [j.id, j.status])); + for (const job of finished) { + this.watched.delete(job.id); + this.lastFinished = job; + if (!this.hooks.isPanelActive(job.id)) { + void this.notify(job); + } + } + const state = proverStatusState({ + jobs: snapshot.configured ? snapshot.jobs : [], + problem: snapshot.problem, + lastFinished: this.lastFinished, + nameOf: (job) => this.hooks.nameOf(job), + }); + this.target = state.jobId; + if (!state.visible) { + this.item.hide(); + return; + } + const icon = state.icon === 'server' ? 'cloud' : VERDICT_CODICONS[state.icon].id; + this.item.text = `$(${icon}) ${state.text}`; + this.item.tooltip = state.tooltip; + this.item.backgroundColor = state.icon === 'server' + ? new vscode.ThemeColor('statusBarItem.warningBackground') + : undefined; + this.item.show(); + } + + private async notify(job: JobResponse): Promise { + const verdict = listVerdict(job); + const name = this.hooks.nameOf(job); + const counts = typeof job.holesTotal === 'number' && job.holesTotal > 0 + ? ` (${job.holesClosed ?? 0}/${job.holesTotal})` + : ''; + const message = `Inference: ${name} — ${verdict.headline}${counts}.`; + const good = verdict.claim !== 'none'; + const retry = ['failed', 'timed-out', 'provision-failed', 'lost'].includes(verdict.kind); + const actions = retry ? ['Open', 'Run Again'] : ['Open']; + const choice = good && verdict.tone === 'ok' + ? await vscode.window.showInformationMessage(message, ...actions) + : await vscode.window.showWarningMessage(message, ...actions); + if (choice === 'Open') { + await this.hooks.openJob(job); + } else if (choice === 'Run Again') { + await this.hooks.runAgain(job); + } + } + + private async onClick(): Promise { + const job = this.target ? this.snapshot?.jobs.find((j) => j.id === this.target) : undefined; + if (job) { + if (!isActiveJob(job)) { + this.lastFinished = null; // seen + } + await this.hooks.openJob(job); + if (this.snapshot) { + this.update(this.snapshot); + } + return; + } + await vscode.commands.executeCommand('inference.proofJobsView.focus'); + } + + dispose(): void { + this.item.dispose(); + this.command.dispose(); + } +} diff --git a/editors/vscode/src/prover/proverStatusBarState.ts b/editors/vscode/src/prover/proverStatusBarState.ts new file mode 100644 index 00000000..d84e1f18 --- /dev/null +++ b/editors/vscode/src/prover/proverStatusBarState.ts @@ -0,0 +1,80 @@ +/** + * What the proving status bar item shows. Pure — no `vscode` import. + */ + +import { isActiveJob } from './jobList'; +import { listVerdict, type VerdictIcon } from './jobVerdict'; +import type { JobResponse } from './types'; + +export interface ProverStatusInput { + jobs: readonly JobResponse[]; + problem: { kind: 'auth' | 'config' | 'network'; message: string } | null; + /** The newest job that finished while this window watched it. */ + lastFinished: JobResponse | null; + /** The name the user knows a job by (`.inf`, else the upload). */ + nameOf(job: JobResponse): string; +} + +export interface ProverStatusState { + visible: boolean; + /** Codicon key from the verdict, or a fixed one. */ + icon: VerdictIcon | 'server'; + text: string; + tooltip: string; + /** Job to open on click; null = show the Proof Jobs view. */ + jobId: string | null; +} + +function stem(name: string): string { + const dot = name.lastIndexOf('.'); + return dot > 0 ? name.slice(0, dot) : name; +} + +export function proverStatusState(input: ProverStatusInput): ProverStatusState { + if (input.problem && input.problem.kind !== 'config') { + return { + visible: true, + icon: 'server', + text: 'Proof server', + tooltip: input.problem.kind === 'auth' + ? 'The proof server rejected the API key. Click to see Proof Jobs.' + : `Can't reach the proof server: ${input.problem.message}`, + jobId: null, + }; + } + const active = input.jobs.filter(isActiveJob); + if (active.length === 1) { + const job = active[0]; + const verdict = listVerdict(job); + const counts = typeof job.holesTotal === 'number' && job.holesTotal > 0 + ? ` ${job.holesClosed ?? 0}/${job.holesTotal}` + : ''; + return { + visible: true, + icon: verdict.icon, + text: `${stem(input.nameOf(job))}${counts}`, + tooltip: `${input.nameOf(job)}: ${verdict.headline}. Click to open the job.`, + jobId: job.id, + }; + } + if (active.length > 1) { + return { + visible: true, + icon: 'running', + text: `Proving ${active.length}`, + tooltip: `${active.length} proof jobs are in progress: ${active.map((j) => input.nameOf(j)).join(', ')}. Click to see Proof Jobs.`, + jobId: null, + }; + } + if (input.lastFinished) { + const verdict = listVerdict(input.lastFinished); + return { + visible: true, + icon: verdict.icon, + text: stem(input.nameOf(input.lastFinished)), + tooltip: `${input.nameOf(input.lastFinished)}: ${verdict.headline}. Click to open the job.`, + jobId: input.lastFinished.id, + }; + } + return { visible: false, icon: 'server', text: '', tooltip: '', jobId: null }; +} diff --git a/editors/vscode/src/test/prover-job-list.test.ts b/editors/vscode/src/test/prover-job-list.test.ts index 72f9d2cf..1aba6998 100644 --- a/editors/vscode/src/test/prover-job-list.test.ts +++ b/editors/vscode/src/test/prover-job-list.test.ts @@ -1,7 +1,17 @@ import * as assert from 'node:assert'; import { describe, it } from 'node:test'; -import { FILTER_STATUSES, jobContextValue, mergeFirstPage } from '../prover/jobList'; +import { + describeJob, + FILTER_STATUSES, + finishedJobs, + hasCertificate, + isActiveJob, + jobContextValue, + mergeFirstPage, + pollDelay, + relativeTime, +} from '../prover/jobList'; import type { JobResponse, JobStatus } from '../prover/types'; const job = (id: string, createdAt: string, status: JobStatus = 'Succeeded'): JobResponse => ({ @@ -13,7 +23,8 @@ const job = (id: string, createdAt: string, status: JobStatus = 'Succeeded'): Jo describe('jobContextValue', () => { it('separates cancelable, terminal and proof-carrying jobs', () => { assert.strictEqual(jobContextValue({ status: 'Running' }), 'inference.proofJob.cancelable'); - assert.strictEqual(jobContextValue({ status: 'Verifying' }), 'inference.proofJob'); + assert.strictEqual(jobContextValue({ status: 'Verifying' }), 'inference.proofJob.active'); + assert.strictEqual(jobContextValue({ status: 'Lost' }), 'inference.proofJob.lost'); assert.strictEqual(jobContextValue({ status: 'Failed' }), 'inference.proofJob.terminal'); assert.strictEqual(jobContextValue({ status: 'Succeeded' }), 'inference.proofJob.terminal.proof'); assert.strictEqual(jobContextValue({ status: 'PartialSuccess' }), 'inference.proofJob.terminal.proof'); @@ -45,3 +56,65 @@ describe('mergeFirstPage', () => { ); }); }); + +describe('relativeTime and describeJob', () => { + const now = Date.parse('2026-10-09T12:00:00Z'); + it('words recent times', () => { + assert.strictEqual(relativeTime('2026-10-09T11:59:40Z', now), 'just now'); + assert.strictEqual(relativeTime('2026-10-09T11:56:00Z', now), '4m ago'); + assert.strictEqual(relativeTime('2026-10-09T10:00:00Z', now), '2h ago'); + assert.strictEqual(relativeTime('2026-10-08T12:00:00Z', now), 'yesterday'); + assert.strictEqual(relativeTime('2026-10-06T12:00:00Z', now), '3d ago'); + assert.strictEqual(relativeTime('nonsense', now), ''); + }); + + it('describes a row with its verdict, counts and time', () => { + assert.strictEqual( + describeJob({ id: 'a', status: 'Succeeded', mode: 'prove', claimClass: 'Verified', holesTotal: 15, holesClosed: 15, createdAt: '2026-10-09T10:00:00Z' }, now), + 'Verified · 15/15 · 2h ago', + ); + assert.strictEqual( + describeJob({ id: 'b', status: 'Failed', errorCode: 'compile_failed', createdAt: '2026-10-08T12:00:00Z' }, now), + 'Compile error · yesterday', + ); + }); +}); + +describe('pollDelay', () => { + const base = { active: false, visible: true, msSinceSubmit: null, errors: 0 }; + it('polls fast after a submit, steadily while jobs move, slowly when idle', () => { + assert.strictEqual(pollDelay({ ...base, active: true, msSinceSubmit: 30_000 }), 5_000); + assert.strictEqual(pollDelay({ ...base, active: true }), 10_000); + assert.strictEqual(pollDelay({ ...base, active: true, visible: false }), 10_000); + assert.strictEqual(pollDelay(base), 60_000); + assert.strictEqual(pollDelay({ ...base, visible: false }), null); + }); + + it('backs off on errors, capped at five minutes', () => { + assert.strictEqual(pollDelay({ ...base, errors: 1 }), 10_000); + assert.strictEqual(pollDelay({ ...base, errors: 3 }), 40_000); + assert.strictEqual(pollDelay({ ...base, errors: 20 }), 300_000); + }); +}); + +describe('finishedJobs', () => { + it('reports watched jobs that went from moving to finished', () => { + const previous = new Map([['a', 'Running'], ['b', 'Running'], ['c', 'Succeeded']] as const); + const next: JobResponse[] = [ + { id: 'a', status: 'Succeeded' }, + { id: 'b', status: 'Running' }, + { id: 'c', status: 'Succeeded' }, + { id: 'd', status: 'Failed' }, + ]; + assert.deepStrictEqual(finishedJobs(previous, next, new Set(['a', 'b', 'c', 'd'])).map((j) => j.id), ['a']); + assert.deepStrictEqual(finishedJobs(previous, next, new Set(['b'])).map((j) => j.id), []); + }); + + it('treats Lost as still moving (the server re-queues it)', () => { + const previous = new Map([['a', 'Running']] as const); + assert.deepStrictEqual(finishedJobs(previous, [{ id: 'a', status: 'Lost' }], new Set(['a'])), []); + assert.ok(isActiveJob({ status: 'Lost' })); + assert.ok(hasCertificate({ status: 'CompileGoals' })); + assert.ok(!hasCertificate({ status: 'Failed' })); + }); +}); diff --git a/editors/vscode/src/test/prover-job-presentation.test.ts b/editors/vscode/src/test/prover-job-presentation.test.ts index 2e261679..5e5db151 100644 --- a/editors/vscode/src/test/prover-job-presentation.test.ts +++ b/editors/vscode/src/test/prover-job-presentation.test.ts @@ -3,8 +3,6 @@ import { describe, it } from 'node:test'; import { isProvedSuccess, - jobStatusIconId, - jobStatusLabel, } from '../prover/jobPresentation'; import type { ClaimClass, RunMode } from '../prover/types'; @@ -46,82 +44,4 @@ describe('job proof presentation', () => { ); } }); - - it('uses a check icon only for durable proof success', () => { - assert.strictEqual( - jobStatusIconId('Succeeded', 'prove', 2, 2, 'Verified'), - 'check', - ); - assert.strictEqual( - jobStatusIconId('Succeeded', 'prove', 2, 2, 'StructuralOnly'), - 'warning', - ); - assert.strictEqual( - jobStatusIconId('Succeeded', 'prove', 2, 2, undefined), - 'warning', - ); - assert.strictEqual( - jobStatusIconId('Succeeded', 'compile-goals', 2, 2, 'Verified'), - 'warning', - ); - assert.strictEqual( - jobStatusIconId('Succeeded', 'unknown', 2, 2, 'Verified'), - 'warning', - ); - assert.strictEqual( - jobStatusIconId('Succeeded', null, 2, 2, 'Verified'), - 'warning', - ); - assert.strictEqual( - jobStatusIconId('Succeeded', 'prove', 2, 1, 'Verified'), - 'warning', - ); - assert.strictEqual( - jobStatusIconId( - 'CompileGoals', - 'compile-goals', - 2, - 0, - 'Unverified', - ), - 'warning', - ); - }); - - it('qualifies Succeeded text unless mode and counts prove completion', () => { - assert.strictEqual( - jobStatusLabel('Succeeded', 'prove', 2, 2, 'Verified'), - 'Succeeded', - ); - assert.strictEqual( - jobStatusLabel('Succeeded', 'prove', 2, 2, 'StructuralOnly'), - 'Succeeded (structural only)', - ); - assert.strictEqual( - jobStatusLabel('Succeeded', 'prove', 2, 2, undefined), - 'Succeeded (claim unverified)', - ); - assert.strictEqual( - jobStatusLabel('Succeeded', 'compile-goals', 2, 2, 'Verified'), - 'Succeeded (compile-goals)', - ); - assert.strictEqual( - jobStatusLabel('Succeeded', null, 2, 2, 'Verified'), - 'Succeeded (mode unknown)', - ); - assert.strictEqual( - jobStatusLabel('Succeeded', 'prove', 2, 1, 'Verified'), - 'Succeeded (counts invalid)', - ); - assert.strictEqual( - jobStatusLabel( - 'CompileGoals', - 'compile-goals', - 2, - 0, - 'Unverified', - ), - 'CompileGoals', - ); - }); }); diff --git a/editors/vscode/src/test/prover-manifest.test.ts b/editors/vscode/src/test/prover-manifest.test.ts index 9f7ff7e1..72810b0a 100644 --- a/editors/vscode/src/test/prover-manifest.test.ts +++ b/editors/vscode/src/test/prover-manifest.test.ts @@ -40,8 +40,11 @@ describe('proof jobs manifest wiring', () => { const allowed: Record boolean> = { 'inference.cancelProofJob': (s) => ['Accepted', 'Queued', 'Provisioning', 'Booting', 'Running'].includes(s), 'inference.deleteProofJob': (s) => !['Accepted', 'Queued', 'Provisioning', 'Booting', 'Running', 'Verifying', 'Canceling'].includes(s), - 'inference.resubmitProofJob': (s) => !['Accepted', 'Queued', 'Provisioning', 'Booting', 'Running', 'Verifying', 'Canceling'].includes(s), + // Lost is re-queued by the server: deletable, but not run again. + 'inference.resubmitProofJob': (s) => !['Accepted', 'Queued', 'Provisioning', 'Booting', 'Running', 'Verifying', 'Canceling', 'Lost'].includes(s), 'inference.compareProof': (s) => s === 'Succeeded' || s === 'PartialSuccess', + 'inference.openProofJobInPortal': () => true, + 'inference.copyProofJobId': () => true, }; for (const [command, expected] of Object.entries(allowed)) { const entries = itemMenu(command); @@ -72,7 +75,7 @@ describe('proof jobs manifest wiring', () => { const ids = pkg.contributes.commands .map((c: { command: string }) => c.command) .filter((id: string) => /Proof|Prover|proveFile|submitProof|compareProof/.test(id)); - assert.strictEqual(ids.length, 13); + assert.strictEqual(ids.length, 14); for (const id of ids) { assert.ok(source.includes(`'${id}'`), id); } diff --git a/editors/vscode/src/test/prover-status-bar.test.ts b/editors/vscode/src/test/prover-status-bar.test.ts new file mode 100644 index 00000000..0e10cd57 --- /dev/null +++ b/editors/vscode/src/test/prover-status-bar.test.ts @@ -0,0 +1,71 @@ +import * as assert from 'node:assert'; +import { describe, it } from 'node:test'; + +import { proverStatusState } from '../prover/proverStatusBarState'; +import type { DoctorResult } from '../toolchain/doctor'; +import type { JobResponse } from '../prover/types'; +import { determineStatusBarState, failingChecks, toolchainHealth } from '../ui/statusBarState'; + +const nameOf = (job: JobResponse) => (job.filename ?? job.id).replace(/\.v$/, '.inf'); + +describe('proverStatusState', () => { + it('is hidden with nothing running and nothing finished', () => { + assert.strictEqual(proverStatusState({ jobs: [{ id: 'a', status: 'Succeeded' }], problem: null, lastFinished: null, nameOf }).visible, false); + }); + + it('names the one running job with its progress', () => { + const state = proverStatusState({ + jobs: [{ id: 'a', status: 'Running', filename: 'telemetry.v', holesTotal: 15, holesClosed: 3 }], + problem: null, lastFinished: null, nameOf, + }); + assert.deepStrictEqual([state.visible, state.icon, state.text, state.jobId], [true, 'running', 'telemetry 3/15', 'a']); + }); + + it('counts several running jobs and opens the view on click', () => { + const state = proverStatusState({ + jobs: [{ id: 'a', status: 'Queued' }, { id: 'b', status: 'Verifying' }], + problem: null, lastFinished: null, nameOf, + }); + assert.deepStrictEqual([state.text, state.jobId], ['Proving 2', null]); + }); + + it('shows the last finished result, and server problems first', () => { + const done: JobResponse = { id: 'a', status: 'Succeeded', mode: 'prove', claimClass: 'Verified', holesTotal: 1, holesClosed: 1, filename: 'b.v' }; + const state = proverStatusState({ jobs: [done], problem: null, lastFinished: done, nameOf }); + assert.deepStrictEqual([state.icon, state.text], ['pass', 'b']); + assert.ok(state.tooltip.includes('Proved and independently verified')); + const problem = proverStatusState({ jobs: [], problem: { kind: 'network', message: 'offline' }, lastFinished: done, nameOf }); + assert.deepStrictEqual([problem.icon, problem.text], ['server', 'Proof server']); + }); +}); + +describe('toolchainHealth', () => { + const doctor = (checks: DoctorResult['checks']): DoctorResult => ({ + checks, + hasErrors: checks.some((c) => c.status === 'fail'), + hasWarnings: checks.some((c) => c.status === 'warn'), + summary: 'Some checks failed.', + }); + + it('is degraded, not red, when only non-compiler checks fail', () => { + const result = doctor([ + { name: 'Platform', status: 'fail', message: 'Unsupported platform: linux on aarch64' }, + { name: 'Resolved infc', status: 'ok', message: '/x/infc (source: sibling of infs)' }, + ]); + assert.strictEqual(toolchainHealth(result), 'degraded'); + const state = determineStatusBarState(result); + assert.deepStrictEqual([state.icon, state.background], ['warning', 'none']); + assert.ok(state.tooltip.includes('the compiler works')); + assert.deepStrictEqual(failingChecks(result), ['Platform — Unsupported platform: linux on aarch64']); + }); + + it('stays an error when no working compiler resolved', () => { + const result = doctor([ + { name: 'Platform', status: 'fail', message: 'x' }, + { name: 'Resolved infc', status: 'fail', message: 'not found' }, + ]); + assert.strictEqual(toolchainHealth(result), 'errors'); + assert.strictEqual(determineStatusBarState(result).background, 'error'); + assert.strictEqual(toolchainHealth(null), 'missing'); + }); +}); diff --git a/editors/vscode/src/test/settings-schema.test.ts b/editors/vscode/src/test/settings-schema.test.ts index f8d541a6..91d6dfed 100644 --- a/editors/vscode/src/test/settings-schema.test.ts +++ b/editors/vscode/src/test/settings-schema.test.ts @@ -86,8 +86,8 @@ describe('settings schema (QA Section 8)', () => { describe('commands schema (QA Section 8)', () => { const commands: Array<{ command: string; title: string }> = contributes.commands; - it('has exactly 24 commands registered', () => { - assert.strictEqual(commands.length, 24); + it('has exactly 25 commands registered', () => { + assert.strictEqual(commands.length, 25); }); it('contains expected command IDs', () => { @@ -110,6 +110,7 @@ describe('commands schema (QA Section 8)', () => { 'inference.clearProverApiKey', 'inference.refreshProofJobs', 'inference.filterProofJobs', + 'inference.clearProofJobsFilter', 'inference.openProofJob', 'inference.cancelProofJob', 'inference.deleteProofJob', diff --git a/editors/vscode/src/ui/configTree.ts b/editors/vscode/src/ui/configTree.ts index 65b66492..2b38ac76 100644 --- a/editors/vscode/src/ui/configTree.ts +++ b/editors/vscode/src/ui/configTree.ts @@ -7,6 +7,7 @@ import { exec } from '../utils/exec'; import { DoctorResult } from '../toolchain/doctor'; import { describeError, getServerUrl, SERVER_URL_SETTING } from '../prover/config'; import type { ProverStatusSource } from '../prover'; +import { toolchainHealth, toolchainHealthLabel } from './statusBarState'; type GroupId = 'toolchain' | 'prover' | 'settings'; @@ -178,20 +179,15 @@ export class InferenceConfigProvider platformItem.iconPath = new vscode.ThemeIcon('device-desktop'); items.push(platformItem); - const status = this.doctorResult - ? this.doctorResult.hasErrors - ? 'errors' - : this.doctorResult.hasWarnings - ? 'warnings' - : 'healthy' - : 'unknown'; - const statusIcon = this.doctorResult - ? this.doctorResult.hasErrors - ? 'error' - : this.doctorResult.hasWarnings - ? 'warning' - : 'pass' - : 'question'; + const health = toolchainHealth(this.doctorResult ?? null); + const status = toolchainHealthLabel(health); + const statusIcon = { + missing: 'question', + healthy: 'pass', + warnings: 'warning', + degraded: 'warning', + errors: 'error', + }[health]; const statusItem = new ConfigItem( `Status: ${status}`, 'property', diff --git a/editors/vscode/src/ui/statusBarState.ts b/editors/vscode/src/ui/statusBarState.ts index 59a63f68..cd1f7fdd 100644 --- a/editors/vscode/src/ui/statusBarState.ts +++ b/editors/vscode/src/ui/statusBarState.ts @@ -10,6 +10,43 @@ export interface StatusBarState { background: StatusBarBackground; } +export type ToolchainHealth = 'missing' | 'healthy' | 'warnings' | 'degraded' | 'errors'; + +/** + * Overall toolchain health. `degraded`: some doctor check failed, but `infs` + * resolved a working `infc` — compiling (and proving) works. A custom + * `inference.path` binary, for example, can fail the Platform check. + */ +export function toolchainHealth(result: DoctorResult | null): ToolchainHealth { + if (result === null) { + return 'missing'; + } + if (result.hasErrors) { + const compiler = result.checks.find((c) => c.name === 'Resolved infc'); + return compiler?.status === 'ok' ? 'degraded' : 'errors'; + } + return result.hasWarnings ? 'warnings' : 'healthy'; +} + +/** The failing checks, as `Name — message`, for tooltips and logs. */ +export function failingChecks(result: DoctorResult | null): string[] { + return (result?.checks ?? []) + .filter((c) => c.status === 'fail') + .map((c) => `${c.name} — ${c.message}`); +} + +/** One-word status for the Configuration view and the log. */ +export function toolchainHealthLabel(health: ToolchainHealth): string { + switch (health) { + case 'missing': + return 'unknown'; + case 'degraded': + return 'works with issues'; + default: + return health; + } +} + /** * Determine the status bar display state from a doctor result. * @@ -28,6 +65,15 @@ export function determineStatusBarState(result: DoctorResult | null): StatusBarS }; } + if (toolchainHealth(result) === 'degraded') { + return { + icon: 'warning', + label: 'Inference', + tooltip: `Inference: the compiler works (infc found), but some toolchain checks failed: ${failingChecks(result).join('; ')}. Click to run the doctor.`, + background: 'none', + }; + } + if (result.hasErrors) { return { icon: 'error', From 744ee1cb7d1703eb8662dd7b9ce7f40f0e3c4d81 Mon Sep 17 00:00:00 2001 From: 0xGeorgii Date: Sat, 10 Oct 2026 11:10:52 +0900 Subject: [PATCH 2/4] vscode: address review of the Proof Jobs view and status bar - The status bar, finish notices and polling follow every job, not the filtered view: a filtered load also reads the newest page of all jobs, and moving jobs pushed off that page by newer ones are re-read one by one (at most 10), so they no longer look moving forever. - Keep polling right after a submit even when the view is hidden and the list does not show the new job yet. - Remember a submitted job's status, so a job that finishes before the next load still gets its notice and status bar result. - When several jobs finish between loads, the status bar shows the newest. - Forget the last result and watched jobs when the server or key changes. - No polling after the view is disposed. - "Open in Portal" opens the job page for jobs without a certificate. - Offer Run Again in the notice when the returned proof did not compile. Co-Authored-By: Claude Opus 5.5 --- editors/vscode/src/prover/index.ts | 3 +- editors/vscode/src/prover/jobList.ts | 64 +++++++++++++++++-- editors/vscode/src/prover/jobsTree.ts | 36 ++++++++++- editors/vscode/src/prover/proverStatusBar.ts | 33 +++++++--- .../vscode/src/test/prover-job-list.test.ts | 57 +++++++++++++++++ 5 files changed, 176 insertions(+), 17 deletions(-) diff --git a/editors/vscode/src/prover/index.ts b/editors/vscode/src/prover/index.ts index 17448a15..109ac246 100644 --- a/editors/vscode/src/prover/index.ts +++ b/editors/vscode/src/prover/index.ts @@ -178,13 +178,14 @@ export function registerProver( command('inference.openProofJobInPortal', async (arg) => { const job = jobOf(arg); if (job) { - await openInPortal(secrets, job, hasCertificate(job) ? 'certificate' : undefined); + 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(); diff --git a/editors/vscode/src/prover/jobList.ts b/editors/vscode/src/prover/jobList.ts index 137a8eba..465900ab 100644 --- a/editors/vscode/src/prover/jobList.ts +++ b/editors/vscode/src/prover/jobList.ts @@ -133,23 +133,77 @@ export interface PollState { /** * When to load the job list next (ms), or null to stop: fast right after a - * submit, steady while jobs move (also hidden, for the status bar and finish - * notices), slow when idle and visible, off when idle and hidden, and backing - * off on errors. + * submit (even before the list shows the new job), steady while jobs move + * (also hidden, for the status bar and finish notices), slow when idle and + * visible, off when idle and hidden, and backing off on errors. */ export function pollDelay(state: PollState): number | null { - if (!state.active && !state.visible) { + const recentSubmit = state.msSinceSubmit !== null && state.msSinceSubmit < 120_000; + if (!state.active && !state.visible && !recentSubmit) { return null; } if (state.errors > 0) { return Math.min(300_000, 10_000 * 2 ** Math.min(state.errors - 1, 5)); } - if (state.msSinceSubmit !== null && state.msSinceSubmit < 120_000) { + if (recentSubmit) { return 5_000; } return state.active ? 10_000 : 60_000; } +/** At most this many moving jobs outside the first page are re-read per load. */ +export const MAX_STALE_REFRESH = 10; + +/** + * Moving jobs known from earlier loads that a fresh first page no longer + * covers (newer jobs pushed them out): re-read them one by one, or they would + * look moving forever. Newest first, at most {@link MAX_STALE_REFRESH}. + */ +export function staleActiveJobs(known: readonly JobResponse[], firstPage: readonly JobResponse[]): JobResponse[] { + const fresh = new Set(firstPage.map((j) => j.id)); + const seen = new Set(); + return known + .filter((j) => { + if (fresh.has(j.id) || seen.has(j.id) || !isActiveJob(j)) { + return false; + } + seen.add(j.id); + return true; + }) + .slice(0, MAX_STALE_REFRESH); +} + +/** + * The statuses to compare the next load against: the loaded ones, plus the + * last known status of watched jobs the load did not include (a list request + * that started before the submit, or a filtered page). + */ +export function nextStatuses( + previous: ReadonlyMap, + jobs: readonly JobResponse[], + watched: ReadonlySet, +): Map { + const next = new Map(jobs.map((j) => [j.id, j.status] as [string, JobStatus])); + for (const id of watched) { + const before = previous.get(id); + if (!next.has(id) && before !== undefined) { + next.set(id, before); + } + } + return next; +} + +/** The most recently submitted job (by `createdAt`), or null. */ +export function newestJob(jobs: readonly JobResponse[]): JobResponse | null { + let newest: JobResponse | null = null; + for (const job of jobs) { + if (!newest || Date.parse(job.createdAt ?? '') > Date.parse(newest.createdAt ?? '')) { + newest = job; + } + } + return newest; +} + /** * Jobs that finished since the previous load, among those this window saw * moving (`watched`). A job that disappears or was never seen active is not diff --git a/editors/vscode/src/prover/jobsTree.ts b/editors/vscode/src/prover/jobsTree.ts index d1ba89b4..875a6ccd 100644 --- a/editors/vscode/src/prover/jobsTree.ts +++ b/editors/vscode/src/prover/jobsTree.ts @@ -11,6 +11,7 @@ import { mergeFirstPage, PAGE_SIZE, pollDelay, + staleActiveJobs, } from './jobList'; import { listVerdict, type Verdict, type VerdictIcon } from './jobVerdict'; import type { JobResponse, JobStatus } from './types'; @@ -37,7 +38,14 @@ export function verdictThemeIcon(verdict: Verdict): vscode.ThemeIcon { /** What the last load ended with, for the status bar and notifications. */ export interface JobsSnapshot { + /** The jobs the view shows (filtered, with older pages). */ jobs: readonly JobResponse[]; + /** + * The jobs the status bar, finish notices and polling follow, whatever + * the filter: the newest page of all jobs plus moving jobs re-read + * because newer ones pushed them off that page. + */ + tracking: readonly JobResponse[]; /** A problem to show instead of jobs, or null. */ problem: { kind: 'auth' | 'config' | 'network'; message: string } | null; configured: boolean; @@ -74,6 +82,7 @@ export class ProofJobsProvider implements vscode.TreeDataProvider, readonly onDidLoad = this.loaded.event; private jobs: JobResponse[] = []; + private tracked: JobResponse[] = []; private hasMore = false; private problem: JobsSnapshot['problem'] = null; private configured = false; @@ -87,6 +96,7 @@ export class ProofJobsProvider implements vscode.TreeDataProvider, /** Bumped on a server or account change; replies from older generations are dropped. */ private generation = 0; private groups = new Map(); + private disposed = false; constructor( private readonly secrets: vscode.SecretStorage, @@ -99,7 +109,7 @@ export class ProofJobsProvider implements vscode.TreeDataProvider, } get snapshot(): JobsSnapshot { - return { jobs: this.jobs, problem: this.problem, configured: this.configured, serverUrl: this.serverUrl }; + return { jobs: this.jobs, tracking: this.tracked, problem: this.problem, configured: this.configured, serverUrl: this.serverUrl }; } /** Show only `status` (undefined = all); a load in flight finishes first. */ @@ -118,6 +128,9 @@ export class ProofJobsProvider implements vscode.TreeDataProvider, /** Reload the first page; concurrent calls share one load. */ refresh(): Promise { + if (this.disposed) { + return Promise.resolve(); + } return this.loading ?? this.track(this.load(false)); } @@ -135,6 +148,7 @@ export class ProofJobsProvider implements vscode.TreeDataProvider, reset(): void { this.generation++; this.jobs = []; + this.tracked = []; this.hasMore = false; this.problem = null; this.loading = null; @@ -168,8 +182,11 @@ export class ProofJobsProvider implements vscode.TreeDataProvider, clearTimeout(this.timer); this.timer = undefined; } + if (this.disposed) { + return; + } const delay = pollDelay({ - active: this.jobs.some(isActiveJob), + active: this.tracked.some(isActiveJob), visible: this.visible, msSinceSubmit: this.lastSubmit === null ? null : Date.now() - this.lastSubmit, errors: this.errors, @@ -245,10 +262,21 @@ export class ProofJobsProvider implements vscode.TreeDataProvider, const api = new ProverApi(config.serverUrl, config.apiKey); const before = more ? this.jobs[this.jobs.length - 1]?.createdAt ?? undefined : undefined; const page = await api.listJobs({ status: this.filter, limit: PAGE_SIZE, before }); + let tracked = this.tracked; + if (!more) { + const newest = this.filter ? await api.listJobs({ limit: PAGE_SIZE }) : page; + const stale = staleActiveJobs([...this.tracked, ...this.jobs], newest); + const reread = await Promise.all(stale.map((j) => api.getJob(j.id).catch(() => null))); + tracked = [...newest, ...reread.filter((j): j is JobResponse => j !== null)]; + } if (generation !== this.generation) { return; // a reply from the previous server or account } - this.jobs = more ? [...this.jobs, ...page] : mergeFirstPage(page, this.jobs, PAGE_SIZE); + this.tracked = tracked; + const latest = new Map(tracked.map((j) => [j.id, j])); + this.jobs = (more ? [...this.jobs, ...page] : mergeFirstPage(page, this.jobs, PAGE_SIZE)) + .map((j) => latest.get(j.id) ?? j) + .filter((j) => !this.filter || j.status === this.filter); if (more || page.length < PAGE_SIZE || this.jobs.length === page.length) { // A full page may have older jobs behind it. A refresh that kept // older loaded pages keeps the answer from the last "Load more". @@ -375,8 +403,10 @@ export class ProofJobsProvider implements vscode.TreeDataProvider, } dispose(): void { + this.disposed = true; if (this.timer) { clearTimeout(this.timer); + this.timer = undefined; } this.changed.dispose(); this.loaded.dispose(); diff --git a/editors/vscode/src/prover/proverStatusBar.ts b/editors/vscode/src/prover/proverStatusBar.ts index 3086d0a5..28c6ef71 100644 --- a/editors/vscode/src/prover/proverStatusBar.ts +++ b/editors/vscode/src/prover/proverStatusBar.ts @@ -1,6 +1,6 @@ import * as vscode from 'vscode'; -import { finishedJobs, isActiveJob } from './jobList'; +import { finishedJobs, isActiveJob, newestJob, nextStatuses } from './jobList'; import { listVerdict } from './jobVerdict'; import { VERDICT_CODICONS, type JobsSnapshot } from './jobsTree'; import { proverStatusState } from './proverStatusBarState'; @@ -40,30 +40,45 @@ export class ProverStatus implements vscode.Disposable { /** A job was just submitted here: watch it and stop showing the last result. */ watch(job: JobResponse): void { this.watched.add(job.id); + // Its submitted status, so a finish before the next load is noticed. + if (!this.previous.has(job.id)) { + this.previous.set(job.id, job.status); + } this.lastFinished = null; if (this.snapshot) { this.update(this.snapshot); } } + /** The server or account changed: forget its jobs and last result. */ + reset(): void { + this.previous = new Map(); + this.watched.clear(); + this.lastFinished = null; + this.target = null; + this.snapshot = null; + this.item.hide(); + } + update(snapshot: JobsSnapshot): void { this.snapshot = snapshot; - for (const job of snapshot.jobs) { + const jobs = snapshot.tracking; + for (const job of jobs) { if (isActiveJob(job)) { this.watched.add(job.id); } } - const finished = finishedJobs(this.previous, snapshot.jobs, this.watched); - this.previous = new Map(snapshot.jobs.map((j) => [j.id, j.status])); + const finished = finishedJobs(this.previous, jobs, this.watched); + this.previous = nextStatuses(this.previous, jobs, this.watched); for (const job of finished) { this.watched.delete(job.id); - this.lastFinished = job; if (!this.hooks.isPanelActive(job.id)) { void this.notify(job); } } + this.lastFinished = newestJob(finished) ?? this.lastFinished; const state = proverStatusState({ - jobs: snapshot.configured ? snapshot.jobs : [], + jobs: snapshot.configured ? jobs : [], problem: snapshot.problem, lastFinished: this.lastFinished, nameOf: (job) => this.hooks.nameOf(job), @@ -90,7 +105,9 @@ export class ProverStatus implements vscode.Disposable { : ''; const message = `Inference: ${name} — ${verdict.headline}${counts}.`; const good = verdict.claim !== 'none'; - const retry = ['failed', 'timed-out', 'provision-failed', 'lost'].includes(verdict.kind); + // A returned proof that did not compile may succeed on another run; a + // submitted file that did not compile fails again until it is changed. + const retry = ['failed', 'timed-out', 'provision-failed', 'lost', 'completed-compile-error'].includes(verdict.kind); const actions = retry ? ['Open', 'Run Again'] : ['Open']; const choice = good && verdict.tone === 'ok' ? await vscode.window.showInformationMessage(message, ...actions) @@ -103,7 +120,7 @@ export class ProverStatus implements vscode.Disposable { } private async onClick(): Promise { - const job = this.target ? this.snapshot?.jobs.find((j) => j.id === this.target) : undefined; + const job = this.target ? this.snapshot?.tracking.find((j) => j.id === this.target) : undefined; if (job) { if (!isActiveJob(job)) { this.lastFinished = null; // seen diff --git a/editors/vscode/src/test/prover-job-list.test.ts b/editors/vscode/src/test/prover-job-list.test.ts index 1aba6998..c7830a3d 100644 --- a/editors/vscode/src/test/prover-job-list.test.ts +++ b/editors/vscode/src/test/prover-job-list.test.ts @@ -5,6 +5,10 @@ import { describeJob, FILTER_STATUSES, finishedJobs, + MAX_STALE_REFRESH, + newestJob, + nextStatuses, + staleActiveJobs, hasCertificate, isActiveJob, jobContextValue, @@ -90,6 +94,12 @@ describe('pollDelay', () => { assert.strictEqual(pollDelay({ ...base, visible: false }), null); }); + it('keeps polling right after a submit even before the list shows the job', () => { + assert.strictEqual(pollDelay({ ...base, visible: false, msSinceSubmit: 1_000 }), 5_000); + assert.strictEqual(pollDelay({ ...base, visible: false, msSinceSubmit: 1_000, errors: 1 }), 10_000); + assert.strictEqual(pollDelay({ ...base, visible: false, msSinceSubmit: 200_000 }), null); + }); + it('backs off on errors, capped at five minutes', () => { assert.strictEqual(pollDelay({ ...base, errors: 1 }), 10_000); assert.strictEqual(pollDelay({ ...base, errors: 3 }), 40_000); @@ -118,3 +128,50 @@ describe('finishedJobs', () => { assert.ok(!hasCertificate({ status: 'Failed' })); }); }); + +describe('staleActiveJobs', () => { + it('re-reads moving jobs that fell off the first page, newest first, once each', () => { + const known: JobResponse[] = [ + { id: 'a', status: 'Running' }, + { id: 'b', status: 'Succeeded' }, + { id: 'c', status: 'Lost' }, + { id: 'a', status: 'Running' }, + { id: 'd', status: 'Queued' }, + ]; + const firstPage: JobResponse[] = [{ id: 'd', status: 'Running' }]; + assert.deepStrictEqual(staleActiveJobs(known, firstPage).map((j) => j.id), ['a', 'c']); + }); + + it('is bounded', () => { + const known = Array.from({ length: 30 }, (_, i): JobResponse => ({ id: `j${i}`, status: 'Running' })); + assert.strictEqual(staleActiveJobs(known, []).length, MAX_STALE_REFRESH); + }); +}); + +describe('nextStatuses', () => { + it('keeps the last status of watched jobs a load did not include', () => { + const previous = new Map([['new', 'Accepted'], ['gone', 'Running']] as const); + const next = nextStatuses(previous, [{ id: 'x', status: 'Running' }], new Set(['new'])); + assert.deepStrictEqual([...next.entries()], [['x', 'Running'], ['new', 'Accepted']]); + }); + + it('lets a quick job that finished before the first load be reported', () => { + const watched = new Set(['q']); + // Submitted as Accepted; the next load already shows it finished. + const previous = nextStatuses(new Map([['q', 'Accepted']] as const), [], watched); + const done: JobResponse[] = [{ id: 'q', status: 'Succeeded' }]; + assert.deepStrictEqual(finishedJobs(previous, done, watched).map((j) => j.id), ['q']); + }); +}); + +describe('newestJob', () => { + it('picks the latest submission', () => { + const jobs: JobResponse[] = [ + { id: 'b', status: 'Failed', createdAt: '2026-10-10T02:00:00Z' }, + { id: 'a', status: 'Failed', createdAt: '2026-10-10T01:00:00Z' }, + { id: 'c', status: 'Failed', createdAt: '2026-10-10T03:00:00Z' }, + ]; + assert.strictEqual(newestJob(jobs)?.id, 'c'); + assert.strictEqual(newestJob([]), null); + }); +}); From 7ceb0c9f014aa814511eb654507a00b762d158ab Mon Sep 17 00:00:00 2001 From: 0xGeorgii Date: Sat, 10 Oct 2026 20:53:03 +0900 Subject: [PATCH 3/4] vscode: status bar opens the saved result; stale notices do nothing - A click opens the last finished job even after newer jobs push it out of the loaded page (clickedJob falls back to the saved result). - A finish notice answered after the server or account changed is ignored, so Open and Run Again never act on the old job against the new server. Co-Authored-By: Claude Opus 5.5 --- editors/vscode/src/prover/proverStatusBar.ts | 11 +++++++++-- .../vscode/src/prover/proverStatusBarState.ts | 16 ++++++++++++++++ .../vscode/src/test/prover-status-bar.test.ts | 12 +++++++++++- 3 files changed, 36 insertions(+), 3 deletions(-) diff --git a/editors/vscode/src/prover/proverStatusBar.ts b/editors/vscode/src/prover/proverStatusBar.ts index 28c6ef71..867cf345 100644 --- a/editors/vscode/src/prover/proverStatusBar.ts +++ b/editors/vscode/src/prover/proverStatusBar.ts @@ -3,7 +3,7 @@ import * as vscode from 'vscode'; import { finishedJobs, isActiveJob, newestJob, nextStatuses } from './jobList'; import { listVerdict } from './jobVerdict'; import { VERDICT_CODICONS, type JobsSnapshot } from './jobsTree'; -import { proverStatusState } from './proverStatusBarState'; +import { clickedJob, proverStatusState } from './proverStatusBarState'; import type { JobResponse, JobStatus } from './types'; /** Internal command behind the status bar item. */ @@ -30,6 +30,8 @@ export class ProverStatus implements vscode.Disposable { private lastFinished: JobResponse | null = null; private target: string | null = null; private snapshot: JobsSnapshot | null = null; + /** Counts resets, so a notice answered after one does not act on the new server. */ + private generation = 0; constructor(private readonly hooks: ProverStatusHooks) { this.item.name = 'Inference Proof Jobs'; @@ -52,6 +54,7 @@ export class ProverStatus implements vscode.Disposable { /** The server or account changed: forget its jobs and last result. */ reset(): void { + this.generation++; this.previous = new Map(); this.watched.clear(); this.lastFinished = null; @@ -109,9 +112,13 @@ export class ProverStatus implements vscode.Disposable { // submitted file that did not compile fails again until it is changed. const retry = ['failed', 'timed-out', 'provision-failed', 'lost', 'completed-compile-error'].includes(verdict.kind); const actions = retry ? ['Open', 'Run Again'] : ['Open']; + const generation = this.generation; const choice = good && verdict.tone === 'ok' ? await vscode.window.showInformationMessage(message, ...actions) : await vscode.window.showWarningMessage(message, ...actions); + if (generation !== this.generation) { + return; // the job belongs to the server or account used before + } if (choice === 'Open') { await this.hooks.openJob(job); } else if (choice === 'Run Again') { @@ -120,7 +127,7 @@ export class ProverStatus implements vscode.Disposable { } private async onClick(): Promise { - const job = this.target ? this.snapshot?.tracking.find((j) => j.id === this.target) : undefined; + const job = clickedJob(this.target, this.snapshot?.tracking ?? [], this.lastFinished); if (job) { if (!isActiveJob(job)) { this.lastFinished = null; // seen diff --git a/editors/vscode/src/prover/proverStatusBarState.ts b/editors/vscode/src/prover/proverStatusBarState.ts index d84e1f18..fc004ad6 100644 --- a/editors/vscode/src/prover/proverStatusBarState.ts +++ b/editors/vscode/src/prover/proverStatusBarState.ts @@ -78,3 +78,19 @@ export function proverStatusState(input: ProverStatusInput): ProverStatusState { } return { visible: false, icon: 'server', text: '', tooltip: '', jobId: null }; } + +/** + * The job a click opens: its copy in the latest load, else the saved result + * the item shows (a finished job drops out of the load once newer jobs push + * it off the first page). + */ +export function clickedJob( + jobId: string | null, + jobs: readonly JobResponse[], + lastFinished: JobResponse | null, +): JobResponse | undefined { + if (!jobId) { + return undefined; + } + return jobs.find((j) => j.id === jobId) ?? (lastFinished?.id === jobId ? lastFinished : undefined); +} diff --git a/editors/vscode/src/test/prover-status-bar.test.ts b/editors/vscode/src/test/prover-status-bar.test.ts index 0e10cd57..1db377ce 100644 --- a/editors/vscode/src/test/prover-status-bar.test.ts +++ b/editors/vscode/src/test/prover-status-bar.test.ts @@ -1,7 +1,7 @@ import * as assert from 'node:assert'; import { describe, it } from 'node:test'; -import { proverStatusState } from '../prover/proverStatusBarState'; +import { clickedJob, proverStatusState } from '../prover/proverStatusBarState'; import type { DoctorResult } from '../toolchain/doctor'; import type { JobResponse } from '../prover/types'; import { determineStatusBarState, failingChecks, toolchainHealth } from '../ui/statusBarState'; @@ -37,6 +37,16 @@ describe('proverStatusState', () => { const problem = proverStatusState({ jobs: [], problem: { kind: 'network', message: 'offline' }, lastFinished: done, nameOf }); assert.deepStrictEqual([problem.icon, problem.text], ['server', 'Proof server']); }); + + it('opens the saved result on click after newer jobs push it out of the load', () => { + const done: JobResponse = { id: 'a', status: 'Succeeded', filename: 'b.v' }; + const fresh: JobResponse = { ...done, holesTotal: 1 }; + const state = proverStatusState({ jobs: [], problem: null, lastFinished: done, nameOf }); + assert.strictEqual(clickedJob(state.jobId, [], done), done); + assert.strictEqual(clickedJob('a', [fresh], done), fresh, 'the loaded copy is newer'); + assert.strictEqual(clickedJob('c', [fresh], done), undefined); + assert.strictEqual(clickedJob(null, [fresh], done), undefined); + }); }); describe('toolchainHealth', () => { From f79a65c7e585d6f227541a445fb9ba829f349ddf Mon Sep 17 00:00:00 2001 From: 0xGeorgii Date: Sat, 10 Oct 2026 21:51:58 +0900 Subject: [PATCH 4/4] vscode: keep tracking a running job when its re-read fails; no Run Again for Lost - A moving job that newer jobs pushed off the first page is re-read on each load. A failed read used to drop it from tracking for good, so its progress and finish notice were lost (and polling could stop). It now keeps the last known copy and tries again on the next load; only a job the server deleted (404) is dropped (rereadJob, tested). - The job panel no longer offers Run Again for a Lost job, matching the Proof Jobs menu: the server runs it again by itself, and a second job would prove the same file twice. The Lost wording now says so. Co-Authored-By: Claude Opus 5.5 --- editors/vscode/src/prover/jobDetailModel.ts | 3 ++- editors/vscode/src/prover/jobList.ts | 17 +++++++++++++++++ editors/vscode/src/prover/jobVerdict.ts | 2 +- editors/vscode/src/prover/jobsTree.ts | 3 ++- editors/vscode/src/prover/proverStatusBar.ts | 2 +- .../src/test/prover-job-detail-html.test.ts | 7 +++++++ editors/vscode/src/test/prover-job-list.test.ts | 13 +++++++++++++ 7 files changed, 43 insertions(+), 4 deletions(-) diff --git a/editors/vscode/src/prover/jobDetailModel.ts b/editors/vscode/src/prover/jobDetailModel.ts index 7acbf5ba..f7f9ee8f 100644 --- a/editors/vscode/src/prover/jobDetailModel.ts +++ b/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; diff --git a/editors/vscode/src/prover/jobList.ts b/editors/vscode/src/prover/jobList.ts index 465900ab..451770aa 100644 --- a/editors/vscode/src/prover/jobList.ts +++ b/editors/vscode/src/prover/jobList.ts @@ -3,6 +3,7 @@ * under plain node. */ +import { ApiError } from './api'; import { isCancelableStatus, isTerminalStatus } from './jobStatus'; import { listVerdict } from './jobVerdict'; import type { JobResponse, JobStatus } from './types'; @@ -173,6 +174,22 @@ export function staleActiveJobs(known: readonly JobResponse[], firstPage: readon .slice(0, MAX_STALE_REFRESH); } +/** + * A stale job after its re-read: the server's copy, or the last known one when + * the read fails, so it stays tracked and the next load tries again. Only a + * job the server no longer has (deleted) is dropped. + */ +export async function rereadJob( + job: JobResponse, + read: (id: string) => Promise, +): Promise { + try { + return await read(job.id); + } catch (err) { + return err instanceof ApiError && err.status === 404 ? null : job; + } +} + /** * The statuses to compare the next load against: the loaded ones, plus the * last known status of watched jobs the load did not include (a list request diff --git a/editors/vscode/src/prover/jobVerdict.ts b/editors/vscode/src/prover/jobVerdict.ts index 96053145..30858b98 100644 --- a/editors/vscode/src/prover/jobVerdict.ts +++ b/editors/vscode/src/prover/jobVerdict.ts @@ -235,7 +235,7 @@ function terminalFailure(job: JobResponse, input: VerdictInput): Verdict { job.errorReason ? [job.errorReason] : []); case 'Lost': return verdict('lost', 'warn', 'warning', 'Worker lost', 'Worker lost', - 'The worker stopped responding. The server retries lost jobs automatically; if this one stays lost, run it again.'); + 'The worker stopped responding. The server runs the job again by itself; a job that loses its worker three times fails.'); case 'Canceled': return verdict('canceled', 'muted', 'canceled', 'Canceled', 'Canceled', 'The run was canceled before it finished.'); diff --git a/editors/vscode/src/prover/jobsTree.ts b/editors/vscode/src/prover/jobsTree.ts index 875a6ccd..afcefce6 100644 --- a/editors/vscode/src/prover/jobsTree.ts +++ b/editors/vscode/src/prover/jobsTree.ts @@ -11,6 +11,7 @@ import { mergeFirstPage, PAGE_SIZE, pollDelay, + rereadJob, staleActiveJobs, } from './jobList'; import { listVerdict, type Verdict, type VerdictIcon } from './jobVerdict'; @@ -266,7 +267,7 @@ export class ProofJobsProvider implements vscode.TreeDataProvider, if (!more) { const newest = this.filter ? await api.listJobs({ limit: PAGE_SIZE }) : page; const stale = staleActiveJobs([...this.tracked, ...this.jobs], newest); - const reread = await Promise.all(stale.map((j) => api.getJob(j.id).catch(() => null))); + const reread = await Promise.all(stale.map((j) => rereadJob(j, (id) => api.getJob(id)))); tracked = [...newest, ...reread.filter((j): j is JobResponse => j !== null)]; } if (generation !== this.generation) { diff --git a/editors/vscode/src/prover/proverStatusBar.ts b/editors/vscode/src/prover/proverStatusBar.ts index 867cf345..7cc98cc8 100644 --- a/editors/vscode/src/prover/proverStatusBar.ts +++ b/editors/vscode/src/prover/proverStatusBar.ts @@ -110,7 +110,7 @@ export class ProverStatus implements vscode.Disposable { const good = verdict.claim !== 'none'; // A returned proof that did not compile may succeed on another run; a // submitted file that did not compile fails again until it is changed. - const retry = ['failed', 'timed-out', 'provision-failed', 'lost', 'completed-compile-error'].includes(verdict.kind); + const retry = ['failed', 'timed-out', 'provision-failed', 'completed-compile-error'].includes(verdict.kind); const actions = retry ? ['Open', 'Run Again'] : ['Open']; const generation = this.generation; const choice = good && verdict.tone === 'ok' diff --git a/editors/vscode/src/test/prover-job-detail-html.test.ts b/editors/vscode/src/test/prover-job-detail-html.test.ts index 96ab1391..edbebb8e 100644 --- a/editors/vscode/src/test/prover-job-detail-html.test.ts +++ b/editors/vscode/src/test/prover-job-detail-html.test.ts @@ -507,6 +507,13 @@ describe('renderJobDetailHtml', () => { assert.ok(html.includes('fixture-stdlib.v')); }); + it('offers no Run Again for a Lost job (the server runs it again by itself)', () => { + const html = renderJobDetailHtml({ ...JOB, status: 'Lost' }, BASE_OPTS); + assert.strictEqual(verdictOf(html).kind, 'lost'); + assert.ok(!html.includes('data-action="resubmit"')); + assert.ok(html.includes('runs the job again by itself')); + }); + it('explains a failed job in words and keeps the raw code under Technical details', () => { const failed: JobResponse = { ...JOB, diff --git a/editors/vscode/src/test/prover-job-list.test.ts b/editors/vscode/src/test/prover-job-list.test.ts index c7830a3d..8f8735de 100644 --- a/editors/vscode/src/test/prover-job-list.test.ts +++ b/editors/vscode/src/test/prover-job-list.test.ts @@ -15,7 +15,9 @@ import { mergeFirstPage, pollDelay, relativeTime, + rereadJob, } from '../prover/jobList'; +import { ApiError } from '../prover/api'; import type { JobResponse, JobStatus } from '../prover/types'; const job = (id: string, createdAt: string, status: JobStatus = 'Succeeded'): JobResponse => ({ @@ -120,6 +122,17 @@ describe('finishedJobs', () => { assert.deepStrictEqual(finishedJobs(previous, next, new Set(['b'])).map((j) => j.id), []); }); + it('keeps a stale job whose re-read fails, and drops one the server deleted', async () => { + const running: JobResponse = { id: 'a', status: 'Running', holesClosed: 1 }; + const fresh: JobResponse = { id: 'a', status: 'Succeeded', holesClosed: 2 }; + assert.strictEqual(await rereadJob(running, async () => fresh), fresh); + assert.strictEqual(await rereadJob(running, async () => { throw new Error('socket hang up'); }), running); + assert.strictEqual(await rereadJob(running, async () => { throw new ApiError(503, 'unavailable'); }), running); + assert.strictEqual(await rereadJob(running, async () => { throw new ApiError(404, 'not found'); }), null); + // Kept as active, so the next load re-reads it again. + assert.deepStrictEqual(staleActiveJobs([running], []), [running]); + }); + it('treats Lost as still moving (the server re-queues it)', () => { const previous = new Map([['a', 'Running']] as const); assert.deepStrictEqual(finishedJobs(previous, [{ id: 'a', status: 'Lost' }], new Set(['a'])), []);