refactor: clean up semver handling (#761)

Author: mhuisi

package-lock.json

@@ -1,5 +1,5 @@
 import * as os from 'os'
-import * as s from 'semver'
+import * as semver from 'semver'
 import { SemVer } from 'semver'
 import { OutputChannel, extensions, version } from 'vscode'
 import { ExecutionExitCode, ExecutionResult, batchExecute } from '../utils/batch'
@@ -8,10 +8,11 @@ import {
     ElanDumpStateWithoutNetResult,
     elanDumpStateWithNet,
     elanDumpStateWithoutNet,
+    elanVersionRegex,
     isElanEagerResolutionVersion,
 } from '../utils/elan'
 import { FileUri } from '../utils/exturi'
-import { ToolchainUpdateMode, leanRunner } from '../utils/leanCmdRunner'
+import { ToolchainUpdateMode, leanRunner, leanVersionRegex } from '../utils/leanCmdRunner'
 import { checkParentFoldersForLeanProject, isValidLeanProject } from '../utils/projectInfo'
 
 const minimumSupportedMacOSVersion = new SemVer('19.0.0')
@@ -23,11 +24,10 @@ export type OSVersionDiagnosis =
 
 function diagnoseOSVersion(): OSVersionDiagnosis {
     // When in doubt, we consider an OS version as not being unsupported.
-    const release = os.release()
-    if (!s.valid(release)) {
+    const currentVersion = semver.parse(os.release())
+    if (currentVersion === null) {
         return { kind: 'NotUnsupported' }
     }
-    const currentVersion = new SemVer(release)
     switch (os.type()) {
         case 'Darwin':
             if (currentVersion.compare(minimumSupportedMacOSVersion) >= 0) {
@@ -114,7 +114,12 @@ export function versionQueryResult(executionResult: ExecutionResult, versionRege
         return { kind: 'InvalidVersion', versionResult: executionResult.stdout }
     }
 
-    return { kind: 'Success', version: new SemVer(match[1]) }
+    const parsed = semver.parse(match[1])
+    if (parsed === null) {
+        return { kind: 'InvalidVersion', versionResult: executionResult.stdout }
+    }
+
+    return { kind: 'Success', version: parsed }
 }
 
 export function checkElanVersion(elanVersionResult: VersionQueryResult): ElanVersionDiagnosis {
@@ -313,12 +318,12 @@ export class SetupDiagnoser {
 
     async queryLeanVersion(): Promise<VersionQueryResult> {
         const leanVersionResult = await this.runLeanCommand('lean', ['--version'], 'Checking Lean version')
-        return versionQueryResult(leanVersionResult, /version (\d+\.\d+\.\d+(\w|-)*)/)
+        return versionQueryResult(leanVersionResult, leanVersionRegex)
     }
 
     async queryElanVersion(): Promise<VersionQueryResult> {
         const elanVersionResult = await this.runSilently('elan', ['--version'])
-        return versionQueryResult(elanVersionResult, /elan (\d+\.\d+\.\d+)/)
+        return versionQueryResult(elanVersionResult, elanVersionRegex)
     }
 
     async queryElanShow(): Promise<ExecutionResult> {

vscode-lean4/src/diagnostics/setupDiagnoser.ts

@@ -51,7 +51,7 @@ import { logger } from './utils/logger'
 // @ts-ignore
 import * as fs from 'fs'
 import { glob } from 'glob'
-import { SemVer } from 'semver'
+import * as semver from 'semver'
 import { formatCommandExecutionOutput } from './utils/batch'
 import {
     c2pConverter,
@@ -541,8 +541,9 @@ export class LeanClient implements Disposable {
                 }
             })
             await this.client.start()
-            const version = this.client.initializeResult?.serverInfo?.version
-            if (version && new SemVer(version).compare('0.2.0') < 0) {
+            const rawVersion = this.client.initializeResult?.serverInfo?.version
+            const version = rawVersion !== undefined ? semver.parse(rawVersion) : null
+            if (version !== null && version.compare('0.2.0') < 0) {
                 if (this.staleDepNotifier) {
                     this.staleDepNotifier.dispose()
                 }

vscode-lean4/src/leanclient.ts

@@ -1,10 +1,11 @@
+import * as semver from 'semver'
 import { SemVer } from 'semver'
 import { OutputChannel } from 'vscode'
 import { z, ZodTypeAny } from 'zod'
 import { batchExecute, batchExecuteWithProgress, ExecutionExitCode, ExecutionResult } from './batch'
 import { FileUri } from './exturi'
 import { groupByUniqueKey } from './groupBy'
-import { semVerRegex } from './semverRegex'
+import { semVerSchema } from './zod'
 
 export const elanStableChannel = 'leanprover/lean4:stable'
 export const elanNightlyChannel = 'leanprover/lean4:nightly'
@@ -15,8 +16,7 @@ export function isElanEagerResolutionVersion(version: SemVer) {
     return version.major >= elanEagerResolutionMajorVersion
 }
 
-const elanVersionRegex =
-    /^elan ((0|[1-9]\d*)\.(0|[1-9]\d*)\.(0|[1-9]\d*)(?:-((?:0|[1-9]\d*|\d*[a-zA-Z-][0-9a-zA-Z-]*)(?:\.(?:0|[1-9]\d*|\d*[a-zA-Z-][0-9a-zA-Z-]*))*))?(?:\+([0-9a-zA-Z-]+(?:\.[0-9a-zA-Z-]+)*))?)/
+export const elanVersionRegex = /^elan (\S+)/
 
 export type ElanVersionResult =
     | { kind: 'Success'; version: SemVer }
@@ -31,7 +31,11 @@ export async function elanVersion(): Promise<ElanVersionResult> {
             if (match === null) {
                 return { kind: 'ExecutionError', message: 'Cannot parse output of `elan --version`: ' + r.stdout }
             }
-            return { kind: 'Success', version: new SemVer(match[1]) }
+            const version = semver.parse(match[1])
+            if (version === null) {
+                return { kind: 'ExecutionError', message: 'Cannot parse output of `elan --version`: ' + r.stdout }
+            }
+            return { kind: 'Success', version }
         case ExecutionExitCode.CannotLaunch:
             return { kind: 'ElanNotInstalled' }
         case ExecutionExitCode.ExecutionError:
@@ -305,8 +309,8 @@ function parseElanStateDump(elanDumpStateOutput: string): ElanStateDump | undefi
 
     const stateDumpSchema = z.object({
         elan_version: z.object({
-            current: z.string().regex(semVerRegex),
-            newest: zodElanResult(z.string().regex(semVerRegex)),
+            current: semVerSchema,
+            newest: zodElanResult(semVerSchema),
         }),
         toolchains: z.object({
             installed: z.array(
@@ -349,8 +353,8 @@ function parseElanStateDump(elanDumpStateOutput: string): ElanStateDump | undefi
 
     const stateDump: ElanStateDump = {
         elanVersion: {
-            current: new SemVer(s.elan_version.current),
-            newest: convertElanResult(s.elan_version.newest, version => new SemVer(version)),
+            current: s.elan_version.current,
+            newest: convertElanResult(s.elan_version.newest, v => v),
         },
         toolchains: {
             installed,

vscode-lean4/src/utils/elan.ts

@@ -1,6 +1,7 @@
 import assert from 'assert'
 import { promises } from 'fs'
-import { SemVer, valid } from 'semver'
+import * as semver from 'semver'
+import { SemVer } from 'semver'
 import { commands, Disposable, OutputChannel, QuickPickItem, QuickPickItemKind, window } from 'vscode'
 import { ExecutionExitCode } from './batch'
 import { LeanClientProvider } from './clientProvider'
@@ -43,8 +44,9 @@ function parseToolchain(toolchain: string): LeanToolchain {
         if (version[0] === 'v') {
             version = version.substring(1)
         }
-        if (valid(version)) {
-            return { kind: 'Release', fullName: toolchain, version: new SemVer(version) }
+        const parsed = semver.parse(version)
+        if (parsed !== null) {
+            return { kind: 'Release', fullName: toolchain, version: parsed }
         }
     }
 

vscode-lean4/src/utils/elanCommands.ts

@@ -17,6 +17,8 @@ import {
 import { FileUri } from './exturi'
 import { displayNotification, displayNotificationWithInput } from './notifs'
 
+export const leanVersionRegex = /version ([^,\s]+)/
+
 export type ToolchainUpdateMode = 'UpdateAutomatically' | 'PromptAboutUpdate' | 'DoNotUpdate'
 
 function shouldUpdateToolchainAutomatically(mode: ToolchainUpdateMode) {

vscode-lean4/src/utils/leanCmdRunner.ts

@@ -3,7 +3,7 @@ import { SemVer } from 'semver'
 import { Uri } from 'vscode'
 import { z } from 'zod'
 import { FileUri } from './exturi'
-import { semVerRegex } from './semverRegex'
+import { semVerSchema } from './zod'
 
 export interface DirectGitDependency {
     name: string
@@ -23,17 +23,15 @@ type ManifestVersion =
     | { kind: 'LegacyNumberVersion'; version: number; versionAsSemVer: SemVer }
     | { kind: 'SemVer'; version: SemVer }
 
-function asManifestVersion(versionField: number | string): ManifestVersion {
-    switch (typeof versionField) {
-        case 'string':
-            return { kind: 'SemVer', version: new SemVer(versionField) }
-        case 'number':
-            return {
-                kind: 'LegacyNumberVersion',
-                version: versionField,
-                versionAsSemVer: new SemVer(`0.${versionField}.0`),
-            }
+function asManifestVersion(versionField: number | SemVer): ManifestVersion {
+    if (typeof versionField === 'number') {
+        return {
+            kind: 'LegacyNumberVersion',
+            version: versionField,
+            versionAsSemVer: new SemVer(`0.${versionField}.0`),
+        }
     }
+    return { kind: 'SemVer', version: versionField }
 }
 
 function parseVersion1To6Manifest(version: SemVer, parsedJson: any) {
@@ -150,7 +148,10 @@ export function parseAsManifest(jsonString: string): Manifest | undefined {
     }
 
     const versionSchema = z.object({
-        version: z.union([z.number().int().nonnegative(), z.string().regex(semVerRegex)]),
+        version: z.union([
+            z.number().int().nonnegative(),
+            semVerSchema,
+        ]),
     })
     const versionResult = versionSchema.safeParse(parsedJson)
     if (!versionResult.success) {

vscode-lean4/src/utils/manifest.ts

@@ -0,0 +1,11 @@
+import * as semver from 'semver'
+import { z } from 'zod'
+
+export const semVerSchema = z.string().transform((v, ctx) => {
+    const parsed = semver.parse(v)
+    if (parsed === null) {
+        ctx.addIssue({ code: z.ZodIssueCode.custom, message: 'Invalid semver' })
+        return z.NEVER
+    }
+    return parsed
+})