diff --git a/vscode-lean4/src/projectinit.ts b/vscode-lean4/src/projectinit.ts index 06f410fc..d0a6b5c0 100644 --- a/vscode-lean4/src/projectinit.ts +++ b/vscode-lean4/src/projectinit.ts @@ -435,6 +435,15 @@ Open this project instead?` return } + const buildResult = await lakeRunner.build() + if (buildResult.kind === 'Cancelled') { + return + } + if (buildResult.kind === 'Error') { + displayLakeRunnerError(buildResult, 'Cannot build downloaded project.') + return + } + await ProjectInitializationProvider.openNewFolder(projectFolder) })