test: detect Lean toolchain-install prompt in CI

.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://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
+
       - name: "Tier 6: Install Playwright test deps"
         shell: pwsh
         run: |

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)

templates/start_lean.cmd

@@ -9,11 +9,31 @@ 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%
+:: 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=
 
-:: Prevent elan from interfering
-set ELAN_HOME=%BUNDLE_ROOT%\lean
+:: Register the bundled toolchain with the student's elan if present
+:: (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

templates/start_lean.sh

@@ -10,11 +10,38 @@ BUNDLE_ROOT="$(cd "$(dirname "$0")" && pwd)"
 # path logic and works uniformly on Linux, macOS, and Windows.
 export VSCODE_PORTABLE="$BUNDLE_ROOT/vscodium/data"
 
+# 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"
 
-# Prevent elan from interfering
-export ELAN_HOME="$BUNDLE_ROOT/lean"
+# Register the bundled toolchain with the student's elan (no-op if
+# 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.
+# 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"

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

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(
@@ -114,9 +117,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"]
@@ -165,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).
@@ -213,8 +234,22 @@ 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 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 in ("", "!ELAN_HOME!") or val.startswith("ECHO is "), (
+            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 +345,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 +410,22 @@ 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", "")
+        # 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}"
+        )
+
+    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(";"):

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():