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.

vscode-lean4/src/diagnostics/fullDiagnostics.ts

@@ -116,6 +116,7 @@ export async function performFullDiagnosis(
     channel: OutputChannel,
     cwdUri: FileUri | undefined,
 ): Promise<FullDiagnostics> {
+    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(),
     }

vscode-lean4/src/diagnostics/setupDiagnoser.ts

@@ -140,13 +140,13 @@ export class SetupDiagnoser {
         return gitVersionResult.exitCode === ExecutionExitCode.Success
     }
 
-    async queryLakeVersion(): Promise<VersionQueryResult> {
-        const lakeVersionResult = await this.runLeanCommand('lake', ['--version'], 'Checking Lake version')
+    async queryLakeVersion(context: string): Promise<VersionQueryResult> {
+        const lakeVersionResult = await this.runLeanCommand('lake', ['--version'], context, 'Checking Lake version')
         return versionQueryResult(lakeVersionResult, /version (\d+\.\d+\.\d+(\w|-)*)/)
     }
 
-    async checkLakeAvailable(): Promise<boolean> {
-        const lakeVersionResult = await this.queryLakeVersion()
+    async checkLakeAvailable(context: string): Promise<boolean> {
+        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<VersionQueryResult> {
-        const leanVersionResult = await this.runLeanCommand('lean', ['--version'], 'Checking Lean version')
+    async queryLeanVersion(context: string): Promise<VersionQueryResult> {
+        const leanVersionResult = await this.runLeanCommand('lean', ['--version'], context, 'Checking Lean version')
         return versionQueryResult(leanVersionResult, /version (\d+\.\d+\.\d+(\w|-)*)/)
     }
 
@@ -223,28 +223,33 @@ export class SetupDiagnoser {
         return { kind: 'ValidProjectSetup', projectFolder: this.cwdUri }
     }
 
-    async leanVersion(): Promise<LeanVersionDiagnosis> {
-        const leanVersionResult = await this.queryLeanVersion()
+    async leanVersion(context: string): Promise<LeanVersionDiagnosis> {
+        const leanVersionResult = await this.queryLeanVersion(context)
         return checkLeanVersion(leanVersionResult)
     }
 
     private async runSilently(executablePath: string, args: string[]): Promise<ExecutionResult> {
         return batchExecute(executablePath, args, this.cwdUri?.fsPath, { combined: this.channel })
     }
 
-    private async runWithProgress(executablePath: string, args: string[], title: string): Promise<ExecutionResult> {
-        return batchExecuteWithProgress(executablePath, args, title, {
+    private async runWithProgress(
+        executablePath: string,
+        args: string[],
+        context: string,
+        title: string,
+    ): Promise<ExecutionResult> {
+        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)
     }
 }
 

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<PreconditionCheckResult> {
-    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<PreconditionCheckResult> {
@@ -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,14 +200,15 @@ export async function checkIsLeanVersionUpToDate(
 
 export async function checkIsLakeInstalledCorrectly(
     channel: OutputChannel,
+    context: string,
     folderUri: ExtUri,
     options: { toolchainOverride?: string | undefined },
 ): Promise<PreconditionCheckResult> {
     const lakeVersionResult = await diagnose(
         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.")

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<PreconditionCheckResult> {
     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<Lean4EnabledFeatures | undefined> {
-    const preconditionCheckResult = await checkLean4FeaturePreconditions(installer, projectUri)
+    const preconditionCheckResult = await checkLean4FeaturePreconditions(
+        installer,
+        'Activate Lean 4 Extension',
+        projectUri,
+    )
     if (preconditionCheckResult === 'Fatal') {
         return undefined
     }

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<PreconditionCheckResult> {
@@ -31,22 +32,26 @@ 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 }),
     )
 }
 
 async function checkPreCloneLean4ProjectPreconditions(channel: OutputChannel, cwdUri: FileUri | undefined) {
     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,15 +106,21 @@ 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
         }
 
         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<FileUri | 'DidNotComplete'> {
@@ -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<QuickPickItem & { isPreset: boolean }>()
         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
             }