bump

leanprover · Jan 10, 2025 · f30accf · f30accf
1 parent 835bbd3
commit f30accf
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 3 deletions.
diff --git a/vscode-lean4/src/diagnostics/setupDiagnostics.ts b/vscode-lean4/src/diagnostics/setupDiagnostics.ts
@@ -279,16 +279,24 @@ export async function checkAll(
 
 export async function checkLean4ProjectPreconditions(
     channel: OutputChannel,
+    context: string,
     folderUri: ExtUri,
 ): Promise<PreconditionCheckResult> {
+    const options: SetupNotificationOptions = {
+        errorMode: { mode: 'NonModal' },
+        warningMode: { modal: false, proceedByDefault: true },
+    }
+    const d = new SetupDiagnostics(options)
     return await checkAll(
-        () => checkIsValidProjectFolder(channel, folderUri),
-        () => checkIsLeanVersionUpToDate(channel, folderUri, { modal: false }),
+        () => d.checkIsValidProjectFolder(channel, folderUri),
+        () => d.checkIsLeanVersionUpToDate(channel, context, folderUri, { toolchainUpdateMode: 'PromptAboutUpdate' }),
         async () => {
             if (!(await willUseLakeServer(folderUri))) {
                 return 'Fulfilled'
             }
-            return await checkIsLakeInstalledCorrectly(channel, folderUri, {})
+            return await d.checkIsLakeInstalledCorrectly(channel, context, folderUri, {
+                toolchainUpdateMode: 'PromptAboutUpdate',
+            })
         },
     )
 }
diff --git a/vscode-lean4/src/utils/clientProvider.ts b/vscode-lean4/src/utils/clientProvider.ts
@@ -38,6 +38,7 @@ export class LeanClientProvider implements Disposable {
         outputChannel: OutputChannel,
         private checkLean4ProjectPreconditions: (
             channel: OutputChannel,
+            context: string,
             folderUri: ExtUri,
         ) => Promise<PreconditionCheckResult>,
     ) {
@@ -115,6 +116,7 @@ export class LeanClientProvider implements Disposable {
 
                 const preconditionCheckResult = await this.checkLean4ProjectPreconditions(
                     this.outputChannel,
+                    'Client Restart',
                     projectUri,
                 )
                 if (preconditionCheckResult !== 'Fatal') {
@@ -240,6 +242,7 @@ export class LeanClientProvider implements Disposable {
 
         const preconditionCheckResult = await this.checkLean4ProjectPreconditions(
             this.outputChannel,
+            'Client Startup',
             folderUri,
         )
         if (preconditionCheckResult === 'Fatal') {