fix: offer update options for all dependencies in manifest (#638)

This PR removes the logic from the 'Update Dependency' command that
hides dependencies that are already up-to-date relative to the manifest
and removes the revision information from the selection dialog.

The reason for this is that the manifest is not an up-to-date
representation of the set of dependencies in the `lakefile.lean` or the
`lakefile.toml`, e.g. if the input revision in the Lake configuration
file was changed. I don't know of a way to query this information from
Lake without also updating all the revisions of the manifest in the
process, so we now just avoid this situation entirely by considering the
revision information in the manifest to be unreliable.

Note that there is still a shortcoming of this approach: When adding a
new dependency to the `lakefile.lean` or the `lakefile.toml`, we won't
display it in the update dialog until the manifest is updated.

This came up at [#general > Updating Mathlib via VSCode menu does not
work @
💬](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Updating.20Mathlib.20via.20VSCode.20menu.20does.20not.20work/near/526969295).

Author: mhuisi

vscode-lean4/manual/images/update-dependency.png

@@ -2,7 +2,6 @@ import * as fs from 'fs'
 import { join } from 'path'
 import { commands, Disposable, OutputChannel, QuickPickItem, window } from 'vscode'
 import { LeanClient } from './leanclient'
-import { batchExecute, ExecutionExitCode, ExecutionResult } from './utils/batch'
 import { LeanClientProvider } from './utils/clientProvider'
 import {
     CacheGetAvailabilityResult,
@@ -226,28 +225,11 @@ export class ProjectOperationProvider implements Disposable {
             return
         }
 
-        const dependencies: (DirectGitDependency & { remoteRevision?: string | undefined })[] =
-            await this.findUpdateableDependencies(manifestResult.directGitDependencies)
-        if (dependencies.length === 0) {
-            displayNotification('Information', 'Nothing to update - all dependencies are up-to-date.')
-            return
-        }
-
-        const items: GitDependencyQuickPickItem[] = dependencies.map(gitDep => {
-            const shortLocalRevision: string = gitDep.revision.substring(0, 7)
-            const shortRemoteRevision: string | undefined = gitDep.remoteRevision?.substring(0, 7)
-
-            const detail: string = shortRemoteRevision
-                ? `Current: ${shortLocalRevision} ⟹ New: ${shortRemoteRevision}`
-                : `Current: ${shortLocalRevision}`
-
-            return {
-                label: `${gitDep.name} @ ${gitDep.inputRevision}`,
-                description: gitDep.uri.toString(),
-                detail,
-                ...gitDep,
-            }
-        })
+        const items: GitDependencyQuickPickItem[] = manifestResult.directGitDependencies.map(gitDep => ({
+            label: gitDep.name,
+            description: gitDep.uri.toString(),
+            ...gitDep,
+        }))
 
         const dependencyChoice: GitDependencyQuickPickItem | undefined = await window.showQuickPick(items, {
             title: 'Choose a dependency to update',
@@ -306,38 +288,6 @@ export class ProjectOperationProvider implements Disposable {
         })
     }
 
-    private async findUpdateableDependencies(dependencies: DirectGitDependency[]) {
-        const augmented: (DirectGitDependency & { remoteRevision?: string | undefined })[] = []
-
-        for (const dependency of dependencies) {
-            const result: ExecutionResult = await batchExecute('git', [
-                'ls-remote',
-                dependency.uri.toString(),
-                dependency.inputRevision,
-            ])
-            if (result.exitCode !== ExecutionExitCode.Success) {
-                augmented.push(dependency)
-                continue
-            }
-
-            const matches: RegExpMatchArray | null = result.stdout.match(/^[a-z0-9]+/)
-            if (!matches) {
-                augmented.push(dependency)
-                continue
-            }
-
-            const remoteRevision: string = matches[0]
-            if (dependency.revision === remoteRevision) {
-                // Cannot be updated - filter it
-                continue
-            }
-
-            augmented.push({ remoteRevision, ...dependency })
-        }
-
-        return augmented
-    }
-
     private async determineDependencyToolchain(
         localToolchainPath: string,
         dependencyToolchainPath: string,

vscode-lean4/src/projectoperations.ts

@@ -1,5 +1,6 @@
 import * as os from 'os'
 import { OutputChannel } from 'vscode'
+import { z } from 'zod'
 import { displayOutputError, ExecutionExitCode } from './batch'
 import { FileUri } from './exturi'
 import { leanRunner, ToolchainUpdateMode } from './leanCmdRunner'
@@ -15,8 +16,9 @@ export type LakeRunnerOptions = {
 export type LakeRunnerErrorDiagnosis =
     | { kind: 'WindowsFetchError'; details: string }
     | { kind: 'CommandNotFound'; details: string }
+    | { kind: 'SubCommandNotFound'; details: string }
 export type LakeRunnerError = { kind: 'Error'; diagnosis: LakeRunnerErrorDiagnosis | undefined; output: string }
-export type LakeRunnerResult = { kind: 'Success' } | { kind: 'Cancelled' } | LakeRunnerError
+export type LakeRunnerResult = { kind: 'Success'; output: string } | { kind: 'Cancelled' } | LakeRunnerError
 
 export function displayLakeRunnerError(error: LakeRunnerError, message: string) {
     if (error.diagnosis === undefined) {
@@ -27,7 +29,7 @@ export function displayLakeRunnerError(error: LakeRunnerError, message: string)
 }
 
 export type FetchMathlibCacheResult =
-    | { kind: 'Success' }
+    | { kind: 'Success'; output: string }
     | { kind: 'CacheUnavailable' }
     | { kind: 'Cancelled' }
     | LakeRunnerError
@@ -38,6 +40,13 @@ export type CacheGetAvailabilityResult =
     | { kind: 'Cancelled' }
     | LakeRunnerError
 
+export type QueryDepsResult =
+    | { kind: 'Success'; deps: string[] }
+    | { kind: 'InvalidOutput'; output: string }
+    | { kind: 'QueryUnavailable' }
+    | { kind: 'Cancelled' }
+    | LakeRunnerError
+
 export class LakeRunner {
     constructor(readonly options: LakeRunnerOptions) {}
 
@@ -62,6 +71,35 @@ export class LakeRunner {
         return this.runLakeCommandWithProgress('clean', [], 'Cleaning Lean project')
     }
 
+    async queryDeps(): Promise<QueryDepsResult> {
+        const queryResult = await this.runLakeCommandWithProgress(
+            'query',
+            [':deps', '--json'],
+            'Querying project dependencies',
+        )
+        switch (queryResult.kind) {
+            case 'Success':
+                let parsedJson: any
+                try {
+                    parsedJson = JSON.parse(queryResult.output)
+                } catch (e) {
+                    return { kind: 'InvalidOutput', output: queryResult.output }
+                }
+                const r = z.array(z.string()).safeParse(parsedJson)
+                if (!r.success) {
+                    return { kind: 'InvalidOutput', output: queryResult.output }
+                }
+                return { kind: 'Success', deps: r.data }
+            case 'Cancelled':
+                return { kind: 'Cancelled' }
+            case 'Error':
+                if (queryResult.diagnosis?.kind === 'SubCommandNotFound') {
+                    return { kind: 'QueryUnavailable' }
+                }
+                return queryResult
+        }
+    }
+
     private async runFetchMathlibCacheCommand(args: string[], prompt: string): Promise<FetchMathlibCacheResult> {
         const availabilityResult = await this.isMathlibCacheGetAvailable()
         if (availabilityResult.kind !== 'CacheAvailable') {
@@ -73,7 +111,7 @@ export class LakeRunner {
     private async tryRunFetchMathlibCacheCommand(args: string[], prompt: string): Promise<LakeRunnerResult> {
         const fetchResult = await this.runFetchMathlibCacheCommand(args, prompt)
         if (fetchResult.kind === 'CacheUnavailable') {
-            return { kind: 'Success' }
+            return { kind: 'Success', output: '' }
         }
         return fetchResult
     }
@@ -143,7 +181,7 @@ export class LakeRunner {
         })
         switch (r.exitCode) {
             case ExecutionExitCode.Success:
-                return { kind: 'Success' }
+                return { kind: 'Success', output: r.stdout }
             case ExecutionExitCode.CannotLaunch:
                 return {
                     kind: 'Error',
@@ -152,6 +190,12 @@ export class LakeRunner {
                 }
             case ExecutionExitCode.ExecutionError:
                 let diagnosis: LakeRunnerErrorDiagnosis | undefined
+                if (r.combined.includes(`error: unknown command '${subCommand}'`)) {
+                    diagnosis = {
+                        kind: 'SubCommandNotFound',
+                        details: `Lake sub-command '${subCommand}' is not available.`,
+                    }
+                }
                 if (
                     os.platform() === 'win32' &&
                     (r.combined.includes('failed to fetch GitHub release') ||