From 8b58dd31c737f116c3c3b3ac62d69bff974e0beb Mon Sep 17 00:00:00 2001
From: BalaM314 <71201189+BalaM314@users.noreply.github.com>
Date: Thu, 2 Oct 2025 21:39:33 +0530
Subject: [PATCH] Use shallow clone when cloning mathlib

The project setup currently downloads the entire repository history of mathlib, consisting of 24 thousand commits. This requires an additional 388 megabytes of disk space.

Passing `--depth=1` to git performs a shallow clone, which does not download all the commits, saving 388 megabytes of disk space.
---
 vscode-lean4/src/projectinit.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/vscode-lean4/src/projectinit.ts b/vscode-lean4/src/projectinit.ts
index d109a65b..3421fab9 100644
--- a/vscode-lean4/src/projectinit.ts
+++ b/vscode-lean4/src/projectinit.ts
@@ -392,7 +392,7 @@ Open this project instead?`
 
             const result: ExecutionResult = await batchExecuteWithProgress(
                 'git',
-                ['clone', projectUri, projectFolder.fsPath],
+                ['clone', '--depth=1', projectUri, projectFolder.fsPath],
                 downloadProjectContext,
                 'Cloning project',
                 { channel: this.channel, allowCancellation: true },