From 39b52834f9b6a26a4258edc72668adb34cfa3984 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Thu, 23 May 2024 10:41:25 +0200 Subject: [PATCH] feat: check preconditions during project initialization (#450) This PR adds additional diagnostics when creating and cloning projects, as both of these commands depend on various external dependencies and can be used before opening a Lean file for the first time (i.e. the global setup diagnostics of #436 do not catch issues at this point). It also refactors the architecture in #436 to make it easier to add new kinds of diagnostics. The following aspects of the user's setup are checked when creating projects: 1. Whether Curl and Git are installed (Error; reference to setup guide) 2. Whether Elan is installed and reasonably up-to-date (Error if not installed as we use `lean +toolchain` for new project, modal warning if out-of-date; Elan installation / Elan update offered) 3. Whether some version of Lean can be found (Error) 4. Whether the toolchain associated with the new project is a Lean 3 toolchain (Error) 5. Whether the toolchain associated with the new project is using a Lean version from before the first Lean 4 stable release (Modal warning) 6. Whether some version of Lake can be found (Error) The following aspects of the user's setup are checked when cloning projects: 1. Before cloning: Whether Curl and Git are installed (Error; reference to setup guide) 2. Whether Elan is installed and reasonably up-to-date (Modal warning; Elan installation / Elan update offered) 3. Whether some version of Lean can be found (Error) 4. Whether the toolchain associated with the new project is a Lean 3 toolchain (Error) 5. Whether the toolchain associated with the new project is using a Lean version from before the first Lean 4 stable release (Modal warning) 6. Whether some version of Lake can be found (Error) --- .../src/diagnostics/fullDiagnostics.ts | 192 +++++++ .../src/diagnostics/setupDiagnoser.ts | 234 ++++++++ .../src/diagnostics/setupDiagnostics.ts | 224 ++++++++ vscode-lean4/src/diagnostics/setupNotifs.ts | 216 ++++++++ vscode-lean4/src/exports.ts | 2 +- vscode-lean4/src/extension.ts | 40 +- vscode-lean4/src/globalDiagnostics.ts | 162 ------ vscode-lean4/src/projectDiagnostics.ts | 149 ------ vscode-lean4/src/projectinit.ts | 100 ++-- vscode-lean4/src/utils/clientProvider.ts | 47 +- vscode-lean4/src/utils/configwatchservice.ts | 3 - vscode-lean4/src/utils/exturi.ts | 7 + vscode-lean4/src/utils/leanInstaller.ts | 79 ++- vscode-lean4/src/utils/notifs.ts | 108 +++- vscode-lean4/src/utils/setupDiagnostics.ts | 498 ------------------ 15 files changed, 1155 insertions(+), 906 deletions(-) create mode 100644 vscode-lean4/src/diagnostics/fullDiagnostics.ts create mode 100644 vscode-lean4/src/diagnostics/setupDiagnoser.ts create mode 100644 vscode-lean4/src/diagnostics/setupDiagnostics.ts create mode 100644 vscode-lean4/src/diagnostics/setupNotifs.ts delete mode 100644 vscode-lean4/src/globalDiagnostics.ts delete mode 100644 vscode-lean4/src/projectDiagnostics.ts delete mode 100644 vscode-lean4/src/utils/setupDiagnostics.ts diff --git a/vscode-lean4/src/diagnostics/fullDiagnostics.ts b/vscode-lean4/src/diagnostics/fullDiagnostics.ts new file mode 100644 index 000000000..bedb43488 --- /dev/null +++ b/vscode-lean4/src/diagnostics/fullDiagnostics.ts @@ -0,0 +1,192 @@ +import { Disposable, OutputChannel, TextDocument, commands, env, window, workspace } from 'vscode' +import { ExecutionExitCode, ExecutionResult } from '../utils/batch' +import { ExtUri, FileUri, extUriEquals, toExtUri } from '../utils/exturi' +import { displayInformationWithInput } from '../utils/notifs' +import { findLeanProjectRoot } from '../utils/projectInfo' +import { + ElanVersionDiagnosis, + LeanVersionDiagnosis, + ProjectSetupDiagnosis, + SetupDiagnoser, + SystemQueryResult, +} from './setupDiagnoser' + +export type FullDiagnostics = { + systemInfo: SystemQueryResult + isCurlAvailable: boolean + isGitAvailable: boolean + elanVersionDiagnosis: ElanVersionDiagnosis + leanVersionDiagnosis: LeanVersionDiagnosis + projectSetupDiagnosis: ProjectSetupDiagnosis + elanShowOutput: ExecutionResult +} + +function formatCommandOutput(cmdOutput: string): string { + return '\n```\n' + cmdOutput + '\n```' +} + +function formatElanVersionDiagnosis(d: ElanVersionDiagnosis): string { + switch (d.kind) { + case 'UpToDate': + return `Reasonably up-to-date (version: ${d.version.toString()})` + case 'Outdated': + return `Outdated (version: ${d.currentVersion.toString()}, recommended version: ${d.recommendedVersion.toString()})` + case 'ExecutionError': + return 'Execution error: ' + formatCommandOutput(d.message) + case 'NotInstalled': + return 'Not installed' + } +} + +function formatLeanVersionDiagnosis(d: LeanVersionDiagnosis): string { + switch (d.kind) { + case 'UpToDate': + return `Reasonably up-to-date (version: ${d.version})` + case 'IsLean3Version': + return `Lean 3 version (version: ${d.version})` + case 'IsAncientLean4Version': + return `Pre-stable-release Lean 4 version (version: ${d.version})` + case 'ExecutionError': + return 'Execution error: ' + formatCommandOutput(d.message) + case 'NotInstalled': + return 'Not installed' + } +} + +function formatProjectSetupDiagnosis(d: ProjectSetupDiagnosis): string { + switch (d.kind) { + case 'SingleFile': + return 'No open project' + case 'MissingLeanToolchain': + const parentProjectFolder = + d.parentProjectFolder === undefined + ? '' + : `(Valid Lean project in parent folder: ${d.parentProjectFolder.fsPath})` + return `Folder without lean-toolchain file (no valid Lean project) (path: ${d.folder.fsPath}) ${parentProjectFolder}` + case 'ValidProjectSetup': + return `Valid Lean project (path: ${d.projectFolder.fsPath})` + } +} + +function formatElanShowOutput(r: ExecutionResult): string { + if (r.exitCode === ExecutionExitCode.CannotLaunch) { + return 'Elan not installed' + } + if (r.exitCode === ExecutionExitCode.ExecutionError) { + return 'Execution error: ' + formatCommandOutput(r.combined) + } + return formatCommandOutput(r.stdout) +} + +export function formatFullDiagnostics(d: FullDiagnostics): string { + return [ + `**Operating system**: ${d.systemInfo.operatingSystem}`, + `**CPU architecture**: ${d.systemInfo.cpuArchitecture}`, + `**CPU model**: ${d.systemInfo.cpuModels}`, + `**Available RAM**: ${d.systemInfo.totalMemory}`, + '', + `**Curl installed**: ${d.isCurlAvailable}`, + `**Git installed**: ${d.isGitAvailable}`, + `**Elan**: ${formatElanVersionDiagnosis(d.elanVersionDiagnosis)}`, + `**Lean**: ${formatLeanVersionDiagnosis(d.leanVersionDiagnosis)}`, + `**Project**: ${formatProjectSetupDiagnosis(d.projectSetupDiagnosis)}`, + '', + '-------------------------------------', + '', + `**Elan toolchains**: ${formatElanShowOutput(d.elanShowOutput)}`, + ].join('\n') +} + +export async function performFullDiagnosis( + channel: OutputChannel, + cwdUri: FileUri | undefined, +): Promise { + const diagnose = new SetupDiagnoser(channel, cwdUri) + return { + systemInfo: diagnose.querySystemInformation(), + isCurlAvailable: await diagnose.checkCurlAvailable(), + isGitAvailable: await diagnose.checkGitAvailable(), + elanVersionDiagnosis: await diagnose.elanVersion(), + leanVersionDiagnosis: await diagnose.leanVersion(), + projectSetupDiagnosis: await diagnose.projectSetup(), + elanShowOutput: await diagnose.queryElanShow(), + } +} + +export class FullDiagnosticsProvider implements Disposable { + private subscriptions: Disposable[] = [] + private outputChannel: OutputChannel + // Under normal circumstances, we would use the last active `LeanClient` from `LeanClientProvider.getActiveClient()` + // to determine the document that the user is currently working on. + // However, when providing setup diagnostics, there might not be an active client due to errors in the user's setup, + // in which case we still want to provide adequate diagnostics. Hence, we track the last active lean document + // separately, regardless of whether there is an actual `LeanClient` managing it. + private lastActiveLeanDocumentUri: ExtUri | undefined + + constructor(outputChannel: OutputChannel) { + this.outputChannel = outputChannel + + if (window.activeTextEditor !== undefined) { + this.lastActiveLeanDocumentUri = FullDiagnosticsProvider.getLean4DocUri(window.activeTextEditor.document) + } + + window.onDidChangeActiveTextEditor(e => { + if (e === undefined) { + return + } + const docUri = FullDiagnosticsProvider.getLean4DocUri(e.document) + if (docUri === undefined) { + return + } + + this.lastActiveLeanDocumentUri = docUri + }, this.subscriptions) + workspace.onDidCloseTextDocument(doc => { + if (this.lastActiveLeanDocumentUri === undefined) { + return + } + + const docUri = FullDiagnosticsProvider.getLean4DocUri(doc) + if (docUri === undefined) { + return + } + + if (extUriEquals(docUri, this.lastActiveLeanDocumentUri)) { + this.lastActiveLeanDocumentUri = undefined + } + }, this.subscriptions) + + this.subscriptions.push( + commands.registerCommand('lean4.troubleshooting.showSetupInformation', () => + this.performAndDisplayFullDiagnosis(), + ), + ) + } + + async performAndDisplayFullDiagnosis() { + const projectUri = + this.lastActiveLeanDocumentUri !== undefined && this.lastActiveLeanDocumentUri.scheme === 'file' + ? await findLeanProjectRoot(this.lastActiveLeanDocumentUri) + : undefined + const fullDiagnostics = await performFullDiagnosis(this.outputChannel, projectUri) + const formattedFullDiagnostics = formatFullDiagnostics(fullDiagnostics) + const copyToClipboardInput = 'Copy to Clipboard' + const choice = await displayInformationWithInput(formattedFullDiagnostics, copyToClipboardInput) + if (choice === copyToClipboardInput) { + await env.clipboard.writeText(formattedFullDiagnostics) + } + } + + private static getLean4DocUri(doc: TextDocument): ExtUri | undefined { + if (doc.languageId !== 'lean4') { + return undefined + } + return toExtUri(doc.uri) + } + + dispose() { + for (const s of this.subscriptions) { + s.dispose() + } + } +} diff --git a/vscode-lean4/src/diagnostics/setupDiagnoser.ts b/vscode-lean4/src/diagnostics/setupDiagnoser.ts new file mode 100644 index 000000000..46433ea05 --- /dev/null +++ b/vscode-lean4/src/diagnostics/setupDiagnoser.ts @@ -0,0 +1,234 @@ +import * as os from 'os' +import { SemVer } from 'semver' +import { OutputChannel } from 'vscode' +import { ExecutionExitCode, ExecutionResult, batchExecute, batchExecuteWithProgress } from '../utils/batch' +import { FileUri } from '../utils/exturi' +import { checkParentFoldersForLeanProject, isValidLeanProject } from '../utils/projectInfo' + +export type SystemQueryResult = { + operatingSystem: string + cpuArchitecture: string + cpuModels: string + totalMemory: string +} + +export type VersionQueryResult = + | { kind: 'Success'; version: SemVer } + | { kind: 'CommandNotFound' } + | { kind: 'CommandError'; message: string } + | { kind: 'InvalidVersion'; versionResult: string } + +const recommendedElanVersion = new SemVer('3.1.1') + +export type ElanVersionDiagnosis = + | { kind: 'UpToDate'; version: SemVer } + | { kind: 'Outdated'; currentVersion: SemVer; recommendedVersion: SemVer } + | { kind: 'NotInstalled' } + | { kind: 'ExecutionError'; message: string } + +export type ProjectSetupDiagnosis = + | { kind: 'SingleFile' } + | { kind: 'MissingLeanToolchain'; folder: FileUri; parentProjectFolder: FileUri | undefined } + | { kind: 'ValidProjectSetup'; projectFolder: FileUri } + +export type LeanVersionDiagnosis = + | { kind: 'UpToDate'; version: SemVer } + | { kind: 'IsLean3Version'; version: SemVer } + | { kind: 'IsAncientLean4Version'; version: SemVer } + | { kind: 'NotInstalled' } + | { kind: 'ExecutionError'; message: string } + +export function versionQueryResult(executionResult: ExecutionResult, versionRegex: RegExp): VersionQueryResult { + if (executionResult.exitCode === ExecutionExitCode.CannotLaunch) { + return { kind: 'CommandNotFound' } + } + + if (executionResult.exitCode === ExecutionExitCode.ExecutionError) { + return { kind: 'CommandError', message: executionResult.combined } + } + + const match = versionRegex.exec(executionResult.stdout) + if (!match) { + return { kind: 'InvalidVersion', versionResult: executionResult.stdout } + } + + return { kind: 'Success', version: new SemVer(match[1]) } +} + +export function checkElanVersion(elanVersionResult: VersionQueryResult): ElanVersionDiagnosis { + switch (elanVersionResult.kind) { + case 'CommandNotFound': + return { kind: 'NotInstalled' } + + case 'CommandError': + return { kind: 'ExecutionError', message: elanVersionResult.message } + + case 'InvalidVersion': + return { + kind: 'ExecutionError', + message: `Invalid Elan version format: '${elanVersionResult.versionResult}'`, + } + + case 'Success': + if (elanVersionResult.version.compare(recommendedElanVersion) < 0) { + return { + kind: 'Outdated', + currentVersion: elanVersionResult.version, + recommendedVersion: recommendedElanVersion, + } + } + return { kind: 'UpToDate', version: elanVersionResult.version } + } +} + +export function checkLeanVersion(leanVersionResult: VersionQueryResult): LeanVersionDiagnosis { + if (leanVersionResult.kind === 'CommandNotFound') { + return { kind: 'NotInstalled' } + } + + if (leanVersionResult.kind === 'CommandError') { + return { + kind: 'ExecutionError', + message: leanVersionResult.message, + } + } + + if (leanVersionResult.kind === 'InvalidVersion') { + return { + kind: 'ExecutionError', + message: `Invalid Lean version format: '${leanVersionResult.versionResult}'`, + } + } + + const leanVersion = leanVersionResult.version + if (leanVersion.major === 3) { + return { kind: 'IsLean3Version', version: leanVersion } + } + + if (leanVersion.major === 4 && leanVersion.minor === 0 && leanVersion.prerelease.length > 0) { + return { kind: 'IsAncientLean4Version', version: leanVersion } + } + + return { kind: 'UpToDate', version: leanVersion } +} + +export class SetupDiagnoser { + readonly channel: OutputChannel + readonly cwdUri: FileUri | undefined + readonly toolchain: string | undefined + + constructor(channel: OutputChannel, cwdUri: FileUri | undefined, toolchain?: string | undefined) { + this.channel = channel + this.cwdUri = cwdUri + this.toolchain = toolchain + } + + async checkCurlAvailable(): Promise { + const curlVersionResult = await this.runSilently('curl', ['--version']) + return curlVersionResult.exitCode === ExecutionExitCode.Success + } + + async checkGitAvailable(): Promise { + const gitVersionResult = await this.runSilently('git', ['--version']) + return gitVersionResult.exitCode === ExecutionExitCode.Success + } + + async queryLakeVersion(): Promise { + const lakeVersionResult = await this.runLeanCommand('lake', ['--version'], 'Checking Lake version') + return versionQueryResult(lakeVersionResult, /version (\d+\.\d+\.\d+(\w|-)*)/) + } + + async checkLakeAvailable(): Promise { + const lakeVersionResult = await this.queryLakeVersion() + return lakeVersionResult.kind === 'Success' + } + + querySystemInformation(): SystemQueryResult { + const cpuModels = os.cpus().map(cpu => cpu.model) + const groupedCpuModels = new Map() + for (const cpuModel of cpuModels) { + const counter: number | undefined = groupedCpuModels.get(cpuModel) + if (counter === undefined) { + groupedCpuModels.set(cpuModel, 1) + } else { + groupedCpuModels.set(cpuModel, counter + 1) + } + } + const formattedCpuModels = Array.from(groupedCpuModels.entries()) + .map(([cpuModel, amount]) => `${amount} x ${cpuModel}`) + .join(', ') + + const totalMemory = (os.totalmem() / 1_000_000_000).toFixed(2) + + return { + operatingSystem: `${os.type()} (release: ${os.release()})`, + cpuArchitecture: os.arch(), + cpuModels: formattedCpuModels, + totalMemory: `${totalMemory} GB`, + } + } + + async queryLeanVersion(): Promise { + const leanVersionResult = await this.runLeanCommand('lean', ['--version'], 'Checking Lean version') + return versionQueryResult(leanVersionResult, /version (\d+\.\d+\.\d+(\w|-)*)/) + } + + async queryElanVersion(): Promise { + const elanVersionResult = await this.runSilently('elan', ['--version']) + return versionQueryResult(elanVersionResult, /elan (\d+\.\d+\.\d+)/) + } + + async queryElanShow(): Promise { + return await this.runSilently('elan', ['show']) + } + + async elanVersion(): Promise { + const elanVersionResult = await this.queryElanVersion() + return checkElanVersion(elanVersionResult) + } + + async projectSetup(): Promise { + if (this.cwdUri === undefined) { + return { kind: 'SingleFile' } + } + + if (!(await isValidLeanProject(this.cwdUri))) { + const parentProjectFolder: FileUri | undefined = await checkParentFoldersForLeanProject(this.cwdUri) + return { kind: 'MissingLeanToolchain', folder: this.cwdUri, parentProjectFolder } + } + + return { kind: 'ValidProjectSetup', projectFolder: this.cwdUri } + } + + async leanVersion(): Promise { + const leanVersionResult = await this.queryLeanVersion() + return checkLeanVersion(leanVersionResult) + } + + private async runSilently(executablePath: string, args: string[]): Promise { + return batchExecute(executablePath, args, this.cwdUri?.fsPath, { combined: this.channel }) + } + + private async runWithProgress(executablePath: string, args: string[], title: string): Promise { + return batchExecuteWithProgress(executablePath, args, title, { + cwd: this.cwdUri?.fsPath, + channel: this.channel, + }) + } + + private async runLeanCommand(executablePath: string, args: string[], title: string) { + const leanArgs = [...args] + if (this.toolchain !== undefined) { + leanArgs.unshift(`+${this.toolchain}`) + } + return await this.runWithProgress(executablePath, leanArgs, title) + } +} + +export function diagnose( + channel: OutputChannel, + cwdUri: FileUri | undefined, + toolchain?: string | undefined, +): SetupDiagnoser { + return new SetupDiagnoser(channel, cwdUri, toolchain) +} diff --git a/vscode-lean4/src/diagnostics/setupDiagnostics.ts b/vscode-lean4/src/diagnostics/setupDiagnostics.ts new file mode 100644 index 000000000..d19132a0f --- /dev/null +++ b/vscode-lean4/src/diagnostics/setupDiagnostics.ts @@ -0,0 +1,224 @@ +import { SemVer } from 'semver' +import { OutputChannel, commands } from 'vscode' +import { ExtUri, FileUri, extUriToCwdUri } from '../utils/exturi' +import { LeanInstaller } from '../utils/leanInstaller' +import { diagnose } from './setupDiagnoser' +import { + PreconditionCheckResult, + displayDependencySetupError, + displayElanOutdatedSetupWarning, + displayElanSetupError, + displayElanSetupWarning, + displaySetupError, + displaySetupErrorWithOutput, + displaySetupWarning, + displaySetupWarningWithOptionalInput, + displaySetupWarningWithOutput, + worstPreconditionViolation, +} from './setupNotifs' + +export async function checkAll( + ...checks: (() => Promise)[] +): Promise { + let worstViolation: PreconditionCheckResult = 'Fulfilled' + for (const check of checks) { + const result = await check() + worstViolation = worstPreconditionViolation(worstViolation, result) + if (worstViolation === 'Fatal') { + return 'Fatal' + } + } + return worstViolation +} + +const singleFileWarningMessage = `Lean 4 server is operating in restricted single file mode. +Please open a valid Lean 4 project containing a \'lean-toolchain\' file for full functionality. +Click the following link to learn how to set up or open Lean projects: [(Show Setup Guide)](command:lean4.setup.showSetupGuide)` + +const missingLeanToolchainWarningMessage = `Opened folder does not contain a valid Lean 4 project. +Please open a valid Lean 4 project containing a \'lean-toolchain\' file for full functionality. +Click the following link to learn how to set up or open Lean projects: [(Show Setup Guide)](command:lean4.setup.showSetupGuide)` + +const missingLeanToolchainWithParentProjectWarningMessage = (parentProjectFolder: FileUri) => + `Opened folder does not contain a valid Lean 4 project folder because it does not contain a 'lean-toolchain' file. +However, a valid Lean 4 project folder was found in one of the parent directories at '${parentProjectFolder.fsPath}'. +Open this project instead?` + +const lean3ProjectErrorMessage = (origin: string, projectVersion: SemVer) => + `${origin} is using Lean 3 (version: ${projectVersion.toString()}). +If you want to use Lean 3, disable this extension ('Extensions' in the left sidebar > Cog icon on 'lean4' > 'Disable') and install the 'lean' extension for Lean 3 support.` + +const ancientLean4ProjectWarningMessage = (origin: string, projectVersion: SemVer) => + `${origin} is using a Lean 4 version (${projectVersion.toString()}) from before the first Lean 4 stable release (4.0.0). +Pre-stable Lean 4 versions are increasingly less supported, so please consider updating to a newer Lean 4 version.` + +export async function checkAreDependenciesInstalled( + channel: OutputChannel, + cwdUri: FileUri | undefined, +): Promise { + const missingDeps = [] + if (!(await diagnose(channel, cwdUri).checkCurlAvailable())) { + missingDeps.push('curl') + } + if (!(await diagnose(channel, cwdUri).checkGitAvailable())) { + missingDeps.push('git') + } + if (missingDeps.length === 0) { + return 'Fulfilled' + } + displayDependencySetupError(missingDeps) + return 'Fatal' +} + +export async function checkIsLean4Installed( + installer: LeanInstaller, + cwdUri: FileUri | undefined, +): Promise { + const leanVersionResult = await diagnose(installer.getOutputChannel(), cwdUri).queryLeanVersion() + switch (leanVersionResult.kind) { + case 'Success': + return 'Fulfilled' + + case 'CommandError': + return displaySetupErrorWithOutput(`Error while checking Lean version: ${leanVersionResult.message}`) + + case 'InvalidVersion': + return displaySetupErrorWithOutput( + `Error while checking Lean version: 'lean --version' returned a version that could not be parsed: '${leanVersionResult.versionResult}'`, + ) + + case 'CommandNotFound': + return await displayElanSetupError(installer, 'Lean is not installed.') + } +} + +export async function checkIsElanUpToDate( + installer: LeanInstaller, + cwdUri: FileUri | undefined, + options: { elanMustBeInstalled: boolean; modal: boolean }, +): Promise { + const elanDiagnosis = await diagnose(installer.getOutputChannel(), cwdUri).elanVersion() + + switch (elanDiagnosis.kind) { + case 'NotInstalled': + if (options.elanMustBeInstalled) { + return await displayElanSetupError(installer, "Lean's version manager Elan is not installed.") + } + return await displayElanSetupWarning( + installer, + "Lean's version manager Elan is not installed. This means that the correct Lean 4 toolchain version of Lean 4 projects will not be selected or installed automatically.", + ) + + case 'ExecutionError': + return await displaySetupWarningWithOutput('Cannot determine Elan version: ' + elanDiagnosis.message, { + modal: options.modal, + }) + + case 'Outdated': + return await displayElanOutdatedSetupWarning( + installer, + elanDiagnosis.currentVersion, + elanDiagnosis.recommendedVersion, + ) + + case 'UpToDate': + return 'Fulfilled' + } +} + +export async function checkIsValidProjectFolder( + channel: OutputChannel, + folderUri: ExtUri, +): Promise { + const projectSetupDiagnosis = await diagnose(channel, extUriToCwdUri(folderUri)).projectSetup() + switch (projectSetupDiagnosis.kind) { + case 'SingleFile': + return await displaySetupWarning(singleFileWarningMessage) + + case 'MissingLeanToolchain': + const parentProjectFolder = projectSetupDiagnosis.parentProjectFolder + if (parentProjectFolder === undefined) { + return await displaySetupWarning(missingLeanToolchainWarningMessage) + } else { + return displaySetupWarningWithOptionalInput( + missingLeanToolchainWithParentProjectWarningMessage(parentProjectFolder), + 'Open Parent Directory Project', + // this kills the extension host + () => commands.executeCommand('vscode.openFolder', parentProjectFolder), + ) + } + + case 'ValidProjectSetup': + return 'Fulfilled' + } +} + +export async function checkIsLeanVersionUpToDate( + channel: OutputChannel, + folderUri: ExtUri, + options: { toolchainOverride?: string | undefined; modal: boolean }, +): Promise { + let origin: string + if (options.toolchainOverride !== undefined) { + origin = `Project toolchain '${options.toolchainOverride}'` + } else if (folderUri.scheme === 'untitled') { + origin = 'Opened file' + } else { + origin = 'Opened project' + } + const projectLeanVersionDiagnosis = await diagnose( + channel, + extUriToCwdUri(folderUri), + options.toolchainOverride, + ).leanVersion() + switch (projectLeanVersionDiagnosis.kind) { + case 'NotInstalled': + return displaySetupErrorWithOutput("Error while checking Lean version: 'lean' command was not found.") + + case 'ExecutionError': + return displaySetupErrorWithOutput( + `Error while checking Lean version: ${projectLeanVersionDiagnosis.message}`, + ) + + case 'IsLean3Version': + return displaySetupError(lean3ProjectErrorMessage(origin, projectLeanVersionDiagnosis.version)) + + case 'IsAncientLean4Version': + return await displaySetupWarning( + ancientLean4ProjectWarningMessage(origin, projectLeanVersionDiagnosis.version), + { + modal: options.modal, + }, + ) + + case 'UpToDate': + return 'Fulfilled' + } +} + +export async function checkIsLakeInstalledCorrectly( + channel: OutputChannel, + folderUri: ExtUri, + options: { toolchainOverride?: string | undefined }, +): Promise { + const lakeVersionResult = await diagnose( + channel, + extUriToCwdUri(folderUri), + options.toolchainOverride, + ).queryLakeVersion() + switch (lakeVersionResult.kind) { + case 'CommandNotFound': + return displaySetupErrorWithOutput("Error while checking Lake version: 'lake' command was not found.") + + case 'CommandError': + return displaySetupErrorWithOutput(`Error while checking Lake version: ${lakeVersionResult.message}`) + + case 'InvalidVersion': + return displaySetupErrorWithOutput( + `Error while checking Lake version: Invalid Lake version format: '${lakeVersionResult.versionResult}'`, + ) + + case 'Success': + return 'Fulfilled' + } +} diff --git a/vscode-lean4/src/diagnostics/setupNotifs.ts b/vscode-lean4/src/diagnostics/setupNotifs.ts new file mode 100644 index 000000000..ab4952528 --- /dev/null +++ b/vscode-lean4/src/diagnostics/setupNotifs.ts @@ -0,0 +1,216 @@ +import { SemVer } from 'semver' +import { shouldShowSetupWarnings } from '../config' +import { LeanInstaller } from '../utils/leanInstaller' +import { + displayError, + displayErrorWithInput, + displayErrorWithOptionalInput, + displayErrorWithOutput, + displayErrorWithSetupGuide, + displayModalWarning, + displayModalWarningWithOutput, + displayModalWarningWithSetupGuide, + displayWarning, + displayWarningWithInput, + displayWarningWithOptionalInput, + displayWarningWithOutput, + displayWarningWithSetupGuide, +} from '../utils/notifs' + +export type PreconditionCheckResult = 'Fulfilled' | 'Warning' | 'Fatal' + +export function preconditionCheckResultToSeverity(result: PreconditionCheckResult): 0 | 1 | 2 { + switch (result) { + case 'Fulfilled': + return 0 + case 'Warning': + return 1 + case 'Fatal': + return 2 + } +} + +export function severityToPreconditionCheckResult(severity: 0 | 1 | 2): PreconditionCheckResult { + switch (severity) { + case 0: + return 'Fulfilled' + case 1: + return 'Warning' + case 2: + return 'Fatal' + } +} + +export function worstPreconditionViolation(...results: PreconditionCheckResult[]): PreconditionCheckResult { + let worstViolation: PreconditionCheckResult = 'Fulfilled' + for (const r of results) { + if (preconditionCheckResultToSeverity(r) > preconditionCheckResultToSeverity(worstViolation)) { + worstViolation = r + } + } + return worstViolation +} + +export type SetupWarningOptions = { modal: true } | { modal: false; finalizer?: (() => void) | undefined } + +export function displaySetupError(message: string, finalizer?: (() => void) | undefined): PreconditionCheckResult { + displayError(message, finalizer) + return 'Fatal' +} + +export async function displaySetupErrorWithInput( + message: string, + ...items: T[] +): Promise { + return await displayErrorWithInput(message, ...items) +} + +export function displaySetupErrorWithOptionalInput( + message: string, + input: T, + action: () => void, + finalizer?: (() => void) | undefined, +): PreconditionCheckResult { + displayErrorWithOptionalInput(message, input, action, finalizer) + return 'Fatal' +} + +export function displaySetupErrorWithOutput( + message: string, + finalizer?: (() => void) | undefined, +): PreconditionCheckResult { + displayErrorWithOutput(message, finalizer) + return 'Fatal' +} + +export function displaySetupErrorWithSetupGuide( + message: string, + finalizer?: (() => void) | undefined, +): PreconditionCheckResult { + displayErrorWithSetupGuide(message, finalizer) + return 'Fatal' +} + +export function displayDependencySetupError(missingDeps: string[]): PreconditionCheckResult { + if (missingDeps.length === 0) { + throw new Error() + } + let missingDepMessage: string + if (missingDeps.length === 1) { + missingDepMessage = `One of Lean's dependencies ('${missingDeps.at(0)}') is missing` + } else { + missingDepMessage = `Multiple of Lean's dependencies (${missingDeps.map(dep => `'${dep}'`).join(', ')}) are missing` + } + + const errorMessage = `${missingDepMessage}. Please read the Setup Guide on how to install missing dependencies and set up Lean 4.` + displaySetupErrorWithSetupGuide(errorMessage) + return 'Fatal' +} + +export async function displayElanSetupError( + installer: LeanInstaller, + reason: string, +): Promise { + const isElanInstalled = await installer.displayInstallElanPrompt('Error', reason) + return isElanInstalled ? 'Fulfilled' : 'Fatal' +} + +export async function displayElanOutdatedSetupError( + installer: LeanInstaller, + currentVersion: SemVer, + recommendedVersion: SemVer, +): Promise { + const isElanUpToDate = await installer.displayUpdateElanPrompt('Error', currentVersion, recommendedVersion) + return isElanUpToDate ? 'Fulfilled' : 'Fatal' +} + +export async function displaySetupWarning( + message: string, + options: SetupWarningOptions = { modal: false }, +): Promise { + if (!shouldShowSetupWarnings()) { + return 'Warning' + } + if (options.modal) { + const choice = await displayModalWarning(message) + return choice === 'Proceed' ? 'Warning' : 'Fatal' + } + displayWarning(message, options.finalizer) + return 'Warning' +} + +export async function displaySetupWarningWithInput( + message: string, + ...items: T[] +): Promise { + if (!shouldShowSetupWarnings()) { + return undefined + } + return await displayWarningWithInput(message, ...items) +} + +export function displaySetupWarningWithOptionalInput( + message: string, + input: T, + action: () => void, + finalizer?: (() => void) | undefined, +): PreconditionCheckResult { + if (!shouldShowSetupWarnings()) { + return 'Warning' + } + displayWarningWithOptionalInput(message, input, action, finalizer) + return 'Warning' +} + +export async function displaySetupWarningWithOutput( + message: string, + options: SetupWarningOptions = { modal: false }, +): Promise { + if (!shouldShowSetupWarnings()) { + return 'Warning' + } + if (options.modal) { + const choice = await displayModalWarningWithOutput(message) + return choice === 'Proceed' ? 'Warning' : 'Fatal' + } + displayWarningWithOutput(message, options.finalizer) + return 'Warning' +} + +export async function displaySetupWarningWithSetupGuide( + message: string, + options: SetupWarningOptions = { modal: false }, +): Promise { + if (!shouldShowSetupWarnings()) { + return 'Warning' + } + if (options.modal) { + const choice = await displayModalWarningWithSetupGuide(message) + return choice === 'Proceed' ? 'Warning' : 'Fatal' + } + displayWarningWithSetupGuide(message, options.finalizer) + return 'Warning' +} + +export async function displayElanSetupWarning( + installer: LeanInstaller, + reason: string, +): Promise { + if (!shouldShowSetupWarnings()) { + return 'Warning' + } + const isElanInstalled = await installer.displayInstallElanPrompt('Warning', reason) + return isElanInstalled ? 'Fulfilled' : 'Warning' +} + +export async function displayElanOutdatedSetupWarning( + installer: LeanInstaller, + currentVersion: SemVer, + recommendedVersion: SemVer, +): Promise { + if (!shouldShowSetupWarnings()) { + return 'Warning' + } + const isElanUpToDate = await installer.displayUpdateElanPrompt('Warning', currentVersion, recommendedVersion) + return isElanUpToDate ? 'Fulfilled' : 'Warning' +} diff --git a/vscode-lean4/src/exports.ts b/vscode-lean4/src/exports.ts index 6cfc9179f..24af16291 100644 --- a/vscode-lean4/src/exports.ts +++ b/vscode-lean4/src/exports.ts @@ -1,11 +1,11 @@ import { OutputChannel } from 'vscode' +import { FullDiagnosticsProvider } from './diagnostics/fullDiagnostics' import { DocViewProvider } from './docview' import { InfoProvider } from './infoview' import { ProjectInitializationProvider } from './projectinit' import { ProjectOperationProvider } from './projectoperations' import { LeanClientProvider } from './utils/clientProvider' import { LeanInstaller } from './utils/leanInstaller' -import { FullDiagnosticsProvider } from './utils/setupDiagnostics' export interface AlwaysEnabledFeatures { docView: DocViewProvider diff --git a/vscode-lean4/src/extension.ts b/vscode-lean4/src/extension.ts index 614368600..50aacc825 100644 --- a/vscode-lean4/src/extension.ts +++ b/vscode-lean4/src/extension.ts @@ -3,9 +3,16 @@ import * as path from 'path' import { commands, Disposable, ExtensionContext, extensions, TextDocument, window, workspace } from 'vscode' import { AbbreviationFeature } from './abbreviation' import { getDefaultLeanVersion } from './config' +import { FullDiagnosticsProvider } from './diagnostics/fullDiagnostics' +import { + checkAll, + checkAreDependenciesInstalled, + checkIsElanUpToDate, + checkIsLean4Installed, +} from './diagnostics/setupDiagnostics' +import { PreconditionCheckResult } from './diagnostics/setupNotifs' import { DocViewProvider } from './docview' import { AlwaysEnabledFeatures, Exports, Lean4EnabledFeatures } from './exports' -import { checkLean4FeaturePreconditions } from './globalDiagnostics' import { InfoProvider } from './infoview' import { LeanClient } from './leanclient' import { ProjectInitializationProvider } from './projectinit' @@ -14,12 +21,11 @@ import { LeanTaskGutter } from './taskgutter' import { LeanClientProvider } from './utils/clientProvider' import { LeanConfigWatchService } from './utils/configwatchservice' import { PATH, setProcessEnvPATH } from './utils/envPath' -import { isExtUri, toExtUriOrError } from './utils/exturi' +import { FileUri, isExtUri, toExtUriOrError } from './utils/exturi' import { LeanInstaller } from './utils/leanInstaller' import { displayWarning } from './utils/notifs' import { PathExtensionProvider } from './utils/pathExtensionProvider' import { findLeanProjectRoot } from './utils/projectInfo' -import { FullDiagnosticsProvider, PreconditionCheckResult } from './utils/setupDiagnostics' async function setLeanFeatureSetActive(isActive: boolean) { await commands.executeCommand('setContext', 'lean4.isLeanFeatureSetActive', isActive) @@ -79,13 +85,16 @@ function activateAlwaysEnabledFeatures(context: ExtensionContext): AlwaysEnabled commands.registerCommand('lean4.troubleshooting.showOutput', () => outputChannel.show(true)), ) - const projectInitializationProvider = new ProjectInitializationProvider(outputChannel) - context.subscriptions.push(projectInitializationProvider) const defaultToolchain = getDefaultLeanVersion() - const installer = new LeanInstaller(outputChannel, defaultToolchain) + context.subscriptions.push( + commands.registerCommand('lean4.setup.installElan', () => + installer.displayInstallElanPrompt('Information', undefined), + ), + ) - context.subscriptions.push(commands.registerCommand('lean4.setup.installElan', () => installer.installElan())) + const projectInitializationProvider = new ProjectInitializationProvider(outputChannel, installer) + context.subscriptions.push(projectInitializationProvider) const checkForExtensionConflict = (doc: TextDocument) => { const isLean3ExtensionInstalled = extensions.getExtension('jroesch.lean') !== undefined @@ -114,6 +123,21 @@ function activateAbbreviationFeature(context: ExtensionContext, docView: DocView return abbrev } +async function checkLean4FeaturePreconditions( + installer: LeanInstaller, + cwdUri: FileUri | undefined, +): Promise { + return await checkAll( + () => checkAreDependenciesInstalled(installer.getOutputChannel(), cwdUri), + () => checkIsLean4Installed(installer, cwdUri), + () => + checkIsElanUpToDate(installer, cwdUri, { + elanMustBeInstalled: false, + modal: false, + }), + ) +} + async function activateLean4Features( context: ExtensionContext, installer: LeanInstaller, @@ -122,7 +146,7 @@ async function activateLean4Features( const docUri = toExtUriOrError(doc.uri) const cwd = docUri.scheme === 'file' ? await findLeanProjectRoot(docUri) : undefined const preconditionCheckResult = await checkLean4FeaturePreconditions(installer, cwd) - if (preconditionCheckResult === PreconditionCheckResult.Fatal) { + if (preconditionCheckResult === 'Fatal') { return undefined } diff --git a/vscode-lean4/src/globalDiagnostics.ts b/vscode-lean4/src/globalDiagnostics.ts deleted file mode 100644 index 5eb840878..000000000 --- a/vscode-lean4/src/globalDiagnostics.ts +++ /dev/null @@ -1,162 +0,0 @@ -import { OutputChannel } from 'vscode' -import { ExecutionExitCode, displayResultError } from './utils/batch' -import { elanSelfUpdate } from './utils/elan' -import { FileUri } from './utils/exturi' -import { LeanInstaller } from './utils/leanInstaller' -import { - PreconditionCheckResult, - SetupDiagnoser, - diagnose, - displaySetupErrorWithInput, - displaySetupErrorWithOutput, - displaySetupErrorWithSetupGuide, - displaySetupWarningWithInput, - displaySetupWarningWithOutput, -} from './utils/setupDiagnostics' - -class GlobalDiagnosticsProvider { - readonly installer: LeanInstaller - readonly channel: OutputChannel - readonly cwdUri: FileUri | undefined - - constructor(installer: LeanInstaller, cwdUri: FileUri | undefined) { - this.installer = installer - this.channel = installer.getOutputChannel() - this.cwdUri = cwdUri - } - - private diagnose(): SetupDiagnoser { - return diagnose(this.channel, this.cwdUri) - } - - async checkDependenciesAreInstalled(): Promise { - const isCurlInstalled = await this.diagnose().checkCurlAvailable() - const isGitInstalled = await this.diagnose().checkGitAvailable() - if (isCurlInstalled && isGitInstalled) { - return true - } - - let missingDepMessage: string - if (!isCurlInstalled && isGitInstalled) { - missingDepMessage = "One of Lean's dependencies ('curl') is missing" - } else if (isCurlInstalled && !isGitInstalled) { - missingDepMessage = "One of Lean's dependencies ('git') is missing" - } else { - missingDepMessage = "Both of Lean's dependencies ('curl' and 'git') are missing" - } - - const errorMessage = `${missingDepMessage}. Please read the Setup Guide on how to install missing dependencies and set up Lean 4.` - displaySetupErrorWithSetupGuide(errorMessage) - return false - } - - async checkLean4IsInstalled(): Promise { - const leanVersionResult = await this.diagnose().queryLeanVersion() - switch (leanVersionResult.kind) { - case 'Success': - return true - - case 'CommandError': - displaySetupErrorWithOutput(`Error while checking Lean version: ${leanVersionResult.message}`) - return false - - case 'InvalidVersion': - displaySetupErrorWithOutput( - `Error while checking Lean version: 'lean --version' returned a version that could not be parsed: '${leanVersionResult.versionResult}'`, - ) - return false - - case 'CommandNotFound': - if (!this.installer.getPromptUser()) { - // Used in tests - await this.installer.autoInstall() - return true - } - - const installElanItem = 'Install Elan and Lean 4' - const installElanChoice = await displaySetupErrorWithInput( - "Lean is not installed. Do you want to install Lean's version manager Elan and a recent stable version of Lean 4?", - installElanItem, - ) - if (installElanChoice === undefined) { - return false - } - await this.installer.installElan() - return true - } - } - - async checkElanIsUpToDate(): Promise { - const elanDiagnosis = await this.diagnose().elanVersion() - - switch (elanDiagnosis.kind) { - case 'NotInstalled': - const installElanItem = 'Install Elan and Lean 4' - const installElanChoice = await displaySetupWarningWithInput( - "Lean's version manager Elan is not installed. This means that the correct Lean 4 toolchain version of Lean 4 projects will not be selected or installed automatically. Do you want to install Elan and a recent stable version of Lean 4?", - installElanItem, - ) - if (installElanChoice === undefined) { - return false - } - await this.installer.installElan() - return true - - case 'ExecutionError': - displaySetupWarningWithOutput('Cannot determine Elan version: ' + elanDiagnosis.message) - return false - - case 'Outdated': - const updateElanItem = 'Update Elan' - const updateElanChoice = await displaySetupWarningWithInput( - `Lean's version manager Elan is outdated: the installed version is ${elanDiagnosis.currentVersion.toString()}, but a version of ${elanDiagnosis.recommendedVersion.toString()} is recommended. Do you want to update Elan?`, - updateElanItem, - ) - if (updateElanChoice === undefined) { - return false - } - if (elanDiagnosis.currentVersion.compare('3.1.0') === 0) { - // `elan self update` was broken in elan 3.1.0, so we need to take a different approach to updating elan here. - const installElanResult = await this.installer.installElan() - return installElanResult !== 'InstallationFailed' - } - const elanSelfUpdateResult = await elanSelfUpdate(this.channel) - if (elanSelfUpdateResult.exitCode !== ExecutionExitCode.Success) { - displayResultError( - elanSelfUpdateResult, - "Cannot update Elan. If you suspect that this is due to the way that you have set up Elan (e.g. from a package repository that ships an outdated version of Elan), you can disable these warnings using the 'Lean4: Show Setup Warnings' setting under 'File' > 'Preferences' > 'Settings'.", - ) - return false - } - - return true - - case 'UpToDate': - return true - } - } -} - -export async function checkLean4FeaturePreconditions( - installer: LeanInstaller, - cwdUri: FileUri | undefined, -): Promise { - const diagnosticsProvider = new GlobalDiagnosticsProvider(installer, cwdUri) - - const areDependenciesInstalled = await diagnosticsProvider.checkDependenciesAreInstalled() - if (!areDependenciesInstalled) { - return PreconditionCheckResult.Fatal - } - - const isLean4Installed = await diagnosticsProvider.checkLean4IsInstalled() - if (!isLean4Installed) { - return PreconditionCheckResult.Fatal - } - - const isElanUpToDate = await diagnosticsProvider.checkElanIsUpToDate() - if (!isElanUpToDate) { - return PreconditionCheckResult.Warning - } - - return PreconditionCheckResult.Fulfilled -} diff --git a/vscode-lean4/src/projectDiagnostics.ts b/vscode-lean4/src/projectDiagnostics.ts deleted file mode 100644 index c32966082..000000000 --- a/vscode-lean4/src/projectDiagnostics.ts +++ /dev/null @@ -1,149 +0,0 @@ -import { SemVer } from 'semver' -import { OutputChannel, commands } from 'vscode' -import { ExtUri, FileUri } from './utils/exturi' -import { willUseLakeServer } from './utils/projectInfo' -import { - PreconditionCheckResult, - SetupDiagnoser, - diagnose, - displaySetupError, - displaySetupErrorWithOutput, - displaySetupWarning, - displaySetupWarningWithOptionalInput, - worstPreconditionViolation, -} from './utils/setupDiagnostics' - -const singleFileWarningMessage = `Lean 4 server is operating in restricted single file mode. -Please open a valid Lean 4 project containing a \'lean-toolchain\' file for full functionality. -Click the following link to learn how to set up or open Lean projects: [(Show Setup Guide)](command:lean4.setup.showSetupGuide)` - -const missingLeanToolchainWarningMessage = `Opened folder does not contain a valid Lean 4 project. -Please open a valid Lean 4 project containing a \'lean-toolchain\' file for full functionality. -Click the following link to learn how to set up or open Lean projects: [(Show Setup Guide)](command:lean4.setup.showSetupGuide)` - -const missingLeanToolchainWithParentProjectWarningMessage = (parentProjectFolder: FileUri) => - `Opened folder does not contain a valid Lean 4 project folder because it does not contain a 'lean-toolchain' file. -However, a valid Lean 4 project folder was found in one of the parent directories at '${parentProjectFolder.fsPath}'. -Open this project instead?` - -const lean3ProjectErrorMessage = (projectVersion: SemVer) => - `Opened file is using Lean 3 (version: ${projectVersion.toString()}). -If you want to use Lean 3, disable this extension ('Extensions' in the left sidebar > Cog icon on 'lean4' > 'Disable') and install the 'lean' extension for Lean 3 support.` - -const ancientLean4ProjectWarningMessage = (projectVersion: SemVer) => - `Opened file is using a Lean 4 version (${projectVersion.toString()}) from before the first Lean 4 stable release (4.0.0). -Pre-stable Lean 4 versions are increasingly less supported, so please consider updating to a newer Lean 4 version.` - -class ProjectDiagnosticsProvider { - readonly channel: OutputChannel - readonly folderUri: ExtUri - - constructor(channel: OutputChannel, folderUri: ExtUri) { - this.channel = channel - this.folderUri = folderUri - } - - private diagnose(): SetupDiagnoser { - const cwd = this.folderUri.scheme === 'file' ? this.folderUri : undefined - return diagnose(this.channel, cwd) - } - - async checkIsValidProjectFolder(): Promise { - const projectSetupDiagnosis = await this.diagnose().projectSetup() - switch (projectSetupDiagnosis.kind) { - case 'SingleFile': - displaySetupWarning(singleFileWarningMessage) - return false - - case 'MissingLeanToolchain': - const parentProjectFolder = projectSetupDiagnosis.parentProjectFolder - if (parentProjectFolder === undefined) { - displaySetupWarning(missingLeanToolchainWarningMessage) - } else { - displaySetupWarningWithOptionalInput( - missingLeanToolchainWithParentProjectWarningMessage(parentProjectFolder), - 'Open Parent Directory Project', - // this kills the extension host - () => commands.executeCommand('vscode.openFolder', parentProjectFolder), - ) - } - return false - - case 'ValidProjectSetup': - return true - } - } - - async checkIsLeanVersionUpToDate(): Promise { - const projectLeanVersionDiagnosis = await this.diagnose().projectLeanVersion() - switch (projectLeanVersionDiagnosis.kind) { - case 'NotInstalled': - displaySetupErrorWithOutput("Error while checking Lean version: 'lean' command was not found.") - return PreconditionCheckResult.Fatal - - case 'ExecutionError': - displaySetupErrorWithOutput(`Error while checking Lean version: ${projectLeanVersionDiagnosis.message}`) - return PreconditionCheckResult.Fatal - - case 'IsLean3Version': - void displaySetupError(lean3ProjectErrorMessage(projectLeanVersionDiagnosis.version)) - return PreconditionCheckResult.Fatal - - case 'IsAncientLean4Version': - displaySetupWarning(ancientLean4ProjectWarningMessage(projectLeanVersionDiagnosis.version)) - return PreconditionCheckResult.Warning - - case 'UpToDate': - return PreconditionCheckResult.Fulfilled - } - } - - async checkIsLakeInstalledCorrectly(): Promise { - if (!(await willUseLakeServer(this.folderUri))) { - return PreconditionCheckResult.Fulfilled - } - - const lakeVersionResult = await this.diagnose().queryLakeVersion() - switch (lakeVersionResult.kind) { - case 'CommandNotFound': - displaySetupErrorWithOutput("Error while checking Lake version: 'lake' command was not found.") - return PreconditionCheckResult.Fatal - - case 'CommandError': - displaySetupErrorWithOutput(`Error while checking Lake version: ${lakeVersionResult.message}`) - return PreconditionCheckResult.Fatal - - case 'InvalidVersion': - displaySetupErrorWithOutput( - `Error while checking Lake version: Invalid Lake version format: '${lakeVersionResult.versionResult}'`, - ) - return PreconditionCheckResult.Fatal - - case 'Success': - return PreconditionCheckResult.Fulfilled - } - } -} - -export async function checkLean4ProjectPreconditions( - channel: OutputChannel, - folderUri: ExtUri, -): Promise { - const diagnosticsProvider = new ProjectDiagnosticsProvider(channel, folderUri) - - const isValidProjectFolder = await diagnosticsProvider.checkIsValidProjectFolder() - const validProjectFolderCheckResult = isValidProjectFolder - ? PreconditionCheckResult.Fulfilled - : PreconditionCheckResult.Warning - - const leanVersionCheckResult = await diagnosticsProvider.checkIsLeanVersionUpToDate() - - const leanProjectCheckResult = worstPreconditionViolation(validProjectFolderCheckResult, leanVersionCheckResult) - if (leanProjectCheckResult === PreconditionCheckResult.Fatal) { - return PreconditionCheckResult.Fatal - } - - const lakeVersionCheckResult = await diagnosticsProvider.checkIsLakeInstalledCorrectly() - - return worstPreconditionViolation(leanProjectCheckResult, lakeVersionCheckResult) -} diff --git a/vscode-lean4/src/projectinit.ts b/vscode-lean4/src/projectinit.ts index ef5ee2dcf..2e15b5764 100644 --- a/vscode-lean4/src/projectinit.ts +++ b/vscode-lean4/src/projectinit.ts @@ -1,4 +1,12 @@ import { commands, Disposable, OutputChannel, SaveDialogOptions, Uri, window, workspace } from 'vscode' +import { + checkAll, + checkAreDependenciesInstalled, + checkIsElanUpToDate, + checkIsLakeInstalledCorrectly, + checkIsLeanVersionUpToDate, +} from './diagnostics/setupDiagnostics' +import { PreconditionCheckResult } from './diagnostics/setupNotifs' import { batchExecute, batchExecuteWithProgress, @@ -6,17 +14,49 @@ import { ExecutionExitCode, ExecutionResult, } from './utils/batch' -import { FileUri } from './utils/exturi' +import { ExtUri, extUriToCwdUri, FileUri } from './utils/exturi' import { lake } from './utils/lake' +import { LeanInstaller } from './utils/leanInstaller' import { displayError, displayInformationWithInput } from './utils/notifs' import { checkParentFoldersForLeanProject, isValidLeanProject } from './utils/projectInfo' -import { diagnose } from './utils/setupDiagnostics' import path = require('path') +async function checkCreateLean4ProjectPreconditions( + installer: LeanInstaller, + folderUri: ExtUri, + projectToolchain: string, +): Promise { + const channel = installer.getOutputChannel() + const cwdUri = extUriToCwdUri(folderUri) + return await checkAll( + () => checkAreDependenciesInstalled(channel, cwdUri), + () => checkIsElanUpToDate(installer, cwdUri, { elanMustBeInstalled: true, modal: true }), + () => checkIsLeanVersionUpToDate(channel, folderUri, { toolchainOverride: projectToolchain, modal: true }), + () => checkIsLakeInstalledCorrectly(channel, folderUri, { toolchainOverride: projectToolchain }), + ) +} + +async function checkPreCloneLean4ProjectPreconditions(channel: OutputChannel, cwdUri: FileUri | undefined) { + return await checkAll(() => checkAreDependenciesInstalled(channel, cwdUri)) +} + +async function checkPostCloneLean4ProjectPreconditions(installer: LeanInstaller, folderUri: ExtUri) { + const channel = installer.getOutputChannel() + const cwdUri = extUriToCwdUri(folderUri) + return await checkAll( + () => checkIsElanUpToDate(installer, cwdUri, { elanMustBeInstalled: false, modal: true }), + () => checkIsLeanVersionUpToDate(channel, folderUri, { modal: true }), + () => checkIsLakeInstalledCorrectly(channel, folderUri, {}), + ) +} + export class ProjectInitializationProvider implements Disposable { private subscriptions: Disposable[] = [] - constructor(private channel: OutputChannel) { + constructor( + private channel: OutputChannel, + private installer: LeanInstaller, + ) { this.subscriptions.push( commands.registerCommand('lean4.project.createStandaloneProject', () => this.createStandaloneProject()), commands.registerCommand('lean4.project.createMathlibProject', () => this.createMathlibProject()), @@ -102,7 +142,12 @@ export class ProjectInitializationProvider implements Disposable { await workspace.fs.createDirectory(projectFolder.asUri()) - if ((await this.checkSetupDeps(projectFolder)) === 'IncompleteSetup') { + const preconditionCheckResult = await checkCreateLean4ProjectPreconditions( + this.installer, + projectFolder, + toolchain, + ) + if (preconditionCheckResult === 'Fatal') { return 'DidNotComplete' } @@ -205,10 +250,6 @@ Open this project instead?` } private async cloneProject() { - if ((await this.checkGit()) === 'GitNotInstalled') { - return - } - const projectUri: string | undefined = await window.showInputBox({ title: 'URL Input', value: 'https://github.com/leanprover-community/mathlib4', @@ -226,6 +267,16 @@ Open this project instead?` return } + await workspace.fs.createDirectory(projectFolder.asUri()) + + const preCloneCheckResult = await checkPreCloneLean4ProjectPreconditions( + this.installer.getOutputChannel(), + projectFolder, + ) + if (preCloneCheckResult === 'Fatal') { + return + } + const result: ExecutionResult = await batchExecuteWithProgress( 'git', ['clone', projectUri, projectFolder.fsPath], @@ -240,7 +291,8 @@ Open this project instead?` return } - if ((await this.checkLake(projectFolder)) === 'LakeNotInstalled') { + const postCloneCheckResult = await checkPostCloneLean4ProjectPreconditions(this.installer, projectFolder) + if (postCloneCheckResult === 'Fatal') { return } @@ -280,36 +332,6 @@ Open this project instead?` } } - private async checkSetupDeps(projectFolder: FileUri): Promise<'CompleteSetup' | 'IncompleteSetup'> { - if ((await this.checkGit(projectFolder)) === 'GitNotInstalled') { - return 'IncompleteSetup' - } - if ((await this.checkLake(projectFolder)) === 'LakeNotInstalled') { - return 'IncompleteSetup' - } - return 'CompleteSetup' - } - - private async checkGit(projectFolder?: FileUri | undefined): Promise<'GitInstalled' | 'GitNotInstalled'> { - if (!(await diagnose(this.channel, projectFolder).checkGitAvailable())) { - const message = `Git is not installed. Lean uses Git to download and install specific versions of Lean packages. -Click the following link to learn how to install Git: [(Show Setup Guide)](command:lean4.setup.showSetupGuide)` - displayError(message) - return 'GitNotInstalled' - } - return 'GitInstalled' - } - - private async checkLake(projectFolder: FileUri): Promise<'LakeInstalled' | 'LakeNotInstalled'> { - if (!(await diagnose(this.channel, projectFolder).checkLakeAvailable())) { - const message = `Lean's package manager Lake is not installed. This likely means that Lean itself is also not installed. -Click the following link to learn how to install Lean: [(Show Setup Guide)](command:lean4.setup.showSetupGuide)` - displayError(message) - return 'LakeNotInstalled' - } - return 'LakeInstalled' - } - dispose() { for (const s of this.subscriptions) { s.dispose() diff --git a/vscode-lean4/src/utils/clientProvider.ts b/vscode-lean4/src/utils/clientProvider.ts index 6bc8988cb..feafb50aa 100644 --- a/vscode-lean4/src/utils/clientProvider.ts +++ b/vscode-lean4/src/utils/clientProvider.ts @@ -1,13 +1,34 @@ import { LeanFileProgressProcessingInfo, ServerStoppedReason } from '@leanprover/infoview-api' import { Disposable, EventEmitter, OutputChannel, TextDocument, TextEditor, commands, window, workspace } from 'vscode' +import { + checkAll, + checkIsLakeInstalledCorrectly, + checkIsLeanVersionUpToDate, + checkIsValidProjectFolder, +} from '../diagnostics/setupDiagnostics' +import { PreconditionCheckResult } from '../diagnostics/setupNotifs' import { LeanClient } from '../leanclient' -import { checkLean4ProjectPreconditions } from '../projectDiagnostics' import { ExtUri, FileUri, UntitledUri, getWorkspaceFolderUri, toExtUri } from './exturi' import { LeanInstaller } from './leanInstaller' import { logger } from './logger' import { displayError } from './notifs' -import { findLeanProjectRoot } from './projectInfo' -import { PreconditionCheckResult } from './setupDiagnostics' +import { findLeanProjectRoot, willUseLakeServer } from './projectInfo' + +async function checkLean4ProjectPreconditions( + channel: OutputChannel, + folderUri: ExtUri, +): Promise { + return await checkAll( + () => checkIsValidProjectFolder(channel, folderUri), + () => checkIsLeanVersionUpToDate(channel, folderUri, { modal: false }), + async () => { + if (!(await willUseLakeServer(folderUri))) { + return 'Fulfilled' + } + return await checkIsLakeInstalledCorrectly(channel, folderUri, {}) + }, + ) +} // This class ensures we have one LeanClient per folder. export class LeanClientProvider implements Disposable { @@ -60,7 +81,7 @@ export class LeanClientProvider implements Disposable { workspace.onDidChangeWorkspaceFolders(event => { // Remove all clients that are not referenced by any folder anymore - if (!event.removed) { + if (event.removed.length === 0) { return } this.clients.forEach((client, key) => { @@ -99,7 +120,7 @@ export class LeanClientProvider implements Disposable { const projectUri = await findLeanProjectRoot(uri) const preconditionCheckResult = await checkLean4ProjectPreconditions(this.outputChannel, projectUri) - if (preconditionCheckResult !== PreconditionCheckResult.Fatal) { + if (preconditionCheckResult !== 'Fatal') { logger.log('[ClientProvider] got lean version 4') const [cached, client] = await this.ensureClient(uri) if (cached && client) { @@ -172,16 +193,12 @@ export class LeanClientProvider implements Disposable { return } - try { - const [_, client] = await this.ensureClient(uri) - if (!client) { - return - } - - await client.openLean4Document(document) - } catch (e) { - logger.log(`[ClientProvider] ### Error opening document: ${e}`) + const [_, client] = await this.ensureClient(uri) + if (!client) { + return } + + await client.openLean4Document(document) } // Find the client for a given document. @@ -234,7 +251,7 @@ export class LeanClientProvider implements Disposable { this.pending.set(key, true) const preconditionCheckResult = await checkLean4ProjectPreconditions(this.outputChannel, folderUri) - if (preconditionCheckResult === PreconditionCheckResult.Fatal) { + if (preconditionCheckResult === 'Fatal') { this.pending.delete(key) return [false, undefined] } diff --git a/vscode-lean4/src/utils/configwatchservice.ts b/vscode-lean4/src/utils/configwatchservice.ts index d46717e74..72181c7a7 100644 --- a/vscode-lean4/src/utils/configwatchservice.ts +++ b/vscode-lean4/src/utils/configwatchservice.ts @@ -79,9 +79,6 @@ export class LeanConfigWatchService implements Disposable { // we compare the contents just to be sure and normalize whitespace so that // just adding a new line doesn't trigger the prompt. const [packageUri, _] = await findLeanProjectRootInfo(fileUri) - if (!packageUri) { - return - } const contents = await this.readWhitespaceNormalized(fileUri) let existing: string | undefined diff --git a/vscode-lean4/src/utils/exturi.ts b/vscode-lean4/src/utils/exturi.ts index 391198dc6..cb94e7c38 100644 --- a/vscode-lean4/src/utils/exturi.ts +++ b/vscode-lean4/src/utils/exturi.ts @@ -157,3 +157,10 @@ export function extUriEquals(a: ExtUri, b: ExtUri): boolean { } return false } + +export function extUriToCwdUri(uri: ExtUri): FileUri | undefined { + if (uri.scheme === 'untitled') { + return undefined + } + return uri +} diff --git a/vscode-lean4/src/utils/leanInstaller.ts b/vscode-lean4/src/utils/leanInstaller.ts index f80d11f01..31cafec9e 100644 --- a/vscode-lean4/src/utils/leanInstaller.ts +++ b/vscode-lean4/src/utils/leanInstaller.ts @@ -1,9 +1,16 @@ +import { SemVer } from 'semver' import { EventEmitter, OutputChannel, TerminalOptions, window } from 'vscode' import { getPowerShellPath, isRunningTest } from '../config' -import { batchExecute } from './batch' +import { ExecutionExitCode, batchExecute, displayResultError } from './batch' +import { elanSelfUpdate } from './elan' import { ExtUri, FileUri } from './exturi' import { logger } from './logger' -import { displayError, displayErrorWithOptionalInput } from './notifs' +import { + NotificationSeverity, + displayError, + displayErrorWithOptionalInput, + displayNotificationWithInput, +} from './notifs' export class LeanVersion { version: string @@ -142,13 +149,77 @@ export class LeanInstaller { } } - async autoInstall(): Promise { + async displayInstallElanPrompt(severity: NotificationSeverity, reason: string | undefined): Promise { + if (!this.getPromptUser()) { + // Used in tests + await this.autoInstall() + return true + } + + const reasonPrefix = reason ? reason + ' ' : '' + const installElanItem = 'Install Elan and Lean 4' + const installElanChoice = await displayNotificationWithInput( + severity, + reasonPrefix + "Do you want to install Lean's version manager Elan and a recent stable version of Lean 4?", + installElanItem, + ) + if (installElanChoice === undefined) { + return false + } + + await this.installElan() + return true + } + + async displayUpdateElanPrompt( + severity: NotificationSeverity, + currentVersion: SemVer, + recommendedVersion: SemVer, + ): Promise { + const updateElanItem = 'Update Elan' + const updateElanChoice = await displayNotificationWithInput( + severity, + `Lean's version manager Elan is outdated: the installed version is ${currentVersion.toString()}, but a version of ${recommendedVersion.toString()} is recommended. Do you want to update Elan?`, + updateElanItem, + ) + if (updateElanChoice === undefined) { + return false + } + + if (currentVersion.compare('3.1.0') === 0) { + // `elan self update` was broken in elan 3.1.0, so we need to take a different approach to updating elan here. + const installElanResult = await this.installElan() + switch (installElanResult) { + case 'PendingInstallation': + displayError('Elan is already being installed. Please wait until the installation has finished.') + return false + case 'InstallationFailed': + displayError('Cannot install Elan due to an error. Check the terminal for details.') + return false + case 'Success': + return true + } + } + + const elanSelfUpdateResult = await elanSelfUpdate(this.outputChannel) + if (elanSelfUpdateResult.exitCode !== ExecutionExitCode.Success) { + displayResultError( + elanSelfUpdateResult, + "Cannot update Elan. If you suspect that this is due to the way that you have set up Elan (e.g. from a package repository that ships an outdated version of Elan), you can disable these warnings using the 'Lean4: Show Setup Warnings' setting under 'File' > 'Preferences' > 'Settings'.", + ) + return false + } + + return true + } + + private async autoInstall(): Promise { logger.log('[LeanInstaller] Installing Elan ...') await this.installElan() logger.log('[LeanInstaller] Elan installed') } - async installElan(): Promise<'Success' | 'InstallationFailed' | 'PendingInstallation'> { + private async installElan(): Promise<'Success' | 'InstallationFailed' | 'PendingInstallation'> { if (this.installing) { displayError('Elan is already being installed.') return 'PendingInstallation' diff --git a/vscode-lean4/src/utils/notifs.ts b/vscode-lean4/src/utils/notifs.ts index 4b290ff4e..3ab76c8da 100644 --- a/vscode-lean4/src/utils/notifs.ts +++ b/vscode-lean4/src/utils/notifs.ts @@ -7,38 +7,55 @@ import { MessageOptions, commands, window } from 'vscode' // - Notifications with optional input should never block the extension // - Notifications that block the extension must be modal +export type NotificationSeverity = 'Information' | 'Warning' | 'Error' + type Notification = ( message: string, options: MessageOptions, ...items: T[] ) => Thenable -function displayNotification(notif: Notification, message: string, finalizer?: (() => void) | undefined) { +function toNotif(severity: NotificationSeverity): Notification { + switch (severity) { + case 'Information': + return window.showInformationMessage + case 'Warning': + return window.showWarningMessage + case 'Error': + return window.showErrorMessage + } +} + +export function displayNotification( + severity: NotificationSeverity, + message: string, + finalizer?: (() => void) | undefined, +) { void (async () => { - await notif(message, {}) + await toNotif(severity)(message, {}) if (finalizer) { finalizer() } })() } -async function displayNotificationWithInput( - notif: Notification, +export async function displayNotificationWithInput( + severity: NotificationSeverity, message: string, ...items: T[] ): Promise { - return await notif(message, { modal: true }, ...items) + return await toNotif(severity)(message, { modal: true }, ...items) } -function displayNotificationWithOptionalInput( - notif: Notification, +export function displayNotificationWithOptionalInput( + severity: NotificationSeverity, message: string, input: T, action: () => void, finalizer?: (() => void) | undefined, ) { void (async () => { - const choice = await notif(message, {}, input) + const choice = await toNotif(severity)(message, {}, input) if (choice === input) { action() } @@ -48,9 +65,13 @@ function displayNotificationWithOptionalInput( })() } -function displayNotificationWithOutput(notif: Notification, message: string, finalizer?: (() => void) | undefined) { +export function displayNotificationWithOutput( + severity: NotificationSeverity, + message: string, + finalizer?: (() => void) | undefined, +) { displayNotificationWithOptionalInput( - notif, + severity, message, 'Show Output', () => commands.executeCommand('lean4.troubleshooting.showOutput'), @@ -58,9 +79,13 @@ function displayNotificationWithOutput(notif: Notification, message: string, fin ) } -function displayNotificationWithSetupGuide(notif: Notification, message: string, finalizer?: (() => void) | undefined) { +export function displayNotificationWithSetupGuide( + severity: NotificationSeverity, + message: string, + finalizer?: (() => void) | undefined, +) { displayNotificationWithOptionalInput( - notif, + severity, message, 'Open Setup Guide', () => commands.executeCommand('lean4.setup.showSetupGuide'), @@ -69,11 +94,11 @@ function displayNotificationWithSetupGuide(notif: Notification, message: string, } export function displayError(message: string, finalizer?: (() => void) | undefined) { - displayNotification(window.showErrorMessage, message, finalizer) + displayNotification('Error', message, finalizer) } export async function displayErrorWithInput(message: string, ...items: T[]): Promise { - return await displayNotificationWithInput(window.showErrorMessage, message, ...items) + return await displayNotificationWithInput('Error', message, ...items) } export function displayErrorWithOptionalInput( @@ -82,26 +107,31 @@ export function displayErrorWithOptionalInput( action: () => void, finalizer?: (() => void) | undefined, ) { - displayNotificationWithOptionalInput(window.showErrorMessage, message, input, action, finalizer) + displayNotificationWithOptionalInput('Error', message, input, action, finalizer) } export function displayErrorWithOutput(message: string, finalizer?: (() => void) | undefined) { - displayNotificationWithOutput(window.showErrorMessage, message, finalizer) + displayNotificationWithOutput('Error', message, finalizer) } export function displayErrorWithSetupGuide(message: string, finalizer?: (() => void) | undefined) { - displayNotificationWithSetupGuide(window.showErrorMessage, message, finalizer) + displayNotificationWithSetupGuide('Error', message, finalizer) } export function displayWarning(message: string, finalizer?: (() => void) | undefined) { - displayNotification(window.showWarningMessage, message, finalizer) + displayNotification('Warning', message, finalizer) +} + +export async function displayModalWarning(message: string): Promise<'Proceed' | 'Abort'> { + const choice = await window.showWarningMessage(message, { modal: true }, 'Proceed Regardless') + return choice === 'Proceed Regardless' ? 'Proceed' : 'Abort' } export async function displayWarningWithInput( message: string, ...items: T[] ): Promise { - return await displayNotificationWithInput(window.showWarningMessage, message, ...items) + return await displayNotificationWithInput('Warning', message, ...items) } export function displayWarningWithOptionalInput( @@ -110,26 +140,50 @@ export function displayWarningWithOptionalInput( action: () => void, finalizer?: (() => void) | undefined, ) { - displayNotificationWithOptionalInput(window.showWarningMessage, message, input, action, finalizer) + displayNotificationWithOptionalInput('Warning', message, input, action, finalizer) } export function displayWarningWithOutput(message: string, finalizer?: (() => void) | undefined) { - displayNotificationWithOutput(window.showWarningMessage, message, finalizer) + displayNotificationWithOutput('Warning', message, finalizer) +} + +export async function displayModalWarningWithOutput(message: string): Promise<'Proceed' | 'Abort'> { + const choice = await window.showWarningMessage(message, 'Show Output', 'Proceed Regardless') + if (choice === undefined) { + return 'Abort' + } + if (choice === 'Proceed Regardless') { + return 'Proceed' + } + await commands.executeCommand('lean4.troubleshooting.showOutput') + return 'Abort' } export function displayWarningWithSetupGuide(message: string, finalizer?: (() => void) | undefined) { - displayNotificationWithSetupGuide(window.showWarningMessage, message, finalizer) + displayNotificationWithSetupGuide('Warning', message, finalizer) +} + +export async function displayModalWarningWithSetupGuide(message: string): Promise<'Proceed' | 'Abort'> { + const choice = await window.showWarningMessage(message, 'Open Setup Guide', 'Proceed Regardless') + if (choice === undefined) { + return 'Abort' + } + if (choice === 'Proceed Regardless') { + return 'Proceed' + } + await commands.executeCommand('lean4.setup.showSetupGuide') + return 'Abort' } export function displayInformation(message: string, finalizer?: (() => void) | undefined) { - displayNotification(window.showInformationMessage, message, finalizer) + displayNotification('Information', message, finalizer) } export async function displayInformationWithInput( message: string, ...items: T[] ): Promise { - return await displayNotificationWithInput(window.showInformationMessage, message, ...items) + return await displayNotificationWithInput('Information', message, ...items) } export function displayInformationWithOptionalInput( @@ -138,13 +192,13 @@ export function displayInformationWithOptionalInput( action: () => void, finalizer?: (() => void) | undefined, ) { - displayNotificationWithOptionalInput(window.showInformationMessage, message, input, action, finalizer) + displayNotificationWithOptionalInput('Information', message, input, action, finalizer) } export function displayInformationWithOutput(message: string, finalizer?: (() => void) | undefined) { - displayNotificationWithOutput(window.showInformationMessage, message, finalizer) + displayNotificationWithOutput('Information', message, finalizer) } export function displayInformationWithSetupGuide(message: string, finalizer?: (() => void) | undefined) { - displayNotificationWithSetupGuide(window.showInformationMessage, message, finalizer) + displayNotificationWithSetupGuide('Information', message, finalizer) } diff --git a/vscode-lean4/src/utils/setupDiagnostics.ts b/vscode-lean4/src/utils/setupDiagnostics.ts deleted file mode 100644 index 3812c4496..000000000 --- a/vscode-lean4/src/utils/setupDiagnostics.ts +++ /dev/null @@ -1,498 +0,0 @@ -import * as os from 'os' -import { SemVer } from 'semver' -import { Disposable, OutputChannel, TextDocument, commands, env, window, workspace } from 'vscode' -import { shouldShowSetupWarnings } from '../config' -import { ExecutionExitCode, ExecutionResult, batchExecute, batchExecuteWithProgress } from './batch' -import { ExtUri, FileUri, extUriEquals, toExtUri } from './exturi' -import { - displayError, - displayErrorWithInput, - displayErrorWithOptionalInput, - displayErrorWithOutput, - displayErrorWithSetupGuide, - displayInformationWithInput, - displayWarning, - displayWarningWithInput, - displayWarningWithOptionalInput, - displayWarningWithOutput, - displayWarningWithSetupGuide, -} from './notifs' -import { checkParentFoldersForLeanProject, findLeanProjectRoot, isValidLeanProject } from './projectInfo' - -export type SystemQueryResult = { - operatingSystem: string - cpuArchitecture: string - cpuModels: string - totalMemory: string -} - -export type VersionQueryResult = - | { kind: 'Success'; version: SemVer } - | { kind: 'CommandNotFound' } - | { kind: 'CommandError'; message: string } - | { kind: 'InvalidVersion'; versionResult: string } - -const recommendedElanVersion = new SemVer('3.1.1') - -export type ElanVersionDiagnosis = - | { kind: 'UpToDate'; version: SemVer } - | { kind: 'Outdated'; currentVersion: SemVer; recommendedVersion: SemVer } - | { kind: 'NotInstalled' } - | { kind: 'ExecutionError'; message: string } - -export type ProjectSetupDiagnosis = - | { kind: 'SingleFile' } - | { kind: 'MissingLeanToolchain'; folder: FileUri; parentProjectFolder: FileUri | undefined } - | { kind: 'ValidProjectSetup'; projectFolder: FileUri } - -export type LeanVersionDiagnosis = - | { kind: 'UpToDate'; version: SemVer } - | { kind: 'IsLean3Version'; version: SemVer } - | { kind: 'IsAncientLean4Version'; version: SemVer } - | { kind: 'NotInstalled' } - | { kind: 'ExecutionError'; message: string } - -export enum PreconditionCheckResult { - Fulfilled = 0, - Warning = 1, - Fatal = 2, -} - -export function worstPreconditionViolation( - a: PreconditionCheckResult, - b: PreconditionCheckResult, -): PreconditionCheckResult { - return Math.max(a, b) -} - -export function versionQueryResult(executionResult: ExecutionResult, versionRegex: RegExp): VersionQueryResult { - if (executionResult.exitCode === ExecutionExitCode.CannotLaunch) { - return { kind: 'CommandNotFound' } - } - - if (executionResult.exitCode === ExecutionExitCode.ExecutionError) { - return { kind: 'CommandError', message: executionResult.combined } - } - - const match = versionRegex.exec(executionResult.stdout) - if (!match) { - return { kind: 'InvalidVersion', versionResult: executionResult.stdout } - } - - return { kind: 'Success', version: new SemVer(match[1]) } -} - -export function checkElanVersion(elanVersionResult: VersionQueryResult): ElanVersionDiagnosis { - switch (elanVersionResult.kind) { - case 'CommandNotFound': - return { kind: 'NotInstalled' } - - case 'CommandError': - return { kind: 'ExecutionError', message: elanVersionResult.message } - - case 'InvalidVersion': - return { - kind: 'ExecutionError', - message: `Invalid Elan version format: '${elanVersionResult.versionResult}'`, - } - - case 'Success': - if (elanVersionResult.version.compare(recommendedElanVersion) < 0) { - return { - kind: 'Outdated', - currentVersion: elanVersionResult.version, - recommendedVersion: recommendedElanVersion, - } - } - return { kind: 'UpToDate', version: elanVersionResult.version } - } -} - -export function checkLeanVersion(leanVersionResult: VersionQueryResult): LeanVersionDiagnosis { - if (leanVersionResult.kind === 'CommandNotFound') { - return { kind: 'NotInstalled' } - } - - if (leanVersionResult.kind === 'CommandError') { - return { - kind: 'ExecutionError', - message: leanVersionResult.message, - } - } - - if (leanVersionResult.kind === 'InvalidVersion') { - return { - kind: 'ExecutionError', - message: `Invalid Lean version format: '${leanVersionResult.versionResult}'`, - } - } - - const leanVersion = leanVersionResult.version - if (leanVersion.major === 3) { - return { kind: 'IsLean3Version', version: leanVersion } - } - - if (leanVersion.major === 4 && leanVersion.minor === 0 && leanVersion.prerelease.length > 0) { - return { kind: 'IsAncientLean4Version', version: leanVersion } - } - - return { kind: 'UpToDate', version: leanVersion } -} - -export class SetupDiagnoser { - readonly channel: OutputChannel - readonly cwdUri: FileUri | undefined - - constructor(channel: OutputChannel, cwdUri: FileUri | undefined) { - this.channel = channel - this.cwdUri = cwdUri - } - - async checkCurlAvailable(): Promise { - const curlVersionResult = await this.runSilently('curl', ['--version']) - return curlVersionResult.exitCode === ExecutionExitCode.Success - } - - async checkGitAvailable(): Promise { - const gitVersionResult = await this.runSilently('git', ['--version']) - return gitVersionResult.exitCode === ExecutionExitCode.Success - } - - async queryLakeVersion(): Promise { - const lakeVersionResult = await this.runWithProgress('lake', ['--version'], 'Checking Lake version') - return versionQueryResult(lakeVersionResult, /version (\d+\.\d+\.\d+(\w|-)*)/) - } - - async checkLakeAvailable(): Promise { - const lakeVersionResult = await this.queryLakeVersion() - return lakeVersionResult.kind === 'Success' - } - - querySystemInformation(): SystemQueryResult { - const cpuModels = os.cpus().map(cpu => cpu.model) - const groupedCpuModels = new Map() - for (const cpuModel of cpuModels) { - const counter: number | undefined = groupedCpuModels.get(cpuModel) - if (counter === undefined) { - groupedCpuModels.set(cpuModel, 1) - } else { - groupedCpuModels.set(cpuModel, counter + 1) - } - } - const formattedCpuModels = Array.from(groupedCpuModels.entries()) - .map(([cpuModel, amount]) => `${amount} x ${cpuModel}`) - .join(', ') - - const totalMemory = (os.totalmem() / 1_000_000_000).toFixed(2) - - return { - operatingSystem: `${os.type()} (release: ${os.release()})`, - cpuArchitecture: os.arch(), - cpuModels: formattedCpuModels, - totalMemory: `${totalMemory} GB`, - } - } - - async queryLeanVersion(): Promise { - const leanVersionResult = await this.runWithProgress('lean', ['--version'], 'Checking Lean version') - return versionQueryResult(leanVersionResult, /version (\d+\.\d+\.\d+(\w|-)*)/) - } - - async queryElanVersion(): Promise { - const elanVersionResult = await this.runSilently('elan', ['--version']) - return versionQueryResult(elanVersionResult, /elan (\d+\.\d+\.\d+)/) - } - - async queryElanShow(): Promise { - return await this.runSilently('elan', ['show']) - } - - async elanVersion(): Promise { - const elanVersionResult = await this.queryElanVersion() - return checkElanVersion(elanVersionResult) - } - - async projectSetup(): Promise { - if (this.cwdUri === undefined) { - return { kind: 'SingleFile' } - } - - if (!(await isValidLeanProject(this.cwdUri))) { - const parentProjectFolder: FileUri | undefined = await checkParentFoldersForLeanProject(this.cwdUri) - return { kind: 'MissingLeanToolchain', folder: this.cwdUri, parentProjectFolder } - } - - return { kind: 'ValidProjectSetup', projectFolder: this.cwdUri } - } - - async projectLeanVersion(): Promise { - const leanVersionResult = await this.queryLeanVersion() - return checkLeanVersion(leanVersionResult) - } - - private async runSilently(executablePath: string, args: string[]): Promise { - return batchExecute(executablePath, args, this.cwdUri?.fsPath, { combined: this.channel }) - } - - private async runWithProgress(executablePath: string, args: string[], title: string): Promise { - return batchExecuteWithProgress(executablePath, args, title, { - cwd: this.cwdUri?.fsPath, - channel: this.channel, - }) - } -} - -export function diagnose(channel: OutputChannel, cwdUri: FileUri | undefined): SetupDiagnoser { - return new SetupDiagnoser(channel, cwdUri) -} - -export type FullDiagnostics = { - systemInfo: SystemQueryResult - isCurlAvailable: boolean - isGitAvailable: boolean - elanVersionDiagnosis: ElanVersionDiagnosis - leanVersionDiagnosis: LeanVersionDiagnosis - projectSetupDiagnosis: ProjectSetupDiagnosis - elanShowOutput: ExecutionResult -} - -function formatCommandOutput(cmdOutput: string): string { - return '\n```\n' + cmdOutput + '\n```' -} - -function formatElanVersionDiagnosis(d: ElanVersionDiagnosis): string { - switch (d.kind) { - case 'UpToDate': - return `Reasonably up-to-date (version: ${d.version.toString()})` - case 'Outdated': - return `Outdated (version: ${d.currentVersion.toString()}, recommended version: ${d.recommendedVersion.toString()})` - case 'ExecutionError': - return 'Execution error: ' + formatCommandOutput(d.message) - case 'NotInstalled': - return 'Not installed' - } -} - -function formatLeanVersionDiagnosis(d: LeanVersionDiagnosis): string { - switch (d.kind) { - case 'UpToDate': - return `Reasonably up-to-date (version: ${d.version})` - case 'IsLean3Version': - return `Lean 3 version (version: ${d.version})` - case 'IsAncientLean4Version': - return `Pre-stable-release Lean 4 version (version: ${d.version})` - case 'ExecutionError': - return 'Execution error: ' + formatCommandOutput(d.message) - case 'NotInstalled': - return 'Not installed' - } -} - -function formatProjectSetupDiagnosis(d: ProjectSetupDiagnosis): string { - switch (d.kind) { - case 'SingleFile': - return 'No open project' - case 'MissingLeanToolchain': - const parentProjectFolder = - d.parentProjectFolder === undefined - ? '' - : `(Valid Lean project in parent folder: ${d.parentProjectFolder.fsPath})` - return `Folder without lean-toolchain file (no valid Lean project) (path: ${d.folder.fsPath}) ${parentProjectFolder}` - case 'ValidProjectSetup': - return `Valid Lean project (path: ${d.projectFolder.fsPath})` - } -} - -function formatElanShowOutput(r: ExecutionResult): string { - if (r.exitCode === ExecutionExitCode.CannotLaunch) { - return 'Elan not installed' - } - if (r.exitCode === ExecutionExitCode.ExecutionError) { - return 'Execution error: ' + formatCommandOutput(r.combined) - } - return formatCommandOutput(r.stdout) -} - -export function formatFullDiagnostics(d: FullDiagnostics): string { - return [ - `**Operating system**: ${d.systemInfo.operatingSystem}`, - `**CPU architecture**: ${d.systemInfo.cpuArchitecture}`, - `**CPU model**: ${d.systemInfo.cpuModels}`, - `**Available RAM**: ${d.systemInfo.totalMemory}`, - '', - `**Curl installed**: ${d.isCurlAvailable}`, - `**Git installed**: ${d.isGitAvailable}`, - `**Elan**: ${formatElanVersionDiagnosis(d.elanVersionDiagnosis)}`, - `**Lean**: ${formatLeanVersionDiagnosis(d.leanVersionDiagnosis)}`, - `**Project**: ${formatProjectSetupDiagnosis(d.projectSetupDiagnosis)}`, - '', - '-------------------------------------', - '', - `**Elan toolchains**: ${formatElanShowOutput(d.elanShowOutput)}`, - ].join('\n') -} - -export async function performFullDiagnosis( - channel: OutputChannel, - cwdUri: FileUri | undefined, -): Promise { - const diagnose = new SetupDiagnoser(channel, cwdUri) - return { - systemInfo: diagnose.querySystemInformation(), - isCurlAvailable: await diagnose.checkCurlAvailable(), - isGitAvailable: await diagnose.checkGitAvailable(), - elanVersionDiagnosis: await diagnose.elanVersion(), - leanVersionDiagnosis: await diagnose.projectLeanVersion(), - projectSetupDiagnosis: await diagnose.projectSetup(), - elanShowOutput: await diagnose.queryElanShow(), - } -} - -export class FullDiagnosticsProvider implements Disposable { - private subscriptions: Disposable[] = [] - private outputChannel: OutputChannel - // Under normal circumstances, we would use the last active `LeanClient` from `LeanClientProvider.getActiveClient()` - // to determine the document that the user is currently working on. - // However, when providing setup diagnostics, there might not be an active client due to errors in the user's setup, - // in which case we still want to provide adequate diagnostics. Hence, we track the last active lean document - // separately, regardless of whether there is an actual `LeanClient` managing it. - private lastActiveLeanDocumentUri: ExtUri | undefined - - constructor(outputChannel: OutputChannel) { - this.outputChannel = outputChannel - - if (window.activeTextEditor !== undefined) { - this.lastActiveLeanDocumentUri = FullDiagnosticsProvider.getLean4DocUri(window.activeTextEditor.document) - } - - window.onDidChangeActiveTextEditor(e => { - if (e === undefined) { - return - } - const docUri = FullDiagnosticsProvider.getLean4DocUri(e.document) - if (docUri === undefined) { - return - } - - this.lastActiveLeanDocumentUri = docUri - }, this.subscriptions) - workspace.onDidCloseTextDocument(doc => { - if (this.lastActiveLeanDocumentUri === undefined) { - return - } - - const docUri = FullDiagnosticsProvider.getLean4DocUri(doc) - if (docUri === undefined) { - return - } - - if (extUriEquals(docUri, this.lastActiveLeanDocumentUri)) { - this.lastActiveLeanDocumentUri = undefined - } - }, this.subscriptions) - - this.subscriptions.push( - commands.registerCommand('lean4.troubleshooting.showSetupInformation', () => - this.performAndDisplayFullDiagnosis(), - ), - ) - } - - async performAndDisplayFullDiagnosis() { - const projectUri = - this.lastActiveLeanDocumentUri !== undefined && this.lastActiveLeanDocumentUri.scheme === 'file' - ? await findLeanProjectRoot(this.lastActiveLeanDocumentUri) - : undefined - const fullDiagnostics = await performFullDiagnosis(this.outputChannel, projectUri) - const formattedFullDiagnostics = formatFullDiagnostics(fullDiagnostics) - const copyToClipboardInput = 'Copy to Clipboard' - const choice = await displayInformationWithInput(formattedFullDiagnostics, copyToClipboardInput) - if (choice === copyToClipboardInput) { - await env.clipboard.writeText(formattedFullDiagnostics) - } - } - - private static getLean4DocUri(doc: TextDocument): ExtUri | undefined { - if (doc.languageId !== 'lean4') { - return undefined - } - return toExtUri(doc.uri) - } - - dispose() { - for (const s of this.subscriptions) { - s.dispose() - } - } -} - -export function displaySetupError(message: string, finalizer?: (() => void) | undefined) { - displayError(message, finalizer) -} - -export async function displaySetupErrorWithInput( - message: string, - ...items: T[] -): Promise { - return await displayErrorWithInput(message, ...items) -} - -export function displaySetupErrorWithOptionalInput( - message: string, - input: T, - action: () => void, - finalizer?: (() => void) | undefined, -) { - displayErrorWithOptionalInput(message, input, action, finalizer) -} - -export function displaySetupErrorWithOutput(message: string, finalizer?: (() => void) | undefined) { - displayErrorWithOutput(message, finalizer) -} - -export function displaySetupErrorWithSetupGuide(message: string, finalizer?: (() => void) | undefined) { - displayErrorWithSetupGuide(message, finalizer) -} - -export function displaySetupWarning(message: string, finalizer?: (() => void) | undefined) { - if (!shouldShowSetupWarnings()) { - return - } - displayWarning(message, finalizer) -} - -export async function displaySetupWarningWithInput( - message: string, - ...items: T[] -): Promise { - if (!shouldShowSetupWarnings()) { - return undefined - } - return await displayWarningWithInput(message, ...items) -} - -export function displaySetupWarningWithOptionalInput( - message: string, - input: T, - action: () => void, - finalizer?: (() => void) | undefined, -) { - if (!shouldShowSetupWarnings()) { - return - } - displayWarningWithOptionalInput(message, input, action, finalizer) -} - -export function displaySetupWarningWithOutput(message: string, finalizer?: (() => void) | undefined) { - if (!shouldShowSetupWarnings()) { - return - } - displayWarningWithOutput(message, finalizer) -} - -export function displaySetupWarningWithSetupGuide(message: string, finalizer?: (() => void) | undefined) { - if (!shouldShowSetupWarnings()) { - return - } - displayWarningWithSetupGuide(message, finalizer) -}