Repository navigation
test: detect Lean toolchain-install prompt in CI - #46
Merged
Merged
Conversation
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>
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>
…dent" This reverts commit 083cf48.
…rompt 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>
…default-toolchain)
… Lean install 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>
…or elan 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>
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>
…installed
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>
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>
…t 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.
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).
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.
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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Add a Tier 6 test that catches the lean4 extension's modal dialog asking students to install the Lean toolchain. This is the symptom of a real bundle bug where our shipped Lean isn't laid out as elan expects.
Why CI didn't catch this
The bundled Lean lives at `lean/bin/lean`, not at the elan-style `lean/toolchains/leanprover--lean4---vX.Y.Z/bin/lean` that the extension queries. So:
Expected CI outcome
This PR should fail test-macos-gui (and likely test-windows-gui / test-linux-gui too) with a clear message: `"Lean version is not installed" prompt should NOT appear`. That confirms CI now catches the bundle breakage.
The bundle fix (laying out the Lean toolchain in elan's expected directory structure) will follow in a separate PR once we see CI is detecting it correctly.
🤖 Prepared with Claude Code