fix: don't resolve deps as part of lake exe cache query step (#748)

Author: mhuisi

vscode-lean4/src/leanclient.ts

@@ -456,7 +456,7 @@ export class LeanClient implements Disposable {
 
             const progressOptions: ProgressOptions = {
                 location: ProgressLocation.Notification,
-                title: '[Server Startup] Starting Lean language server and cloning missing packages [(Click for details)](command:lean4.troubleshooting.showOutput)',
+                title: '[Server Startup] Starting Lean language server and cloning missing project dependencies [(Click for details)](command:lean4.troubleshooting.showOutput)',
                 cancellable: false,
             }
             await window.withProgress(

vscode-lean4/src/projectinit.ts

@@ -414,12 +414,23 @@ Open this project instead?`
                 return
             }
 
-            const fetchResult: 'Success' | 'Failure' = await lake({
+            const lakeRunner = lake({
                 channel: this.channel,
                 cwdUri: projectFolder,
                 context: downloadProjectContext,
                 toolchainUpdateMode: 'UpdateAutomatically',
-            }).tryFetchMathlibCacheWithError()
+            })
+
+            const resolveResult: LakeRunnerResult = await lakeRunner.resolveDeps()
+            if (resolveResult.kind === 'Cancelled') {
+                return
+            }
+            if (resolveResult.kind !== 'Success') {
+                displayLakeRunnerError(resolveResult, 'Cannot clone missing project dependencies.')
+                return
+            }
+
+            const fetchResult: 'Success' | 'Failure' = await lakeRunner.tryFetchMathlibCacheWithError()
             if (fetchResult !== 'Success') {
                 return
             }

vscode-lean4/src/projectoperations.ts

@@ -4,7 +4,6 @@ import { commands, Disposable, OutputChannel, QuickPickItem, window } from 'vsco
 import { LeanClient } from './leanclient'
 import { LeanClientProvider } from './utils/clientProvider'
 import {
-    CacheGetAvailabilityResult,
     displayLakeRunnerError,
     FetchMathlibCacheResult,
     lake,
@@ -39,6 +38,15 @@ export class ProjectOperationProvider implements Disposable {
 
     private async buildProject() {
         await this.runOperation('Build Project', async lakeRunner => {
+            const resolveResult: LakeRunnerResult = await lakeRunner.resolveDeps()
+            if (resolveResult.kind === 'Cancelled') {
+                return
+            }
+            if (resolveResult.kind !== 'Success') {
+                displayLakeRunnerError(resolveResult, 'Cannot clone missing project dependencies.')
+                return
+            }
+
             const fetchResult: 'Success' | 'Failure' = await lakeRunner.tryFetchMathlibCacheWithError()
             if (fetchResult !== 'Success') {
                 return
@@ -79,36 +87,33 @@ export class ProjectOperationProvider implements Disposable {
                 return
             }
 
-            const checkResult: CacheGetAvailabilityResult = await lakeRunner.isMathlibCacheGetAvailable()
-            if (checkResult.kind === 'Cancelled') {
-                return
-            }
-            if (checkResult.kind === 'CacheUnavailable') {
-                displayNotification('Information', 'Project cleaned successfully.')
-                return
-            }
-            if (checkResult.kind !== 'CacheAvailable') {
-                displayLakeRunnerError(checkResult, 'Cannot check availability of Mathlib cache.')
-                return
-            }
-
-            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(
+            const rebuildMessage = 'Project cleaned successfully. Do you wish to rebuild the project?'
+            const rebuildInput = 'Rebuild Project'
+            const rebuildChoice: string | undefined = await displayNotificationWithInput(
                 'Information',
-                fetchMessage,
-                [fetchInput],
-                'Do Not Fetch Cache',
+                rebuildMessage,
+                [rebuildInput],
+                'Do Not Rebuild',
             )
-            if (fetchChoice !== fetchInput) {
+            if (rebuildChoice !== rebuildInput) {
                 return
             }
 
             const fetchResult: 'Success' | 'Failure' = await lakeRunner.tryFetchMathlibCacheWithError()
             if (fetchResult !== 'Success') {
                 return
             }
-            displayNotification('Information', 'Mathlib build artifact cache fetched successfully.')
+
+            const buildResult: LakeRunnerResult = await lakeRunner.build()
+            if (buildResult.kind === 'Cancelled') {
+                return
+            }
+            if (buildResult.kind !== 'Success') {
+                displayLakeRunnerError(buildResult, 'Cannot build project.')
+                return
+            }
+
+            displayNotification('Information', 'Project rebuilt successfully.')
         })
     }
 

vscode-lean4/src/utils/lake.ts

@@ -143,6 +143,10 @@ export class LakeRunner {
         )
     }
 
+    async resolveDeps(): Promise<LakeRunnerResult> {
+        return this.runLakeCommandWithProgress('resolve-deps', [], 'Cloning missing project dependencies')
+    }
+
     async isMathlibCacheGetAvailable(): Promise<CacheGetAvailabilityResult> {
         const result: LakeRunnerResult = await this.runLakeCommandWithProgress(
             'exe',