feat: support for elan 4.0.0

vscode-lean4/package.json

@@ -81,6 +81,11 @@
                         "description": "Entry to add to the PATH variable"
                     }
                 },
+                "lean4.alwaysAskBeforeInstallingLeanVersions": {
+                    "type": "boolean",
+                    "default": false,
+                    "markdownDescription": "Enable to display a prompt whenever Elan will download and install a new Lean version"
+                },
                 "lean4.serverArgs": {
                     "type": "array",
                     "default": [],
@@ -314,6 +319,36 @@
                 "title": "Setup: Install Elan",
                 "description": "Install Lean's version manager 'Elan'"
             },
+            {
+                "command": "lean4.setup.updateElan",
+                "category": "Lean 4",
+                "title": "Setup: Update Elan",
+                "description": "Update Lean's version manager 'Elan' to the most recent version"
+            },
+            {
+                "command": "lean4.setup.uninstallElan",
+                "category": "Lean 4",
+                "title": "Setup: Uninstall Elan",
+                "description": "Uninstall Lean's version manager 'Elan' and all installed Lean versions"
+            },
+            {
+                "command": "lean4.setup.selectDefaultToolchain",
+                "category": "Lean 4",
+                "title": "Setup: Select Default Lean Version…",
+                "description": "Sets a given Lean version to be the default for non-project files and command-line operations outside of projects"
+            },
+            {
+                "command": "lean4.setup.updateReleaseChannel",
+                "category": "Lean 4",
+                "title": "Setup: Update Release Channel Lean Version…",
+                "description": "Updates the Lean version for a given release channel"
+            },
+            {
+                "command": "lean4.setup.uninstallToolchains",
+                "category": "Lean 4",
+                "title": "Setup: Uninstall Lean Versions…",
+                "description": "Uninstalls given Lean versions"
+            },
             {
                 "command": "lean4.project.createStandaloneProject",
                 "category": "Lean 4",
@@ -367,6 +402,12 @@
                 "category": "Lean 4",
                 "title": "Project: Fetch Mathlib Build Cache For Current Imports",
                 "description": "Downloads cached Mathlib build artifacts of the focused file and all of its imports to avoid full elaboration"
+            },
+            {
+                "command": "lean4.project.selectProjectToolchain",
+                "category": "Lean 4",
+                "title": "Project: Select Project Lean Version…",
+                "description": "Updates the 'lean-toolchain' file of the currently focused project with a given Lean version"
             }
         ],
         "languages": [
@@ -573,6 +614,21 @@
                 {
                     "command": "lean4.setup.installElan"
                 },
+                {
+                    "command": "lean4.setup.updateElan"
+                },
+                {
+                    "command": "lean4.setup.uninstallElan"
+                },
+                {
+                    "command": "lean4.setup.selectDefaultToolchain"
+                },
+                {
+                    "command": "lean4.setup.updateReleaseChannel"
+                },
+                {
+                    "command": "lean4.setup.uninstallToolchains"
+                },
                 {
                     "command": "lean4.project.createStandaloneProject"
                 },
@@ -604,6 +660,10 @@
                 {
                     "command": "lean4.project.fetchFileCache",
                     "when": "lean4.isLeanFeatureSetActive"
+                },
+                {
+                    "command": "lean4.project.selectProjectToolchain",
+                    "when": "lean4.isLeanFeatureSetActive"
                 }
             ],
             "editor/title": [
@@ -700,10 +760,35 @@
                 }
             ],
             "lean4.titlebar.versions": [
+                {
+                    "command": "lean4.setup.selectDefaultToolchain",
+                    "when": "lean4.isLeanFeatureSetActive || lean4.isLeanFeatureSetActive",
+                    "group": "1_toolchains@1"
+                },
+                {
+                    "command": "lean4.setup.updateReleaseChannel",
+                    "when": "lean4.isLeanFeatureSetActive || lean4.isLeanFeatureSetActive",
+                    "group": "1_toolchains@2"
+                },
+                {
+                    "command": "lean4.setup.uninstallToolchains",
+                    "when": "lean4.isLeanFeatureSetActive || lean4.isLeanFeatureSetActive",
+                    "group": "1_toolchains@3"
+                },
                 {
                     "command": "lean4.setup.installElan",
                     "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive",
-                    "group": "1_setup@1"
+                    "group": "2_elan@1"
+                },
+                {
+                    "command": "lean4.setup.updateElan",
+                    "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive",
+                    "group": "2_elan@2"
+                },
+                {
+                    "command": "lean4.setup.uninstallElan",
+                    "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive",
+                    "group": "2_elan@3"
                 }
             ],
             "lean4.titlebar.projectActions": [
@@ -731,6 +816,11 @@
                     "command": "lean4.project.fetchFileCache",
                     "when": "lean4.isLeanFeatureSetActive",
                     "group": "2_mathlibActions@2"
+                },
+                {
+                    "command": "lean4.project.selectProjectToolchain",
+                    "when": "lean4.isLeanFeatureSetActive",
+                    "group": "3_projectToolchains@1"
                 }
             ],
             "lean4.titlebar.documentation": [

vscode-lean4/src/config.ts

@@ -1,4 +1,4 @@
-import { workspace } from 'vscode'
+import { ConfigurationTarget, workspace } from 'vscode'
 import { PATH } from './utils/envPath'
 
 // TODO: does currently not contain config options for `./abbreviation`
@@ -17,6 +17,20 @@ export function envPathExtensions(): PATH {
     return new PATH(workspace.getConfiguration('lean4').get('envPathExtensions', []))
 }
 
+export function alwaysAskBeforeInstallingLeanVersions(): boolean {
+    return workspace.getConfiguration('lean4').get('alwaysAskBeforeInstallingLeanVersions', false)
+}
+
+export async function setAlwaysAskBeforeInstallingLeanVersions(alwaysAskBeforeInstallingLeanVersions: boolean) {
+    await workspace
+        .getConfiguration('lean4')
+        .update(
+            'alwaysAskBeforeInstallingLeanVersions',
+            alwaysAskBeforeInstallingLeanVersions,
+            ConfigurationTarget.Global,
+        )
+}
+
 export function serverArgs(): string[] {
     return workspace.getConfiguration('lean4').get('serverArgs', [])
 }

vscode-lean4/src/diagnostics/fullDiagnostics.ts

@@ -1,11 +1,13 @@
 import { SemVer } from 'semver'
 import { Disposable, OutputChannel, commands, env } from 'vscode'
 import { ExecutionExitCode, ExecutionResult } from '../utils/batch'
+import { ElanInstalledToolchain, ElanToolchains, ElanUnresolvedToolchain } from '../utils/elan'
 import { FileUri } from '../utils/exturi'
 import { lean } from '../utils/leanEditorProvider'
 import { displayNotification, displayNotificationWithInput } from '../utils/notifs'
 import { findLeanProjectRoot } from '../utils/projectInfo'
 import {
+    ElanDumpStateWithoutNetQueryResult,
     ElanVersionDiagnosis,
     LeanVersionDiagnosis,
     ProjectSetupDiagnosis,
@@ -24,6 +26,7 @@ export type FullDiagnostics = {
     leanVersionDiagnosis: LeanVersionDiagnosis
     projectSetupDiagnosis: ProjectSetupDiagnosis
     elanShowOutput: ExecutionResult
+    elanDumpStateOutput: ElanDumpStateWithoutNetQueryResult
 }
 
 function formatCommandOutput(cmdOutput: string): string {
@@ -62,6 +65,8 @@ function formatLeanVersionDiagnosis(d: LeanVersionDiagnosis): string {
             return `Pre-stable-release Lean 4 version (version: ${d.version})`
         case 'ExecutionError':
             return 'Execution error: ' + formatCommandOutput(d.message)
+        case 'Cancelled':
+            return 'Operation cancelled'
         case 'NotInstalled':
             return 'Not installed'
     }
@@ -92,6 +97,74 @@ function formatElanShowOutput(r: ExecutionResult): string {
     return formatCommandOutput(r.stdout)
 }
 
+function formatElanActiveToolchain(r: ElanToolchains): string {
+    if (r.activeOverride !== undefined) {
+        const toolchain = r.activeOverride.unresolved
+        const overrideReason = r.activeOverride.reason
+        let formattedOverrideReason: string
+        switch (overrideReason.kind) {
+            case 'Environment':
+                formattedOverrideReason = 'set by `ELAN_TOOLCHAIN`'
+                break
+            case 'Manual':
+                formattedOverrideReason = `set by \`elan override\` in \`${overrideReason.directoryPath}\``
+                break
+            case 'ToolchainFile':
+                formattedOverrideReason = `set by \`${overrideReason.toolchainPath}\``
+                break
+            case 'LeanpkgFile':
+                formattedOverrideReason = `set by Leanpkg file in \`${overrideReason.leanpkgPath}\``
+                break
+            case 'ToolchainDirectory':
+                formattedOverrideReason = `of core toolchain directory at \`${overrideReason.directoryPath}\``
+                break
+        }
+        return `${ElanUnresolvedToolchain.toolchainName(toolchain)} (${formattedOverrideReason})`
+    }
+    if (r.default !== undefined) {
+        return `${ElanUnresolvedToolchain.toolchainName(r.default.unresolved)} (default Lean version)`
+    }
+    return 'No active Lean version'
+}
+
+function formatElanInstalledToolchains(toolchains: Map<string, ElanInstalledToolchain>) {
+    const installed = [...toolchains.values()].map(t => t.resolvedName)
+    if (installed.length > 20) {
+        return `${installed.slice(0, 20).join(', ')} ...`
+    }
+    return installed.join(', ')
+}
+
+function formatElanDumpState(r: ElanDumpStateWithoutNetQueryResult): string {
+    if (r.kind === 'ElanNotFound') {
+        return '**Elan**: Elan not installed'
+    }
+    if (r.kind === 'ExecutionError') {
+        return `**Elan**: Execution error: ${r.message}`
+    }
+    if (r.kind === 'PreEagerResolutionVersion') {
+        return '**Elan**: Pre-4.0.0 version'
+    }
+    r.kind satisfies 'Success'
+    const stateDump = r.state
+    return [
+        `**Active Lean version**: ${formatElanActiveToolchain(stateDump.toolchains)}`,
+        `**Installed Lean versions**: ${formatElanInstalledToolchains(stateDump.toolchains.installed)}`,
+    ].join('\n')
+}
+
+function formatElanInfo(d: FullDiagnostics): string {
+    if (d.elanDumpStateOutput.kind === 'PreEagerResolutionVersion') {
+        return [
+            '',
+            '-------------------------------------',
+            '',
+            `**Elan toolchains**: ${formatElanShowOutput(d.elanShowOutput)}`,
+        ].join('\n')
+    }
+    return formatElanDumpState(d.elanDumpStateOutput)
+}
+
 export function formatFullDiagnostics(d: FullDiagnostics): string {
     return [
         `**Operating system**: ${d.systemInfo.operatingSystem}`,
@@ -106,29 +179,31 @@ export function formatFullDiagnostics(d: FullDiagnostics): string {
         `**Elan**: ${formatElanVersionDiagnosis(d.elanVersionDiagnosis)}`,
         `**Lean**: ${formatLeanVersionDiagnosis(d.leanVersionDiagnosis)}`,
         `**Project**: ${formatProjectSetupDiagnosis(d.projectSetupDiagnosis)}`,
-        '',
-        '-------------------------------------',
-        '',
-        `**Elan toolchains**: ${formatElanShowOutput(d.elanShowOutput)}`,
+        formatElanInfo(d),
     ].join('\n')
 }
 
 export async function performFullDiagnosis(
     channel: OutputChannel,
     cwdUri: FileUri | undefined,
 ): Promise<FullDiagnostics> {
-    const showSetupInformationContext = 'Show Setup Information'
-    const diagnose = new SetupDiagnoser(channel, cwdUri)
+    const diagnose = new SetupDiagnoser({
+        channel,
+        cwdUri,
+        context: 'Show Setup Information',
+        toolchainUpdateMode: 'DoNotUpdate',
+    })
     return {
         systemInfo: diagnose.querySystemInformation(),
         vscodeVersionDiagnosis: diagnose.queryVSCodeVersion(),
         extensionVersion: diagnose.queryExtensionVersion(),
         isCurlAvailable: await diagnose.checkCurlAvailable(),
         isGitAvailable: await diagnose.checkGitAvailable(),
         elanVersionDiagnosis: await diagnose.elanVersion(),
-        leanVersionDiagnosis: await diagnose.leanVersion(showSetupInformationContext),
+        leanVersionDiagnosis: await diagnose.leanVersion(),
         projectSetupDiagnosis: await diagnose.projectSetup(),
         elanShowOutput: await diagnose.queryElanShow(),
+        elanDumpStateOutput: await diagnose.queryElanStateDumpWithoutNet(),
     }
 }
 
@@ -167,7 +242,12 @@ export class FullDiagnosticsProvider implements Disposable {
         const fullDiagnostics = await performFullDiagnosis(this.outputChannel, projectUri)
         const formattedFullDiagnostics = formatFullDiagnostics(fullDiagnostics)
         const copyToClipboardInput = 'Copy to Clipboard'
-        const choice = await displayNotificationWithInput('Information', formattedFullDiagnostics, copyToClipboardInput)
+        const choice = await displayNotificationWithInput(
+            'Information',
+            formattedFullDiagnostics,
+            [copyToClipboardInput],
+            'Close',
+        )
         if (choice === copyToClipboardInput) {
             await env.clipboard.writeText(formattedFullDiagnostics)
         }