wip

lean4-infoview/src/infoview/info.tsx

@@ -498,6 +498,8 @@ function InfoAux(props: InfoProps) {
                             errorString = mapRpcError(ex).message
                         } else if (ex instanceof Error) {
                             errorString = ex.toString()
+                        } else if ('message' in ex && typeof ex.message === 'string') {
+                            errorString = ex.message
                         } else {
                             errorString = `Unrecognized error: ${JSON.stringify(ex)}`
                         }

vscode-lean4/src/leanclient.ts

@@ -196,7 +196,7 @@ export class LeanClient implements Disposable {
 
             const progressOptions: ProgressOptions = {
                 location: ProgressLocation.Notification,
-                title: 'Starting Lean language client',
+                title: '[Server Startup] Starting Lean language client',
                 cancellable: false,
             }
             await window.withProgress(

vscode-lean4/src/projectoperations.ts

@@ -82,7 +82,7 @@ export class ProjectOperationProvider implements Disposable {
                 return
             }
 
-            const fetchMessage = "Project cleaned successfully. Do you want to fetch Mathlib's build artifact cache?"
+            const fetchMessage = "Project cleaned successfully. Do you wish to fetch Mathlib's build artifact cache?"
             const fetchInput = 'Fetch Cache'
             const fetchChoice: string | undefined = await displayNotificationWithInput(
                 'Information',
@@ -332,7 +332,7 @@ export class ProjectOperationProvider implements Disposable {
                 toolchainResult === 'CannotReadLocalToolchain'
                     ? `Could not read Lean version of open project at '${localToolchainPath}'`
                     : `Could not read Lean version of ${dependencyName} at ${dependencyToolchainPath}`
-            const message = `${errorFlavor}. Do you want to update ${dependencyName} without updating the Lean version of the open project to that of ${dependencyName} regardless?`
+            const message = `${errorFlavor}. Do you wish to update ${dependencyName} without updating the Lean version of the open project to that of ${dependencyName} regardless?`
             const input = 'Proceed'
             const choice: string | undefined = await displayNotificationWithInput('Information', message, [input])
             return choice === 'input' ? { kind: 'DoNotUpdate' } : { kind: 'Cancelled' }
@@ -343,7 +343,7 @@ export class ProjectOperationProvider implements Disposable {
             return { kind: 'DoNotUpdate' }
         }
 
-        const message = `The Lean version '${localToolchain}' of the open project differs from the Lean version '${dependencyToolchain}' of ${dependencyName}. Do you want to update the Lean version of the open project to the Lean version of ${dependencyName}?`
+        const message = `The Lean version '${localToolchain}' of the open project differs from the Lean version '${dependencyToolchain}' of ${dependencyName}. Do you wish to update the Lean version of the open project to the Lean version of ${dependencyName}?`
         const updateInput = 'Update Lean Version'
         const keepInput = 'Keep Lean Version'
         const choice = await displayNotificationWithInput('Information', message, [keepInput, updateInput])

vscode-lean4/src/utils/clientProvider.ts

@@ -106,6 +106,7 @@ export class LeanClientProvider implements Disposable {
     }
 
     getActiveClient(): LeanClient | undefined {
+        // TODO: Most callers of this function probably don't need an active client, just the folder URI.
         return this.activeClient
     }
 
@@ -180,18 +181,31 @@ export class LeanClientProvider implements Disposable {
         this.restartFile(doc.extUri)
     }
 
-    private stopActiveClient() {
+    private async stopActiveClient() {
         if (this.activeClient && this.activeClient.isStarted()) {
-            void this.activeClient?.stop()
+            await this.activeClient?.stop()
         }
     }
 
     private async restartActiveClient() {
-        void this.activeClient?.restart()
-    }
+        if (this.activeClient === undefined) {
+            const activeUri = lean.lastActiveLeanDocument?.extUri
+            if (activeUri === undefined) {
+                displayNotification(
+                    'Error',
+                    'Cannot restart server: No focused Lean tab. Please focus the Lean tab for which you want to restart the server.',
+                )
+                return
+            }
+
+            const [cached, client] = await this.ensureClient(activeUri)
+            if (cached) {
+                await client?.restart()
+            }
+            return
+        }
 
-    clientIsStarted() {
-        void this.activeClient?.isStarted()
+        await this.activeClient?.restart()
     }
 
     // Find the client for a given document.
@@ -250,6 +264,7 @@ export class LeanClientProvider implements Disposable {
         )
         if (preconditionCheckResult === 'Fatal') {
             this.pending.delete(key)
+            this.activeClient = undefined
             return [false, undefined]
         }
 
@@ -259,6 +274,9 @@ export class LeanClientProvider implements Disposable {
         this.clients.set(key, client)
 
         client.serverFailed(err => {
+            if (this.activeClient === client) {
+                this.activeClient = undefined
+            }
             this.clients.delete(key)
             client.dispose()
             displayNotification('Error', err)

vscode-lean4/src/utils/elanCommands.ts

@@ -19,7 +19,7 @@ import {
 } from './elan'
 import { FileUri, UntitledUri } from './exturi'
 import { fileExists } from './fsHelper'
-import { groupByUniqueKey } from './groupBy'
+import { groupByKey } from './groupBy'
 import { displayNotification, displayNotificationWithInput } from './notifs'
 import { LeanReleaseChannel, queryLeanReleases } from './releaseQuery'
 
@@ -206,7 +206,7 @@ export class ElanCommandProvider implements Disposable {
         }
         const unusedToolchains = queryGcResult.info.unusedToolchains
         const unusedToolchainIndex = new Set(unusedToolchains)
-        const usedToolchainIndex = groupByUniqueKey(queryGcResult.info.usedToolchains, u => u.toolchain)
+        const usedToolchainIndex = groupByKey(queryGcResult.info.usedToolchains, u => u.toolchain)
 
         const toolchainInfo = await this.installedToolchains()
         if (toolchainInfo === undefined) {
@@ -218,16 +218,19 @@ export class ElanCommandProvider implements Disposable {
             return
         }
         const installedToolchainItems = installedToolchains.map(t => {
-            let user = usedToolchainIndex.get(t)?.user
-            if (user === 'default toolchain') {
-                // Translate Elan nomenclature to vscode-lean4 nomenclature
-                user = 'default Lean version'
-            } else if (user !== undefined) {
-                user = `'${user}'`
-            }
+            const users = usedToolchainIndex
+                .get(t)
+                ?.map(t => {
+                    if (t.user === 'default toolchain') {
+                        // Translate Elan nomenclature to vscode-lean4 nomenclature
+                        return 'default Lean version'
+                    }
+                    return `'${t.user}'`
+                })
+                .join(', ')
             return {
                 label: t,
-                description: user !== undefined ? `(used by ${user})` : '(unused)',
+                description: users !== undefined ? `(used by ${users})` : '(unused)',
             }
         })
 

vscode-lean4/src/utils/leanCmdRunner.ts

@@ -57,17 +57,27 @@ function leanNotInstalledError(
     activeOverride: ElanOverrideReason | undefined,
     unresolvedActiveToolchain: ElanRemoteUnresolvedToolchain,
 ): string {
-    let toolchainName: string
+    const or = overrideReason(activeOverride)
+    const formattedOverride = or !== undefined ? ' ' + or : ''
     if (unresolvedActiveToolchain.fromChannel !== undefined) {
         const prefix = activeOverride === undefined ? 'default ' : ''
-        toolchainName = `Lean version for ${prefix}release channel '${ElanUnresolvedToolchain.toolchainName(unresolvedActiveToolchain)}'`
+        return `No Lean version for ${prefix}release channel '${ElanUnresolvedToolchain.toolchainName(unresolvedActiveToolchain)}'${formattedOverride} is installed.`
     } else {
         const prefix = activeOverride === undefined ? 'Default ' : ''
-        toolchainName = `${prefix}Lean version '${ElanUnresolvedToolchain.toolchainName(unresolvedActiveToolchain)}'`
+        return `${prefix}Lean version '${ElanUnresolvedToolchain.toolchainName(unresolvedActiveToolchain)}'${formattedOverride} is not installed.`
     }
+}
 
-    const or = overrideReason(activeOverride)
-    return `${toolchainName}${or !== undefined ? ' ' + or : ''} is not installed.`
+function installationPrompt(
+    activeOverride: ElanOverrideReason | undefined,
+    unresolvedActiveToolchain: ElanRemoteUnresolvedToolchain,
+): string {
+    const error = leanNotInstalledError(activeOverride, unresolvedActiveToolchain)
+    if (unresolvedActiveToolchain.fromChannel !== undefined) {
+        return `${error}\n\n` + 'Do you wish to install one?'
+    } else {
+        return `${error}\n\n` + 'Do you wish to install it?'
+    }
 }
 
 function updatePrompt(
@@ -78,7 +88,10 @@ function updatePrompt(
 ): string {
     const prefix = activeOverride === undefined ? 'default ' : ''
     const reason = overrideReason(activeOverride)
-    return `Installed Lean version '${cachedActiveToolchain}' for ${prefix}release channel '${releaseChannel}'${reason !== undefined ? ' ' + reason : ''} is outdated. Do you want to install the new Lean version '${resolvedActiveToolchain}' or continue using the outdated Lean version?`
+    return (
+        `Installed Lean version '${cachedActiveToolchain}' for ${prefix}release channel '${releaseChannel}'${reason !== undefined ? ' ' + reason : ''} is outdated.\n\n` +
+        `Do you wish to install the new Lean version '${resolvedActiveToolchain}' or continue using the outdated Lean version?`
+    )
 }
 
 function updateDecisionKey(cwdUri: FileUri | undefined, cachedToolchain: string): string {
@@ -179,9 +192,10 @@ export class LeanCommandRunner {
             if (!alwaysAskBeforeInstallingLeanVersions()) {
                 return await installNewToolchain()
             }
+            let prompt: string
             const choice = await displayNotificationWithInput(
                 'Information',
-                `${leanNotInstalledError(elanState.toolchains.activeOverride?.reason, unresolvedToolchain)} Do you want to install it?`,
+                installationPrompt(elanState.toolchains.activeOverride?.reason, unresolvedToolchain),
                 ['Install Version'],
             )
             if (choice === undefined) {