Repository navigation
test: detect missing extension and broken portable mode in CI - #45
Merged
Merged
Conversation
The Playwright and Tier 5 test launchers passed --extensions-dir explicitly, telling VSCodium exactly where to find extensions. The real student launcher (start_lean.sh/cmd) passes no such flag and relies on VSCodium portable mode auto-discovering data/extensions/. This meant CI passed even when portable mode was broken and students saw no lean4 extension. Changes: - Remove --extensions-dir from Playwright launch helper and Tier 5 runner so tests mirror the real student experience. - Add extension.spec.ts: explicit checks that the lean4 extension appears in the sidebar, .lean files get lean4 language mode, and the infoview panel opens. Fails fast with clear messages instead of 120-second timeouts. - Enhance verify_bundle.py: validate extensions.json registry has a leanprover.lean4 entry pointing to a real directory with a valid package.json and main entry point. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
VSCodium's portable-mode detection uses a platform-specific folder name: 'data' on Windows/Linux but '<applicationName>-portable-data' on macOS (= 'codium-portable-data' for VSCodium). The bundle creates 'vscodium/data/' uniformly, so macOS silently failed to enter portable mode — extensions.json never read, settings.json never applied, no infoview, Welcome tab still shown. Set VSCODE_PORTABLE=$BUNDLE_ROOT/vscodium/data in both start_lean.sh and start_lean.cmd. This env var short-circuits VSCodium's platform- specific path detection and works uniformly everywhere. Also fix a test-brittleness bug introduced in the prior commit: extension.spec.ts's first test opens the Extensions sidebar, which replaces the File Explorer view. The second test then couldn't find the fixture_goals.lean treeitem because Explorer wasn't visible. Use Quick Open (Ctrl/Cmd+P) instead, matching the existing pattern in 'project file activates infoview'. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@vscode/test-electron's runTests() launches VSCodium directly — it never calls the launcher script — so the VSCODE_PORTABLE export in start_lean.sh/cmd never reaches VSCodium. Set the env var in the Node process before runTests() is called, matching what the launcher does. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…xtensions) Tier 5 runs through @vscode/test-electron's runTests(), which creates its own ".vscode-test/extensions" folder and does not honor portable mode — so it never finds the bundle's extensions without the flag. This is fundamentally different from Tier 6 (Playwright launches the real launcher script) where --extensions-dir would mask portable-mode bugs. Tier 6 remains without --extensions-dir and now passes on macOS, proving the VSCODE_PORTABLE fix in the launcher works end-to-end. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
macOS's stock bsdtar 3.5.3 / libarchive 3.5.3 cannot read .tar.zst archives (no zstd in libarchive until 3.6). GitHub Actions runners have a newer libarchive so CI doesn't notice, but local builds on default macOS error out with "tar --list -f archive.tar.zst" failing. When the in-process tar can't read the archive, decompress with the zstd CLI first and feed the resulting plain .tar to tar. Helpful error if neither tar nor zstd can handle it. 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
--extensions-dirfrom Playwright and Tier 5 test launchers so they mirror the real student experience. The launcher scripts don't pass this flag — they rely on VSCodium portable mode auto-discoveringdata/extensions/. Passing it explicitly in tests masked portable-mode bugs.extension.spec.tswith explicit checks that the lean4 extension appears in the sidebar,.leanfiles getlean4language mode, and the infoview panel opens. Fails fast with clear error messages instead of silent 120-second timeouts.verify_bundle.py(Tier 1) to validate theextensions.jsonregistry has aleanprover.lean4entry pointing to a real directory with a validpackage.jsonand main entry point.Motivation
Building a darwin-arm64 bundle and opening it showed no lean4 extension and no infoview — yet CI was green. The root cause: tests passed
--extensions-direxplicitly, telling VSCodium exactly where extensions live, while the real student launcher relies on portable-mode auto-discovery. If portable mode is broken, tests still pass but students see a broken editor.Expected CI outcome
This PR should cause Tier 5 and/or Tier 6 GUI tests to fail if the extension is not loading through portable mode — surfacing the current breakage rather than masking it.
🤖 Prepared with Claude Code