feat: build lean project after initialization (#363)

leanprover · Nov 26, 2023 · 2fd18c6 · 2fd18c6
1 parent 08d46f1
commit 2fd18c6
Showing 1 changed file with 14 additions and 3 deletions.
diff --git a/vscode-lean4/src/projectinit.ts b/vscode-lean4/src/projectinit.ts
@@ -19,11 +19,22 @@ export class ProjectInitializationProvider implements Disposable {
     }
 
     private async createStandaloneProject() {
-        const projectFolder: Uri | 'DidNotComplete' = await this.createProject()
+        const toolchain = 'leanprover/lean4:stable'
+        const projectFolder: Uri | 'DidNotComplete' = await this.createProject(undefined, toolchain)
+        if (projectFolder === 'DidNotComplete') {
+            return
+        }
 
-        if (projectFolder !== 'DidNotComplete') {
-            await ProjectInitializationProvider.openNewFolder(projectFolder)
+        const buildResult: ExecutionResult = await lake(this.channel, projectFolder, toolchain).build()
+        if (buildResult.exitCode === ExecutionExitCode.Cancelled) {
+            return
         }
+        if (buildResult.exitCode !== ExecutionExitCode.Success) {
+            await displayError(buildResult, 'Cannot build Lean project.')
+            return
+        }
+
+        await ProjectInitializationProvider.openNewFolder(projectFolder)
     }
 
     private async createMathlibProject() {