From d9a092089abbb09590731fa10d092d9e100123ac Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sat, 18 Apr 2026 10:47:16 +1000
Subject: [PATCH 01/14] test: detect "Lean toolchain not installed" prompt in
 CI

The lean4 extension queries elan to verify the project's declared
toolchain is installed.  Our bundle ships Lean directly at lean/bin/
without the elan toolchain directory layout (lean/toolchains/<encoded
-name>/), so the extension thinks no toolchain is installed and pops
up a modal dialog asking the student to download one.

The existing "no notification popups" check only inspects toast
notifications and doesn't catch modal dialogs.  Add a focused test
that matches the prompt by characteristic text ("is not installed"),
which works for both modal dialogs and toasts and survives DOM-class
churn between VS Code versions.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 tests/gui-playwright/tests/startup.spec.ts | 38 ++++++++++++++++++++++
 1 file changed, 38 insertions(+)

diff --git a/tests/gui-playwright/tests/startup.spec.ts b/tests/gui-playwright/tests/startup.spec.ts
index 5c34210..a9777a5 100644
--- a/tests/gui-playwright/tests/startup.spec.ts
+++ b/tests/gui-playwright/tests/startup.spec.ts
@@ -64,3 +64,41 @@ test('no notification popups on startup', async () => {
 
     expect(count, 'No notification popups should appear on startup').toBe(0);
 });
+
+test('no Lean toolchain install prompt on first launch', async () => {
+    const page = result.page;
+    await page.waitForSelector('.monaco-workbench', { timeout: 30_000 });
+
+    // The launcher auto-opens a .lean file, which activates the lean4
+    // extension; the extension then queries elan to verify that the
+    // declared toolchain is installed.  If our bundled lean isn't laid
+    // out as elan expects, a modal dialog pops up:
+    //
+    //   "Lean version 'leanprover/lean4:vX.Y.Z' of Lean project '...' is
+    //    not installed.  Do you wish to install it?"
+    //
+    // This is *modal*, so the existing "no notification popups" check
+    // (which only inspects toast notifications) misses it entirely.
+    // Wait long enough for the extension to fully activate.
+    await page.waitForTimeout(20_000);
+
+    await page.screenshot({ path: 'test-results/startup-no-toolchain-prompt.png' });
+
+    // Match by characteristic text from the prompt — works for both modal
+    // dialogs and notification toasts, and survives DOM-class churn.
+    const installPrompt = page.getByText(/is not installed/i).first();
+    const visible = await installPrompt.isVisible().catch(() => false);
+
+    if (visible) {
+        const fullText = await installPrompt.textContent().catch(() => '<unreadable>');
+        console.log(`  Toolchain install prompt visible: ${fullText}`);
+    }
+
+    expect(visible,
+        '"Lean version is not installed" prompt should NOT appear. ' +
+        'If this fails, the bundled Lean toolchain is not in the elan ' +
+        'layout (lean/toolchains/<encoded-name>/) the lean4 extension ' +
+        'expects, so the extension thinks no toolchain is installed and ' +
+        'asks the student to download one.',
+    ).toBe(false);
+});

From 083cf486c25d489c099a3c7df082891d47ddf2fa Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sat, 18 Apr 2026 11:20:37 +1000
Subject: [PATCH 02/14] test: strip runner's elan from env so Tier 6 mimics
 fresh student
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

GitHub macOS/Linux runners have ~/.elan/bin on PATH from prior Lean
toolchain installs.  Our test launches the bundle through the real
launcher script, which prepends the bundle's lean/bin to PATH but
keeps the rest — including the runner's elan.  The lean4 extension
then finds the runner's elan, queries `elan toolchain list`, sees
that the runner has the toolchain installed in ~/.elan/toolchains/,
and never shows the "Lean version is not installed" prompt.

A real student doesn't have a previously-set-up elan with the right
toolchain.  Strip elan-containing PATH entries (and any inherited
ELAN_HOME) before invoking the launcher so the test environment
matches what students actually see.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 tests/gui-playwright/helpers/launch.ts | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

