diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 8f8ab40325..6b7c44946f 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -344,10 +344,10 @@ jobs:
       - name: List Install Tree
         run: |
           # omit contents of Init/, ...
-          tree --du -h lean-* | grep -E ' (Init|Lean|Lake|LICENSE|[a-z])'
+          tree --du -h lean-*-* | grep -E ' (Init|Lean|Lake|LICENSE|[a-z])'
       - name: Pack
         run: |
-          dir=$(echo lean-*)
+          dir=$(echo lean-*-*)
           mkdir pack
           # high-compression tar.zst + zip for release, fast tar.zst otherwise
           if [[ '${{ startsWith(github.ref, 'refs/tags/') && matrix.release }}' == true || -n '${{ needs.configure.outputs.nightly }}' || -n '${{ needs.configure.outputs.RELEASE_TAG }}' ]]; then
diff --git a/.vscode/settings.json b/.vscode/settings.json
deleted file mode 100644
index 7f92a670e2..0000000000
--- a/.vscode/settings.json
+++ /dev/null
@@ -1,7 +0,0 @@
-{
-    "files.insertFinalNewline": true,
-    "files.trimTrailingWhitespace": true,
-    "[markdown]": {
-        "rewrap.wrappingColumn": 70
-    }
-}
diff --git a/doc/dev/index.md b/doc/dev/index.md
index 1832dea5d3..7f125ca61e 100644
--- a/doc/dev/index.md
+++ b/doc/dev/index.md
@@ -30,20 +30,14 @@ powershell -f elan-init.ps1 --default-toolchain none
 del elan-init.ps1
 ```
 
-You can use `elan toolchain link` to give a specific stage build
-directory a reference name, then use `elan override set` to associate
-such a name to the current directory. We usually want to use `stage0`
-for editing files in `src` and `stage1` for everything else (e.g.
-tests).
+The `lean-toolchain` files in the Lean 4 repository are set up to use the `lean4-stage0`
+toolchain for editing files in `src` and the `lean4` toolchain for editing files in `tests`.
+
+Run the following commands to make `lean4` point at `stage1` and `lean4-stage0` point at `stage0`:
 ```bash
 # in the Lean rootdir
 elan toolchain link lean4 build/release/stage1
 elan toolchain link lean4-stage0 build/release/stage0
-# make `lean` etc. point to stage1 in the rootdir and subdirs
-elan override set lean4
-cd src
-# make `lean` etc. point to stage0 anywhere inside `src`
-elan override set lean4-stage0
 ```
 
 You can also use the `+toolchain` shorthand (e.g. `lean +lean4-debug`) to switch
@@ -65,6 +59,15 @@ If you push `my-tag` to a fork in your github account `my_name`,
 you can then put `my_name/lean4:my-tag` in your `lean-toolchain` file in a project using `lake`.
 (You must use a tag name that does not start with a numeral, or contain `_`).
 
+### 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
+```
+code lean.code-workspace
+```
+on the command line.
+
 ### `ccache`
 
 Lean's build process uses [`ccache`](https://ccache.dev/) if it is
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 0000000000..dcca6df980
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+lean4
diff --git a/lean.code-workspace b/lean.code-workspace
new file mode 100644
index 0000000000..587b184efa
--- /dev/null
+++ b/lean.code-workspace
@@ -0,0 +1,50 @@
+{
+	"folders": [
+		{
+			"path": "."
+		},
+		{
+			"path": "src"
+		},
+		{
+			"path": "tests"
+		}
+	],
+	"settings": {
+		"files.insertFinalNewline": true,
+		"files.trimTrailingWhitespace": true,
+		"[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": "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/src/lean-toolchain b/src/lean-toolchain
new file mode 100644
index 0000000000..0694e2bc29
--- /dev/null
+++ b/src/lean-toolchain
@@ -0,0 +1 @@
+lean4-stage0
diff --git a/tests/lean-toolchain b/tests/lean-toolchain
new file mode 100644
index 0000000000..dcca6df980
--- /dev/null
+++ b/tests/lean-toolchain
@@ -0,0 +1 @@
+lean4