From 7c86548486b8f97a0767c7bd343185b39e3fe8dc Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Fri, 25 Oct 2024 18:04:18 +0200 Subject: [PATCH] feat: better progress ux (#542) This PR improves two things about the way we report progress: - Instead of attempting to badly approximate an accurate progress bar that gets stuck whenever the output of a command doesn't change, we now use VS Code's "infinite" progress bars everywhere that clearly show that an operation is actively running in the background. - Every progress bar is prefixed with a context to make it clear which operation caused the operation. For example, when creating a new mathlib project, all external commands executed while creating the project are prefixed with "[Create Mathlib Project]". Closes #457. IMO, our dialog UX still isn't perfect, but there doesn't seem to be a good way to improve these things short of implementing our own webviews for every command. --- .../src/diagnostics/fullDiagnostics.ts | 3 +- .../src/diagnostics/setupDiagnoser.ts | 29 ++++---- .../src/diagnostics/setupDiagnostics.ts | 9 ++- vscode-lean4/src/extension.ts | 9 ++- vscode-lean4/src/projectinit.ts | 70 +++++++++++++++---- vscode-lean4/src/projectoperations.ts | 14 ++-- vscode-lean4/src/utils/batch.ts | 14 ++-- vscode-lean4/src/utils/clientProvider.ts | 17 +++-- vscode-lean4/src/utils/elan.ts | 2 +- vscode-lean4/src/utils/lake.ts | 20 ++++-- 10 files changed, 132 insertions(+), 55 deletions(-) diff --git a/vscode-lean4/src/diagnostics/fullDiagnostics.ts b/vscode-lean4/src/diagnostics/fullDiagnostics.ts index 0c34c1b08..26ce982be 100644 --- a/vscode-lean4/src/diagnostics/fullDiagnostics.ts +++ b/vscode-lean4/src/diagnostics/fullDiagnostics.ts @@ -116,6 +116,7 @@ export async function performFullDiagnosis( channel: OutputChannel, cwdUri: FileUri | undefined, ): Promise { + const showSetupInformationContext = 'Show Setup Information' const diagnose = new SetupDiagnoser(channel, cwdUri) return { systemInfo: diagnose.querySystemInformation(), @@ -124,7 +125,7 @@ export async function performFullDiagnosis( isCurlAvailable: await diagnose.checkCurlAvailable(), isGitAvailable: await diagnose.checkGitAvailable(), elanVersionDiagnosis: await diagnose.elanVersion(), - leanVersionDiagnosis: await diagnose.leanVersion(), + leanVersionDiagnosis: await diagnose.leanVersion(showSetupInformationContext), projectSetupDiagnosis: await diagnose.projectSetup(), elanShowOutput: await diagnose.queryElanShow(), } diff --git a/vscode-lean4/src/diagnostics/setupDiagnoser.ts b/vscode-lean4/src/diagnostics/setupDiagnoser.ts index 7e03ad3c6..a2dd9a012 100644 --- a/vscode-lean4/src/diagnostics/setupDiagnoser.ts +++ b/vscode-lean4/src/diagnostics/setupDiagnoser.ts @@ -140,13 +140,13 @@ export class SetupDiagnoser { return gitVersionResult.exitCode === ExecutionExitCode.Success } - async queryLakeVersion(): Promise { - const lakeVersionResult = await this.runLeanCommand('lake', ['--version'], 'Checking Lake version') + async queryLakeVersion(context: string): Promise { + const lakeVersionResult = await this.runLeanCommand('lake', ['--version'], context, 'Checking Lake version') return versionQueryResult(lakeVersionResult, /version (\d+\.\d+\.\d+(\w|-)*)/) } - async checkLakeAvailable(): Promise { - const lakeVersionResult = await this.queryLakeVersion() + async checkLakeAvailable(context: string): Promise { + const lakeVersionResult = await this.queryLakeVersion(context) return lakeVersionResult.kind === 'Success' } @@ -191,8 +191,8 @@ export class SetupDiagnoser { return { kind: 'UpToDate', version: currentVSCodeVersion } } - async queryLeanVersion(): Promise { - const leanVersionResult = await this.runLeanCommand('lean', ['--version'], 'Checking Lean version') + async queryLeanVersion(context: string): Promise { + const leanVersionResult = await this.runLeanCommand('lean', ['--version'], context, 'Checking Lean version') return versionQueryResult(leanVersionResult, /version (\d+\.\d+\.\d+(\w|-)*)/) } @@ -223,8 +223,8 @@ export class SetupDiagnoser { return { kind: 'ValidProjectSetup', projectFolder: this.cwdUri } } - async leanVersion(): Promise { - const leanVersionResult = await this.queryLeanVersion() + async leanVersion(context: string): Promise { + const leanVersionResult = await this.queryLeanVersion(context) return checkLeanVersion(leanVersionResult) } @@ -232,19 +232,24 @@ export class SetupDiagnoser { return batchExecute(executablePath, args, this.cwdUri?.fsPath, { combined: this.channel }) } - private async runWithProgress(executablePath: string, args: string[], title: string): Promise { - return batchExecuteWithProgress(executablePath, args, title, { + private async runWithProgress( + executablePath: string, + args: string[], + context: string, + title: string, + ): Promise { + return batchExecuteWithProgress(executablePath, args, context, title, { cwd: this.cwdUri?.fsPath, channel: this.channel, }) } - private async runLeanCommand(executablePath: string, args: string[], title: string) { + private async runLeanCommand(executablePath: string, args: string[], context: string, title: string) { const leanArgs = [...args] if (this.toolchain !== undefined) { leanArgs.unshift(`+${this.toolchain}`) } - return await this.runWithProgress(executablePath, leanArgs, title) + return await this.runWithProgress(executablePath, leanArgs, context, title) } } diff --git a/vscode-lean4/src/diagnostics/setupDiagnostics.ts b/vscode-lean4/src/diagnostics/setupDiagnostics.ts index 37f4cee92..7aa8cacad 100644 --- a/vscode-lean4/src/diagnostics/setupDiagnostics.ts +++ b/vscode-lean4/src/diagnostics/setupDiagnostics.ts @@ -72,9 +72,10 @@ export async function checkAreDependenciesInstalled( export async function checkIsLean4Installed( installer: LeanInstaller, + context: string, cwdUri: FileUri | undefined, ): Promise { - const leanVersionResult = await diagnose(installer.getOutputChannel(), cwdUri).queryLeanVersion() + const leanVersionResult = await diagnose(installer.getOutputChannel(), cwdUri).queryLeanVersion(context) switch (leanVersionResult.kind) { case 'Success': return 'Fulfilled' @@ -155,6 +156,7 @@ export async function checkIsValidProjectFolder( export async function checkIsLeanVersionUpToDate( channel: OutputChannel, + context: string, folderUri: ExtUri, options: { toolchainOverride?: string | undefined; modal: boolean }, ): Promise { @@ -170,7 +172,7 @@ export async function checkIsLeanVersionUpToDate( channel, extUriToCwdUri(folderUri), options.toolchainOverride, - ).leanVersion() + ).leanVersion(context) switch (projectLeanVersionDiagnosis.kind) { case 'NotInstalled': return displaySetupErrorWithOutput("Error while checking Lean version: 'lean' command was not found.") @@ -198,6 +200,7 @@ export async function checkIsLeanVersionUpToDate( export async function checkIsLakeInstalledCorrectly( channel: OutputChannel, + context: string, folderUri: ExtUri, options: { toolchainOverride?: string | undefined }, ): Promise { @@ -205,7 +208,7 @@ export async function checkIsLakeInstalledCorrectly( channel, extUriToCwdUri(folderUri), options.toolchainOverride, - ).queryLakeVersion() + ).queryLakeVersion(context) switch (lakeVersionResult.kind) { case 'CommandNotFound': return displaySetupErrorWithOutput("Error while checking Lake version: 'lake' command was not found.") diff --git a/vscode-lean4/src/extension.ts b/vscode-lean4/src/extension.ts index 1ae235e39..82283377b 100644 --- a/vscode-lean4/src/extension.ts +++ b/vscode-lean4/src/extension.ts @@ -150,11 +150,12 @@ function activateAlwaysEnabledFeatures(context: ExtensionContext): AlwaysEnabled async function checkLean4FeaturePreconditions( installer: LeanInstaller, + context: string, cwdUri: FileUri | undefined, ): Promise { return await checkAll( () => checkAreDependenciesInstalled(installer.getOutputChannel(), cwdUri), - () => checkIsLean4Installed(installer, cwdUri), + () => checkIsLean4Installed(installer, context, cwdUri), () => checkIsElanUpToDate(installer, cwdUri, { elanMustBeInstalled: false, @@ -169,7 +170,11 @@ async function activateLean4Features( installer: LeanInstaller, projectUri: FileUri | undefined, ): Promise { - const preconditionCheckResult = await checkLean4FeaturePreconditions(installer, projectUri) + const preconditionCheckResult = await checkLean4FeaturePreconditions( + installer, + 'Activate Lean 4 Extension', + projectUri, + ) if (preconditionCheckResult === 'Fatal') { return undefined } diff --git a/vscode-lean4/src/projectinit.ts b/vscode-lean4/src/projectinit.ts index 1edc38ff8..feefad36c 100644 --- a/vscode-lean4/src/projectinit.ts +++ b/vscode-lean4/src/projectinit.ts @@ -23,6 +23,7 @@ import path = require('path') async function checkCreateLean4ProjectPreconditions( installer: LeanInstaller, + context: string, folderUri: ExtUri, projectToolchain: string, ): Promise { @@ -31,8 +32,12 @@ async function checkCreateLean4ProjectPreconditions( return await checkAll( () => checkAreDependenciesInstalled(channel, cwdUri), () => checkIsElanUpToDate(installer, cwdUri, { elanMustBeInstalled: true, modal: true }), - () => checkIsLeanVersionUpToDate(channel, folderUri, { toolchainOverride: projectToolchain, modal: true }), - () => checkIsLakeInstalledCorrectly(channel, folderUri, { toolchainOverride: projectToolchain }), + () => + checkIsLeanVersionUpToDate(channel, context, folderUri, { + toolchainOverride: projectToolchain, + modal: true, + }), + () => checkIsLakeInstalledCorrectly(channel, context, folderUri, { toolchainOverride: projectToolchain }), ) } @@ -40,13 +45,13 @@ async function checkPreCloneLean4ProjectPreconditions(channel: OutputChannel, cw return await checkAll(() => checkAreDependenciesInstalled(channel, cwdUri)) } -async function checkPostCloneLean4ProjectPreconditions(installer: LeanInstaller, folderUri: ExtUri) { +async function checkPostCloneLean4ProjectPreconditions(installer: LeanInstaller, context: string, folderUri: ExtUri) { const channel = installer.getOutputChannel() const cwdUri = extUriToCwdUri(folderUri) return await checkAll( () => checkIsElanUpToDate(installer, cwdUri, { elanMustBeInstalled: false, modal: true }), - () => checkIsLeanVersionUpToDate(channel, folderUri, { modal: true }), - () => checkIsLakeInstalledCorrectly(channel, folderUri, {}), + () => checkIsLeanVersionUpToDate(channel, context, folderUri, { modal: true }), + () => checkIsLakeInstalledCorrectly(channel, context, folderUri, {}), ) } @@ -66,13 +71,23 @@ export class ProjectInitializationProvider implements Disposable { } private async createStandaloneProject() { + const createStandaloneProjectContext = 'Create Standalone Project' const toolchain = 'leanprover/lean4:stable' - const projectFolder: FileUri | 'DidNotComplete' = await this.createProject(undefined, toolchain) + const projectFolder: FileUri | 'DidNotComplete' = await this.createProject( + createStandaloneProjectContext, + undefined, + toolchain, + ) if (projectFolder === 'DidNotComplete') { return } - const buildResult: ExecutionResult = await lake(this.channel, projectFolder, toolchain).build() + const buildResult: ExecutionResult = await lake( + this.channel, + projectFolder, + createStandaloneProjectContext, + toolchain, + ).build() if (buildResult.exitCode === ExecutionExitCode.Cancelled) { return } @@ -91,8 +106,13 @@ export class ProjectInitializationProvider implements Disposable { } private async createMathlibProject() { + const createMathlibProjectContext = 'Create Project Using Mathlib' const mathlibToolchain = 'leanprover-community/mathlib4:lean-toolchain' - const projectFolder: FileUri | 'DidNotComplete' = await this.createProject('math', mathlibToolchain) + const projectFolder: FileUri | 'DidNotComplete' = await this.createProject( + createMathlibProjectContext, + 'math', + mathlibToolchain, + ) if (projectFolder === 'DidNotComplete') { return } @@ -100,6 +120,7 @@ export class ProjectInitializationProvider implements Disposable { const cacheGetResult: ExecutionResult = await lake( this.channel, projectFolder, + createMathlibProjectContext, mathlibToolchain, ).fetchMathlibCache() if (cacheGetResult.exitCode === ExecutionExitCode.Cancelled) { @@ -110,7 +131,12 @@ export class ProjectInitializationProvider implements Disposable { return } - const buildResult: ExecutionResult = await lake(this.channel, projectFolder, mathlibToolchain).build() + const buildResult: ExecutionResult = await lake( + this.channel, + projectFolder, + createMathlibProjectContext, + mathlibToolchain, + ).build() if (buildResult.exitCode === ExecutionExitCode.Cancelled) { return } @@ -129,6 +155,7 @@ export class ProjectInitializationProvider implements Disposable { } private async createProject( + context: string, kind?: string | undefined, toolchain: string = 'leanprover/lean4:stable', ): Promise { @@ -144,6 +171,7 @@ export class ProjectInitializationProvider implements Disposable { const preconditionCheckResult = await checkCreateLean4ProjectPreconditions( this.installer, + context, projectFolder, toolchain, ) @@ -152,7 +180,7 @@ export class ProjectInitializationProvider implements Disposable { } const projectName: string = path.basename(projectFolder.fsPath) - const result: ExecutionResult = await lake(this.channel, projectFolder, toolchain).initProject( + const result: ExecutionResult = await lake(this.channel, projectFolder, context, toolchain).initProject( projectName, kind, ) @@ -161,7 +189,12 @@ export class ProjectInitializationProvider implements Disposable { return 'DidNotComplete' } - const updateResult: ExecutionResult = await lake(this.channel, projectFolder, toolchain).updateDependencies() + const updateResult: ExecutionResult = await lake( + this.channel, + projectFolder, + context, + toolchain, + ).updateDependencies() if (updateResult.exitCode === ExecutionExitCode.Cancelled) { return 'DidNotComplete' } @@ -253,6 +286,8 @@ Open this project instead?` } private async cloneProject() { + const downloadProjectContext = 'Download Project' + const quickPick = window.createQuickPick() quickPick.title = "Enter a Git repository URL or choose a preset project to download (Press 'Escape' to cancel)" quickPick.placeholder = 'URL of Git repository for existing Lean 4 project' @@ -323,6 +358,7 @@ Open this project instead?` const result: ExecutionResult = await batchExecuteWithProgress( 'git', ['clone', projectUri, projectFolder.fsPath], + downloadProjectContext, 'Cloning project', { channel: this.channel, allowCancellation: true }, ) @@ -334,13 +370,21 @@ Open this project instead?` return } - const postCloneCheckResult = await checkPostCloneLean4ProjectPreconditions(this.installer, projectFolder) + const postCloneCheckResult = await checkPostCloneLean4ProjectPreconditions( + this.installer, + downloadProjectContext, + projectFolder, + ) if (postCloneCheckResult === 'Fatal') { return } // Try it. If this is not a mathlib project, it will fail silently. Otherwise, it will grab the cache. - const fetchResult: ExecutionResult = await lake(this.channel, projectFolder).fetchMathlibCache(true) + const fetchResult: ExecutionResult = await lake( + this.channel, + projectFolder, + downloadProjectContext, + ).fetchMathlibCache(true) if (fetchResult.exitCode === ExecutionExitCode.Cancelled) { return } diff --git a/vscode-lean4/src/projectoperations.ts b/vscode-lean4/src/projectoperations.ts index 75ad7c157..7eb11201f 100644 --- a/vscode-lean4/src/projectoperations.ts +++ b/vscode-lean4/src/projectoperations.ts @@ -32,7 +32,7 @@ export class ProjectOperationProvider implements Disposable { } private async buildProject() { - await this.runOperation(async lakeRunner => { + await this.runOperation('Build Project', async lakeRunner => { const fetchResult: 'Success' | 'CacheNotAvailable' | 'Cancelled' = await this.tryFetchingCache(lakeRunner) if (fetchResult === 'Cancelled') { return @@ -62,7 +62,7 @@ export class ProjectOperationProvider implements Disposable { return } - await this.runOperation(async lakeRunner => { + await this.runOperation('Clean Project', async lakeRunner => { const cleanResult: ExecutionResult = await lakeRunner.clean() if (cleanResult.exitCode === ExecutionExitCode.Cancelled) { return @@ -101,7 +101,7 @@ export class ProjectOperationProvider implements Disposable { } private async fetchMathlibCache() { - await this.runOperation(async lakeRunner => { + await this.runOperation('Fetch Mathlib Build Cache', async lakeRunner => { const result: ExecutionResult = await lakeRunner.fetchMathlibCache() if (result.exitCode === ExecutionExitCode.Cancelled) { return @@ -120,7 +120,7 @@ export class ProjectOperationProvider implements Disposable { } private async fetchMathlibCacheForFocusedFile() { - await this.runOperation(async lakeRunner => { + await this.runOperation('Fetch Mathlib Build Cache For Focused File', async lakeRunner => { const projectUri = lakeRunner.cwdUri! if (!window.activeTextEditor || window.activeTextEditor.document.languageId !== 'lean4') { @@ -246,7 +246,7 @@ export class ProjectOperationProvider implements Disposable { return } - await this.runOperation(async lakeRunner => { + await this.runOperation('Update Dependency', async lakeRunner => { const result: ExecutionResult = await lakeRunner.updateDependency(dependencyChoice.name) if (result.exitCode === ExecutionExitCode.Cancelled) { return @@ -386,7 +386,7 @@ export class ProjectOperationProvider implements Disposable { } } - private async runOperation(command: (lakeRunner: LakeRunner) => Promise) { + private async runOperation(context: string, command: (lakeRunner: LakeRunner) => Promise) { if (this.isRunningOperation) { displayError('Another project action is already being executed. Please wait for its completion.') return @@ -412,7 +412,7 @@ export class ProjectOperationProvider implements Disposable { return } - const lakeRunner: LakeRunner = lake(this.channel, activeClient.folderUri) + const lakeRunner: LakeRunner = lake(this.channel, activeClient.folderUri, context) const result: 'Success' | 'IsRestarting' = await activeClient.withStoppedClient(() => command(lakeRunner)) if (result === 'IsRestarting') { diff --git a/vscode-lean4/src/utils/batch.ts b/vscode-lean4/src/utils/batch.ts index 15e2db3f9..499891d40 100644 --- a/vscode-lean4/src/utils/batch.ts +++ b/vscode-lean4/src/utils/batch.ts @@ -147,18 +147,19 @@ interface ProgressExecutionOptions { export async function batchExecuteWithProgress( executablePath: string, args: string[], + context: string | undefined, title: string, options: ProgressExecutionOptions = {}, ): Promise { - const titleSuffix = options.channel ? ' [(Details)](command:lean4.troubleshooting.showOutput)' : '' + const titlePrefix = context ? `[${context}] ` : '' + const titleSuffix = options.channel ? ' [(Click for details)](command:lean4.troubleshooting.showOutput)' : '' const progressOptions: ProgressOptions = { location: ProgressLocation.Notification, - title: title + titleSuffix, + title: titlePrefix + title + titleSuffix, cancellable: options.allowCancellation === true, } - let inc = 0 let lastReportedMessage: string | undefined let progress: | Progress<{ @@ -180,11 +181,8 @@ export async function batchExecuteWithProgress( if (options.channel) { options.channel.appendLine(value.trimEnd()) } - if (inc < 90) { - inc += 2 - } if (progress !== undefined) { - progress.report({ increment: inc, message: value }) + progress.report({ message: value }) } lastReportedMessage = value }, @@ -227,7 +225,7 @@ export async function batchExecuteWithProgress( const result: ExecutionResult = await window.withProgress(progressOptions, (p, token) => { progress = p token.onCancellationRequested(() => proc.kill()) - progress.report({ message: lastReportedMessage, increment: inc }) + progress.report({ message: lastReportedMessage }) return executionPromise }) return result diff --git a/vscode-lean4/src/utils/clientProvider.ts b/vscode-lean4/src/utils/clientProvider.ts index 24212b73f..c825bef23 100644 --- a/vscode-lean4/src/utils/clientProvider.ts +++ b/vscode-lean4/src/utils/clientProvider.ts @@ -16,16 +16,17 @@ import { findLeanProjectRoot, willUseLakeServer } from './projectInfo' async function checkLean4ProjectPreconditions( channel: OutputChannel, + context: string, folderUri: ExtUri, ): Promise { return await checkAll( () => checkIsValidProjectFolder(channel, folderUri), - () => checkIsLeanVersionUpToDate(channel, folderUri, { modal: false }), + () => checkIsLeanVersionUpToDate(channel, context, folderUri, { modal: false }), async () => { if (!(await willUseLakeServer(folderUri))) { return 'Fulfilled' } - return await checkIsLakeInstalledCorrectly(channel, folderUri, {}) + return await checkIsLakeInstalledCorrectly(channel, context, folderUri, {}) }, ) } @@ -122,7 +123,11 @@ export class LeanClientProvider implements Disposable { continue } - const preconditionCheckResult = await checkLean4ProjectPreconditions(this.outputChannel, projectUri) + const preconditionCheckResult = await checkLean4ProjectPreconditions( + this.outputChannel, + 'Restart Client', + projectUri, + ) if (preconditionCheckResult !== 'Fatal') { logger.log('[ClientProvider] got lean version 4') const [cached, client] = await this.ensureClient(uri) @@ -234,7 +239,11 @@ export class LeanClientProvider implements Disposable { } this.pending.set(key, true) - const preconditionCheckResult = await checkLean4ProjectPreconditions(this.outputChannel, folderUri) + const preconditionCheckResult = await checkLean4ProjectPreconditions( + this.outputChannel, + 'Start Client', + folderUri, + ) if (preconditionCheckResult === 'Fatal') { this.pending.delete(key) return [false, undefined] diff --git a/vscode-lean4/src/utils/elan.ts b/vscode-lean4/src/utils/elan.ts index 164e09868..4cedcb0dc 100644 --- a/vscode-lean4/src/utils/elan.ts +++ b/vscode-lean4/src/utils/elan.ts @@ -2,5 +2,5 @@ import { OutputChannel } from 'vscode' import { batchExecuteWithProgress, ExecutionResult } from './batch' export async function elanSelfUpdate(channel: OutputChannel): Promise { - return await batchExecuteWithProgress('elan', ['self', 'update'], 'Updating Elan', { channel }) + return await batchExecuteWithProgress('elan', ['self', 'update'], undefined, 'Updating Elan', { channel }) } diff --git a/vscode-lean4/src/utils/lake.ts b/vscode-lean4/src/utils/lake.ts index 88367bd75..3d103fe08 100644 --- a/vscode-lean4/src/utils/lake.ts +++ b/vscode-lean4/src/utils/lake.ts @@ -9,11 +9,18 @@ export const cacheNotFoundExitError = '=> Operation failed. Exit Code: 1.' export class LakeRunner { channel: OutputChannel cwdUri: FileUri | undefined + context: string | undefined toolchain: string | undefined - constructor(channel: OutputChannel, cwdUri: FileUri | undefined, toolchain?: string | undefined) { + constructor( + channel: OutputChannel, + cwdUri: FileUri | undefined, + context: string | undefined, + toolchain?: string | undefined, + ) { this.channel = channel this.cwdUri = cwdUri + this.context = context this.toolchain = toolchain } @@ -88,7 +95,7 @@ export class LakeRunner { if (this.toolchain) { args.unshift(`+${this.toolchain}`) } - return await batchExecuteWithProgress('lake', args, waitingPrompt, { + return await batchExecuteWithProgress('lake', args, this.context, waitingPrompt, { cwd: this.cwdUri?.fsPath, channel: this.channel, translator, @@ -97,6 +104,11 @@ export class LakeRunner { } } -export function lake(channel: OutputChannel, cwdUri: FileUri | undefined, toolchain?: string | undefined): LakeRunner { - return new LakeRunner(channel, cwdUri, toolchain) +export function lake( + channel: OutputChannel, + cwdUri: FileUri | undefined, + context: string | undefined, + toolchain?: string | undefined, +): LakeRunner { + return new LakeRunner(channel, cwdUri, context, toolchain) }