From 01d0e260a934fc226c03339343979543f635a039 Mon Sep 17 00:00:00 2001
From: mhuisi <mhuisi@protonmail.com>
Date: Tue, 30 Jun 2026 09:41:43 +0200
Subject: [PATCH] fix: build project after "Download Project"

---
 vscode-lean4/src/projectinit.ts | 9 +++++++++
 1 file changed, 9 insertions(+)

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)
         })