From d03499322de6e7b5d9a47f0ce2ad003506114b6c Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Wed, 4 Mar 2026 12:10:04 +1100
Subject: [PATCH] chore: replace workspace file with .vscode/ settings (#12770)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR replaces `lean.code-workspace` with standard `.vscode/`
configuration
files (`settings.json`, `tasks.json`, `extensions.json`). The workspace
file
required users to explicitly "Open Workspace from File" (and moreover
gives a
noisy prompt whether or not they want to open it), while `.vscode/`
settings
are picked up automatically when opening the folder. This became
possible after
#12652 reduced the workspace to a single folder.

Also drops the `rewrap.wrappingColumn` markdown setting, as the Rewrap
extension
is no longer signed on the VS Code marketplace.

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
---
 .gitignore              |  3 +++
 .vscode/extensions.json |  5 ++++
 .vscode/settings.json   | 12 +++++++++
 .vscode/tasks.json      | 34 +++++++++++++++++++++++
 doc/dev/index.md        |  6 ++---
 lean.code-workspace     | 60 -----------------------------------------
 6 files changed, 57 insertions(+), 63 deletions(-)
 create mode 100644 .vscode/extensions.json
 create mode 100644 .vscode/settings.json
 create mode 100644 .vscode/tasks.json
 delete mode 100644 lean.code-workspace

diff --git a/.gitignore b/.gitignore
index cdde464513..1d348e9ca4 100644
--- a/.gitignore
+++ b/.gitignore
@@ -20,6 +20,9 @@ settings.json
 !.claude/settings.json
 .gdb_history
 .vscode/*
+!.vscode/settings.json
+!.vscode/tasks.json
+!.vscode/extensions.json
 script/__pycache__
 *.produced.out
 CMakeSettings.json
diff --git a/.vscode/extensions.json b/.vscode/extensions.json
new file mode 100644
index 0000000000..e2c0159543
--- /dev/null
+++ b/.vscode/extensions.json
@@ -0,0 +1,5 @@
+{
+	"recommendations": [
+		"leanprover.lean4"
+	]
+}
diff --git a/.vscode/settings.json b/.vscode/settings.json
new file mode 100644
index 0000000000..7f657a1d9e
--- /dev/null
+++ b/.vscode/settings.json
@@ -0,0 +1,12 @@
+{
+	"files.insertFinalNewline": true,
+	"files.trimTrailingWhitespace": true,
+	// These require the CMake Tools extension (ms-vscode.cmake-tools).
+	"cmake.buildDirectory": "${workspaceFolder}/build/release",
+	"cmake.generator": "Unix Makefiles",
+	"[lean4]": {
+		"editor.rulers": [
+			100
+		]
+	}
+}
diff --git a/.vscode/tasks.json b/.vscode/tasks.json
new file mode 100644
index 0000000000..9a308a7035
--- /dev/null
+++ b/.vscode/tasks.json
@@ -0,0 +1,34 @@
+{
+	"version": "2.0.0",
+	"tasks": [
+		{
+			"label": "build",
+			"type": "shell",
+			"command": "make -C build/release -j$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)",
+			"problemMatcher": [],
+			"group": {
+				"kind": "build",
+				"isDefault": true
+			}
+		},
+		{
+			"label": "build-old",
+			"type": "shell",
+			"command": "make -C build/release -j$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4) LAKE_EXTRA_ARGS=--old",
+			"problemMatcher": [],
+			"group": {
+				"kind": "build"
+			}
+		},
+		{
+			"label": "test",
+			"type": "shell",
+			"command": "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4); CTEST_OUTPUT_ON_FAILURE=1 make -C build/release test -j$NPROC ARGS=\"-j$NPROC\"",
+			"problemMatcher": [],
+			"group": {
+				"kind": "test",
+				"isDefault": true
+			}
+		}
+	]
+}
diff --git a/doc/dev/index.md b/doc/dev/index.md
index 58d5f61b1d..4e8c5b3e77 100644
--- a/doc/dev/index.md
+++ b/doc/dev/index.md
@@ -61,10 +61,10 @@ you can then put `my_name/lean4:my-tag` in your `lean-toolchain` file in a proje
 
 ### VS Code
 
-There is a `lean.code-workspace` file that correctly sets up VS Code with workspace roots for the stage0/stage1 setup described above as well as with other settings.
-You should always load it when working on Lean, such as by invoking
+There is a `.vscode/` directory that correctly sets up VS Code with settings, tasks, and recommended extensions.
+Simply open the repository folder in VS Code, such as by invoking
 ```
-code lean.code-workspace
+code .
 ```
 on the command line.
 
diff --git a/lean.code-workspace b/lean.code-workspace
deleted file mode 100644
index 9d53f4b0f7..0000000000
--- a/lean.code-workspace
+++ /dev/null
@@ -1,60 +0,0 @@
-{
-	"folders": [
-		{
-			"path": "."
-		}
-	],
-	"settings": {
-		"files.insertFinalNewline": true,
-		"files.trimTrailingWhitespace": true,
-		"cmake.buildDirectory": "${workspaceFolder}/build/release",
-		"cmake.generator": "Unix Makefiles",
-		"[markdown]": {
-			"rewrap.wrappingColumn": 70
-		},
-		"[lean4]": {
-			"editor.rulers": [
-				100
-			]
-		}
-	},
-	"tasks": {
-		"version": "2.0.0",
-		"tasks": [
-			{
-				"label": "build",
-				"type": "shell",
-				"command": "make -C build/release -j$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)",
-				"problemMatcher": [],
-				"group": {
-					"kind": "build",
-					"isDefault": true
-				}
-			},
-			{
-				"label": "build-old",
-				"type": "shell",
-				"command": "make -C build/release -j$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4) LAKE_EXTRA_ARGS=--old",
-				"problemMatcher": [],
-				"group": {
-					"kind": "build"
-				}
-			},
-			{
-				"label": "test",
-				"type": "shell",
-				"command": "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4); CTEST_OUTPUT_ON_FAILURE=1 make -C build/release test -j$NPROC ARGS=\"-j$NPROC\"",
-				"problemMatcher": [],
-				"group": {
-					"kind": "test",
-					"isDefault": true
-				}
-			}
-		]
-	},
-	"extensions": {
-		"recommendations": [
-			"leanprover.lean4"
-		]
-	}
-}