feat: more helpful error when setting up project without lean/git (#407)

vscode-lean4/src/projectinit.ts

@@ -4,6 +4,7 @@ import { checkParentFoldersForLeanProject, isValidLeanProject } from './utils/pr
 import { elanSelfUpdate } from './utils/elan';
 import { lake } from './utils/lake';
 import { ExecutionExitCode, ExecutionResult, batchExecute, batchExecuteWithProgress, displayError } from './utils/batch';
+import { diagnose } from './utils/setupDiagnostics';
 
 export class ProjectInitializationProvider implements Disposable {
 
@@ -87,6 +88,10 @@ export class ProjectInitializationProvider implements Disposable {
             return 'DidNotComplete'
         }
 
+        if (await this.checkSetupDeps(projectFolder) === 'IncompleteSetup') {
+            return 'DidNotComplete'
+        }
+
         await workspace.fs.createDirectory(projectFolder)
 
         // This can fail silently in setups without Elan.
@@ -176,6 +181,10 @@ 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',
@@ -202,6 +211,10 @@ Open this project instead?`
             return
         }
 
+        if (await this.checkLake(projectFolder) === 'LakeNotInstalled') {
+            return
+        }
+
         // Try it. If this is not a mathlib project, it will fail silently. Otherwise, it will grab the cache.
         const fetchResult: ExecutionResult = await lake(this.channel, projectFolder).fetchMathlibCache(true)
         if (fetchResult.exitCode === ExecutionExitCode.Cancelled) {
@@ -238,6 +251,36 @@ Open this project instead?`
         }
     }
 
+    private async checkSetupDeps(projectFolder: Uri): 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?: Uri | 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)`
+            void window.showErrorMessage(message)
+            return 'GitNotInstalled'
+        }
+        return 'GitInstalled'
+    }
+
+    private async checkLake(projectFolder: Uri): 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)`
+            void window.showErrorMessage(message)
+            return 'LakeNotInstalled'
+        }
+        return 'LakeInstalled'
+    }
+
     dispose() {
         for (const s of this.subscriptions) { s.dispose(); }
     }

vscode-lean4/src/utils/projectInfo.ts

@@ -1,6 +1,6 @@
 import * as fs from 'fs';
 import { URL } from 'url';
-import { FileType, Uri, workspace, WorkspaceFolder } from 'vscode';
+import { Uri, workspace, WorkspaceFolder } from 'vscode';
 import { fileExists } from './fsHelper';
 import { logger } from './logger'
 import path = require('path');

vscode-lean4/src/utils/setupDiagnostics.ts

@@ -0,0 +1,41 @@
+import { OutputChannel, Uri } from 'vscode';
+import { ExecutionExitCode, ExecutionResult, batchExecute } from './batch';
+
+export class SetupDiagnoser {
+    channel: OutputChannel
+    cwdUri: Uri | undefined
+
+    constructor(channel: OutputChannel, cwdUri: Uri | undefined) {
+        this.channel = channel
+        this.cwdUri = cwdUri
+    }
+
+    async checkLakeAndDepsAvailable(): Promise<'Success' | 'LakeUnavailable' | 'GitUnavailable'> {
+        if (!await this.checkLakeAvailable()) {
+            return 'LakeUnavailable'
+        }
+        if (!await this.checkGitAvailable()) {
+            return 'GitUnavailable'
+        }
+        return 'Success'
+    }
+
+    async checkLakeAvailable(): Promise<boolean> {
+        const lakeVersionResult = await this.runSilently('lake', ['--version'])
+        return lakeVersionResult.exitCode === ExecutionExitCode.Success
+    }
+
+    async checkGitAvailable(): Promise<boolean> {
+        const gitVersionResult = await batchExecute('git', ['--version'])
+        return gitVersionResult.exitCode === ExecutionExitCode.Success
+    }
+
+    private async runSilently(executablePath: string, args: string[]): Promise<ExecutionResult> {
+        return batchExecute(executablePath, args, this.cwdUri?.fsPath, { combined: this.channel })
+    }
+}
+
+export function diagnose(channel: OutputChannel, cwdUri: Uri | undefined): SetupDiagnoser {
+    return new SetupDiagnoser(channel, cwdUri)
+}
+