fix: workaround for invalid lake version in v4.21.0-rc1 (#618)

This PR fixes the fallout of a small ticking time bomb that exploded in
v4.21.0-rc1.

Lake reports its version strings as follows, where `77cfc4d` is the
commit ID of the corresponding release:
```
[mhuisi@fedora ~]$ lake --version
Lake version 5.0.0-77cfc4d (Lean version 4.20.0)
```
In v4.21.0-rc1, the commit ID is `0168680`, so Lake reports the
following version string:
```
[mhuisi@fedora ~]$ lake --version
Lake version 5.0.0-0168680 (Lean version 4.21.0-rc1)
```

Unfortunately, `5.0.0-0168680` is *not* a [valid semantic
version](https://semver.org/), since it both contains a 0 at the start
and only numbers. This is fairly rare, but it now happened on
v4.21.0-rc1 for the first time.
The VS Code extension parses this version as part of its precondition
checks, which now fails because the version is not a valid semantic
version.

The workaround for this issue is to remove the step that parses the
version. The extension only parsed it for consistency with other
precondition checks and doesn't actually do anything interesting with
the version, so removing it doesn't lose us anything.

Author: mhuisi

vscode-lean4/src/diagnostics/setupDiagnoser.ts

@@ -27,6 +27,11 @@ export type VersionQueryResult =
     | { kind: 'Cancelled' }
     | { kind: 'InvalidVersion'; versionResult: string }
 
+export type LakeAvailabilityResult =
+    | { kind: 'Available' }
+    | { kind: 'NotAvailable' }
+    | { kind: 'Error'; message: string }
+    | { kind: 'Cancelled' }
 export type ElanDumpStateWithoutNetQueryResult = ElanDumpStateWithoutNetResult | { kind: 'PreEagerResolutionVersion' }
 export type ElanDumpStateWithNetQueryResult = ElanDumpStateWithNetResult | { kind: 'PreEagerResolutionVersion' }
 
@@ -176,14 +181,18 @@ export class SetupDiagnoser {
         return gitVersionResult.exitCode === ExecutionExitCode.Success
     }
 
-    async queryLakeVersion(): Promise<VersionQueryResult> {
+    async checkLakeAvailable(): Promise<LakeAvailabilityResult> {
         const lakeVersionResult = await this.runLeanCommand('lake', ['--version'], 'Checking Lake version')
-        return versionQueryResult(lakeVersionResult, /version (\d+\.\d+\.\d+(\w|-)*)/)
-    }
-
-    async checkLakeAvailable(): Promise<boolean> {
-        const lakeVersionResult = await this.queryLakeVersion()
-        return lakeVersionResult.kind === 'Success'
+        switch (lakeVersionResult.exitCode) {
+            case ExecutionExitCode.Success:
+                return { kind: 'Available' }
+            case ExecutionExitCode.CannotLaunch:
+                return { kind: 'NotAvailable' }
+            case ExecutionExitCode.ExecutionError:
+                return { kind: 'Error', message: lakeVersionResult.combined }
+            case ExecutionExitCode.Cancelled:
+                return { kind: 'Cancelled' }
+        }
     }
 
     querySystemInformation(): SystemQueryResult {

vscode-lean4/src/diagnostics/setupDiagnostics.ts

@@ -284,33 +284,30 @@ export class SetupDiagnostics {
         folderUri: ExtUri,
         options: { toolchainOverride?: string | undefined; toolchainUpdateMode: ToolchainUpdateMode },
     ): Promise<PreconditionCheckResult> {
-        const lakeVersionResult = await diagnose({
+        const lakeAvailabilityResult = await diagnose({
             channel,
             cwdUri: extUriToCwdUri(folderUri),
             toolchain: options.toolchainOverride,
             context,
             toolchainUpdateMode: options.toolchainUpdateMode,
-        }).queryLakeVersion()
-        switch (lakeVersionResult.kind) {
-            case 'CommandNotFound':
+        }).checkLakeAvailable()
+        switch (lakeAvailabilityResult.kind) {
+            case 'NotAvailable':
                 return this.n.displaySetupErrorWithOutput(
-                    "Error while checking Lake version: 'lake' command was not found.",
+                    "Error while checking Lake availability: 'lake' command was not found.",
                 )
 
-            case 'CommandError':
+            case 'Error':
                 return this.n.displaySetupErrorWithOutput(
-                    `Error while checking Lake version: ${lakeVersionResult.message}`,
+                    `Error while checking Lake availability: ${lakeAvailabilityResult.message}`,
                 )
 
             case 'Cancelled':
-                return this.n.displaySetupErrorWithOutput('Error while checking Lake version: Operation cancelled.')
-
-            case 'InvalidVersion':
                 return this.n.displaySetupErrorWithOutput(
-                    `Error while checking Lake version: Invalid Lake version format: '${lakeVersionResult.versionResult}'`,
+                    'Error while checking Lake availability: Operation cancelled.',
                 )
 
-            case 'Success':
+            case 'Available':
                 return 'Fulfilled'
         }
     }