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)

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<FullDiagnostics> {
+    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()
+        }
+    }
+}