feat: sorted installed toolchains (#611)

This PR ensures that the installed toolchains in all commands that
display them are sorted in a sensible manner.

Author: mhuisi

vscode-lean4/src/utils/elan.ts

@@ -4,6 +4,7 @@ import { z, ZodTypeAny } from 'zod'
 import { batchExecute, batchExecuteWithProgress, ExecutionExitCode, ExecutionResult } from './batch'
 import { FileUri } from './exturi'
 import { groupByUniqueKey } from './groupBy'
+import { semVerRegex } from './semverRegex'
 
 export const elanStableChannel = 'leanprover/lean4:stable'
 export const elanNightlyChannel = 'leanprover/lean4:nightly'
@@ -14,11 +15,6 @@ export function isElanEagerResolutionVersion(version: SemVer) {
     return version.major >= elanEagerResolutionMajorVersion
 }
 
-// Suggested at https://semver.org/#is-there-a-suggested-regular-expression-regex-to-check-a-semver-string
-
-const semVerRegex =
-    /^(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-]+)*))?$/
-
 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-]+)*))?)/
 

vscode-lean4/src/utils/elanCommands.ts

@@ -1,4 +1,6 @@
+import assert from 'assert'
 import { promises } from 'fs'
+import { SemVer, valid } from 'semver'
 import { commands, Disposable, OutputChannel, QuickPickItem, QuickPickItemKind, window } from 'vscode'
 import { ExecutionExitCode } from './batch'
 import { LeanClientProvider } from './clientProvider'
@@ -27,6 +29,89 @@ function displayElanNotInstalledError() {
     displayNotification('Error', 'Elan is not installed.')
 }
 
+type LeanToolchain =
+    | { kind: 'Unknown'; fullName: string }
+    | { kind: 'Release'; fullName: string; version: SemVer }
+    | { kind: 'Nightly'; fullName: string; date: Date }
+    | { kind: 'PRRelease'; fullName: string; pr: number }
+
+function parseToolchain(toolchain: string): LeanToolchain {
+    const releaseMatch = toolchain.match(/leanprover\/lean4:(.+)/)
+    if (releaseMatch) {
+        let version = releaseMatch[1]
+        if (version[0] === 'v') {
+            version = version.substring(1)
+        }
+        if (valid(version)) {
+            return { kind: 'Release', fullName: toolchain, version: new SemVer(version) }
+        }
+    }
+
+    const nightlyMatch = toolchain.match(/leanprover\/lean4-nightly:nightly-(.+)/)
+    if (nightlyMatch) {
+        const date = new Date(nightlyMatch[1])
+        if (!isNaN(date.valueOf())) {
+            return { kind: 'Nightly', fullName: toolchain, date }
+        }
+    }
+
+    const prReleaseMatch = toolchain.match(/leanprover\/lean4-pr-releases:pr-release-(\d+)/)
+    if (prReleaseMatch) {
+        const pr = Number.parseInt(prReleaseMatch[1])
+        return { kind: 'PRRelease', fullName: toolchain, pr }
+    }
+
+    return { kind: 'Unknown', fullName: toolchain }
+}
+
+function toolchainKindPrio(k: 'Unknown' | 'Release' | 'Nightly' | 'PRRelease'): number {
+    switch (k) {
+        case 'Unknown':
+            return 3
+        case 'Release':
+            return 2
+        case 'Nightly':
+            return 1
+        case 'PRRelease':
+            return 0
+    }
+}
+
+function compareToolchainKinds(
+    k1: 'Unknown' | 'Release' | 'Nightly' | 'PRRelease',
+    k2: 'Unknown' | 'Release' | 'Nightly' | 'PRRelease',
+): number {
+    return toolchainKindPrio(k1) - toolchainKindPrio(k2)
+}
+
+function compareToolchains(t1: LeanToolchain, t2: LeanToolchain): number {
+    const kindComparison = compareToolchainKinds(t1.kind, t2.kind)
+    if (kindComparison !== 0) {
+        return kindComparison
+    }
+    switch (t1.kind) {
+        case 'Unknown':
+            assert(t2.kind === 'Unknown')
+            return -1 * t1.fullName.localeCompare(t2.fullName)
+        case 'Release':
+            assert(t2.kind === 'Release')
+            return t1.version.compare(t2.version)
+        case 'Nightly':
+            assert(t2.kind === 'Nightly')
+            return t1.date.valueOf() - t2.date.valueOf()
+        case 'PRRelease':
+            assert(t2.kind === 'PRRelease')
+            return t1.pr - t2.pr
+    }
+}
+
+function sortToolchains(ts: string[]): string[] {
+    return ts
+        .map(t => parseToolchain(t))
+        .sort((t1, t2) => -1 * compareToolchains(t1, t2))
+        .map(t => t.fullName)
+}
+
 export class ElanCommandProvider implements Disposable {
     private subscriptions: Disposable[] = []
 
@@ -212,7 +297,7 @@ export class ElanCommandProvider implements Disposable {
         if (toolchainInfo === undefined) {
             return
         }
-        const installedToolchains = toolchainInfo.toolchains
+        const installedToolchains = sortToolchains(toolchainInfo.toolchains)
         if (installedToolchains.length === 0) {
             displayNotification('Information', 'No Lean versions installed.')
             return
@@ -375,7 +460,7 @@ export class ElanCommandProvider implements Disposable {
         if (toolchainInfo === undefined) {
             return undefined
         }
-        const installedToolchains = toolchainInfo.toolchains
+        const installedToolchains = sortToolchains(toolchainInfo.toolchains)
         const installedToolchainIndex = new Set(installedToolchains)
 
         let stableToolchains: string[] = []

vscode-lean4/src/utils/manifest.ts

@@ -3,10 +3,7 @@ import { SemVer } from 'semver'
 import { Uri } from 'vscode'
 import { z } from 'zod'
 import { FileUri } from './exturi'
-
-// Suggested at https://semver.org/#is-there-a-suggested-regular-expression-regex-to-check-a-semver-string
-const semVerRegex =
-    /^(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-]+)*))?$/
+import { semVerRegex } from './semverRegex'
 
 export interface DirectGitDependency {
     name: string

vscode-lean4/src/utils/semverRegex.ts

@@ -0,0 +1,3 @@
+// Suggested at https://semver.org/#is-there-a-suggested-regular-expression-regex-to-check-a-semver-string
+export const semVerRegex =
+    /^(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-]+)*))?$/