diff --git a/.github/workflows/build-and-test.yml b/.github/workflows/build-and-test.yml index 3c85691..57ddab1 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://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: | 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 c3611dd..be1183a 100644 --- a/templates/start_lean.cmd +++ b/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 diff --git a/templates/start_lean.sh b/templates/start_lean.sh index ecdd089..a8c3d99 100644 --- a/templates/start_lean.sh +++ b/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" 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(() => ''); + 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//) the lean4 extension ' + + 'expects, so the extension thinks no toolchain is installed and ' + + 'asks the student to download one.', + ).toBe(false); +}); diff --git a/tests/test_launcher.py b/tests/test_launcher.py index 08c520c..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( @@ -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(";"): 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():