diff --git a/tests/gui-playwright/helpers/launch.ts b/tests/gui-playwright/helpers/launch.ts
index 191d893..2becb42 100644
--- a/tests/gui-playwright/helpers/launch.ts
+++ b/tests/gui-playwright/helpers/launch.ts
@@ -87,8 +87,26 @@ export async function launchVSCodium(options?: {
 
     // Only set test-infrastructure env vars. The launcher script owns
     // PATH, ELAN_HOME, and LEAN_PATH — that's what we're testing.
+    //
+    // Critically, strip the runner's elan from the inherited environment
+    // to mimic a fresh student install.  GitHub macOS/Linux runners have
+    // ~/.elan/bin on PATH from prior Lean steps; without stripping it,
+    // the lean4 extension finds the runner's elan, sees the toolchain
+    // installed in ~/.elan/toolchains/, and never shows the "Lean
+    // version is not installed" prompt that real students hit.  We're
+    // testing whether the BUNDLE works on its own, not whether the
+    // runner happens to have a working Lean.
+    const filteredEnv = Object.fromEntries(
+        Object.entries(process.env).filter(([k]) => k !== 'ELAN_HOME')
+    ) as Record<string, string>;
+    const sep = process.platform === 'win32' ? ';' : ':';
+    if (filteredEnv.PATH) {
+        filteredEnv.PATH = filteredEnv.PATH.split(sep)
+            .filter(p => !/[\\/]\.?elan[\\/]/.test(p) && !p.endsWith('elan/bin') && !p.endsWith('elan\\bin'))
+            .join(sep);
+    }
     const env: Record<string, string> = {
-        ...process.env as Record<string, string>,
+        ...filteredEnv,
         BUNDLE_ROOT: bundleRoot,
         DONT_PROMPT_WSL_INSTALL: '1',
     };

From 3a73d0c7528ec37e70e0d97679d861066898e040 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sat, 18 Apr 2026 11:52:12 +1000
Subject: [PATCH 03/14] Revert "test: strip runner's elan from env so Tier 6
 mimics fresh student"

This reverts commit 083cf486c25d489c099a3c7df082891d47ddf2fa.
---
 tests/gui-playwright/helpers/launch.ts | 20 +-------------------
 1 file changed, 1 insertion(+), 19 deletions(-)

diff --git a/tests/gui-playwright/helpers/launch.ts b/tests/gui-playwright/helpers/launch.ts
index 2becb42..191d893 100644
--- a/tests/gui-playwright/helpers/launch.ts
+++ b/tests/gui-playwright/helpers/launch.ts
@@ -87,26 +87,8 @@ export async function launchVSCodium(options?: {
 
     // Only set test-infrastructure env vars. The launcher script owns
     // PATH, ELAN_HOME, and LEAN_PATH — that's what we're testing.
-    //
-    // Critically, strip the runner's elan from the inherited environment
-    // to mimic a fresh student install.  GitHub macOS/Linux runners have
-    // ~/.elan/bin on PATH from prior Lean steps; without stripping it,
-    // the lean4 extension finds the runner's elan, sees the toolchain
-    // installed in ~/.elan/toolchains/, and never shows the "Lean
-    // version is not installed" prompt that real students hit.  We're
-    // testing whether the BUNDLE works on its own, not whether the
-    // runner happens to have a working Lean.
-    const filteredEnv = Object.fromEntries(
-        Object.entries(process.env).filter(([k]) => k !== 'ELAN_HOME')
-    ) as Record<string, string>;
-    const sep = process.platform === 'win32' ? ';' : ':';
-    if (filteredEnv.PATH) {
-        filteredEnv.PATH = filteredEnv.PATH.split(sep)
-            .filter(p => !/[\\/]\.?elan[\\/]/.test(p) && !p.endsWith('elan/bin') && !p.endsWith('elan\\bin'))
-            .join(sep);
-    }
     const env: Record<string, string> = {
-        ...filteredEnv,
+        ...process.env as Record<string, string>,
         BUNDLE_ROOT: bundleRoot,
         DONT_PROMPT_WSL_INSTALL: '1',
     };

From 73969c4ff0851e63e9451cff735718c9454520b5 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sat, 18 Apr 2026 11:53:33 +1000
Subject: [PATCH 04/14] ci: install elan (no toolchain) on GUI runners to
 trigger toolchain prompt
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The new "no Lean toolchain install prompt" test passed in CI even
though the bundle clearly shows the prompt on real student macs.
Investigation: CI runners don't have elan installed, so the lean4
extension can't query elan and falls back to using lean from PATH
directly — never showing the prompt.

Real students who took a previous Lean course typically have elan
installed via brew or a Lean course setup script.  Their elan has
toolchains for whatever course they did before, but not necessarily
the one this bundle's project pins.  In that state, the lean4
extension finds elan, asks "is leanprover/lean4:vX.Y.Z installed?",
elan says no, and the modal install prompt pops up.

Install elan (with --default-toolchain none, so no toolchains are
installed) on every GUI test runner before launching the bundle.
This is the most common student state and the one the bundle most
needs to handle correctly.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 .github/workflows/build-and-test.yml | 42 ++++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)

diff --git a/.github/workflows/build-and-test.yml b/.github/workflows/build-and-test.yml
index 3c85691..fb5d6a2 100644
--- a/.github/workflows/build-and-test.yml
+++ b/.github/workflows/build-and-test.yml
@@ -325,6 +325,13 @@ jobs:
       - name: Install xvfb
         run: sudo apt-get update && sudo apt-get install -y xvfb
 
+      # Mimic a student with elan but no matching toolchain (see test-macos-gui).
+      - name: "Install elan (no toolchain) to simulate fresh student"
+        run: |
+          curl -sSf https://raw.githubusercontent.com/leanprover/elan/v4.2.1/elan-init.sh \
+            | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
       - name: "Tier 6: Install Playwright test deps"
         run: |
           cd tests/gui-playwright
@@ -432,6 +439,13 @@ jobs:
       - name: Install xvfb
         run: sudo apt-get update && sudo apt-get install -y xvfb
 
+      # Mimic a student with elan but no matching toolchain (see test-macos-gui).
+      - name: "Install elan (no toolchain) to simulate fresh student"
+        run: |
+          curl -sSf https://raw.githubusercontent.com/leanprover/elan/v4.2.1/elan-init.sh \
+            | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
       - name: "Tier 6: Install Playwright test deps"
         run: |
           cd tests/gui-playwright
@@ -915,6 +929,21 @@ jobs:
           root="${{ steps.find-root.outputs.BUNDLE_ROOT }}"
           xattr -dr com.apple.quarantine "$root" 2>/dev/null || true
 
+      # Install elan but no toolchain.  Mimics the most common student
+      # state: they did a Lean course before and have ~/.elan/bin/elan
+      # on their PATH from a prior install, but no toolchain matching
+      # the project's lean-toolchain pin.  Without this, the lean4
+      # extension can't find elan on a clean runner and falls back to
+      # using the bundled `lean` directly — masking the bug where the
+      # bundle isn't laid out as elan expects.
+      - name: "Install elan (no toolchain) to simulate fresh student"
+        run: |
+          curl -sSf https://raw.githubusercontent.com/leanprover/elan/v4.2.1/elan-init.sh \
+            | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+          # Sanity: elan should be installed but no toolchains present.
+          "$HOME/.elan/bin/elan" --version
+          "$HOME/.elan/bin/elan" toolchain list || true
 
       - name: "Tier 6: Install Playwright test deps"
         run: |
@@ -962,6 +991,19 @@ jobs:
 
       # Olean timestamps are now preserved by create_zip (4-second advance).
 
+      # Mimic a student with elan but no matching toolchain (see test-macos-gui).
+      - name: "Install elan (no toolchain) to simulate fresh student"
+        shell: pwsh
+        run: |
+          $url = "https://raw.githubusercontent.com/leanprover/elan/v4.2.1/elan-init.ps1"
+          $script = Invoke-WebRequest -Uri $url -UseBasicParsing
+          $tmpFile = Join-Path $env:TEMP "elan-init.ps1"
+          [System.IO.File]::WriteAllText($tmpFile, $script.Content)
+          & $tmpFile -y --default-toolchain none
+          $elanBin = Join-Path $env:USERPROFILE ".elan\bin"
+          echo $elanBin | Out-File -FilePath $env:GITHUB_PATH -Append -Encoding utf8
+          & "$elanBin\elan.exe" --version
+
       - name: "Tier 6: Install Playwright test deps"
         shell: pwsh
         run: |

From cdab77a2311ce8b03b382d0f94f85d3393c58be9 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sat, 18 Apr 2026 12:23:51 +1000
Subject: [PATCH 05/14] ci: use elan-init.exe from zip for Windows (PS script
 doesn't take --default-toolchain)

---
 .github/workflows/build-and-test.yml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/build-and-test.yml b/.github/workflows/build-and-test.yml
index fb5d6a2..57ddab1 100644
--- a/.github/workflows/build-and-test.yml
+++ b/.github/workflows/build-and-test.yml
@@ -995,11 +995,11 @@ jobs:
       - name: "Install elan (no toolchain) to simulate fresh student"
         shell: pwsh
         run: |
-          $url = "https://raw.githubusercontent.com/leanprover/elan/v4.2.1/elan-init.ps1"
-          $script = Invoke-WebRequest -Uri $url -UseBasicParsing
-          $tmpFile = Join-Path $env:TEMP "elan-init.ps1"
-          [System.IO.File]::WriteAllText($tmpFile, $script.Content)
-          & $tmpFile -y --default-toolchain none
+          $url = "https://github.com/leanprover/elan/releases/download/v4.2.1/elan-x86_64-pc-windows-msvc.zip"
+          $zip = Join-Path $env:TEMP "elan-init.zip"
+          Invoke-WebRequest -Uri $url -OutFile $zip -UseBasicParsing
+          Expand-Archive -Path $zip -DestinationPath $env:TEMP -Force
+          & "$env:TEMP\elan-init.exe" -y --default-toolchain none
           $elanBin = Join-Path $env:USERPROFILE ".elan\bin"
           echo $elanBin | Out-File -FilePath $env:GITHUB_PATH -Append -Encoding utf8
           & "$elanBin\elan.exe" --version

From 4219e596367ffd1399bcb1ade5c5c618e1f79f27 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sun, 19 Apr 2026 10:17:02 +1000
Subject: [PATCH 06/14] fix: launcher scrubs elan from PATH so bundle ignores
 student's prior Lean install
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

A student who took a prior Lean course typically has elan at
~/.elan/bin/elan on PATH.  Our launcher inherited that PATH and only
prepended the bundle's lean/bin.  The lean4 VS Code extension then
found the student's elan, asked it whether our pinned toolchain
(leanprover/lean4:v4.26.0) was installed, and (since their elan only
knew about the toolchains they'd installed previously) popped a modal
"Lean version ... is not installed.  Do you wish to install it?"
dialog — exactly the breakage the user reported.

The principled fix: make the bundle self-contained, as its name
implies.  It bundles its own lean, its own lake, its own VSCodium.
It shouldn't consult the student's elan at all.  So the launcher
now removes any PATH entry containing ".elan/" or ending in
"/elan/bin" (and unsets any inherited ELAN_HOME) before prepending
the bundle's own paths.  With no elan to consult, the lean4 extension
falls back to using `lean` directly — which, on our PATH, is the
bundled one.

On macOS/Linux: filter PATH entries via tr/grep/paste.
On Windows: cmd.exe string manipulation is brittle, so we reset
PATH to a minimal known-good value (bundle + Windows System32 +
friends).  Students don't need their personal PATH inside VSCodium.

Also add a Tier 1 (verify_bundle.py) check that the launcher
contains elan-scrubbing logic, so a future refactor that drops it
fails CI loudly rather than silently re-introducing the bug.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 templates/start_lean.cmd | 11 ++++++++---
 templates/start_lean.sh  | 13 ++++++++++++-
 tests/verify_bundle.py   | 17 +++++++++++++++++
 3 files changed, 37 insertions(+), 4 deletions(-)

diff --git a/templates/start_lean.cmd b/templates/start_lean.cmd
index c3611dd..64e13e3 100644
--- a/templates/start_lean.cmd
+++ b/templates/start_lean.cmd
@@ -9,10 +9,15 @@ set BUNDLE_ROOT=%BUNDLE_ROOT:~0,-1%
 :: detection so extensions and settings load consistently across OSes.
 set VSCODE_PORTABLE=%BUNDLE_ROOT%\vscodium\data
 
-:: Add lean and git to PATH
-set PATH=%BUNDLE_ROOT%\lean\bin;%BUNDLE_ROOT%\git\cmd;%PATH%
+:: Reset PATH to a minimal known-good value (bundle + Windows essentials).
+:: This prevents the lean4 VS Code extension from finding the student's
+:: pre-existing elan (%USERPROFILE%\.elan\bin\elan.exe from a prior Lean
+:: course) and popping a modal "Lean version ... is not installed"
+:: dialog.  We deliberately drop the student's customised PATH: inside
+:: VSCodium the bundle is self-contained, so nothing else is needed.
+set PATH=%BUNDLE_ROOT%\lean\bin;%BUNDLE_ROOT%\git\cmd;%SystemRoot%\System32;%SystemRoot%;%SystemRoot%\System32\Wbem
 
-:: Prevent elan from interfering
+:: Point elan (if the extension somehow still finds one) at our bundle.
 set ELAN_HOME=%BUNDLE_ROOT%\lean
 
 :: Build LEAN_PATH from all package build directories
diff --git a/templates/start_lean.sh b/templates/start_lean.sh
index ecdd089..b3a9062 100644
--- a/templates/start_lean.sh
+++ b/templates/start_lean.sh
@@ -10,10 +10,21 @@ BUNDLE_ROOT="$(cd "$(dirname "$0")" && pwd)"
 # path logic and works uniformly on Linux, macOS, and Windows.
 export VSCODE_PORTABLE="$BUNDLE_ROOT/vscodium/data"
 
+# Strip any inherited elan from PATH so the lean4 VS Code extension uses
+# the bundled Lean directly.  If the student has ~/.elan/bin on PATH from
+# a prior Lean course, the extension finds their elan, queries it about
+# our toolchain, and (since they don't have our exact version installed)
+# pops a modal "Lean version ... is not installed" dialog.  Removing
+# elan from PATH makes the extension fall back to `lean` on PATH, which
+# is our bundled one.
+PATH="$(printf '%s\n' "$PATH" | tr ':' '\n' | grep -v '\.elan/' | grep -v '/elan/bin$' | paste -sd: -)"
+# Also drop any inherited ELAN_HOME — we set our own below.
+unset ELAN_HOME
+
 # Add lean to PATH
 export PATH="$BUNDLE_ROOT/lean/bin:$PATH"
 
-# Prevent elan from interfering
+# Point elan (if the extension still finds one somewhere) at our bundle.
 export ELAN_HOME="$BUNDLE_ROOT/lean"
 
 # Build LEAN_PATH from all package build directories
diff --git a/tests/verify_bundle.py b/tests/verify_bundle.py
index e3b8c32..5ea7da6 100644
--- a/tests/verify_bundle.py
+++ b/tests/verify_bundle.py
@@ -54,6 +54,23 @@ def verify(bundle_root: Path, platform: str = "windows") -> list[str]:
         if not (bundle_root / r).is_dir():
             errors.append(f"Missing directory: {r}")
 
+    # --- Launcher must strip elan from PATH ---
+    # If a student has elan from a previous Lean course, the lean4 VS
+    # Code extension will find it, query it about our toolchain, and
+    # (when the student doesn't have our version installed) pop a modal
+    # "Lean version ... is not installed" dialog.  The launcher must
+    # scrub elan-containing PATH entries before launching VSCodium so
+    # the extension uses the bundled lean directly.
+    launcher_path = bundle_root / launcher
+    if launcher_path.is_file():
+        text = launcher_path.read_text(errors="ignore")
+        if "elan" not in text.lower():
+            errors.append(
+                f"{launcher}: expected elan-stripping logic "
+                "(students with prior elan installs will hit the "
+                '"Lean version not installed" prompt otherwise)'
+            )
+
     # --- VSCodium ---
     vscodium_path = bundle_root / "vscodium" / vscodium_exe
     if not vscodium_path.is_file():

From d515f9bcacf82053ca7b026e78a87aba7d060922 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sun, 19 Apr 2026 10:53:47 +1000
Subject: [PATCH 07/14] =?UTF-8?q?fix:=20don't=20set=20ELAN=5FHOME=20?=
 =?UTF-8?q?=E2=80=94=20it=20confuses=20lean4=20extension=20into=20looking?=
 =?UTF-8?q?=20for=20elan?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The first pass stripped elan from PATH but still set
ELAN_HOME=<bundle>/lean, which doesn't contain an elan binary.  The
lean4 extension apparently treats ELAN_HOME as "elan is configured
here" and gets stuck when it can't actually find <ELAN_HOME>/bin/elan
— the infoview never opens and no fallback to plain `lean` happens.

Drop ELAN_HOME entirely.  Combined with the PATH stripping, the
extension sees no elan at all and cleanly falls through to using
`lean` from PATH, which the launcher has pointed at the bundled one.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 templates/start_lean.cmd | 17 ++++++++---------
 templates/start_lean.sh  | 19 ++++++++-----------
 2 files changed, 16 insertions(+), 20 deletions(-)

diff --git a/templates/start_lean.cmd b/templates/start_lean.cmd
index 64e13e3..c241f49 100644
--- a/templates/start_lean.cmd
+++ b/templates/start_lean.cmd
@@ -9,16 +9,15 @@ set BUNDLE_ROOT=%BUNDLE_ROOT:~0,-1%
 :: detection so extensions and settings load consistently across OSes.
 set VSCODE_PORTABLE=%BUNDLE_ROOT%\vscodium\data
 
-:: Reset PATH to a minimal known-good value (bundle + Windows essentials).
-:: This prevents the lean4 VS Code extension from finding the student's
-:: pre-existing elan (%USERPROFILE%\.elan\bin\elan.exe from a prior Lean
-:: course) and popping a modal "Lean version ... is not installed"
-:: dialog.  We deliberately drop the student's customised PATH: inside
-:: VSCodium the bundle is self-contained, so nothing else is needed.
+:: Reset PATH to a minimal known-good value (bundle + Windows essentials)
+:: and clear ELAN_HOME.  This prevents the lean4 VS Code extension from
+:: finding the student's pre-existing elan (%USERPROFILE%\.elan\bin\elan.exe
+:: from a prior Lean course) and popping a modal "Lean version ... is
+:: not installed" dialog.  With no elan available and no ELAN_HOME to
+:: confuse it, the extension falls through to `lean` on PATH — our
+:: bundled one.
 set PATH=%BUNDLE_ROOT%\lean\bin;%BUNDLE_ROOT%\git\cmd;%SystemRoot%\System32;%SystemRoot%;%SystemRoot%\System32\Wbem
-
-:: Point elan (if the extension somehow still finds one) at our bundle.
-set ELAN_HOME=%BUNDLE_ROOT%\lean
+set ELAN_HOME=
 
 :: Build LEAN_PATH from all package build directories
 set LEAN_PATH=%BUNDLE_ROOT%\lean\lib\lean;%BUNDLE_ROOT%\project\.lake\build\lib\lean
diff --git a/templates/start_lean.sh b/templates/start_lean.sh
index b3a9062..e975ccd 100644
--- a/templates/start_lean.sh
+++ b/templates/start_lean.sh
@@ -10,23 +10,20 @@ BUNDLE_ROOT="$(cd "$(dirname "$0")" && pwd)"
 # path logic and works uniformly on Linux, macOS, and Windows.
 export VSCODE_PORTABLE="$BUNDLE_ROOT/vscodium/data"
 
-# Strip any inherited elan from PATH so the lean4 VS Code extension uses
-# the bundled Lean directly.  If the student has ~/.elan/bin on PATH from
-# a prior Lean course, the extension finds their elan, queries it about
-# our toolchain, and (since they don't have our exact version installed)
-# pops a modal "Lean version ... is not installed" dialog.  Removing
-# elan from PATH makes the extension fall back to `lean` on PATH, which
-# is our bundled one.
+# Strip any inherited elan from PATH and environment so the lean4 VS
+# Code extension uses the bundled Lean directly.  If the student has
+# ~/.elan/bin on PATH from a prior Lean course, the extension finds
+# their elan, queries it about our toolchain, and (since they don't
+# have our exact version installed) pops a modal "Lean version ... is
+# not installed" dialog.  Removing elan from PATH — and *not* setting
+# ELAN_HOME — makes the extension fall through to `lean` on PATH,
+# which is our bundled one.
 PATH="$(printf '%s\n' "$PATH" | tr ':' '\n' | grep -v '\.elan/' | grep -v '/elan/bin$' | paste -sd: -)"
-# Also drop any inherited ELAN_HOME — we set our own below.
 unset ELAN_HOME
 
 # Add lean to PATH
 export PATH="$BUNDLE_ROOT/lean/bin:$PATH"
 
-# Point elan (if the extension still finds one somewhere) at our bundle.
-export ELAN_HOME="$BUNDLE_ROOT/lean"
-
 # Build LEAN_PATH from all package build directories
 LEAN_PATH="$BUNDLE_ROOT/lean/lib/lean:$BUNDLE_ROOT/project/.lake/build/lib/lean"
 for pkg_dir in "$BUNDLE_ROOT"/project/.lake/packages/*/; do

From 5c3a6504e5584f7b3baba3ea5dba6bee94234d0f Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sun, 19 Apr 2026 11:21:37 +1000
Subject: [PATCH 08/14] test: update launcher tests for ELAN_HOME unset + PATH
 elan-stripping
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The launcher no longer sets ELAN_HOME (it confuses the lean4 extension
into looking for an elan binary that isn't there) and now strips any
inherited elan-containing path entries.  Update tests to match:

  - test_elan_home → test_elan_home_not_set: ELAN_HOME must be absent
  - test_elan_home_exists → test_elan_home_unset/cleared
  - Add test_path_has_no_elan on each launcher variant

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 tests/test_launcher.py | 65 ++++++++++++++++++++++++++++++++++++------
 1 file changed, 56 insertions(+), 9 deletions(-)

diff --git a/tests/test_launcher.py b/tests/test_launcher.py
index 08c520c..5c0d387 100644
--- a/tests/test_launcher.py
+++ b/tests/test_launcher.py
@@ -114,9 +114,24 @@ def test_path_contains_lean_bin(self, result: dict[str, str]) -> None:
             f"PATH should start with {lean_bin}:, got: {result['PATH'][:200]}"
         )
 
-    def test_elan_home(self, result: dict[str, str]) -> None:
-        root = result["_bundle_root"]
-        assert result["ELAN_HOME"] == f"{root}/lean"
+    def test_elan_home_not_set(self, result: dict[str, str]) -> None:
+        # The launcher deliberately unsets ELAN_HOME — if it stays set,
+        # the lean4 VS Code extension tries to use elan as configured
+        # there and gets stuck when there's no elan binary at that path.
+        assert "ELAN_HOME" not in result, (
+            f"ELAN_HOME should be unset, got: {result.get('ELAN_HOME')!r}"
+        )
+
+    def test_path_has_no_elan(self, result: dict[str, str]) -> None:
+        # The launcher strips any inherited elan-containing path entries
+        # so the lean4 extension can't find a student's prior elan install.
+        for entry in result["PATH"].split(":"):
+            assert ".elan/" not in entry, (
+                f"PATH entry contains .elan/: {entry!r}"
+            )
+            assert not entry.endswith("/elan/bin"), (
+                f"PATH entry ends with /elan/bin: {entry!r}"
+            )
 
     def test_lean_path_contains_toolchain_lib(self, result: dict[str, str]) -> None:
         root = result["_bundle_root"]
@@ -213,8 +228,21 @@ def test_path_contains_git_cmd(self, result: dict[str, str]) -> None:
         path_val = result["PATH"]
         assert "\\git\\cmd" in path_val
 
-    def test_elan_home(self, result: dict[str, str]) -> None:
-        assert result["ELAN_HOME"].endswith("\\lean")
+    def test_elan_home_not_set(self, result: dict[str, str]) -> None:
+        # The launcher deliberately clears ELAN_HOME — if it stays set,
+        # the lean4 VS Code extension tries to use elan as configured
+        # there and gets stuck when there's no elan binary at that path.
+        # cmd.exe `echo !VAR!` prints literal `!VAR!` when VAR is unset,
+        # but with EnableDelayedExpansion it prints empty.
+        val = result.get("ELAN_HOME", "")
+        assert val == "" or val == "!ELAN_HOME!", (
+            f"ELAN_HOME should be empty/unset, got: {val!r}"
+        )
+
+    def test_path_has_no_elan(self, result: dict[str, str]) -> None:
+        for entry in result["PATH"].split(";"):
+            assert "\\.elan\\" not in entry, f"PATH entry contains .elan\\: {entry!r}"
+            assert not entry.endswith("\\elan\\bin"), f"PATH entry ends with elan\\bin: {entry!r}"
 
     def test_lean_path_contains_toolchain_lib(self, result: dict[str, str]) -> None:
         entries = result["LEAN_PATH"].split(";")
@@ -310,8 +338,16 @@ def result(self) -> dict[str, str]:
     def test_path_contains_lean_bin(self, result: dict[str, str]) -> None:
         assert "/lean/bin" in result["PATH"]
 
-    def test_elan_home_exists(self, result: dict[str, str]) -> None:
-        assert Path(result["ELAN_HOME"]).is_dir()
+    def test_elan_home_unset(self, result: dict[str, str]) -> None:
+        # Launcher must unset ELAN_HOME so the lean4 extension falls
+        # through to `lean` on PATH rather than getting stuck looking
+        # for an elan binary.
+        assert "ELAN_HOME" not in result
+
+    def test_path_has_no_elan(self, result: dict[str, str]) -> None:
+        for entry in result["PATH"].split(":"):
+            assert ".elan/" not in entry, f"PATH entry contains .elan/: {entry!r}"
+            assert not entry.endswith("/elan/bin"), f"PATH entry ends with /elan/bin: {entry!r}"
 
     def test_lean_path_dirs_exist(self, result: dict[str, str]) -> None:
         for entry in result["LEAN_PATH"].split(":"):
@@ -367,8 +403,19 @@ def result(self) -> dict[str, str]:
     def test_path_contains_lean_bin(self, result: dict[str, str]) -> None:
         assert "\\lean\\bin" in result["PATH"]
 
-    def test_elan_home_exists(self, result: dict[str, str]) -> None:
-        assert Path(result["ELAN_HOME"]).is_dir()
+    def test_elan_home_cleared(self, result: dict[str, str]) -> None:
+        # Launcher clears ELAN_HOME so the lean4 extension falls
+        # through to `lean` on PATH rather than getting stuck looking
+        # for an elan binary.
+        val = result.get("ELAN_HOME", "")
+        assert val == "" or val == "!ELAN_HOME!", (
+            f"ELAN_HOME should be empty, got: {val!r}"
+        )
+
+    def test_path_has_no_elan(self, result: dict[str, str]) -> None:
+        for entry in result["PATH"].split(";"):
+            assert "\\.elan\\" not in entry, f"PATH entry contains .elan\\: {entry!r}"
+            assert not entry.endswith("\\elan\\bin"), f"PATH entry ends with elan\\bin: {entry!r}"
 
     def test_lean_path_dirs_exist(self, result: dict[str, str]) -> None:
         for entry in result["LEAN_PATH"].split(";"):

From 8c7aad8ec29ada0b0eab498b90f2c474e18390ae Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sun, 19 Apr 2026 12:02:00 +1000
Subject: [PATCH 09/14] fix: link bundled toolchain into student's elan so
 extension sees it installed
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Discovered the lean4 VS Code extension unconditionally prepends
\$HOME/.elan/bin to PATH via addToProcessEnvPATH during activation
(vscode-lean4 extension.js):

    addToProcessEnvPATH(join(homedir(), ".elan", "bin"))

So the previous PATH-stripping approach gets undone the moment the
extension activates: the student's elan is back on PATH, gets queried
about our toolchain, reports "not installed", and pops the modal
"Lean version ... is not installed" dialog.

New approach: symlink our bundled Lean directly into the student's
elan toolchains directory, bypassing elan's CLI (which refuses
release-format names like leanprover/lean4:v4.26.0 for `toolchain
link`):

    ln -s \$BUNDLE_ROOT/lean \$HOME/.elan/toolchains/<encoded-name>

Elan treats anything under its toolchains/ dir as an installed
toolchain — it doesn't care who put the dir there.  Now when the
extension asks elan "is leanprover/lean4:v4.26.0 installed?", elan
walks ~/.elan/toolchains/leanprover--lean4---v4.26.0/ (our symlink),
finds bin/lean, and reports "installed".  No dialog; LSP starts
normally via elan's usual proxy mechanism, which dispatches to our
bundled lean via the symlink.

The symlink is skipped if one with that name already exists (student
already installed the toolchain the normal way) or if they have no
~/.elan at all (we fall cleanly through to bundled `lean` on PATH).

Windows uses `mklink /J` for a directory junction, which works
without admin privileges.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 templates/start_lean.cmd | 31 ++++++++++++++++++++++++-------
 templates/start_lean.sh  | 38 ++++++++++++++++++++++++++++++--------
 2 files changed, 54 insertions(+), 15 deletions(-)

diff --git a/templates/start_lean.cmd b/templates/start_lean.cmd
index c241f49..be68b64 100644
--- a/templates/start_lean.cmd
+++ b/templates/start_lean.cmd
@@ -9,16 +9,33 @@ set BUNDLE_ROOT=%BUNDLE_ROOT:~0,-1%
 :: detection so extensions and settings load consistently across OSes.
 set VSCODE_PORTABLE=%BUNDLE_ROOT%\vscodium\data
 
-:: Reset PATH to a minimal known-good value (bundle + Windows essentials)
-:: and clear ELAN_HOME.  This prevents the lean4 VS Code extension from
-:: finding the student's pre-existing elan (%USERPROFILE%\.elan\bin\elan.exe
-:: from a prior Lean course) and popping a modal "Lean version ... is
-:: not installed" dialog.  With no elan available and no ELAN_HOME to
-:: confuse it, the extension falls through to `lean` on PATH — our
-:: bundled one.
+:: If the student has a pre-existing elan install, the lean4 VS Code
+:: extension unconditionally prepends %USERPROFILE%\.elan\bin to PATH
+:: and queries that elan about the project's toolchain.  When elan
+:: doesn't have our exact version installed, a modal "Lean version ...
+:: is not installed" dialog appears.
+::
+:: Fix: junction the bundled Lean into the student's elan toolchains
+:: directory so elan reports our toolchain as installed.  We also
+:: reset PATH to a minimal known-good value and clear ELAN_HOME so
+:: that students without elan fall cleanly through to our bundled
+:: `lean` on PATH.
 set PATH=%BUNDLE_ROOT%\lean\bin;%BUNDLE_ROOT%\git\cmd;%SystemRoot%\System32;%SystemRoot%;%SystemRoot%\System32\Wbem
 set ELAN_HOME=
 
+:: Register the bundled toolchain with the student's elan if present
+:: (no-op otherwise).  mklink /J creates a directory junction, which
+:: on Windows works without admin privileges, unlike symlinks.
+if exist "%USERPROFILE%\.elan\toolchains" (
+    for /f "usebackq delims=" %%A in (`powershell -NoProfile -Command "(Get-Content '%BUNDLE_ROOT%\project\lean-toolchain' -Raw).Trim().Replace('/','--').Replace(':','---')"`) do set "TOOLCHAIN_ENCODED=%%A"
+    setlocal EnableDelayedExpansion
+    if defined TOOLCHAIN_ENCODED if not exist "%USERPROFILE%\.elan\toolchains\!TOOLCHAIN_ENCODED!" (
+        mklink /J "%USERPROFILE%\.elan\toolchains\!TOOLCHAIN_ENCODED!" "%BUNDLE_ROOT%\lean" >nul 2>&1
+    )
+    endlocal
+    set TOOLCHAIN_ENCODED=
+)
+
 :: Build LEAN_PATH from all package build directories
 set LEAN_PATH=%BUNDLE_ROOT%\lean\lib\lean;%BUNDLE_ROOT%\project\.lake\build\lib\lean
 for /d %%P in ("%BUNDLE_ROOT%\project\.lake\packages\*") do (
diff --git a/templates/start_lean.sh b/templates/start_lean.sh
index e975ccd..d6c7881 100644
--- a/templates/start_lean.sh
+++ b/templates/start_lean.sh
@@ -10,20 +10,42 @@ BUNDLE_ROOT="$(cd "$(dirname "$0")" && pwd)"
 # path logic and works uniformly on Linux, macOS, and Windows.
 export VSCODE_PORTABLE="$BUNDLE_ROOT/vscodium/data"
 
-# Strip any inherited elan from PATH and environment so the lean4 VS
-# Code extension uses the bundled Lean directly.  If the student has
-# ~/.elan/bin on PATH from a prior Lean course, the extension finds
-# their elan, queries it about our toolchain, and (since they don't
-# have our exact version installed) pops a modal "Lean version ... is
-# not installed" dialog.  Removing elan from PATH — and *not* setting
-# ELAN_HOME — makes the extension fall through to `lean` on PATH,
-# which is our bundled one.
+# If the student has a pre-existing elan install, the lean4 VS Code
+# extension unconditionally prepends $HOME/.elan/bin to PATH on
+# activation and queries that elan about the project's toolchain.
+# When elan doesn't have our exact toolchain installed, it pops a
+# modal "Lean version ... is not installed" dialog.
+#
+# Fix: symlink the bundled Lean into the student's elan toolchains
+# directory.  Elan then reports the toolchain as installed and the
+# extension proceeds normally.  The symlink reuses our binaries, so
+# no disk duplication.
+#
+# (We also strip elan from PATH and clear ELAN_HOME defensively for
+# students with no elan installed at all: if ~/.elan doesn't exist,
+# the extension's PATH prepend is a no-op and it falls through to
+# `lean` on PATH, which is our bundled one.)
 PATH="$(printf '%s\n' "$PATH" | tr ':' '\n' | grep -v '\.elan/' | grep -v '/elan/bin$' | paste -sd: -)"
 unset ELAN_HOME
 
 # Add lean to PATH
 export PATH="$BUNDLE_ROOT/lean/bin:$PATH"
 
+# Register the bundled toolchain with the student's elan (no-op if
+# they don't have elan, or if a toolchain with this name is already
+# installed).  This bypasses `elan toolchain link` — which refuses
+# release-format names like leanprover/lean4:v4.26.0 — by creating
+# the directory elan expects to find directly.
+if [ -d "$HOME/.elan/toolchains" ]; then
+    _toolchain_pin=$(cat "$BUNDLE_ROOT/project/lean-toolchain" 2>/dev/null | tr -d '[:space:]')
+    _toolchain_encoded=$(printf '%s' "$_toolchain_pin" | sed 's|/|--|g; s|:|---|g')
+    _toolchain_dir="$HOME/.elan/toolchains/$_toolchain_encoded"
+    if [ -n "$_toolchain_encoded" ] && [ ! -e "$_toolchain_dir" ] && [ ! -L "$_toolchain_dir" ]; then
+        ln -s "$BUNDLE_ROOT/lean" "$_toolchain_dir" 2>/dev/null || true
+    fi
+    unset _toolchain_pin _toolchain_encoded _toolchain_dir
+fi
+
 # Build LEAN_PATH from all package build directories
 LEAN_PATH="$BUNDLE_ROOT/lean/lib/lean:$BUNDLE_ROOT/project/.lake/build/lib/lean"
 for pkg_dir in "$BUNDLE_ROOT"/project/.lake/packages/*/; do

From d8db0e8b1bee832385ccdf5a790bfa75f3c7937e Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sun, 19 Apr 2026 12:37:38 +1000
Subject: [PATCH 10/14] fix: check for elan binary, not toolchains/ dir

Fresh `elan-init --default-toolchain none` installs don't create the
~/.elan/toolchains/ subdirectory until the first toolchain install,
so our gate was skipping the symlink creation on exactly the CI
scenario the fix was meant to handle.  Check for the elan binary
itself (~/.elan/bin/elan) instead, and mkdir -p the toolchains dir
before creating the symlink.

Also tolerate cmd.exe's `ECHO is on/off.` when probing an empty
ELAN_HOME in the Windows launcher test.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 templates/start_lean.cmd |  9 ++++++---
 templates/start_lean.sh  | 14 +++++++++-----
 tests/test_launcher.py   |  5 ++++-
 3 files changed, 19 insertions(+), 9 deletions(-)

diff --git a/templates/start_lean.cmd b/templates/start_lean.cmd
index be68b64..c57e3ba 100644
--- a/templates/start_lean.cmd
+++ b/templates/start_lean.cmd
@@ -24,12 +24,15 @@ set PATH=%BUNDLE_ROOT%\lean\bin;%BUNDLE_ROOT%\git\cmd;%SystemRoot%\System32;%Sys
 set ELAN_HOME=
 
 :: Register the bundled toolchain with the student's elan if present
-:: (no-op otherwise).  mklink /J creates a directory junction, which
-:: on Windows works without admin privileges, unlike symlinks.
-if exist "%USERPROFILE%\.elan\toolchains" (
+:: (no-op otherwise).  Check for the elan binary rather than the
+:: toolchains/ dir, which doesn't exist on fresh `elan-init
+:: --default-toolchain none` installs.  mklink /J creates a directory
+:: junction, which works on Windows without admin privileges.
+if exist "%USERPROFILE%\.elan\bin\elan.exe" (
     for /f "usebackq delims=" %%A in (`powershell -NoProfile -Command "(Get-Content '%BUNDLE_ROOT%\project\lean-toolchain' -Raw).Trim().Replace('/','--').Replace(':','---')"`) do set "TOOLCHAIN_ENCODED=%%A"
     setlocal EnableDelayedExpansion
     if defined TOOLCHAIN_ENCODED if not exist "%USERPROFILE%\.elan\toolchains\!TOOLCHAIN_ENCODED!" (
+        if not exist "%USERPROFILE%\.elan\toolchains" mkdir "%USERPROFILE%\.elan\toolchains"
         mklink /J "%USERPROFILE%\.elan\toolchains\!TOOLCHAIN_ENCODED!" "%BUNDLE_ROOT%\lean" >nul 2>&1
     )
     endlocal
diff --git a/templates/start_lean.sh b/templates/start_lean.sh
index d6c7881..6cc58ef 100644
--- a/templates/start_lean.sh
+++ b/templates/start_lean.sh
@@ -32,15 +32,19 @@ unset ELAN_HOME
 export PATH="$BUNDLE_ROOT/lean/bin:$PATH"
 
 # Register the bundled toolchain with the student's elan (no-op if
-# they don't have elan, or if a toolchain with this name is already
-# installed).  This bypasses `elan toolchain link` — which refuses
-# release-format names like leanprover/lean4:v4.26.0 — by creating
-# the directory elan expects to find directly.
-if [ -d "$HOME/.elan/toolchains" ]; then
+# they don't have elan).  Bypasses `elan toolchain link` — which
+# refuses release-format names like leanprover/lean4:v4.26.0 — by
+# creating the directory elan expects to find directly.
+#
+# Check for ~/.elan/bin/elan (the binary), not ~/.elan/toolchains/,
+# because fresh elan installs with --default-toolchain none don't
+# create the toolchains/ subdir until the first install.
+if [ -x "$HOME/.elan/bin/elan" ]; then
     _toolchain_pin=$(cat "$BUNDLE_ROOT/project/lean-toolchain" 2>/dev/null | tr -d '[:space:]')
     _toolchain_encoded=$(printf '%s' "$_toolchain_pin" | sed 's|/|--|g; s|:|---|g')
     _toolchain_dir="$HOME/.elan/toolchains/$_toolchain_encoded"
     if [ -n "$_toolchain_encoded" ] && [ ! -e "$_toolchain_dir" ] && [ ! -L "$_toolchain_dir" ]; then
+        mkdir -p "$HOME/.elan/toolchains"
         ln -s "$BUNDLE_ROOT/lean" "$_toolchain_dir" 2>/dev/null || true
     fi
     unset _toolchain_pin _toolchain_encoded _toolchain_dir
diff --git a/tests/test_launcher.py b/tests/test_launcher.py
index 5c0d387..5295842 100644
--- a/tests/test_launcher.py
+++ b/tests/test_launcher.py
@@ -408,7 +408,10 @@ def test_elan_home_cleared(self, result: dict[str, str]) -> None:
         # through to `lean` on PATH rather than getting stuck looking
         # for an elan binary.
         val = result.get("ELAN_HOME", "")
-        assert val == "" or val == "!ELAN_HOME!", (
+        # cmd.exe quirks: `echo !VAR!` prints `!VAR!` when unexpanded,
+        # or `ECHO is on/off.` when VAR is empty.  All three indicate
+        # the variable is not meaningfully set.
+        assert val in ("", "!ELAN_HOME!") or val.startswith("ECHO is "), (
             f"ELAN_HOME should be empty, got: {val!r}"
         )
 

From 0428e5fdd630dd932931698572a0962c08e05f6b Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sun, 19 Apr 2026 13:08:49 +1000
Subject: [PATCH 11/14] test: tolerate cmd.exe ECHO-is-on/off output in
 template launcher test too

Earlier fix only covered the bundle-launcher test (test_elan_home_cleared);
the template-launcher test (test_elan_home_not_set) still asserted on
the strict empty/literal form.
---
 tests/test_launcher.py | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/tests/test_launcher.py b/tests/test_launcher.py
index 5295842..e01c50b 100644
--- a/tests/test_launcher.py
+++ b/tests/test_launcher.py
@@ -232,10 +232,11 @@ def test_elan_home_not_set(self, result: dict[str, str]) -> None:
         # The launcher deliberately clears ELAN_HOME — if it stays set,
         # the lean4 VS Code extension tries to use elan as configured
         # there and gets stuck when there's no elan binary at that path.
-        # cmd.exe `echo !VAR!` prints literal `!VAR!` when VAR is unset,
-        # but with EnableDelayedExpansion it prints empty.
+        # cmd.exe quirks: `echo !VAR!` may print the literal `!VAR!`, or
+        # `ECHO is on/off.` when VAR is empty.  All three indicate
+        # the variable is not meaningfully set.
         val = result.get("ELAN_HOME", "")
-        assert val == "" or val == "!ELAN_HOME!", (
+        assert val in ("", "!ELAN_HOME!") or val.startswith("ECHO is "), (
             f"ELAN_HOME should be empty/unset, got: {val!r}"
         )
 

From 5730e18fc20a28772beb2df6ad6f8f6bf887ede2 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sun, 19 Apr 2026 16:43:01 +1000
Subject: [PATCH 12/14] fix(windows): use single PowerShell call for toolchain
 junction creation
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The cmd-native version with `for /f` + `setlocal EnableDelayedExpansion`
didn't actually create the junction in CI — the delayed-expansion
variable from an outer `for` scope doesn't reliably survive the
`setlocal`/`endlocal` dance inside a single cmd script.

Rewrite as one PowerShell call using New-Item -ItemType Junction,
which is the PowerShell equivalent of `mklink /J` (no admin needed).
---
 templates/start_lean.cmd | 25 +++++++++++++------------
 1 file changed, 13 insertions(+), 12 deletions(-)

diff --git a/templates/start_lean.cmd b/templates/start_lean.cmd
index c57e3ba..4695b4c 100644
--- a/templates/start_lean.cmd
+++ b/templates/start_lean.cmd
@@ -24,19 +24,20 @@ set PATH=%BUNDLE_ROOT%\lean\bin;%BUNDLE_ROOT%\git\cmd;%SystemRoot%\System32;%Sys
 set ELAN_HOME=
 
 :: Register the bundled toolchain with the student's elan if present
-:: (no-op otherwise).  Check for the elan binary rather than the
-:: toolchains/ dir, which doesn't exist on fresh `elan-init
-:: --default-toolchain none` installs.  mklink /J creates a directory
-:: junction, which works on Windows without admin privileges.
+:: (no-op otherwise).  New-Item -ItemType Junction creates a directory
+:: junction without admin privileges — equivalent to `mklink /J`.
+:: Done in a single PowerShell invocation to avoid cmd.exe's fragile
+:: `for /f` + `setlocal` delayed-expansion dance.
 if exist "%USERPROFILE%\.elan\bin\elan.exe" (
-    for /f "usebackq delims=" %%A in (`powershell -NoProfile -Command "(Get-Content '%BUNDLE_ROOT%\project\lean-toolchain' -Raw).Trim().Replace('/','--').Replace(':','---')"`) do set "TOOLCHAIN_ENCODED=%%A"
-    setlocal EnableDelayedExpansion
-    if defined TOOLCHAIN_ENCODED if not exist "%USERPROFILE%\.elan\toolchains\!TOOLCHAIN_ENCODED!" (
-        if not exist "%USERPROFILE%\.elan\toolchains" mkdir "%USERPROFILE%\.elan\toolchains"
-        mklink /J "%USERPROFILE%\.elan\toolchains\!TOOLCHAIN_ENCODED!" "%BUNDLE_ROOT%\lean" >nul 2>&1
-    )
-    endlocal
-    set TOOLCHAIN_ENCODED=
+    powershell -NoProfile -Command ^
+      "$pin = (Get-Content '%BUNDLE_ROOT%\project\lean-toolchain' -Raw).Trim();" ^
+      "$enc = $pin.Replace('/','--').Replace(':','---');" ^
+      "$tcParent = Join-Path $env:USERPROFILE '.elan\toolchains';" ^
+      "$tcDir = Join-Path $tcParent $enc;" ^
+      "if (-not (Test-Path $tcDir)) {" ^
+      "  New-Item -ItemType Directory -Force -Path $tcParent | Out-Null;" ^
+      "  New-Item -ItemType Junction -Path $tcDir -Target '%BUNDLE_ROOT%\lean' | Out-Null" ^
+      "}" >nul 2>&1
 )
 
 :: Build LEAN_PATH from all package build directories

From 66a14f10c671411741a6da43820dffc821a57962 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sun, 19 Apr 2026 17:16:47 +1000
Subject: [PATCH 13/14] fix(windows): put PowerShell junction call on one line,
 not in parens
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

cmd.exe's `^` line continuation is unreliable inside `( ... )`
blocks — the CI showed VSCodium never launched because the launcher
script hung on malformed PowerShell invocation.

Drop the multi-line PowerShell block and the outer `( ... )` wrapper;
just use an unconditional `if exist ... powershell ...` one-liner.
---
 templates/start_lean.cmd | 17 ++++-------------
 1 file changed, 4 insertions(+), 13 deletions(-)

diff --git a/templates/start_lean.cmd b/templates/start_lean.cmd
index 4695b4c..a67af28 100644
--- a/templates/start_lean.cmd
+++ b/templates/start_lean.cmd
@@ -26,19 +26,10 @@ set ELAN_HOME=
 :: Register the bundled toolchain with the student's elan if present
 :: (no-op otherwise).  New-Item -ItemType Junction creates a directory
 :: junction without admin privileges — equivalent to `mklink /J`.
-:: Done in a single PowerShell invocation to avoid cmd.exe's fragile
-:: `for /f` + `setlocal` delayed-expansion dance.
-if exist "%USERPROFILE%\.elan\bin\elan.exe" (
-    powershell -NoProfile -Command ^
-      "$pin = (Get-Content '%BUNDLE_ROOT%\project\lean-toolchain' -Raw).Trim();" ^
-      "$enc = $pin.Replace('/','--').Replace(':','---');" ^
-      "$tcParent = Join-Path $env:USERPROFILE '.elan\toolchains';" ^
-      "$tcDir = Join-Path $tcParent $enc;" ^
-      "if (-not (Test-Path $tcDir)) {" ^
-      "  New-Item -ItemType Directory -Force -Path $tcParent | Out-Null;" ^
-      "  New-Item -ItemType Junction -Path $tcDir -Target '%BUNDLE_ROOT%\lean' | Out-Null" ^
-      "}" >nul 2>&1
-)
+:: Done in a single PowerShell invocation on one line: cmd.exe's `^`
+:: line continuation is unreliable inside `( ... )` blocks and can
+:: hang the script (seen as VSCodium never launching on Windows CI).
+if exist "%USERPROFILE%\.elan\bin\elan.exe" powershell -NoProfile -Command "$pin = (Get-Content '%BUNDLE_ROOT%\project\lean-toolchain' -Raw).Trim(); $enc = $pin.Replace('/','--').Replace(':','---'); $tcParent = Join-Path $env:USERPROFILE '.elan\toolchains'; $tcDir = Join-Path $tcParent $enc; if (-not (Test-Path $tcDir)) { New-Item -ItemType Directory -Force -Path $tcParent | Out-Null; New-Item -ItemType Junction -Path $tcDir -Target '%BUNDLE_ROOT%\lean' | Out-Null }" >nul 2>&1
 
 :: Build LEAN_PATH from all package build directories
 set LEAN_PATH=%BUNDLE_ROOT%\lean\lib\lean;%BUNDLE_ROOT%\project\.lake\build\lib\lean

From 68b6a27d5edfd6a5040c92842141b60594177448 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sun, 19 Apr 2026 17:53:51 +1000
Subject: [PATCH 14/14] fix(windows): pre-compute encoded toolchain name at
 assembly time
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

CDP timeout failures kept appearing on Windows GUI tests — the cmd
launcher was hanging before VSCodium ever spawned.  Even after moving
the PowerShell call to one line, something about the inline string
manipulation was still causing the launcher to hang.

Cleaner approach: compute the elan-encoded toolchain name in
assemble.py (Python) and substitute it as @@TOOLCHAIN_ENCODED@@ in
both launcher templates at bundle assembly time.  The launcher then
just uses the pre-computed value with a literal `mklink /J` (Windows)
or `ln -s` (Unix) — no string parsing, no PowerShell, no fragility.

Tests updated to substitute the placeholder when patching the
launcher templates.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 assemble.py              | 13 ++++++++++---
 templates/start_lean.cmd | 16 ++++++++++------
 templates/start_lean.sh  | 19 ++++++-------------
 tests/test_launcher.py   |  6 ++++++
 4 files changed, 32 insertions(+), 22 deletions(-)

diff --git a/assemble.py b/assemble.py
index f24e1d4..ce9a580 100644
--- a/assemble.py
+++ b/assemble.py
@@ -779,11 +779,18 @@ def assemble_bundle(
         launcher_src = templates_dir / "start_lean.sh"
         launcher_dst = bundle_dir / "Start_Lean.sh"
 
-    # Substitute @@OPEN_FILE@@ placeholder with the selected file (or
-    # empty string if none).  This happens at assembly time so the
-    # launcher doesn't need to scan for files at runtime.
+    # Substitute placeholders in the launcher template at assembly time
+    # so the launcher script doesn't need to scan files or parse strings
+    # at runtime (cmd.exe parsing is fragile).
+    #
+    #   @@OPEN_FILE@@        - filename to open on launch (or empty)
+    #   @@TOOLCHAIN_ENCODED@@ - elan-encoded toolchain dir name, e.g.
+    #                          leanprover/lean4:v4.26.0 -> leanprover--lean4---v4.26.0
+    toolchain_pin = (project_dir / "lean-toolchain").read_text().strip()
+    toolchain_encoded = toolchain_pin.replace("/", "--").replace(":", "---")
     launcher_text = launcher_src.read_text()
     launcher_text = launcher_text.replace("@@OPEN_FILE@@", open_file or "")
+    launcher_text = launcher_text.replace("@@TOOLCHAIN_ENCODED@@", toolchain_encoded)
     launcher_dst.write_text(launcher_text)
     if not platform.startswith("windows"):
         launcher_dst.chmod(0o755)
diff --git a/templates/start_lean.cmd b/templates/start_lean.cmd
index a67af28..be1183a 100644
--- a/templates/start_lean.cmd
+++ b/templates/start_lean.cmd
@@ -24,12 +24,16 @@ set PATH=%BUNDLE_ROOT%\lean\bin;%BUNDLE_ROOT%\git\cmd;%SystemRoot%\System32;%Sys
 set ELAN_HOME=
 
 :: Register the bundled toolchain with the student's elan if present
-:: (no-op otherwise).  New-Item -ItemType Junction creates a directory
-:: junction without admin privileges — equivalent to `mklink /J`.
-:: Done in a single PowerShell invocation on one line: cmd.exe's `^`
-:: line continuation is unreliable inside `( ... )` blocks and can
-:: hang the script (seen as VSCodium never launching on Windows CI).
-if exist "%USERPROFILE%\.elan\bin\elan.exe" powershell -NoProfile -Command "$pin = (Get-Content '%BUNDLE_ROOT%\project\lean-toolchain' -Raw).Trim(); $enc = $pin.Replace('/','--').Replace(':','---'); $tcParent = Join-Path $env:USERPROFILE '.elan\toolchains'; $tcDir = Join-Path $tcParent $enc; if (-not (Test-Path $tcDir)) { New-Item -ItemType Directory -Force -Path $tcParent | Out-Null; New-Item -ItemType Junction -Path $tcDir -Target '%BUNDLE_ROOT%\lean' | Out-Null }" >nul 2>&1
+:: (no-op otherwise).  The encoded name is substituted at bundle
+:: assembly time so the launcher doesn't have to parse strings at
+:: runtime (cmd.exe string handling is fragile).
+:: `mklink /J` creates a directory junction without admin privileges.
+set TOOLCHAIN_ENCODED=@@TOOLCHAIN_ENCODED@@
+if exist "%USERPROFILE%\.elan\bin\elan.exe" if not exist "%USERPROFILE%\.elan\toolchains\%TOOLCHAIN_ENCODED%" if not "%TOOLCHAIN_ENCODED%"=="" (
+    if not exist "%USERPROFILE%\.elan\toolchains" mkdir "%USERPROFILE%\.elan\toolchains" >nul 2>&1
+    mklink /J "%USERPROFILE%\.elan\toolchains\%TOOLCHAIN_ENCODED%" "%BUNDLE_ROOT%\lean" >nul 2>&1
+)
+set TOOLCHAIN_ENCODED=
 
 :: Build LEAN_PATH from all package build directories
 set LEAN_PATH=%BUNDLE_ROOT%\lean\lib\lean;%BUNDLE_ROOT%\project\.lake\build\lib\lean
diff --git a/templates/start_lean.sh b/templates/start_lean.sh
index 6cc58ef..a8c3d99 100644
--- a/templates/start_lean.sh
+++ b/templates/start_lean.sh
@@ -35,20 +35,13 @@ export PATH="$BUNDLE_ROOT/lean/bin:$PATH"
 # they don't have elan).  Bypasses `elan toolchain link` — which
 # refuses release-format names like leanprover/lean4:v4.26.0 — by
 # creating the directory elan expects to find directly.
-#
-# Check for ~/.elan/bin/elan (the binary), not ~/.elan/toolchains/,
-# because fresh elan installs with --default-toolchain none don't
-# create the toolchains/ subdir until the first install.
-if [ -x "$HOME/.elan/bin/elan" ]; then
-    _toolchain_pin=$(cat "$BUNDLE_ROOT/project/lean-toolchain" 2>/dev/null | tr -d '[:space:]')
-    _toolchain_encoded=$(printf '%s' "$_toolchain_pin" | sed 's|/|--|g; s|:|---|g')
-    _toolchain_dir="$HOME/.elan/toolchains/$_toolchain_encoded"
-    if [ -n "$_toolchain_encoded" ] && [ ! -e "$_toolchain_dir" ] && [ ! -L "$_toolchain_dir" ]; then
-        mkdir -p "$HOME/.elan/toolchains"
-        ln -s "$BUNDLE_ROOT/lean" "$_toolchain_dir" 2>/dev/null || true
-    fi
-    unset _toolchain_pin _toolchain_encoded _toolchain_dir
+# The encoded name is substituted at bundle assembly time.
+_TC_ENC="@@TOOLCHAIN_ENCODED@@"
+if [ -n "$_TC_ENC" ] && [ -x "$HOME/.elan/bin/elan" ] && [ ! -e "$HOME/.elan/toolchains/$_TC_ENC" ]; then
+    mkdir -p "$HOME/.elan/toolchains"
+    ln -s "$BUNDLE_ROOT/lean" "$HOME/.elan/toolchains/$_TC_ENC" 2>/dev/null || true
 fi
+unset _TC_ENC
 
 # Build LEAN_PATH from all package build directories
 LEAN_PATH="$BUNDLE_ROOT/lean/lib/lean:$BUNDLE_ROOT/project/.lake/build/lib/lean"
diff --git a/tests/test_launcher.py b/tests/test_launcher.py
index e01c50b..b74f373 100644
--- a/tests/test_launcher.py
+++ b/tests/test_launcher.py
@@ -62,6 +62,9 @@ def _parse_probe_output(path: Path) -> dict[str, str]:
 def _patch_unix_launcher(template: Path, output: Path) -> None:
     """Replace the VSCodium launch block with an environment probe."""
     text = template.read_text()
+    # Substitute @@-placeholders that assemble.py would normally fill in.
+    text = text.replace("@@OPEN_FILE@@", "")
+    text = text.replace("@@TOOLCHAIN_ENCODED@@", "")
     # Replace from "# Launch VSCodium\n" (exact line) through end of file.
     # This must NOT match "# Launch VSCodium with Lean 4..." on line 2.
     text = re.sub(
@@ -180,6 +183,9 @@ def test_workspace_argument(self, result: dict[str, str]) -> None:
 def _patch_windows_launcher(template: Path, output: Path) -> None:
     """Replace the VSCodium launch block with an environment probe."""
     text = template.read_text()
+    # Substitute @@-placeholders that assemble.py would normally fill in.
+    text = text.replace("@@OPEN_FILE@@", "")
+    text = text.replace("@@TOOLCHAIN_ENCODED@@", "")
     # Replace from ":: Launch VSCodium" through end of file.
     # Use a lambda to avoid re.sub interpreting backslashes in the
     # replacement string as group references (\p → bad escape).