From 20999b563df82dfa6d04ce0918bfa3bca3ce0c56 Mon Sep 17 00:00:00 2001 From: BenjiB Date: Thu, 3 Sep 2026 18:32:15 +0000 Subject: [PATCH] feat: add Waterproof bundle support --- .github/workflows/build-and-test.yml | 79 ++-- AGENTS.md | 18 + README.md | 208 ++++++++-- assemble.py | 378 +++++++++++++---- bundle.py | 449 ++++++++++++++++++--- download.py | 296 +++++++++----- import_closure.py | 336 ++++++++++++++-- shim/git_shim.c | 72 +++- templates/start_lean.cmd | 8 +- templates/start_lean.sh | 9 +- tests/test_assemble.py | 582 ++++++++++++++++++++++++++- tests/test_download.py | 83 ++++ tests/test_git_shim.py | 100 +++-- tests/test_import_closure.py | 213 +++++++++- tests/test_launcher.py | 73 +++- 15 files changed, 2469 insertions(+), 435 deletions(-) create mode 100644 AGENTS.md create mode 100644 tests/test_download.py diff --git a/.github/workflows/build-and-test.yml b/.github/workflows/build-and-test.yml index 75c90e7..cd5366b 100644 --- a/.github/workflows/build-and-test.yml +++ b/.github/workflows/build-and-test.yml @@ -56,8 +56,8 @@ jobs: retention-days: 1 build-windows: - runs-on: ubuntu-latest - needs: build-project + runs-on: windows-latest + needs: unit-tests env: REPO_URL: ${{ github.event.inputs.repo_url || 'https://github.com/PatrickMassot/MDD154' }} steps: @@ -66,40 +66,34 @@ jobs: with: python-version: '3.12' - - uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 # v4 - with: - name: built-project - - - name: Extract project - run: tar xf project.tar -C /tmp - - - name: Install elan - 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: Install mingw-w64 (for git.exe shim cross-build) + - name: Clone project + shell: bash + # Tier 6 GUI tests assert on specific file content (f01_egalites.lean line 44). + # Pin the default project to a known commit so upstream changes don't break tests. run: | - sudo apt-get update - sudo apt-get install -y gcc-mingw-w64-x86-64 + git clone "$REPO_URL" target-project + cd target-project + git checkout 1f32d8e95f5567c9aabcd55297840bda340ad913 2>/dev/null || true - - name: Build Windows bundle + - name: Build Windows bundle natively + shell: bash run: | python bundle.py "$REPO_URL" \ - --project-dir /tmp/project \ + --project-dir target-project \ --platform windows \ - --work-dir /tmp/bundle-work \ - --output /tmp/bundle.zip + --work-dir bundle-work \ + --output bundle.zip - name: Report bundle size + shell: bash run: | - ls -lh /tmp/bundle.zip - du -sh /tmp/bundle-work/*/ + ls -lh bundle.zip + du -sh bundle-work/*/ - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4 with: name: bundle-windows - path: /tmp/bundle.zip + path: bundle.zip retention-days: 7 build-linux: @@ -197,8 +191,8 @@ jobs: retention-days: 7 build-macos-arm64: - runs-on: ubuntu-latest - needs: build-project + runs-on: macos-14 + needs: unit-tests env: REPO_URL: ${{ github.event.inputs.repo_url || 'https://github.com/PatrickMassot/MDD154' }} steps: @@ -207,35 +201,34 @@ jobs: with: python-version: '3.12' - - uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 # v4 - with: - name: built-project - - - name: Extract project - run: tar xf project.tar -C /tmp - - - name: Install elan + - name: Clone project + # Tier 6 GUI tests assert on specific file content (f01_egalites.lean line 44). + # Pin the default project to a known commit so upstream changes don't break tests. 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 + git clone "$REPO_URL" target-project + cd target-project + git checkout 1f32d8e95f5567c9aabcd55297840bda340ad913 2>/dev/null || true + + - name: Ensure zstd is available + run: command -v zstd >/dev/null || brew install zstd - - name: Build macOS arm64 bundle + - name: Build macOS arm64 bundle natively run: | python bundle.py "$REPO_URL" \ - --project-dir /tmp/project \ + --project-dir target-project \ --platform darwin-arm64 \ - --work-dir /tmp/bundle-work \ - --output /tmp/bundle-macos-arm64.zip + --work-dir bundle-work \ + --output bundle-macos-arm64.zip - name: Report bundle size run: | - ls -lh /tmp/bundle-macos-arm64.zip - du -sh /tmp/bundle-work/*/ + ls -lh bundle-macos-arm64.zip + du -sh bundle-work/*/ - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4 with: name: bundle-darwin-arm64 - path: /tmp/bundle-macos-arm64.zip + path: bundle-macos-arm64.zip retention-days: 7 test-linux-offline: diff --git a/AGENTS.md b/AGENTS.md new file mode 100644 index 0000000..cfb26f5 --- /dev/null +++ b/AGENTS.md @@ -0,0 +1,18 @@ +# Gotchas + +**Lakefile must match manifest.** The README mentions rewriting `lake-manifest.json`. +We also rewrite `lakefile.toml`/`lakefile.lean` — Lake validates that both agree on +dep source kinds and marks targets out-of-date if they disagree. + +**Olean timestamps after zip/unzip.** CI touches `.olean`/`.ilean` files after +extraction. Lake also checks `.trace` file hashes, so `lake build --no-build` may +still exit 3 (stale). Exit code 3 is accepted in tests. + +**Network isolation in CI.** `unshare -rn` (unprivileged) fails on GitHub Actions +Ubuntu 24.04 — falls back to `sudo unshare --net`. CI preflight *fails* (not skips) +if neither works. + +**Windows cmd.exe and parentheses.** `%PATH%` expanded inside a `(...)` block +breaks if PATH contains `Program Files (x86)`. Use `!PATH!` (delayed expansion). +Also: `re.sub` replacement strings with backslashes need `lambda _: replacement` +to avoid backreference interpretation. \ No newline at end of file diff --git a/README.md b/README.md index e5ccd7e..9c4ccce 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -# Lean 4 Bundle Builder +# Lean 4 Bundle Builder (Waterproof support) Create self-contained, offline Lean 4 bundles for teaching. @@ -44,7 +44,7 @@ Install the tool with [uv](https://docs.astral.sh/uv/): uv tool install git+https://github.com/leanprover-community/bundle ``` -That puts a `lean-bundle` CLI on your `PATH`. Build a bundle for your +That puts a `lean-bundle` CLI on your `PATH`. Build a bundle for your current platform (auto-detected): ```bash @@ -52,11 +52,14 @@ lean-bundle https://github.com/PatrickMassot/MDD154 ``` The resulting `MDD154-bundle-.zip` lands in your current -directory. Send it to students; they unzip it and double-click +directory. Send it to students; they unzip it and double-click `Start_Lean`. ## Usage +Bundles must be built natively: run a Windows build on Windows, a macOS build +on macOS, and a Linux build on the matching Linux architecture. + ```bash lean-bundle https://github.com/PatrickMassot/MDD154 --platform windows ``` @@ -70,37 +73,126 @@ This produces `MDD154-bundle-windows.zip` containing: - The **project source files** - **Only the oleans transitively needed** by the project (not all of Mathlib) +### Waterproof (Lean genre) projects + +Projects built on [Waterproof](https://github.com/impermeable/waterproof-vscode)'s +Lean genre (`impermeable/waterproof-genre`, built on Verso) are just Lean 4 +projects from this tool's point of view. + +`lake build` resolves the genre +library like any other dependency, and Lean's dependency parser traces its +import closure the same as for Mathlib. The only extra step is bundling the +Waterproof extension itself: + +```bash +lean-bundle https://github.com/your-org/your-waterproof-course --platform windows --waterproof +``` + +If a course deliberately contains Lean files that cannot compile, use +`--allow-unsolved`. The normal build is still attempted so dependencies used +by the exercises are materialized, but its expected failure is tolerated: + +```bash +lean-bundle https://github.com/your-org/incomplete-waterproof-course \ + --waterproof \ + --allow-unsolved +``` + +Waterproof bundles follow the operating system's light or dark appearance. +Waterproof Light remains the fallback when no system preference is available. + +The Waterproof extension is fetched from Open VSX +(`waterproof-tue.waterproof`). To bundle an unpublished build instead: + +```bash +git clone https://github.com/impermeable/waterproof-vscode +cd waterproof-vscode && git lfs pull && npm ci +npm run package # -> test_out/extension.vsix + +lean-bundle https://github.com/your-org/your-waterproof-course \ + --platform windows \ + --waterproof-vsix waterproof-vscode/test_out/extension.vsix +``` + +### Proof-sheet bundle commands + +Run these from the directory containing `bundle.py`. For bundles distributed +to students, use the pinned commands. For this example, we fix the proof sheets at commit +`e62b9166113d3f48b82a09bd5e728fbd779608cc`, VSCodium at `1.126.04524`, and +Waterproof at `0.12.0`. + +**Pinned Windows:** + +```powershell +python3 bundle.py https://github.com/impermeable/introduction-to-proof-sheets-lean --ref e62b9166113d3f48b82a09bd5e728fbd779608cc --platform windows --vscodium-version 1.126.04524 --waterproof-version 0.12.0 --allow-unsolved --work-dir "..\tmp\bewijzen-waterproof-windows" --clean-work-dir --output "..\bewijzen-waterproof-windows.zip" +``` + +**Pinned Linux x86-64:** + +```bash +python3 bundle.py https://github.com/impermeable/introduction-to-proof-sheets-lean --ref e62b9166113d3f48b82a09bd5e728fbd779608cc --platform linux-x64 --vscodium-version 1.126.04524 --waterproof-version 0.12.0 --allow-unsolved --work-dir ../tmp/bewijzen-waterproof-linux-x64 --clean-work-dir --output ../bewijzen-waterproof-linux-x64.zip --open-file "Bewijzen/Lecture1/sheet1/_conjunction.lean" +``` + +The latest commands intentionally omit all three pins: they use the repository's +default branch and the latest VSCodium and Waterproof releases available when +the build starts. + +**Latest Windows:** + +```powershell +python3 bundle.py https://github.com/impermeable/introduction-to-proof-sheets-lean --platform windows --waterproof --allow-unsolved --work-dir "..\tmp\bewijzen-waterproof-windows-latest" --clean-work-dir --output "..\bewijzen-waterproof-windows-latest.zip" +``` + +**Latest Linux x86-64:** + +```bash +python3 bundle.py https://github.com/impermeable/introduction-to-proof-sheets-lean --platform linux-x64 --waterproof --allow-unsolved --work-dir ../tmp/bewijzen-waterproof-linux-x64-latest --clean-work-dir --output ../bewijzen-waterproof-linux-x64-latest.zip --open-file "Bewijzen/Lecture1/sheet1/_conjunction.lean" +``` + +For ARM64 Linux, replace `linux-x64` with `linux-arm64` and adjust the output +names if desired. A work directory created by an older bundler has no ownership +marker; remove that directory manually once or choose a new path. + ### Requirements (build machine only) - Python 3.11+ - Git -- [elan](https://github.com/leanprover/elan) with the project's Lean toolchain -- Lean 4.17+ (for `lean --src-deps`) +- A project pinned to Lean 4.17+ (`--deps-json` accelerates Lean 4.22+) - Network access (to download components and mathlib cache) -- A C compiler able to produce 64-bit Windows PE binaries **when - building Windows bundles** (mingw-w64 is recommended; - `apt-get install gcc-mingw-w64-x86-64` on Debian/Ubuntu). Zig or native - `gcc`/`clang` on a Windows build host also work. +- The build host must match `--platform`; cross-platform builds are rejected. +- On Windows, the downloaded Lean toolchain's `leanc.exe` builds the small + bundled `git.exe` shim; no additional C compiler is required. Students need none of these. ### Options -``` +```` --platform {windows,linux-x64,linux-arm64,darwin-x64,darwin-arm64} - Target platform (default: auto-detect) + Native platform; must match the build host (default: auto-detect) --output PATH Output zip file path --project-dir PATH - Use an already-cloned and built project instead of cloning fresh + Use an already-cloned project instead of cloning fresh --work-dir PATH - Working directory for downloads (default: temp dir) + Working directory for downloads and builds (default: a fresh temporary + directory). Directories created by the bundler receive an ownership marker. + +--clean-work-dir + Remove the entire --work-dir before building instead of cleaning generated + components individually. An existing directory must contain the valid + ownership marker from a previous run. Unmarked directories and paths + overlapping --project-dir or --waterproof-vsix are rejected. + +--allow-unsolved + Continue if the normal Lake build fails because exercises contain unsolved + goals. Repository CI is responsible for catching other build failures. --ref REF - Git ref (branch or tag) to checkout + Git commit, branch, or tag to checkout --vscodium-version VERSION Pin VSCodium version (default: latest) @@ -108,20 +200,57 @@ Students need none of these. --extension-version VERSION Pin lean4 extension version (default: latest) +--waterproof + Bundle the Waterproof VS Code extension instead of the Lean 4 extension, + for projects using the Waterproof Lean genre + (impermeable/waterproof-genre, built on Verso). + Only Waterproof's Lean path is wired up — it spawns `lake serve` + itself via its own `waterproof.lakePath`/`waterproof.lakeArgs` + settings, so no separate LSP setup is needed. The bundle pins + `waterproof.skipLaunchChecks: "lean4"` in the project's workspace + settings so Waterproof only starts the Lean language server. Rocq/ + coq-lsp is out of scope for this bundler: nothing opam-related is + downloaded, built, or configured, and Rocq/`.v` support in the + bundled Waterproof extension will not work. + + Fetched from Open VSX. To bundle an unpublished build, pass it via + --waterproof-vsix. + +--waterproof-version VERSION + Pin the Waterproof extension version fetched from Open VSX (implies + --waterproof; default: latest). Mutually exclusive with --waterproof-vsix. + +--waterproof-vsix PATH + Use an unpublished or locally-built Waterproof .vsix instead of downloading one + (implies --waterproof). Waterproof's own release process (see + CONTRIBUTING.md in impermeable/waterproof-vscode) is `npm run package` + producing `test_out/extension.vsix`, uploaded directly to the VS Code + Marketplace — there's no `.vsix` attached to GitHub releases. Build it + with: + ``` + git clone https://github.com/impermeable/waterproof-vscode + cd waterproof-vscode && git lfs pull && npm ci + npm run package # -> test_out/extension.vsix + ``` + then pass that path here. + --include [PATTERN ...] Additional file patterns to copy from the project (e.g. '*.json' 'data/') --open-file NAME - .lean file to auto-open on launch (default: first .lean file in - project root, alphabetically, excluding lakefile.lean) + .lean file to auto-open on the first launch of an extracted bundle + (default: no file; the workspace opens without an editor tab). Later + launches restore the student's editor state. Not supported when combining + --waterproof with --platform windows; see Known issues below. --no-zip Assemble the bundle directory without creating a zip -``` +```` -### Example: pre-built project +### Example: local project checkout -If you've already cloned and built the project: +If you've already cloned the project, you can use that checkout directly. The +bundler still fetches its dependencies and builds it: ```bash python bundle.py https://github.com/PatrickMassot/MDD154 \ @@ -135,7 +264,7 @@ python bundle.py https://github.com/PatrickMassot/MDD154 \ MDD154-bundle/ Start_Lean.command/.cmd/.sh # Double-click to launch (one per platform) lean/ # Trimmed Lean toolchain - vscodium/ # Portable VSCodium + lean4 extension + vscodium/ # Portable VSCodium + selected editor extension project/ # Course project lakefile.toml lean-toolchain @@ -148,10 +277,12 @@ MDD154-bundle/ ## How it works 1. Clones the target project and builds it (fetching mathlib cache) -2. Downloads VSCodium portable and the lean4 extension -3. Uses `lean --src-deps` to compute the transitive import closure +2. Downloads VSCodium portable and either the lean4 extension or, with + `--waterproof`, the Waterproof extension +3. Uses batched `lean --deps-json` to compute the transitive import closure, + with parallel `lean --src-deps` as a compatibility fallback 4. Copies only the needed modules' build artifacts (`.olean`, `.ilean`, etc.) into the bundle, skipping the thousands of Mathlib modules that aren't transitively imported -5. Trims the Lean toolchain (removes clang, LLVM, ~500 MB saved) +5. Trims the native Lean toolchain (removes clang and LLVM). 6. Creates a launcher script that sets `PATH`, `LEAN_PATH`, and `VSCODE_PORTABLE` (no `ELAN_HOME` — that would confuse the lean4 extension's elan probing), and registers the bundled Lean in @@ -162,13 +293,13 @@ MDD154-bundle/ ## Testing -Run all tests locally against an existing bundle: +Run the local Linux x86-64 test harness against an existing bundle: ```bash ./test.sh /path/to/MDD154-bundle ``` -This runs unit tests, bundle structure verification, launcher tests, and +This runs the core unit tests, bundle structure verification, launcher tests, and Playwright GUI tests (requires Xvfb). Build a bundle first with: ```bash @@ -178,6 +309,15 @@ python bundle.py https://github.com/PatrickMassot/MDD154 --platform linux-x64 -- ## Known issues +- **Opening a default Waterproof file on Windows.** Combining `--open-file`, + `--waterproof`, and `--platform windows` is rejected. On a cold start, VS Code + currently opens a file argument in its text editor instead of honoring + `workbench.editorAssociations`; opening the file after startup uses the + configured custom editor correctly. See + [VS Code issue #325506](https://github.com/microsoft/vscode/issues/325506). + Windows Waterproof bundles therefore open only the project workspace on first + launch. Windows bundles using the regular Lean 4 extension are unaffected. + - **Git shim on Windows.** The lean4 VS Code extension and VS Code's built-in git extension both probe for `git` on PATH at startup. Rather than shipping the full 46 MB MinGit distribution, the bundle includes a @@ -189,7 +329,7 @@ python bundle.py https://github.com/PatrickMassot/MDD154 --platform linux-x64 -- exits. Source: `shim/git_shim.c`. This can be retired entirely once the lean4 extension provides a way to suppress its git check ([Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/trylean.20bundle.20for.20lean4/near/581773347)) - *and* VS Code's built-in git extension is disabled via settings.json + _and_ VS Code's built-in git extension is disabled via settings.json — whichever probe comes last determines whether the shim stays. - **Dep rewriting for offline use.** We rewrite `lake-manifest.json` and @@ -214,15 +354,17 @@ python bundle.py https://github.com/PatrickMassot/MDD154 --platform linux-x64 -- Several component versions are hardcoded and need periodic bumps: -| Component | Where | Notes | -|-----------|-------|-------| -| git shim version string | `shim/git_shim.c` (`VERSION_LINE`) | Must be >= 2.0.0, not 2.25.x/2.26.x | -| even-better-toml extension | `download.py` `ALLOWED_EXTENSION_DEPS` | ID + version | -| elan installer | `.github/workflows/build-and-test.yml` | Tag in curl URL | -| GitHub Actions (checkout, setup-python, etc.) | `.github/workflows/build-and-test.yml` | Pinned by commit SHA | +| Component | Where | Notes | +| --------------------------------------------- | -------------------------------------- | ----------------------------------- | +| git shim version string | `shim/git_shim.c` (`VERSION_LINE`) | Must be >= 2.0.0, not 2.25.x/2.26.x | +| even-better-toml extension | `download.py` `LEAN4_EXTENSION_DEPS` | ID + version | +| elan installer | `.github/workflows/build-and-test.yml` | Tag in curl URL | +| GitHub Actions (checkout, setup-python, etc.) | `.github/workflows/build-and-test.yml` | Pinned by commit SHA | The **Lean toolchain** version comes from the target project's -`lean-toolchain` file and is not pinned here. **VSCodium** and the **lean4 +`lean-toolchain` file and is not pinned here. **Waterproof** defaults to +latest and can be pinned via `--waterproof-version`, same as VSCodium and +the lean4 extension. **VSCodium** and the **lean4 extension** default to the latest release but can be pinned per-build via `--vscodium-version` and `--extension-version`. diff --git a/assemble.py b/assemble.py index 08a6453..81b2a91 100644 --- a/assemble.py +++ b/assemble.py @@ -8,6 +8,7 @@ import os import re import shutil +import stat import subprocess import time from pathlib import Path @@ -20,6 +21,39 @@ ) +def _windows_extended_path(path: Path) -> Path: + """Return an absolute ``\\\\?\\`` path on Windows. + + Python's recursive filesystem helpers can otherwise fail around the + legacy MAX_PATH boundary, even when every individual path component is + valid. Other platforms keep the original path unchanged. + """ + if os.name != "nt": + return path + + value = os.path.abspath(path) + if value.startswith("\\\\?\\"): + return Path(value) + if value.startswith("\\\\"): + return Path("\\\\?\\UNC\\" + value[2:]) + return Path("\\\\?\\" + value) + + +def _rmtree(path: Path) -> None: + """Remove a tree on Windows even when Git left read-only pack files.""" + fs_path = _windows_extended_path(path) + + def remove_readonly(function, failed_path, exc_info): + error = exc_info[1] + if isinstance(error, PermissionError): + os.chmod(failed_path, stat.S_IWRITE) + function(failed_path) + return + raise error + + shutil.rmtree(fs_path, onerror=remove_readonly) + + def _module_stem_from_build_path(rel_parts: tuple[str, ...]) -> str | None: """Extract module stem from a ``.lake/``-relative path if it is a build artifact. @@ -39,9 +73,7 @@ def _module_stem_from_build_path(rel_parts: tuple[str, ...]) -> str | None: filename = after[-1] dot = filename.find(".") base = filename[:dot] if dot > 0 else filename - if len(after) > 1: - return str(Path(*after[:-1]) / base) - return base + return "/".join((*after[:-1], base)) return None @@ -58,11 +90,19 @@ def copy_lake_selective( Returns ``(files_copied, files_skipped)``. """ + src_lake = _windows_extended_path(src_lake) + dst_lake = _windows_extended_path(dst_lake) + if needed_stems is None: shutil.copytree(src_lake, dst_lake, symlinks=True, dirs_exist_ok=True) n = sum(1 for p in dst_lake.rglob("*") if p.is_file() or p.is_symlink()) return n, 0 + # Module identifiers are logical Lean paths, not host filesystem paths. + # A backslash-delimited set on Windows would make every top-level build + # directory look unused, discarding the cached dependency artifacts. + needed_stems = {stem.replace("\\", "/") for stem in needed_stems} + # Pre-compute the set of directory prefixes that contain at least one # needed module so we can skip entire sub-trees early. needed_prefixes: set[str] = set() @@ -110,6 +150,8 @@ def _ignore(directory: str, contents: list[str]) -> set[str]: def _copy_file(src: Path, dst: Path) -> None: + src = _windows_extended_path(src) + dst = _windows_extended_path(dst) dst.parent.mkdir(parents=True, exist_ok=True) shutil.copy2(src, dst) @@ -128,7 +170,7 @@ def _touch_oleans(bundle_project: Path) -> None: close to (or even after) the current time when assembly runs quickly. A relative offset from the actual source timestamps is robust. """ - import os + bundle_project = _windows_extended_path(bundle_project) # Find the newest .lean source file anywhere in the project tree lean_max = 0.0 for f in bundle_project.rglob("*.lean"): @@ -154,27 +196,85 @@ def _touch_oleans(bundle_project: Path) -> None: "lean4.automaticallyBuildDependencies": False, "lean4.alwaysAskBeforeInstallingLeanVersions": True, "lean4.showSetupWarnings": False, - "extensions.autoUpdate": False, "update.mode": "none", "extensions.autoCheckUpdates": False, "telemetry.telemetryLevel": "off", "security.workspace.trust.enabled": False, "workbench.startupEditor": "none", + # Recent VSCodium versions show the secondary sidebar by default for + # workspaces, even when no bundled extension contributes content to it. + "workbench.secondarySideBar.defaultVisibility": "hidden", "git.openRepositoryInParentFolders": "never", } +# Extra critical settings applied only when the Waterproof extension is +# bundled (``assemble_bundle(..., waterproof_included=True)``). This bundler +# only ever wires up Waterproof's Lean-genre path (see +# ``download.download_waterproof_extension``); "lean4" restricts Waterproof +# to starting the Lean language server only, so it never probes for or +# attempts to launch coq-lsp/Rocq, which the bundle deliberately does not +# ship. +_WATERPROOF_CRITICAL_SETTINGS: dict[str, object] = { + "waterproof.skipLaunchChecks": "lean4", + # Together with the extension's default custom-editor priority, ensure the + # first CLI-opened Lean file resolves through Waterproof on a fresh bundle. + "workbench.editorAssociations": { + "*.lean": "waterproofTue.waterproofEditor", + }, + # Waterproof warns that trimming can alter proof documents unexpectedly. + "files.trimTrailingWhitespace": False, + # Keep newly-created documents on the only line-ending format supported + # by Waterproof's custom editor. Existing Lean sources are normalized + # during the copy below. + "files.eol": "\n", + "workbench.iconTheme": "waterproof-icons", +} + +# Application-scoped settings cannot be written to +# project/.vscode/settings.json. Keep extension updates disabled in the +# portable VSCodium user's settings for every offline bundle. +_BUNDLE_USER_SETTINGS: dict[str, object] = { + "extensions.autoUpdate": False, +} + +# Theme selection belongs in the portable user's settings: application-scoped +# OS detection is ignored at workspace scope, and a workspace colorTheme would +# override the user's selection. Light remains the fallback when no OS scheme +# is available; otherwise VSCodium selects the corresponding Waterproof theme. +_WATERPROOF_USER_SETTINGS: dict[str, object] = { + "window.autoDetectColorScheme": True, + "workbench.colorTheme": "waterproof-light", + "workbench.preferredLightColorTheme": "waterproof-light", + "workbench.preferredDarkColorTheme": "waterproof-dark", +} + +_WATERPROOF_WORKSPACE_THEME_SETTINGS = tuple(_WATERPROOF_USER_SETTINGS) + +_USER_ONLY_SETTING_KEYS = { + "extensions.autoUpdate", +} + def copy_project_files( project_dir: Path, bundle_project: Path, extra_include: list[str] | None = None, + normalize_lean_line_endings: bool = False, ) -> None: """Copy the project's own source files into the bundle. Uses an allowlist: .lean files, lakefile configs, lean-toolchain, lake-manifest.json, and .vscode/. Use extra_include for additional glob patterns (e.g. ['*.json', 'data/'] for course data files). + + When *normalize_lean_line_endings* is true, every copied project + ``.lean`` file is rewritten to LF. Waterproof's custom editor does not + support CRLF documents, and a Windows checkout with ``core.autocrlf`` + may otherwise introduce CRLF even when the Git index stores LF. """ + project_dir = _windows_extended_path(project_dir) + bundle_project = _windows_extended_path(bundle_project) + for item in sorted(project_dir.iterdir()): if item.name in _SKIP_DIRS: continue @@ -184,7 +284,11 @@ def copy_project_files( _copy_file(item, dst) elif item.is_dir(): if item.name in _ALLOWLIST_DIRS: - shutil.copytree(item, dst, dirs_exist_ok=True) + shutil.copytree( + _windows_extended_path(item), + _windows_extended_path(dst), + dirs_exist_ok=True, + ) else: # Recursively copy only .lean files from subdirectories for f in item.rglob("*.lean"): @@ -204,10 +308,19 @@ def copy_project_files( _copy_file(match, dst) elif match.is_dir(): shutil.copytree( - match, dst, dirs_exist_ok=True, + _windows_extended_path(match), + _windows_extended_path(dst), + dirs_exist_ok=True, ignore=shutil.ignore_patterns(*_SKIP_DIRS), ) + if normalize_lean_line_endings: + for lean_file in bundle_project.rglob("*.lean"): + contents = lean_file.read_bytes() + normalized = contents.replace(b"\r\n", b"\n").replace(b"\r", b"\n") + if normalized != contents: + lean_file.write_bytes(normalized) + def _parse_jsonc(text: str) -> object: """Parse a JSONC (JSON with Comments) string. @@ -228,6 +341,7 @@ def _parse_jsonc(text: str) -> object: def _patch_workspace_settings( bundle_project: Path, critical_settings: dict[str, object], + remove_settings: tuple[str, ...] = (), ) -> None: """Ensure bundle-critical settings override project workspace settings. @@ -237,8 +351,9 @@ def _patch_workspace_settings( override the bundle's user-level ``false``, re-enabling the exact behaviour the bundle is designed to prevent. - This function merges *critical_settings* into the project's workspace - settings so that bundle-critical values always win. + This function removes *remove_settings* and merges *critical_settings* + into the project's workspace settings so that bundle-critical values + always win. """ vscode_dir = bundle_project / ".vscode" vscode_dir.mkdir(parents=True, exist_ok=True) @@ -248,7 +363,16 @@ def _patch_workspace_settings( if settings_path.is_file(): settings = _parse_jsonc(settings_path.read_text()) - settings.update(critical_settings) + for key in _USER_ONLY_SETTING_KEYS: + settings.pop(key, None) + for key in remove_settings: + settings.pop(key, None) + for key, value in critical_settings.items(): + existing = settings.get(key) + if isinstance(existing, dict) and isinstance(value, dict): + settings[key] = {**existing, **value} + else: + settings[key] = value settings_path.write_text(json.dumps(settings, indent=2) + "\n") @@ -282,6 +406,7 @@ def prune_ir_from_bundle(bundle_project: Path) -> tuple[int, int]: Returns ``(files_removed, bytes_freed)``. """ + bundle_project = _windows_extended_path(bundle_project) files_removed = 0 bytes_freed = 0 @@ -346,6 +471,8 @@ def copy_project_oleans(project_dir: Path, bundle_project: Path) -> int: Returns the number of files copied. """ + project_dir = _windows_extended_path(project_dir) + bundle_project = _windows_extended_path(bundle_project) build_dir = project_dir / ".lake" / "build" / "lib" / "lean" if not build_dir.is_dir(): return 0 @@ -375,11 +502,11 @@ def rewrite_manifest_to_path_deps( if not manifest_path.is_file(): return - manifest = json.loads(manifest_path.read_text()) + manifest = json.loads(manifest_path.read_text(encoding="utf-8")) for pkg in manifest.get("packages", []): if pkg.get("type") == "git": - pkg_name = pkg["name"] + pkg_name = pkg["name"].strip("«»") # Convert all git deps to path deps, even if the package # directory doesn't exist (build-time-only deps like Cli). # This prevents lake from trying any git operations. @@ -389,7 +516,10 @@ def rewrite_manifest_to_path_deps( for key in ["url", "rev", "inputRev", "subDir"]: pkg.pop(key, None) - manifest_path.write_text(json.dumps(manifest, indent=1) + "\n") + manifest_path.write_text( + json.dumps(manifest, indent=1) + "\n", + encoding="utf-8", + ) def _rewrite_lakefile_toml_deps(bundle_project: Path) -> None: @@ -409,7 +539,7 @@ def _rewrite_lakefile_toml_deps(bundle_project: Path) -> None: import re import tomllib - text = lakefile.read_text() + text = lakefile.read_text(encoding="utf-8") try: data = tomllib.loads(text) except Exception: @@ -480,7 +610,7 @@ def _rewrite_lakefile_toml_deps(bundle_project: Path) -> None: text = text[:block_start] + "\n".join(new_lines) + text[block_end:] - lakefile.write_text(text) + lakefile.write_text(text, encoding="utf-8") def _rewrite_lakefile_lean_deps(bundle_project: Path) -> None: @@ -499,7 +629,7 @@ def _rewrite_lakefile_lean_deps(bundle_project: Path) -> None: return import re - text = lakefile.read_text() + text = lakefile.read_text(encoding="utf-8") # Match: require from git "url" [@ "rev"] # can be: bare word, "quoted", or «guillemet» # Anchored to start-of-line (with optional leading whitespace) to avoid @@ -517,7 +647,7 @@ def replace_dep(m): new_text = re.sub(pattern, replace_dep, text) if new_text != text: - lakefile.write_text(new_text) + lakefile.write_text(new_text, encoding="utf-8") def rewrite_deps_to_path(bundle_project: Path) -> None: @@ -535,14 +665,43 @@ def setup_vscodium_portable( vscodium_dir: Path, extension_dirs: list[Path], settings_template: Path, + user_settings_overrides: dict[str, object] | None = None, ) -> None: """Set up VSCodium in portable mode with extensions pre-installed. Args: vscodium_dir: Path to extracted VSCodium. - extension_dirs: Paths to extracted extensions (lean4 + dependencies). + extension_dirs: Paths to the selected editor extension and its + dependencies. Waterproof and Lean 4 must not both be present. settings_template: Path to settings.json template. + user_settings_overrides: Values to merge into the portable user's + settings after copying the template. """ + vscodium_dir = _windows_extended_path(vscodium_dir) + extension_dirs = [_windows_extended_path(path) for path in extension_dirs] + settings_template = _windows_extended_path(settings_template) + + # Refuse a conflicting set even when this low-level assembly API is used + # directly instead of through bundle.py's mutually exclusive selector. + extension_ids: set[str] = set() + for extension_dir in extension_dirs: + extension_root = extension_dir / "extension" + if not extension_root.is_dir(): + extension_root = extension_dir + package_path = extension_root / "package.json" + if package_path.is_file(): + package = json.loads(package_path.read_text()) + extension_ids.add( + f"{package.get('publisher', 'unknown')}." + f"{package.get('name', 'unknown')}" + ) + conflicting_frontends = {"leanprover.lean4", "waterproof-tue.waterproof"} + if conflicting_frontends.issubset(extension_ids): + raise ValueError( + "Lean 4 and Waterproof extensions cannot be installed in the " + "same bundle" + ) + # Create portable data directory data_dir = vscodium_dir / "data" data_dir.mkdir(exist_ok=True) @@ -560,7 +719,7 @@ def setup_vscodium_portable( # Install extension ext_dest = extensions_dir / extension_dir.name if ext_dest.exists(): - shutil.rmtree(ext_dest) + _rmtree(ext_dest) shutil.copytree(extension_root, ext_dest) # Read extension metadata for the registry @@ -573,6 +732,14 @@ def setup_vscodium_portable( ext_version = pkg.get("version", ext_version) ext_publisher = pkg.get("publisher", ext_publisher) ext_name = pkg.get("name", ext_name) + if f"{ext_publisher}.{ext_name}" == "waterproof-tue.waterproof": + for editor in pkg.get("contributes", {}).get("customEditors", []): + if editor.get("viewType") == "waterproofTue.waterproofEditor": + # The first CLI-opened file is resolved before editor + # associations reliably take effect on a fresh profile. + editor["priority"] = "default" + ext_package.write_text(json.dumps(pkg, indent=2) + "\n") + break # Write extensions.json registry entry. # The location field with $mid is VS Code's internal URI format; @@ -598,21 +765,34 @@ def setup_vscodium_portable( # Create user settings user_dir = data_dir / "user-data" / "User" user_dir.mkdir(parents=True, exist_ok=True) - shutil.copy2(settings_template, user_dir / "settings.json") + user_settings_path = user_dir / "settings.json" + _copy_file(settings_template, user_settings_path) + if user_settings_overrides: + user_settings = _parse_jsonc(user_settings_path.read_text()) + user_settings.update(user_settings_overrides) + user_settings_path.write_text(json.dumps(user_settings, indent=2) + "\n") -def _detect_open_file(project_dir: Path) -> str | None: - """Find the first ``.lean`` file in *project_dir* to open on launch. +def _reset_bundle_dir(bundle_dir: Path) -> None: + """Create an empty output directory for a deterministic assembly. - Returns a filename (not a full path) relative to *project_dir*, or - ``None`` if no suitable file is found. ``lakefile.lean`` is excluded - since it's infrastructure, not student content. + A work directory can be reused after a successful or interrupted build. + Merging into its previous bundle output is unsafe: ``copytree`` cannot + overwrite existing symlinks, and files excluded by a newer selective copy + would otherwise remain in the bundle. """ - candidates = sorted( - f.name for f in project_dir.iterdir() - if f.is_file() and f.suffix == ".lean" and f.name != "lakefile.lean" - ) - return candidates[0] if candidates else None + fs_bundle_dir = _windows_extended_path(bundle_dir) + if fs_bundle_dir.is_symlink() or ( + fs_bundle_dir.exists() and not fs_bundle_dir.is_dir() + ): + raise ValueError( + f"Bundle output path exists and is not a directory: {bundle_dir}" + ) + if fs_bundle_dir.is_dir(): + print(f"Removing previous bundle output at {bundle_dir}...") + _rmtree(fs_bundle_dir) + fs_bundle_dir.mkdir(parents=True) + def assemble_bundle( @@ -627,6 +807,8 @@ def assemble_bundle( extra_include: list[str] | None = None, needed_stems: set[str] | None = None, open_file: str | None = None, + waterproof_included: bool = False, + allow_unsolved: bool = False, ) -> None: """Assemble the complete bundle directory. @@ -634,7 +816,9 @@ def assemble_bundle( project_dir: The built project directory (with .lake/packages/ and oleans). lean_dir: Extracted and trimmed lean toolchain directory. vscodium_dir: Extracted VSCodium directory. - extension_dirs: Extracted extension directories (lean4 + dependencies). + extension_dirs: Extracted directories for either Waterproof or Lean 4 + and that extension's dependencies. The two frontends conflict and + must not both be present. git_shim_exe: Path to the built git.exe shim (Windows only, None on other platforms). templates_dir: Directory containing launcher and settings templates. @@ -645,13 +829,29 @@ def assemble_bundle( only build artifacts for these modules are copied into the bundle's ``.lake/`` tree. Pass ``None`` to copy everything (fallback when the import closure cannot be computed). - open_file: Lean file to open on launch (relative to project dir). - If ``None``, auto-detected from the project root. + open_file: Lean file to open on the first launch, relative to the + project directory. If ``None``, only the workspace is opened. + waterproof_included: Whether the Waterproof extension is among + *extension_dirs*. When ``True``, forces + ``waterproof.skipLaunchChecks: "lean4"`` into the project's + workspace settings so Waterproof only starts the Lean + language server (this bundler never ships coq-lsp/Rocq), and + normalizes all copied project Lean sources to LF because the + Waterproof editor does not support CRLF documents. + allow_unsolved: Whether project sources are intentionally incomplete. + When ``True``, skip the final full-project rebuild because Lean's + expected ``unsolved goals`` diagnostics would otherwise abort + assembly. Lake itself is still checked before packaging. """ - bundle_dir.mkdir(parents=True, exist_ok=True) + _reset_bundle_dir(bundle_dir) print("Copying lean toolchain...") - shutil.copytree(lean_dir, bundle_dir / "lean", symlinks=True, dirs_exist_ok=True) + shutil.copytree( + _windows_extended_path(lean_dir), + _windows_extended_path(bundle_dir / "lean"), + symlinks=True, + dirs_exist_ok=True, + ) if git_shim_exe is not None: # Place the shim at /git/cmd/git.exe so start_lean.cmd can @@ -661,22 +861,46 @@ def assemble_bundle( print("Installing git shim...") git_cmd = bundle_dir / "git" / "cmd" git_cmd.mkdir(parents=True, exist_ok=True) - shutil.copy2(git_shim_exe, git_cmd / "git.exe") + _copy_file(git_shim_exe, git_cmd / "git.exe") print("Setting up VSCodium...") - shutil.copytree(vscodium_dir, bundle_dir / "vscodium", symlinks=True, dirs_exist_ok=True) + shutil.copytree( + _windows_extended_path(vscodium_dir), + _windows_extended_path(bundle_dir / "vscodium"), + symlinks=True, + dirs_exist_ok=True, + ) + user_settings = _BUNDLE_USER_SETTINGS + if waterproof_included: + user_settings = {**user_settings, **_WATERPROOF_USER_SETTINGS} setup_vscodium_portable( bundle_dir / "vscodium", extension_dirs, templates_dir / "settings.json", + user_settings_overrides=user_settings, ) print("Copying project files...") bundle_project = bundle_dir / "project" - copy_project_files(project_dir, bundle_project, extra_include=extra_include) + copy_project_files( + project_dir, + bundle_project, + extra_include=extra_include, + normalize_lean_line_endings=waterproof_included, + ) print("Patching workspace settings with bundle-critical overrides...") - _patch_workspace_settings(bundle_project, _BUNDLE_CRITICAL_SETTINGS) + critical_settings = _BUNDLE_CRITICAL_SETTINGS + if waterproof_included: + critical_settings = {**critical_settings, **_WATERPROOF_CRITICAL_SETTINGS} + remove_settings = ( + _WATERPROOF_WORKSPACE_THEME_SETTINGS if waterproof_included else () + ) + _patch_workspace_settings( + bundle_project, + critical_settings, + remove_settings=remove_settings, + ) print("Copying project oleans...") n_proj = copy_project_oleans(project_dir, bundle_project) @@ -698,45 +922,49 @@ def assemble_bundle( print("Rewriting deps to path deps...") rewrite_deps_to_path(bundle_project) - # Rebuild the project's own modules inside the assembled bundle. - # This ensures the project's build traces are valid for the bundle's - # workspace configuration. Only the project's own modules need - # recompilation (~seconds); dependency oleans are already cached. - # Cross-compiled bundles (e.g. macOS built on Linux) can't run lake here; - # the test jobs handle that case by running lake setup-file on the target. - print("Rebuilding project modules with rewritten manifest...") - lake_bin = bundle_dir / "lean" / "bin" / "lake" - can_run = False - if lake_bin.is_file(): + # Validate the copied artifacts inside the assembled native bundle and + # rebuild only if Lake finds a genuinely stale project target. With a + # complete import closure this should normally replay the cached build. + print("Checking project build with rewritten manifest...") + lake_name = "lake.exe" if platform.startswith("windows") else "lake" + lake_bin = bundle_dir / "lean" / "bin" / lake_name + if not lake_bin.is_file(): + raise RuntimeError(f"Bundled native Lake executable is missing: {lake_bin}") + + try: + version_result = subprocess.run( + [str(lake_bin), "--version"], + capture_output=True, timeout=10, + ) + except (OSError, subprocess.TimeoutExpired) as e: + raise RuntimeError(f"Bundled native Lake executable cannot run: {lake_bin}") from e + if version_result.returncode != 0: + stderr = version_result.stderr.decode("utf-8", errors="replace")[:500] + raise RuntimeError(f"Bundled native Lake executable failed: {stderr}") + + rebuild_env = os.environ.copy() + rebuild_env["PATH"] = str(bundle_dir / "lean" / "bin") + os.pathsep + rebuild_env.get("PATH", "") + rebuild_env["ELAN_HOME"] = str(bundle_dir / "lean") + if allow_unsolved: + print(" Skipping full project rebuild (unsolved exercises allowed)") + else: try: subprocess.run( - [str(lake_bin), "--version"], - capture_output=True, timeout=10, - ) - can_run = True - except (OSError, subprocess.TimeoutExpired): - pass - if can_run: - rebuild_env = os.environ.copy() - rebuild_env["PATH"] = str(bundle_dir / "lean" / "bin") + os.pathsep + rebuild_env.get("PATH", "") - rebuild_env["ELAN_HOME"] = str(bundle_dir / "lean") - try: - result = subprocess.run( [str(lake_bin), "build"], cwd=str(bundle_project), env=rebuild_env, - capture_output=True, - timeout=600, + check=True, + timeout=1800, ) - if result.returncode == 0: - print(" Project rebuild successful") - else: - stderr = result.stderr.decode("utf-8", errors="replace")[:500] - print(f" Warning: project rebuild exited {result.returncode}: {stderr}") - except subprocess.TimeoutExpired: - print(" Warning: project rebuild timed out (600s), continuing without rebuild") - else: - print(" Skipped (cross-platform build, lake binary not runnable)") + print(" Project rebuild successful") + except subprocess.CalledProcessError as e: + raise RuntimeError( + f"Native project rebuild exited {e.returncode}" + ) from e + except subprocess.TimeoutExpired as e: + raise RuntimeError( + "Native project rebuild timed out after 1800 seconds" + ) from e # Touch oleans AFTER the rebuild so they're strictly newer than any # source files or trace files the rebuild may have updated. @@ -753,13 +981,11 @@ def assemble_bundle( # otherwise. The lake `setup-file` wrapper is correspondingly # unnecessary and no longer installed. - # Determine which file to open on launch. - if open_file is None: - open_file = _detect_open_file(bundle_project) + # Open a file only when the bundle author explicitly requested one. if open_file: print(f" File to open on launch: {open_file}") else: - print(" No .lean file found to open on launch") + print(" No file configured to open on launch") print("Installing launcher...") if platform.startswith("windows"): diff --git a/bundle.py b/bundle.py index 1c6af0f..4cfd4bc 100644 --- a/bundle.py +++ b/bundle.py @@ -6,8 +6,8 @@ This will: 1. Clone the project and build it (fetching mathlib cache) -2. Download Lean, VSCodium, and the lean4 extension -3. Compute the transitive import closure (via ``lean --src-deps``) +2. Download Lean, VSCodium, and the selected editor extension +3. Compute the transitive import closure (batched with ``lean --deps-json``) 4. Assemble a bundle containing only the needed oleans 5. Package it into a zip file """ @@ -17,14 +17,14 @@ import hashlib import json import os -import shutil +import platform import subprocess import sys import tempfile import zipfile from pathlib import Path -from assemble import assemble_bundle +from assemble import _rmtree, _windows_extended_path, assemble_bundle from import_closure import compute_src_deps, src_paths_to_module_stems from download import ( PLATFORM_MAP, @@ -32,30 +32,126 @@ download_lean4_extension, download_lean_toolchain, download_vscodium, + download_waterproof_extension, + install_local_waterproof_vsix, parse_toolchain, trim_lean_toolchain, ) def clone_project(repo_url: str, dest: Path, ref: str | None = None) -> Path: + if ref and ref.startswith("-"): + raise ValueError("Git ref must not start with '-'") + if dest.is_symlink() or (dest.exists() and not dest.is_dir()): + raise ValueError( + f"Project clone destination exists and is not a directory: {dest}" + ) + if dest.is_dir(): + print(f"Removing previous project clone at {dest}...") + _rmtree(dest) + print(f"Cloning {repo_url}...") cmd = ["git", "clone", "--depth=1"] if ref: - cmd += ["--branch", ref] + cmd.append("--no-checkout") cmd += [repo_url, str(dest)] subprocess.run(cmd, check=True, timeout=300) + if ref: + subprocess.run( + ["git", "-C", str(dest), "fetch", "--depth=1", "origin", ref], + check=True, + timeout=300, + ) + subprocess.run( + ["git", "-C", str(dest), "checkout", "--detach", "FETCH_HEAD"], + check=True, + timeout=300, + ) return dest -def build_project(project_dir: Path) -> None: - """Build the project: fetch cache and run lake build.""" +_WORK_DIR_MARKER = ".lean-bundle-work-dir" + + +def _prepare_work_dir( + requested: Path, + *, + clean: bool = False, + protected_paths: tuple[Path, ...] = (), +) -> Path: + """Create a work directory, or clean it when its ownership marker is valid.""" + work_dir = requested.resolve() + if work_dir.exists() and not work_dir.is_dir(): + raise ValueError(f"Work directory exists and is not a directory: {work_dir}") + + marker = work_dir / _WORK_DIR_MARKER + marker_content = f"lean-bundle work directory\n{work_dir}\n" + + if clean: + guarded_paths = { + Path.cwd().resolve(), + Path(__file__).resolve().parent, + Path.home().resolve(), + Path(tempfile.gettempdir()).resolve(), + } + if work_dir in guarded_paths or any( + work_dir in path.parents for path in guarded_paths + ): + raise ValueError(f"Refusing to remove unsafe work directory: {work_dir}") + + inputs = {path.resolve() for path in protected_paths} + if work_dir in inputs or any( + work_dir in path.parents or path in work_dir.parents for path in inputs + ): + raise ValueError(f"Work directory overlaps an input path: {work_dir}") + + if work_dir.exists(): + try: + owned = ( + not marker.is_symlink() + and marker.read_text(encoding="utf-8") == marker_content + ) + except (OSError, UnicodeError): + owned = False + if not owned: + raise ValueError( + f"Refusing to clean unowned work directory {work_dir}; " + f"{_WORK_DIR_MARKER} is missing or invalid" + ) + print(f"Removing previous work directory at {work_dir}...") + _rmtree(work_dir) + + if not work_dir.exists(): + work_dir.mkdir(parents=True) + marker.write_text(marker_content, encoding="utf-8") + return work_dir + + +def build_project( + project_dir: Path, + lake_executable: Path, + bundle_platform: str, + allow_unsolved: bool = False, +) -> None: + """Materialize, cache, and build a project with the downloaded Lake. + + The source checkout supplied through ``--project-dir`` is deliberately + allowed to be completely unbuilt. Using the downloaded, version-matched + Lake also means the build host does not need elan or Lean preinstalled. + """ + build_env = os.environ.copy() + lean_bin = lake_executable.parent + build_env["PATH"] = str(lean_bin) + os.pathsep + build_env.get("PATH", "") + build_env["ELAN_HOME"] = str(lean_bin.parent) + print("Fetching mathlib cache...") result = subprocess.run( - ["lake", "exe", "cache", "get"], + [str(lake_executable), "exe", "cache", "get"], cwd=project_dir, + env=build_env, capture_output=True, text=True, - timeout=300, + timeout=1800, ) if result.returncode != 0: print(f" Warning: cache get returned {result.returncode}") @@ -63,23 +159,155 @@ def build_project(project_dir: Path) -> None: print(f" {result.stderr[:500]}") print("Building project...") - subprocess.run( - ["lake", "build"], + build_cmd = [str(lake_executable), "build"] + build_result = subprocess.run( + build_cmd, cwd=project_dir, - check=True, + env=build_env, timeout=1800, ) + if build_result.returncode == 0: + return + + # On Windows, companion artifacts such as .olean.private can + # occasionally fail to read under heavy parallel load. Lake preserves + # every target that did build successfully, so retry the remaining work + # with a single runtime worker. A parallel retry can merely move the + # transient failure to a later target instead of resolving it. + if bundle_platform == "windows": + print(" Initial build failed; retrying serially on Windows...") + retry_env = build_env.copy() + retry_env["LEAN_NUM_THREADS"] = "1" + build_result = subprocess.run( + build_cmd, + cwd=project_dir, + env=retry_env, + timeout=1800, + ) + if build_result.returncode == 0: + return + + if allow_unsolved: + print( + " Warning: project build failed, continuing because " + "--allow-unsolved was specified" + ) + return + + build_result.check_returncode() + + +def _detect_host_platform() -> str: + """Return the bundle platform key for a supported host CPU and OS.""" + machine = platform.machine().lower() + system = platform.system().lower() + x64_machines = {"amd64", "x86_64"} + arm64_machines = {"aarch64", "arm64"} + + if system == "windows" and machine in x64_machines: + return "windows" + if system == "linux" and machine in x64_machines: + return "linux-x64" + if system == "linux" and machine in arm64_machines: + return "linux-arm64" + if system == "darwin" and machine in x64_machines: + return "darwin-x64" + if system == "darwin" and machine in arm64_machines: + return "darwin-arm64" + raise RuntimeError(f"Cannot detect a supported platform for {system}/{machine}") + + +def _download_editor_extensions( + downloads_dir: Path, + *, + waterproof: bool, + lean4_version: str | None = None, + waterproof_version: str | None = None, + waterproof_vsix: Path | None = None, +) -> tuple[list[Path], str, str]: + """Download exactly one editor frontend and its declared dependencies. + + Both extensions activate for ``.lean`` files and start a Lean language + server. A Waterproof bundle is already an isolated editor environment, + so it contains Waterproof instead of Lean 4 rather than needing another + VS Code profile. + """ + if waterproof: + print("Downloading Waterproof extension (Lean genre only)...") + if waterproof_vsix is not None: + extension_dirs, resolved_waterproof_version = install_local_waterproof_vsix( + waterproof_vsix, downloads_dir + ) + else: + extension_dirs, resolved_waterproof_version = download_waterproof_extension( + downloads_dir, waterproof_version + ) + return ( + extension_dirs, + "waterproof-tue.waterproof", + resolved_waterproof_version, + ) + + extension_dirs, resolved_lean4_version = download_lean4_extension( + downloads_dir, lean4_version + ) + return extension_dirs, "leanprover.lean4", resolved_lean4_version + + +class _ImportClosureProgress: + """Render per-wave progress without flooding redirected build logs.""" + + def __init__(self) -> None: + self._interactive = sys.stdout.isatty() + self._last_wave = 0 + self._last_bucket = -1 + self._last_width = 0 + + def __call__( + self, + wave: int, + completed: int, + wave_total: int, + checked_total: int, + dependencies_found: int, + ) -> None: + percent = completed * 100 // wave_total + bucket = percent // 10 + + if not self._interactive: + if wave == self._last_wave and completed not in (0, wave_total): + if bucket == self._last_bucket: + return + self._last_wave = wave + self._last_bucket = bucket + + message = ( + f" Wave {wave}: {completed}/{wave_total} files ({percent}%)" + f" | {checked_total} checked, {dependencies_found} dependencies found" + ) + if self._interactive: + padding = " " * max(0, self._last_width - len(message)) + print( + f"\r{message}{padding}", + end="\n" if completed == wave_total else "", + flush=True, + ) + self._last_width = 0 if completed == wave_total else len(message) + else: + print(message, flush=True) def create_zip(bundle_dir: Path, output_path: Path) -> None: print(f"Creating {output_path}...") + archive_root = _windows_extended_path(bundle_dir) + archive_output = _windows_extended_path(output_path) # Compute the latest .lean source mtime so we can force all olean/ilean # entries to be strictly newer in the zip. DOS timestamps have 2-second # granularity, so a small offset isn't reliable — we use 2 full minutes. import datetime as _dt lean_max_mtime = max( - (f.stat().st_mtime for f in bundle_dir.rglob("*.lean") if f.is_file()), + (f.stat().st_mtime for f in archive_root.rglob("*.lean") if f.is_file()), default=0, ) # Convert to a datetime 2 minutes after the latest source, rounded up @@ -90,9 +318,9 @@ def create_zip(bundle_dir: Path, output_path: Path) -> None: olean_ts.hour, olean_ts.minute, olean_ts.second & ~1, # even second ) - with zipfile.ZipFile(output_path, "w", zipfile.ZIP_DEFLATED) as zf: - for path in sorted(bundle_dir.rglob("*")): - arcname = str(path.relative_to(bundle_dir.parent)) + with zipfile.ZipFile(archive_output, "w", zipfile.ZIP_DEFLATED) as zf: + for path in sorted(archive_root.rglob("*")): + arcname = str(path.relative_to(archive_root.parent)) if path.is_symlink(): # Store symlinks with the Unix symlink type flag info = zipfile.ZipInfo(arcname) @@ -111,8 +339,8 @@ def create_zip(bundle_dir: Path, output_path: Path) -> None: # zf.write() streams the file and preserves Unix permissions zf.write(path, arcname) - size_mb = output_path.stat().st_size / (1024 * 1024) - with open(output_path, "rb") as f: + size_mb = archive_output.stat().st_size / (1024 * 1024) + with open(archive_output, "rb") as f: digest = hashlib.file_digest(f, "sha256").hexdigest() print(f"Bundle created: {output_path} ({size_mb:.1f} MB)") print(f"SHA-256: {digest}") @@ -130,7 +358,8 @@ def main() -> None: "--platform", choices=list(PLATFORM_MAP.keys()), default=None, - help="Target platform (default: auto-detect from current OS)", + help="Native bundle platform; must match the current host " + "(default: auto-detect)", ) parser.add_argument( "--output", @@ -142,18 +371,32 @@ def main() -> None: "--work-dir", type=Path, default=None, - help="Working directory for downloads and builds (default: temp dir)", + help="Working directory for downloads and builds (default: a fresh " + "temporary directory)", + ) + parser.add_argument( + "--clean-work-dir", + action="store_true", + help="Remove the entire --work-dir before building; requires a valid " + "lean-bundle ownership marker when the directory already exists", ) parser.add_argument( "--project-dir", type=Path, default=None, - help="Use an already-cloned and built project directory instead of cloning", + help="Use an already-cloned project directory instead of cloning; " + "dependencies are fetched and the project is built automatically", + ) + parser.add_argument( + "--allow-unsolved", + action="store_true", + help="Continue if the project build fails because exercises contain " + "unsolved goals.", ) parser.add_argument( "--ref", default=None, - help="Git ref to checkout (branch or tag)", + help="Git ref to checkout (commit, branch, or tag)", ) parser.add_argument( "--vscodium-version", @@ -163,7 +406,33 @@ def main() -> None: parser.add_argument( "--extension-version", default=None, - help="lean4 VS Code extension version (default: latest)", + help="lean4 VS Code extension version (default: latest; unavailable " + "in Waterproof mode)", + ) + parser.add_argument( + "--waterproof", + action="store_true", + help="Bundle the Waterproof VS Code extension instead of the " + "conflicting Lean 4 extension, for projects " + "using the Waterproof Lean genre (impermeable/waterproof-genre). " + "Only the Lean path is wired up: the bundle's workspace " + "settings restrict Waterproof to its Lean language server " + "(waterproof.skipLaunchChecks=lean4) and no Rocq/coq-lsp " + "components are downloaded or configured. Fetched from Open VSX.", + ) + parser.add_argument( + "--waterproof-version", + default=None, + help="Waterproof extension version to fetch from Open VSX " + "(implies --waterproof; default: latest). Mutually exclusive " + "with --waterproof-vsix.", + ) + parser.add_argument( + "--waterproof-vsix", + type=Path, + default=None, + help="Path to an unpublished or locally-built Waterproof .vsix " + "(implies --waterproof).", ) parser.add_argument( "--include", @@ -174,9 +443,10 @@ def main() -> None: parser.add_argument( "--open-file", default=None, - help="Lean file to open on launch (e.g. 'LibDM3.lean'). " - "If not specified, the first .lean file (alphabetically, " - "excluding lakefile.lean) in the project root is used.", + help="Lean file to open on the bundle's first launch " + "(e.g. 'LibDM3.lean'). If not specified, the workspace opens " + "without an editor tab. Not supported for Waterproof bundles " + "on Windows.", ) parser.add_argument( "--no-zip", @@ -185,29 +455,68 @@ def main() -> None: ) args = parser.parse_args() + if args.clean_work_dir and not args.work_dir: + parser.error("--clean-work-dir requires --work-dir") + + if args.waterproof_version and args.waterproof_vsix: + parser.error("--waterproof-version and --waterproof-vsix are mutually exclusive") + + include_waterproof = ( + args.waterproof + or args.waterproof_version is not None + or args.waterproof_vsix is not None + ) + + if include_waterproof and args.extension_version is not None: + parser.error( + "--extension-version cannot be used in Waterproof mode: " + "the conflicting Lean 4 extension is omitted" + ) if args.no_zip and not args.work_dir: parser.error("--no-zip requires --work-dir (otherwise the bundle is assembled in a temp dir that gets cleaned up)") + try: + host_platform = _detect_host_platform() + except RuntimeError as e: + parser.error(str(e)) if args.platform is None: - import platform - machine = platform.machine().lower() - system = platform.system().lower() - if system == "windows": - args.platform = "windows" - elif system == "linux": - args.platform = "linux-arm64" if machine in ("arm64", "aarch64") else "linux-x64" - elif system == "darwin": - args.platform = "darwin-arm64" if machine in ("arm64", "aarch64") else "darwin-x64" - else: - parser.error(f"Cannot auto-detect platform for {system}/{machine}. Use --platform.") + args.platform = host_platform + elif args.platform != host_platform: + parser.error( + "Cross-platform bundles are not supported: " + f"host is {host_platform}, requested {args.platform}. " + f"Build --platform {args.platform} on that platform instead." + ) + + if ( + args.platform == "windows" + and include_waterproof + and args.open_file is not None + ): + parser.error( + "--open-file is not supported for Waterproof bundles on Windows: " + "a VS Code cold-start bug ignores workbench.editorAssociations " + "for file arguments" + ) project_name = args.repo_url.rstrip("/").split("/")[-1] temp_dir = None if args.work_dir: - work_dir = args.work_dir - work_dir.mkdir(parents=True, exist_ok=True) + protected_inputs = tuple( + path.resolve() + for path in (args.project_dir, args.waterproof_vsix) + if path is not None + ) + try: + work_dir = _prepare_work_dir( + args.work_dir, + clean=args.clean_work_dir, + protected_paths=protected_inputs, + ) + except ValueError as e: + parser.error(str(e)) else: temp_dir = tempfile.mkdtemp(prefix="lean-bundle-") work_dir = Path(temp_dir) @@ -216,7 +525,7 @@ def main() -> None: templates_dir = Path(__file__).parent / "templates" if args.project_dir: - project_dir = args.project_dir + project_dir = args.project_dir.resolve() print(f"Using existing project at {project_dir}") else: project_dir = clone_project(args.repo_url, work_dir / "project", ref=args.ref) @@ -230,20 +539,45 @@ def main() -> None: lean_dir = download_lean_toolchain(lean_version, args.platform, downloads_dir) vscodium_dir, vscodium_version = download_vscodium(args.platform, downloads_dir, args.vscodium_version) - extension_dirs, extension_version = download_lean4_extension(downloads_dir, args.extension_version) - git_shim_exe = build_git_shim(downloads_dir, args.platform) + extension_dirs, editor_extension, extension_version = ( + _download_editor_extensions( + downloads_dir, + waterproof=include_waterproof, + lean4_version=args.extension_version, + waterproof_version=args.waterproof_version, + waterproof_vsix=args.waterproof_vsix, + ) + ) - if not args.project_dir: - print("\n--- Building project ---") - build_project(project_dir) + git_shim_exe = build_git_shim( + downloads_dir, + args.platform, + lean_dir=lean_dir, + ) - print("\n--- Trimming lean toolchain ---") - trim_lean_toolchain(lean_dir, args.platform) + lake_executable = ( + lean_dir + / "bin" + / ("lake.exe" if args.platform == "windows" else "lake") + ) + + print("\n--- Building project ---") + build_project( + project_dir, + lake_executable, + args.platform, + allow_unsolved=args.allow_unsolved, + ) print("\n--- Computing import closure ---") needed_stems: set[str] | None = None try: - needed_srcs = compute_src_deps(project_dir) + closure_progress = _ImportClosureProgress() + needed_srcs = compute_src_deps( + project_dir, + progress=closure_progress, + lake_executable=lake_executable, + ) needed_stems = src_paths_to_module_stems(needed_srcs, project_dir) print(f" {len(needed_stems)} modules in transitive closure") except Exception as e: @@ -251,9 +585,10 @@ def main() -> None: print(" Falling back to copying all build artifacts") # Sanity-check: verify that at least one computed stem corresponds - # to an actual .olean file. If a package uses Lake's srcDir option - # the source→stem mapping is wrong and we must fall back to a full - # copy rather than silently dropping needed modules. + # to an actual .olean file. Source paths are resolved against package + # build trees (including srcDir layouts), but a completely unbuilt or + # unusual project should still fall back to copying all artifacts + # rather than silently dropping every dependency module. if needed_stems: verified = False for bldir in (project_dir / ".lake").rglob("build/lib/lean"): @@ -284,17 +619,24 @@ def main() -> None: extra_include=args.include, needed_stems=needed_stems, open_file=args.open_file, + waterproof_included=include_waterproof, + allow_unsolved=args.allow_unsolved, ) + print("\n--- Trimming bundled lean toolchain ---") + trim_lean_toolchain(bundle_dir / "lean", args.platform) + # Write bundle manifest for reproducibility manifest = { "lean_version": lean_version, "vscodium_version": vscodium_version, "extension_version": extension_version, + "editor_extension": editor_extension, "platform": args.platform, "repo_url": args.repo_url, "ref": args.ref, "include": args.include or None, + "allow_unsolved": args.allow_unsolved, "built_at": datetime.datetime.now(datetime.timezone.utc).isoformat(), } (bundle_dir / "bundle-manifest.json").write_text( @@ -309,7 +651,10 @@ def main() -> None: finally: if temp_dir and not args.work_dir and not args.no_zip: print(f"Cleaning up {temp_dir}") - shutil.rmtree(temp_dir, ignore_errors=True) + try: + _rmtree(Path(temp_dir)) + except OSError: + pass if __name__ == "__main__": diff --git a/download.py b/download.py index dc088b5..8ccf819 100644 --- a/download.py +++ b/download.py @@ -13,6 +13,7 @@ import subprocess import sys import tarfile +import tempfile import time import urllib.error import urllib.request @@ -49,30 +50,13 @@ } -# Candidate C compilers that can produce a 64-bit Windows PE. Each entry is -# ``(binary, extra_args, cross_only)`` — ``cross_only`` binaries are explicit -# cross-compilers and are always safe. Non-``cross_only`` entries are native -# compilers that are only safe when we are already running on Windows (where -# ``gcc``/``clang`` produce PE binaries without extra flags). Running -# ``bundle.py --platform windows`` on Linux/macOS without mingw or zig -# would otherwise silently produce an ELF/Mach-O file named ``git.exe``. -_GIT_SHIM_COMPILERS: tuple[tuple[str, tuple[str, ...], bool], ...] = ( - # Explicit cross-compilers — always safe. - ("x86_64-w64-mingw32-gcc", (), True), - ("x86_64-w64-mingw32-cc", (), True), - # Zig's cc driver ships its own libc and cross-compiles trivially. - ("zig", ("cc", "-target", "x86_64-windows-gnu"), True), - # Native compilers — only trusted on a Windows build host. - ("gcc", (), False), - ("clang", (), False), -) - -# Extension dependencies expected from the lean4 extension's package.json. -# Maps extension ID to pinned version. Reject unknown IDs and fetch only the -# pinned version to prevent dependency injection via a compromised extension. -ALLOWED_EXTENSION_DEPS = { +# Extension dependencies expected from each editor frontend's package.json. +# Keep the allowlists separate: Waterproof and Lean 4 are mutually exclusive, +# so a declaration in one VSIX must never pull in the other's dependency set. +LEAN4_EXTENSION_DEPS = { "tamasfe.even-better-toml": "0.21.2", } +WATERPROOF_EXTENSION_DEPS: dict[str, str] = {} def _sha256_file(path: Path) -> str: @@ -146,7 +130,11 @@ def _safe_extract_tar(tf: tarfile.TarFile, dest: Path) -> None: tf.extractall(dest) -def build_git_shim(dest_dir: Path, platform: str) -> Path | None: +def build_git_shim( + dest_dir: Path, + platform: str, + lean_dir: Path | None = None, +) -> Path | None: """Build a tiny ``git.exe`` shim for Windows bundles. The lean4 VS Code extension and VS Code's built-in git extension both @@ -155,13 +143,9 @@ def build_git_shim(dest_dir: Path, platform: str) -> Path | None: that answers only the probes both extensions perform at activation (see ``shim/git_shim.c`` for the full probe surface). - Returns the path to the built ``git.exe``, or ``None`` on non-Windows - platforms. Raises ``RuntimeError`` if no suitable compiler is found; - on Linux, install ``gcc-mingw-w64-x86-64`` or put ``zig`` on PATH. - Raises ``RuntimeError`` (with the offending bytes) if the compiler - produced something that isn't a Windows PE image — this guards - against accidentally building with a native compiler that doesn't - cross-compile (e.g. clang on macOS without ``-target``). + Windows bundles are built natively, so the downloaded toolchain's + ``leanc.exe`` is the only compiler needed. Returns the path to the built + ``git.exe``, or ``None`` on non-Windows platforms. """ if not platform.startswith("windows"): return None @@ -179,10 +163,15 @@ def build_git_shim(dest_dir: Path, platform: str) -> Path | None: _assert_pe_image(output) return output - compiler, extra = _find_git_shim_compiler() - cmd = [compiler, *extra, "-O2", "-Wall", "-Wextra", "-s", + if lean_dir is None: + raise RuntimeError("Windows git shim build requires the Lean toolchain") + compiler = lean_dir / "bin" / "leanc.exe" + if not compiler.is_file(): + raise RuntimeError(f"Downloaded Lean toolchain is missing {compiler}") + + cmd = [str(compiler), "-O2", "-Wall", "-Wextra", "-s", "-o", str(output), str(source)] - print(f" Building git shim with {compiler}...") + print(" Building git shim with bundled leanc.exe...") result = subprocess.run(cmd, capture_output=True, text=True) if result.returncode != 0: raise RuntimeError( @@ -217,43 +206,10 @@ def _assert_pe_image(path: Path) -> None: if pe_sig != b"PE\x00\x00": raise RuntimeError( f"git shim at {path} is not a PE image " - f"(bad PE signature at 0x{e_lfanew:X}): {pe_sig!r}. " - f"A native non-Windows compiler probably built the shim. " - f"Install mingw-w64 (apt-get install gcc-mingw-w64-x86-64) " - f"or zig." + f"(bad PE signature at 0x{e_lfanew:X}): {pe_sig!r}" ) -def _find_git_shim_compiler() -> tuple[str, tuple[str, ...]]: - """Return ``(binary, extra_args)`` for the first available compiler. - - On non-Windows build hosts, only explicit cross-compilers are - considered — a native ``gcc``/``clang`` on Linux/macOS would produce - an ELF/Mach-O binary rather than a PE image. Raises ``RuntimeError`` - with install instructions if none is found. - """ - on_windows = sys.platform == "win32" - for binary, extra, cross_only in _GIT_SHIM_COMPILERS: - if not cross_only and not on_windows: - continue - resolved = shutil.which(binary) - if resolved: - return resolved, extra - raise RuntimeError( - "No C compiler found for building the Windows git shim.\n" - "\n" - "Install zig (easiest cross-platform option):\n" - " macOS: brew install zig\n" - " Linux: apt-get install zig\n" - " Windows: winget install zig.zig\n" - "\n" - "Or install mingw-w64:\n" - " macOS: brew install mingw-w64\n" - " Linux: apt-get install gcc-mingw-w64-x86-64\n" - " Windows: https://www.msys2.org/" - ) - - def parse_toolchain(toolchain_file: Path) -> str: """Parse the lean-toolchain file and return the version string. @@ -323,7 +279,16 @@ def download_lean_toolchain(version: str, platform: str, dest_dir: Path) -> Path print(f" Extracting {archive_name}...") lean_dir = dest_dir / "lean-extract" - lean_dir.mkdir(exist_ok=True) + if lean_dir.is_symlink() or ( + lean_dir.exists() and not lean_dir.is_dir() + ): + raise ValueError( + f"Lean extraction path exists and is not a directory: {lean_dir}" + ) + if lean_dir.is_dir(): + print(f" Removing previous Lean extraction at {lean_dir}...") + shutil.rmtree(lean_dir) + lean_dir.mkdir() if archive_name.endswith(".zip"): with zipfile.ZipFile(archive_path) as zf: @@ -371,11 +336,20 @@ def download_lean_toolchain(version: str, platform: str, dest_dir: Path) -> Path archive_path.unlink(missing_ok=True) - # The archive typically extracts to a subdirectory like lean-4.26.0-linux/ + # Lean archives extract to one top-level toolchain directory, such as + # lean-4.31.0-linux/. Requiring exactly one prevents a reused work directory + # from silently mixing toolchains from different target platforms. subdirs = [d for d in lean_dir.iterdir() if d.is_dir()] - if len(subdirs) == 1: - return subdirs[0] - return lean_dir + if len(subdirs) != 1: + names = ", ".join(sorted(d.name for d in subdirs)) or "none" + raise RuntimeError( + f"Expected one extracted Lean toolchain in {lean_dir}, found: {names}" + ) + toolchain_dir = subdirs[0] + lake_name = "lake.exe" if platform.startswith("windows") else "lake" + if not (toolchain_dir / "bin" / lake_name).is_file(): + raise RuntimeError(f"Extracted Lean toolchain is missing bin/{lake_name}") + return toolchain_dir def _get_latest_vscodium_version() -> str: @@ -472,6 +446,42 @@ def download_openvsx_extension( return ext_dir +def _download_declared_extension_deps( + ext_dir: Path, + dest_dir: Path, + allowed_dependencies: dict[str, str], +) -> list[Path]: + """Download an extension's declared ``extensionDependencies``. + + Only IDs present in the selected frontend's allowlist are fetched, and + only at their pinned version, to prevent dependency injection via a + compromised or updated upstream extension. Raises ``ValueError`` on any + undeclared dependency so new deps must be reviewed and allowlisted + explicitly rather than silently pulled in. + """ + dep_dirs: list[Path] = [] + pkg_path = ext_dir / "package.json" + if not pkg_path.is_file(): + return dep_dirs + pkg = json.loads(pkg_path.read_text()) + for dep_id in pkg.get("extensionDependencies", []): + pinned_version = allowed_dependencies.get(dep_id) + if pinned_version is None: + raise ValueError( + f"Unexpected extension dependency {dep_id!r} (required by " + f"{ext_dir.name}). Update that frontend's dependency " + f"allowlist in download.py if this is intentional." + ) + parts = dep_id.split(".", 1) + if len(parts) == 2: + dep_dirs.append( + download_openvsx_extension( + parts[0], parts[1], dest_dir, version=pinned_version + ) + ) + return dep_dirs + + def download_lean4_extension( dest_dir: Path, version: str | None = None ) -> tuple[list[Path], str]: @@ -498,36 +508,136 @@ def download_lean4_extension( print(f" Extracting lean4 extension...") _extract_vsix(vsix_path, ext_dir) - extension_dirs = [ext_dir] + extension_dirs = [ + ext_dir, + *_download_declared_extension_deps( + ext_dir, dest_dir, LEAN4_EXTENSION_DEPS + ), + ] + return extension_dirs, version + + +def download_waterproof_extension( + dest_dir: Path, version: str | None = None +) -> tuple[list[Path], str]: + """Download the Waterproof VS Code extension (Lean-genre support only). + + Waterproof (impermeable/waterproof-vscode) is primarily a Coq/Rocq + frontend, but it also drives a Lean-only workflow -- the "Waterproof + Genre" built on Verso (see impermeable/waterproof-genre) -- that needs + nothing beyond a normal Lean toolchain: Waterproof spawns ``lake serve`` + itself via its ``waterproof.lakePath`` / ``waterproof.lakeArgs`` + settings. This bundler only ever wires up that Lean path; it never + downloads or configures coq-lsp/opam. The bundle's workspace settings + pin ``waterproof.skipLaunchChecks: "lean4"`` (see + ``assemble.assemble_bundle``) so the extension only starts the Lean + language server and skips its Rocq/coq-lsp probing entirely. + + Returns (extension_dirs, resolved_version). extension_dirs includes + any allowlisted extensionDependencies declared by Waterproof's own + package.json. + """ + try: + ext_dir = download_openvsx_extension( + "waterproof-tue", "waterproof", dest_dir, version=version + ) + except urllib.error.HTTPError as e: + raise RuntimeError( + "Could not fetch the Waterproof extension from Open VSX " + f"(waterproof-tue.waterproof): {e}\n" + "To use an unpublished build, pass --waterproof-vsix PATH." + ) from e - # Download extension dependencies (only from allowlist, at pinned versions) pkg_path = ext_dir / "package.json" + resolved_version = version or "unknown" if pkg_path.is_file(): - pkg = json.loads(pkg_path.read_text()) - for dep_id in pkg.get("extensionDependencies", []): - pinned_version = ALLOWED_EXTENSION_DEPS.get(dep_id) - if pinned_version is None: - raise ValueError( - f"Unexpected extension dependency {dep_id!r}. " - f"Update ALLOWED_EXTENSION_DEPS in download.py if this is intentional." - ) - parts = dep_id.split(".", 1) - if len(parts) == 2: - dep_dir = download_openvsx_extension( - parts[0], parts[1], dest_dir, version=pinned_version - ) - extension_dirs.append(dep_dir) + resolved_version = json.loads(pkg_path.read_text()).get( + "version", resolved_version + ) - return extension_dirs, version + extension_dirs = [ + ext_dir, + *_download_declared_extension_deps( + ext_dir, dest_dir, WATERPROOF_EXTENSION_DEPS + ), + ] + return extension_dirs, resolved_version + + +def install_local_waterproof_vsix( + vsix_path: Path, dest_dir: Path +) -> tuple[list[Path], str]: + """Install an unpublished or locally-built Waterproof ``.vsix``.""" + if not vsix_path.is_file(): + raise FileNotFoundError(f"--waterproof-vsix path not found: {vsix_path}") + + dest_dir.mkdir(parents=True, exist_ok=True) + + # _extract_vsix() deletes its input after extracting, so stage through a + # unique file. This also works when the caller's VSIX already lives in + # dest_dir; copying to dest_dir / vsix_path.name would be SameFileError. + descriptor, staged_name = tempfile.mkstemp( + prefix=".waterproof-local-", suffix=".vsix", dir=dest_dir, + ) + os.close(descriptor) + local_copy = Path(staged_name) + ext_dir = dest_dir / "waterproof-tue.waterproof-local" + + try: + shutil.copy2(vsix_path, local_copy) + print(f" SHA-256: {_sha256_file(local_copy)}") + + # Reused work directories must not merge a rebuilt VSIX with files + # removed from the previous version. + if ext_dir.is_symlink() or (ext_dir.exists() and not ext_dir.is_dir()): + ext_dir.unlink() + elif ext_dir.is_dir(): + shutil.rmtree(ext_dir) + + print(f" Extracting {vsix_path.name}...") + _extract_vsix(local_copy, ext_dir) + + pkg_path = ext_dir / "package.json" + if not pkg_path.is_file(): + raise ValueError( + f"{vsix_path} doesn't look like a valid VSIX " + "(no package.json found after extraction)" + ) + + package = json.loads(pkg_path.read_text()) + identity = (package.get("publisher"), package.get("name")) + expected_identity = ("waterproof-tue", "waterproof") + if identity != expected_identity: + actual = ".".join(str(part or "") for part in identity) + raise ValueError( + f"{vsix_path} is {actual}, expected " + "waterproof-tue.waterproof" + ) + version = package.get("version", "unknown") + + extension_dirs = [ + ext_dir, + *_download_declared_extension_deps( + ext_dir, dest_dir, WATERPROOF_EXTENSION_DEPS + ), + ] + return extension_dirs, version + except Exception: + local_copy.unlink(missing_ok=True) + if ext_dir.is_symlink() or (ext_dir.exists() and not ext_dir.is_dir()): + ext_dir.unlink() + elif ext_dir.is_dir(): + shutil.rmtree(ext_dir) + raise def trim_lean_toolchain(lean_dir: Path, platform: str) -> None: - """Remove unnecessary files from the lean toolchain to reduce bundle size. + """Keep only the runtime needed by the editor. - Keeps: lean, lake, runtime shared libraries, Init/Lean/Std/Lake oleans. - Removes: clang, lld, LLVM libs, static libraries, include, src, share. + Removes clang, lld, LLVM libraries, static libraries, headers, sources, + and shared data from the native Lean toolchain. """ - is_windows = platform.startswith("windows") + bin_dir = lean_dir / "bin" lib_dir = lean_dir / "lib" diff --git a/import_closure.py b/import_closure.py index 874ad5a..b4bc6aa 100644 --- a/import_closure.py +++ b/import_closure.py @@ -1,16 +1,32 @@ """Compute the transitive import closure for a Lean 4 project. -Uses ``lean --src-deps`` for dependency discovery, running invocations -in parallel to avoid the minutes-long sequential BFS that dominated -bundle build times on mathlib-based projects. +Uses Lean's batched ``--deps-json`` parser when available, with parallel +``--src-deps`` calls as a compatibility fallback for older toolchains. +Lake's environment is computed once instead of reloading the full workspace +for every source file. """ +import json +import os import subprocess -from collections import deque +from collections.abc import Callable from concurrent.futures import ThreadPoolExecutor, as_completed +from dataclasses import dataclass from pathlib import Path +ProgressCallback = Callable[[int, int, int, int, int], None] + + +@dataclass(frozen=True) +class _LeanEnvironment: + """Lean executable and search paths produced by one ``lake env`` call.""" + + executable: str + process_env: dict[str, str] + src_search_path: tuple[Path, ...] + + def module_to_relpath(mod: str) -> Path: """Convert a module name to a relative file path. @@ -19,12 +35,93 @@ def module_to_relpath(mod: str) -> Path: return Path(*mod.split(".")).with_suffix(".lean") +def _load_lean_environment( + project_dir: Path, + lake_executable: str | Path = "lake", +) -> _LeanEnvironment: + """Load Lake's process environment and Lean source path once.""" + base_env = os.environ.copy() + lake_path = Path(lake_executable) + if lake_path.is_absolute(): + lean_bin = lake_path.parent + base_env["PATH"] = ( + str(lean_bin) + os.pathsep + base_env.get("PATH", "") + ) + base_env["ELAN_HOME"] = str(lean_bin.parent) + + result = subprocess.run( + [str(lake_executable), "env"], + cwd=project_dir, + env=base_env, + capture_output=True, + text=True, + timeout=60, + ) + if result.returncode != 0: + stderr = (result.stderr or "").strip() + raise RuntimeError(f"lake env failed.\n{stderr}") + + lake_env: dict[str, str] = {} + for line in result.stdout.splitlines(): + if "=" not in line: + continue + name, value = line.split("=", 1) + lake_env[name] = value + + executable = lake_env.get("LEAN") + if not executable: + raise RuntimeError("lake env did not report the LEAN executable") + + process_env = base_env + process_env.update(lake_env) + + src_search_path: list[Path] = [] + for entry in lake_env.get("LEAN_SRC_PATH", "").split(os.pathsep): + if not entry: + continue + path = Path(entry) + if not path.is_absolute(): + path = project_dir / path + path = path.resolve() + if path not in src_search_path: + src_search_path.append(path) + + # Lean.getSrcSearchPath appends these built-in source roots after + # LEAN_SRC_PATH. Include them so --deps-json resolves exactly the same + # modules as --src-deps, including Init and Lake sources. + sysroot = lake_env.get("LEAN_SYSROOT") + lean_src = ( + Path(sysroot) / "src" / "lean" + if sysroot + else Path(executable).resolve().parent.parent / "src" / "lean" + ) + for path in (lean_src / "lake", lean_src): + path = path.resolve() + if path not in src_search_path: + src_search_path.append(path) + + return _LeanEnvironment( + executable=executable, + process_env=process_env, + src_search_path=tuple(src_search_path), + ) + + def _src_deps_one(lean_file: Path, project_dir: Path, - timeout: int = 60) -> list[Path]: + timeout: int = 60, + lean_env: _LeanEnvironment | None = None) -> list[Path]: """Run ``lean --src-deps`` on a single file and return resolved paths.""" + if lean_env is None: + command = ["lake", "env", "lean"] + process_env = None + else: + command = [lean_env.executable] + process_env = lean_env.process_env + result = subprocess.run( - ["lake", "env", "lean", "--src-deps", str(lean_file)], + [*command, "--src-deps", str(lean_file)], cwd=project_dir, + env=process_env, capture_output=True, text=True, timeout=timeout, @@ -49,20 +146,103 @@ def _src_deps_one(lean_file: Path, project_dir: Path, return paths +def _resolve_module_source( + module: str, + src_search_path: tuple[Path, ...], +) -> Path | None: + """Resolve a module name using Lean's ordered source search path.""" + relative = module_to_relpath(module) + for root in src_search_path: + candidate = root / relative + if candidate.is_file(): + return candidate.resolve() + return None + + +def _src_deps_batch( + lean_files: list[Path], + project_dir: Path, + lean_env: _LeanEnvironment, + module_sources: dict[str, Path] | None = None, + timeout: int = 60, +) -> list[list[Path]] | None: + """Parse direct imports for a wave in one Lean process. + + Returns one dependency list per input file. ``None`` means the batched + mode is unavailable or could not parse the wave, in which case callers + should use the compatibility path. ``--deps-json`` was added in Lean + 4.22, so falling back is expected for older supported toolchains. + """ + if module_sources is None: + module_sources = {} + + try: + result = subprocess.run( + [lean_env.executable, "--deps-json", "--stdin"], + cwd=project_dir, + env=lean_env.process_env, + input="\n".join(str(path) for path in lean_files) + "\n", + capture_output=True, + text=True, + timeout=timeout, + ) + except (OSError, subprocess.TimeoutExpired): + return None + + if result.returncode != 0: + return None + + try: + parsed = json.loads(result.stdout)["imports"] + if len(parsed) != len(lean_files): + return None + + dependencies: list[list[Path]] = [] + for item in parsed: + if item.get("errors") or item.get("result") is None: + return None + paths: list[Path] = [] + for imported in item["result"]["imports"]: + module = imported["module"] + source = module_sources.get(module) + if source is None: + source = _resolve_module_source( + module, lean_env.src_search_path, + ) + if source is None: + return None + module_sources[module] = source + paths.append(source) + dependencies.append(paths) + return dependencies + except (KeyError, TypeError, ValueError, json.JSONDecodeError): + return None + + def compute_src_deps(project_dir: Path, - max_workers: int = 64) -> set[Path]: - """Compute transitive source dependencies using ``lean --src-deps``. + max_workers: int = 16, + progress: ProgressCallback | None = None, + lake_executable: str | Path | None = None) -> set[Path]: + """Compute transitive source dependencies from the project's sources. Returns a set of absolute Paths to ``.lean`` files that are transitively imported by the project's own sources. - Runs ``lean --src-deps`` in parallel (up to *max_workers* at a time) - to avoid the per-invocation ~500 ms overhead from dominating wall - time. BFS levels are processed in waves: all files discovered in - one wave are queried concurrently, then the next wave starts. + On Lean 4.22+, each BFS wave is parsed in one process with + ``lean --deps-json --stdin``. Older toolchains, batch parse failures, and + unusual source layouts automatically fall back to parallel + ``lean --src-deps`` calls. Both paths use a single precomputed Lake + environment, avoiding a full workspace reload for every source file. + + If *progress* is provided, it is called with ``(wave, completed, + wave_total, checked_total, dependencies_found)`` before each wave and + after each file completes. + """ deps: set[Path] = set() seen: set[Path] = set() + checked = 0 + wave_number = 0 # Seed: the project's own .lean files (outside .lake/). wave: list[Path] = [] @@ -73,20 +253,75 @@ def compute_src_deps(project_dir: Path, seen.add(resolved) wave.append(resolved) + if not wave: + return deps + + if lake_executable is None: + lean_env = _load_lean_environment(project_dir) + else: + lean_env = _load_lean_environment(project_dir, lake_executable) + batch_enabled = True + module_sources: dict[str, Path] = {} + while wave: + wave_number += 1 + wave_total = len(wave) + wave_completed = 0 next_wave: list[Path] = [] - with ThreadPoolExecutor(max_workers=min(max_workers, len(wave))) as pool: - futures = { - pool.submit(_src_deps_one, f, project_dir): f - for f in wave - } - for future in as_completed(futures): - for dep_path in future.result(): + if progress is not None: + progress(wave_number, 0, wave_total, checked, len(deps)) + + batch_results = ( + _src_deps_batch( + wave, project_dir, lean_env, module_sources, + ) + if batch_enabled + else None + ) + if batch_results is not None: + for dep_paths in batch_results: + for dep_path in dep_paths: + deps.add(dep_path) if dep_path not in seen: seen.add(dep_path) - deps.add(dep_path) next_wave.append(dep_path) + checked += 1 + wave_completed += 1 + if progress is not None: + progress( + wave_number, wave_completed, wave_total, + checked, len(deps), + ) + else: + # ``--deps-json`` is unavailable before Lean 4.22. It may also + # reject an unusual header which the full parser accepts. Disable + # batching after the first failure and preserve the old behavior. + batch_enabled = False + with ThreadPoolExecutor( + max_workers=min(max_workers, len(wave)), + ) as pool: + futures = { + pool.submit( + _src_deps_one, f, project_dir, + lean_env=lean_env, + ): f + for f in wave + } + for future in as_completed(futures): + dep_paths = future.result() + for dep_path in dep_paths: + deps.add(dep_path) + if dep_path not in seen: + seen.add(dep_path) + next_wave.append(dep_path) + checked += 1 + wave_completed += 1 + if progress is not None: + progress( + wave_number, wave_completed, wave_total, + checked, len(deps), + ) wave = next_wave @@ -98,7 +333,43 @@ def module_build_artifact_prefix(mod: str) -> str: E.g. "Mathlib.Algebra.Group.Basic" -> "Mathlib/Algebra/Group/Basic" """ - return str(Path(*mod.split("."))) + return Path(*mod.split(".")).as_posix() + + +def _resolve_built_module_stem(build_dir: Path, source_rel: Path) -> str: + """Resolve a source path to the module stem used by Lake's build tree. + + Lake stores artifacts by *module name*, not by the path relative to the + package root. Those are the same for the common layout:: + + Mathlib/Foo.lean -> build/lib/lean/Mathlib/Foo.olean + + but differ when a library declares ``srcDir``:: + + src/verso-manual/VersoManual/Foo.lean + -> build/lib/lean/VersoManual/Foo.olean + + We deliberately resolve this against the artifacts of the already-built + project instead of trying to parse arbitrary Lake DSL. A module path is + a suffix of its source path after removing the library's ``srcDir``. Try + suffixes longest-first so nested module names win over coincidental short + names such as ``Foo.olean``. + + If no artifact exists, return the unmodified source-relative stem. This + preserves the old behaviour for source files that are not build targets; + the caller's bundle-level validation can still fall back to a full copy + when none of the computed stems match build artifacts. + """ + source_stem = source_rel.with_suffix("") + parts = source_stem.parts + + if build_dir.is_dir(): + for offset in range(len(parts)): + candidate = Path(*parts[offset:]) + if (build_dir / f"{candidate}.olean").is_file(): + return candidate.as_posix() + + return source_stem.as_posix() def src_paths_to_module_stems( @@ -118,10 +389,9 @@ def src_paths_to_module_stems( dependencies only). The project's own modules are discovered by scanning *project_dir* for ``.lean`` files outside ``.lake/``. - .. note:: This assumes the standard Lean project layout where source - paths directly mirror module names. If a package uses Lake's - ``srcDir`` option the computed stems will be wrong. Callers should - validate the result against actual build artifacts. + Source paths are resolved against each package's existing build tree, so + libraries using Lake's ``srcDir`` option are handled without parsing the + package's Lake configuration. """ project_dir = project_dir.resolve() lake_packages = project_dir / ".lake" / "packages" @@ -135,7 +405,9 @@ def src_paths_to_module_stems( continue if ".lake" in rel.parts: continue - stems.add(str(rel.with_suffix(""))) + stems.add(_resolve_built_module_stem( + project_dir / ".lake" / "build" / "lib" / "lean", rel, + )) # Include dependency modules from the import closure. for src in needed_srcs: @@ -147,8 +419,14 @@ def src_paths_to_module_stems( rel = src.relative_to(lake_packages) parts = rel.parts if len(parts) >= 2: - # parts[0] is the package name, rest is the module path - stems.add(str(Path(*parts[1:]).with_suffix(""))) + # parts[0] is the package name. The remainder is the source + # path relative to that package, which may still include a + # library srcDir such as ``src/verso-manual``. + package_dir = lake_packages / parts[0] + build_dir = package_dir / ".lake" / "build" / "lib" / "lean" + stems.add(_resolve_built_module_stem( + build_dir, Path(*parts[1:]), + )) continue except ValueError: pass @@ -176,6 +454,6 @@ def find_module_build_artifacts(mod: str, build_dir: Path) -> list[tuple[str, Pa results = [] for f in parent.iterdir(): if f.is_file() and f.name.startswith(stem + "."): - rel = str(f.relative_to(build_dir)) + rel = f.relative_to(build_dir).as_posix() results.append((rel, f)) return results diff --git a/shim/git_shim.c b/shim/git_shim.c index 06830d4..790afcc 100644 --- a/shim/git_shim.c +++ b/shim/git_shim.c @@ -35,11 +35,47 @@ * * Build: * x86_64-w64-mingw32-gcc -O2 -s -o git.exe git_shim.c (cross on Linux) - * gcc -O2 -s -o git.exe git_shim.c (native on Windows) + * leanc -O2 -s -o git.exe git_shim.c (bundled on Windows) */ +#ifdef _WIN32 +/* Keep the Windows build independent of SDK/MinGW headers. Lean's Windows + * toolchain includes leanc, the CRT objects, and kernel32 import library, but + * deliberately does not ship the ordinary C/Windows header trees. */ +typedef void *shim_handle; +typedef unsigned long shim_dword; +typedef int shim_bool; + +__declspec(dllimport) shim_handle __stdcall GetStdHandle(shim_dword handle); +__declspec(dllimport) shim_bool __stdcall WriteFile( + shim_handle file, + const void *buffer, + shim_dword bytes_to_write, + shim_dword *bytes_written, + void *overlapped +); + +#define SHIM_STD_OUTPUT_HANDLE ((shim_dword)-11) +#define SHIM_STD_ERROR_HANDLE ((shim_dword)-12) + +static void write_stream(shim_dword stream, const char *text) { + shim_dword length = 0; + shim_dword written; + while (text[length] != '\0') { + length++; + } + (void)WriteFile(GetStdHandle(stream), text, length, &written, 0); +} +#else #include -#include + +#define SHIM_STD_OUTPUT_HANDLE 1 +#define SHIM_STD_ERROR_HANDLE 2 + +static void write_stream(int stream, const char *text) { + fputs(text, stream == SHIM_STD_OUTPUT_HANDLE ? stdout : stderr); +} +#endif /* Must be >= 2.0.0 and must NOT be 2.25.x/2.26.x (VS Code pops a modal * deprecation warning for those on Windows). Choosing 2.47.0 matches the @@ -53,9 +89,17 @@ static const char VERSION_LINE[] = "git version 2.47.0\n"; static const char NOT_A_REPO[] = "fatal: not a git repository (or any of the parent directories): .git\n"; +static int strings_equal(const char *a, const char *b) { + while (*a != '\0' && *a == *b) { + a++; + b++; + } + return *a == *b; +} + static int is_version_flag(const char *a) { - return strcmp(a, "--version") == 0 - || strcmp(a, "-v") == 0; + return strings_equal(a, "--version") + || strings_equal(a, "-v"); } /* A few top-level flags consume the next argv entry (e.g. `git -C @@ -63,15 +107,15 @@ static int is_version_flag(const char *a) { * caller like `git -c user.name=foo commit` doesn't confuse us into thinking * `user.name=foo` is the subcommand. */ static int consumes_next(const char *a) { - return strcmp(a, "-C") == 0 - || strcmp(a, "-c") == 0 - || strcmp(a, "--git-dir") == 0 - || strcmp(a, "--work-tree") == 0 - || strcmp(a, "--namespace") == 0; + return strings_equal(a, "-C") + || strings_equal(a, "-c") + || strings_equal(a, "--git-dir") + || strings_equal(a, "--work-tree") + || strings_equal(a, "--namespace"); } int main(int argc, char *argv[]) { - const char *sub = NULL; + const char *sub = 0; int i = 1; while (i < argc) { @@ -81,7 +125,7 @@ int main(int argc, char *argv[]) { break; } if (is_version_flag(a)) { - fputs(VERSION_LINE, stdout); + write_stream(SHIM_STD_OUTPUT_HANDLE, VERSION_LINE); return 0; } if (consumes_next(a)) { @@ -92,8 +136,8 @@ int main(int argc, char *argv[]) { i += 1; } - if (sub != NULL && strcmp(sub, "version") == 0) { - fputs(VERSION_LINE, stdout); + if (sub != 0 && strings_equal(sub, "version")) { + write_stream(SHIM_STD_OUTPUT_HANDLE, VERSION_LINE); return 0; } @@ -102,6 +146,6 @@ int main(int argc, char *argv[]) { * abort cleanly, and Lake's optional git probes (`captureProc?`, * `testProc`) treat non-zero exit as "no result" without surfacing the * error. The exit code (128) matches real git's "not a repository". */ - fputs(NOT_A_REPO, stderr); + write_stream(SHIM_STD_ERROR_HANDLE, NOT_A_REPO); return 128; } diff --git a/templates/start_lean.cmd b/templates/start_lean.cmd index be1183a..1d1ee1d 100644 --- a/templates/start_lean.cmd +++ b/templates/start_lean.cmd @@ -43,10 +43,13 @@ for /d %%P in ("%BUNDLE_ROOT%\project\.lake\packages\*") do ( ) ) -:: Determine which file to open (set during bundle assembly). +:: Open the configured file only on the first launch of this extracted +:: bundle. Later launches let VSCodium restore the student's own open tabs. set OPEN_FILE=@@OPEN_FILE@@ +set "OPEN_MARKER=%VSCODE_PORTABLE%\user-data\User\.lean-bundle-default-opened" +if exist "!OPEN_MARKER!" set OPEN_FILE= -:: Launch VSCodium with the project folder (and optional file). +:: Launch VSCodium with the project folder (and optional first-launch file). :: Use `start` so the Command Prompt window closes immediately instead of :: staying open for the entire VSCodium session. The empty "" is required :: as the window-title argument (otherwise `start` treats the quoted path @@ -54,6 +57,7 @@ set OPEN_FILE=@@OPEN_FILE@@ if defined OPEN_FILE ( if exist "%BUNDLE_ROOT%\project\!OPEN_FILE!" ( start "" "%BUNDLE_ROOT%\vscodium\VSCodium.exe" "%BUNDLE_ROOT%\project" "%BUNDLE_ROOT%\project\!OPEN_FILE!" %* + type nul > "!OPEN_MARKER!" ) else ( start "" "%BUNDLE_ROOT%\vscodium\VSCodium.exe" "%BUNDLE_ROOT%\project" %* ) diff --git a/templates/start_lean.sh b/templates/start_lean.sh index a8c3d99..8fd17e6 100644 --- a/templates/start_lean.sh +++ b/templates/start_lean.sh @@ -52,13 +52,16 @@ for pkg_dir in "$BUNDLE_ROOT"/project/.lake/packages/*/; do done export LEAN_PATH -# Determine which file to open (set during bundle assembly). +# Open the configured file only on the first launch of this extracted +# bundle. Later launches let VSCodium restore the student's own open tabs. OPEN_FILE="@@OPEN_FILE@@" +OPEN_MARKER="$VSCODE_PORTABLE/user-data/User/.lean-bundle-default-opened" -# Build the argument list: workspace folder, then optional file. +# Build the argument list: workspace folder, then optional first-launch file. ARGS=("$BUNDLE_ROOT/project") -if [ -n "$OPEN_FILE" ] && [ -f "$BUNDLE_ROOT/project/$OPEN_FILE" ]; then +if [ ! -e "$OPEN_MARKER" ] && [ -n "$OPEN_FILE" ] && [ -f "$BUNDLE_ROOT/project/$OPEN_FILE" ]; then ARGS+=("$BUNDLE_ROOT/project/$OPEN_FILE") + : > "$OPEN_MARKER" fi # Launch VSCodium diff --git a/tests/test_assemble.py b/tests/test_assemble.py index d29a3ee..eee5c28 100644 --- a/tests/test_assemble.py +++ b/tests/test_assemble.py @@ -7,11 +7,26 @@ import json import pytest +import bundle + +from bundle import ( + _WORK_DIR_MARKER, + _detect_host_platform, + _prepare_work_dir, + build_project, + clone_project, +) +from download import trim_lean_toolchain + from assemble import ( _BUNDLE_CRITICAL_SETTINGS, + _BUNDLE_USER_SETTINGS, + _WATERPROOF_CRITICAL_SETTINGS, + _WATERPROOF_USER_SETTINGS, _module_stem_from_build_path, _parse_jsonc, _patch_workspace_settings, + _reset_bundle_dir, _rewrite_lakefile_lean_deps, _rewrite_lakefile_toml_deps, copy_lake_selective, @@ -32,6 +47,374 @@ def test_no_zip_without_work_dir_is_rejected() -> None: assert "--no-zip requires --work-dir" in result.stderr +def test_clean_work_dir_without_work_dir_is_rejected() -> None: + result = subprocess.run( + [ + sys.executable, + "bundle.py", + "https://example.invalid/repo", + "--clean-work-dir", + ], + capture_output=True, + text=True, + ) + assert result.returncode == 2 + assert "--clean-work-dir requires --work-dir" in result.stderr + + +def test_cross_platform_bundle_is_rejected_before_work_starts() -> None: + target = "linux-x64" if sys.platform == "win32" else "windows" + result = subprocess.run( + [ + sys.executable, "bundle.py", "https://example.invalid/repo", + "--platform", target, + ], + capture_output=True, + text=True, + ) + assert result.returncode == 2 + assert "Cross-platform bundles are not supported" in result.stderr + assert f"requested {target}" in result.stderr + + +@pytest.mark.parametrize( + "waterproof_args", + [ + ["--waterproof"], + ["--waterproof-version", "0.12.0"], + ["--waterproof-vsix", "waterproof.vsix"], + ], +) +def test_open_file_is_rejected_for_windows_waterproof_before_work_starts( + waterproof_args: list[str], + monkeypatch: pytest.MonkeyPatch, + capsys: pytest.CaptureFixture[str], +) -> None: + monkeypatch.setattr(bundle, "_detect_host_platform", lambda: "windows") + monkeypatch.setattr( + sys, + "argv", + [ + "bundle.py", + "https://example.invalid/repo", + "--platform", + "windows", + *waterproof_args, + "--open-file", + "Course/Sheet.lean", + ], + ) + + with pytest.raises(SystemExit) as exc_info: + bundle.main() + + assert exc_info.value.code == 2 + assert ( + "--open-file is not supported for Waterproof bundles on Windows" + in capsys.readouterr().err + ) + + +def test_open_file_remains_supported_for_regular_windows_bundles( + tmp_path: Path, + monkeypatch: pytest.MonkeyPatch, +) -> None: + class CloneReached(Exception): + pass + + def fake_clone(*args, **kwargs): + raise CloneReached + + monkeypatch.setattr(bundle, "_detect_host_platform", lambda: "windows") + monkeypatch.setattr(bundle, "clone_project", fake_clone) + monkeypatch.setattr( + sys, + "argv", + [ + "bundle.py", + "https://example.invalid/repo", + "--platform", + "windows", + "--open-file", + "Course/Sheet.lean", + "--work-dir", + str(tmp_path / "work"), + ], + ) + + with pytest.raises(CloneReached): + bundle.main() + + +@pytest.mark.parametrize( + ("system", "machine", "expected"), + [ + ("Windows", "AMD64", "windows"), + ("Linux", "x86_64", "linux-x64"), + ("Linux", "aarch64", "linux-arm64"), + ("Darwin", "x86_64", "darwin-x64"), + ("Darwin", "arm64", "darwin-arm64"), + ], +) +def test_detect_host_platform_accepts_supported_architectures( + monkeypatch: pytest.MonkeyPatch, + system: str, + machine: str, + expected: str, +) -> None: + monkeypatch.setattr("bundle.platform.system", lambda: system) + monkeypatch.setattr("bundle.platform.machine", lambda: machine) + + assert _detect_host_platform() == expected + + +@pytest.mark.parametrize("machine", ["i686", "ppc64le", "riscv64", "s390x"]) +def test_detect_host_platform_rejects_unsupported_linux_architectures( + monkeypatch: pytest.MonkeyPatch, + machine: str, +) -> None: + monkeypatch.setattr("bundle.platform.system", lambda: "Linux") + monkeypatch.setattr("bundle.platform.machine", lambda: machine) + + with pytest.raises(RuntimeError, match=f"linux/{machine}"): + _detect_host_platform() + + +def test_clone_project_removes_previous_clone( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + destination = tmp_path / "project" + stale_file = destination / "stale.txt" + stale_file.parent.mkdir() + stale_file.write_text("left by an interrupted run") + + def fake_run(cmd, **kwargs): + assert cmd == [ + "git", + "clone", + "--depth=1", + "https://example.invalid/repo", + str(destination), + ] + assert not destination.exists() + + monkeypatch.setattr("bundle.subprocess.run", fake_run) + + assert clone_project("https://example.invalid/repo", destination) == destination + + +def test_clone_project_checks_out_a_commit( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + destination = tmp_path / "project" + commit = "e62b9166113d3f48b82a09bd5e728fbd779608cc" + calls = [] + monkeypatch.setattr( + "bundle.subprocess.run", + lambda cmd, **kwargs: calls.append(cmd), + ) + + clone_project("https://example.invalid/repo", destination, ref=commit) + + assert calls == [ + [ + "git", "clone", "--depth=1", "--no-checkout", + "https://example.invalid/repo", str(destination), + ], + ["git", "-C", str(destination), "fetch", "--depth=1", "origin", commit], + ["git", "-C", str(destination), "checkout", "--detach", "FETCH_HEAD"], + ] + + +def test_prepare_work_dir_preserves_existing_contents_by_default( + tmp_path: Path, +) -> None: + work_dir = tmp_path / "existing-work" + sentinel = work_dir / "keep.txt" + sentinel.parent.mkdir() + sentinel.write_text("keep") + + prepared = _prepare_work_dir(work_dir) + + assert prepared == work_dir.resolve() + assert sentinel.read_text() == "keep" + assert not (prepared / _WORK_DIR_MARKER).exists() + + +def test_clean_work_dir_removes_all_previous_contents(tmp_path: Path) -> None: + work_dir = _prepare_work_dir(tmp_path / "dedicated-work") + marker = work_dir / _WORK_DIR_MARKER + assert marker.is_file() + + stale_vscodium = work_dir / "downloads" / "vscodium" / "obsolete.exe" + stale_extension = ( + work_dir / "downloads" / "waterproof-tue.waterproof-0.12.0" + / "obsolete.js" + ) + stale_vscodium.parent.mkdir(parents=True) + stale_extension.parent.mkdir(parents=True) + stale_vscodium.write_bytes(b"old") + stale_extension.write_bytes(b"old") + + prepared = _prepare_work_dir(work_dir, clean=True) + + assert prepared == work_dir.resolve() + assert marker.is_file() + assert [path.name for path in prepared.iterdir()] == [_WORK_DIR_MARKER] + + +def test_clean_work_dir_rejects_missing_marker(tmp_path: Path) -> None: + work_dir = tmp_path / "unowned" + sentinel = work_dir / "keep.txt" + sentinel.parent.mkdir() + sentinel.write_text("caller-owned") + + with pytest.raises(ValueError, match="unowned work directory"): + _prepare_work_dir(work_dir, clean=True) + + assert sentinel.read_text() == "caller-owned" + + +def test_clean_work_dir_rejects_an_input_inside_it(tmp_path: Path) -> None: + work_dir = _prepare_work_dir(tmp_path / "work") + project_dir = work_dir / "project" + sentinel = project_dir / "keep.txt" + sentinel.parent.mkdir() + sentinel.write_text("caller-owned") + + with pytest.raises(ValueError, match="overlaps an input path"): + _prepare_work_dir( + work_dir, + clean=True, + protected_paths=(project_dir,), + ) + + assert sentinel.read_text() == "caller-owned" + + +def test_clean_work_dir_rejects_current_directory() -> None: + with pytest.raises(ValueError, match="unsafe work directory"): + _prepare_work_dir(Path.cwd(), clean=True) + + +def test_allow_unsolved_tolerates_failed_build( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + calls: list[list[str]] = [] + lake = str(Path("/toolchain/bin/lake")) + + class Result: + def __init__(self, returncode: int): + self.returncode = returncode + self.stdout = "" + self.stderr = "" + + def fake_run(command, **kwargs): + calls.append(command) + if command == [lake, "build"]: + return Result(1) + return Result(0) + + monkeypatch.setattr("bundle.subprocess.run", fake_run) + + build_project( + tmp_path, + Path(lake), + "linux-x64", + allow_unsolved=True, + ) + + assert calls == [ + [lake, "exe", "cache", "get"], + [lake, "build"], + ] + + +@pytest.mark.parametrize( + ("retry_returncode", "warns"), + [(0, False), (1, True)], +) +def test_allow_unsolved_retries_windows_build_serially_before_continuing( + tmp_path: Path, + monkeypatch: pytest.MonkeyPatch, + capsys: pytest.CaptureFixture[str], + retry_returncode: int, + warns: bool, +) -> None: + calls: list[list[str]] = [] + calls_with_env: list[dict[str, str]] = [] + build_attempt = 0 + lake = str(Path("/toolchain/bin/lake")) + + class Result: + def __init__(self, returncode: int): + self.returncode = returncode + self.stdout = "" + self.stderr = "" + + def fake_run(command, **kwargs): + nonlocal build_attempt + calls.append(command) + calls_with_env.append(kwargs.get("env", {})) + if command == [lake, "build"]: + build_attempt += 1 + return Result(1 if build_attempt == 1 else retry_returncode) + return Result(0) + + monkeypatch.setenv("LEAN_NUM_THREADS", "8") + monkeypatch.setattr("bundle.subprocess.run", fake_run) + + build_project( + tmp_path, + Path(lake), + "windows", + allow_unsolved=True, + ) + + assert calls == [ + [lake, "exe", "cache", "get"], + [lake, "build"], + [lake, "build"], + ] + assert calls_with_env[0]["LEAN_NUM_THREADS"] == "8" + assert calls_with_env[1]["LEAN_NUM_THREADS"] == "8" + assert calls_with_env[2]["LEAN_NUM_THREADS"] == "1" + output = capsys.readouterr().out + assert "retrying serially on Windows" in output + assert ("--allow-unsolved was specified" in output) is warns + + +class TestTrimLeanToolchain: + @staticmethod + def _make_toolchain(root: Path) -> None: + for rel in [ + "bin/lean.exe", + "bin/lake.exe", + "bin/clang.exe", + "bin/llvm-ar.exe", + "bin/ld.lld.exe", + "include/lean/lean.h", + "lib/clang/include/stddef.h", + "lib/lean/libleanrt.a", + ]: + path = root / rel + path.parent.mkdir(parents=True, exist_ok=True) + path.write_bytes(b"tool") + + def test_removes_build_tools(self, tmp_path: Path): + self._make_toolchain(tmp_path) + + trim_lean_toolchain(tmp_path, "windows") + + assert (tmp_path / "bin" / "lean.exe").is_file() + assert (tmp_path / "bin" / "lake.exe").is_file() + assert not (tmp_path / "bin" / "clang.exe").exists() + assert not (tmp_path / "bin" / "llvm-ar.exe").exists() + assert not (tmp_path / "include").exists() + assert not (tmp_path / "lib" / "clang").exists() + assert not (tmp_path / "lib" / "lean" / "libleanrt.a").exists() + + class TestModuleStemFromBuildPath: def test_build_lib_lean_olean(self): parts = ("build", "lib", "lean", "Mathlib", "Algebra", "Group", "Basic.olean") @@ -132,6 +515,42 @@ def test_directory_pruning(self, tmp_path: Path): assert not mathlib_build.exists() +class TestResetBundleDir: + def test_removes_stale_files_and_symlinks(self, tmp_path: Path): + bundle = tmp_path / "course-bundle" + stale = bundle / "project" / ".lake" / "packages" / "mathlib" + stale.mkdir(parents=True) + (stale / "artifact.olean").write_bytes(b"stale") + try: + (stale / "run.py").symlink_to("run") + except OSError as exc: + if sys.platform == "win32" and exc.winerror == 1314: + pytest.skip("Windows user cannot create symbolic links") + raise + + _reset_bundle_dir(bundle) + + assert bundle.is_dir() + assert list(bundle.iterdir()) == [] + + def test_refuses_to_replace_a_symlink(self, tmp_path: Path): + real_dir = tmp_path / "real" + real_dir.mkdir() + bundle = tmp_path / "course-bundle" + try: + bundle.symlink_to(real_dir, target_is_directory=True) + except OSError as exc: + if sys.platform == "win32" and exc.winerror == 1314: + pytest.skip("Windows user cannot create symbolic links") + raise + + with pytest.raises(ValueError, match="not a directory"): + _reset_bundle_dir(bundle) + + assert real_dir.is_dir() + + + def test_prune_ir_from_bundle_removes_lean_ir_payloads(tmp_path: Path) -> None: bundle_project = tmp_path / "project" @@ -271,11 +690,76 @@ def test_setup_vscodium_portable_uses_vsix_extension_subdir(tmp_path) -> None: settings_template = tmp_path / "settings.json" settings_template.write_text("{}") - setup_vscodium_portable(vscodium_dir, [extension_dir], settings_template) + setup_vscodium_portable( + vscodium_dir, + [extension_dir], + settings_template, + user_settings_overrides=_BUNDLE_USER_SETTINGS, + ) ext_dest = vscodium_dir / "data" / "extensions" / extension_dir.name assert (ext_dest / "package.json").is_file() assert not (ext_dest / "extension" / "package.json").exists() + user_settings = json.loads( + (vscodium_dir / "data/user-data/User/settings.json").read_text() + ) + assert user_settings["extensions.autoUpdate"] is False + + +def test_setup_vscodium_portable_makes_waterproof_editor_default(tmp_path) -> None: + vscodium_dir = tmp_path / "vscodium" + vscodium_dir.mkdir() + + extension_dir = tmp_path / "waterproof-tue.waterproof-local" + nested = extension_dir / "extension" + nested.mkdir(parents=True) + package = { + "publisher": "waterproof-tue", + "name": "waterproof", + "version": "0.12.0-dev", + "contributes": { + "customEditors": [{ + "viewType": "waterproofTue.waterproofEditor", + "selector": [{"filenamePattern": "*.lean"}], + }], + }, + } + (nested / "package.json").write_text(json.dumps(package)) + settings_template = tmp_path / "settings.json" + settings_template.write_text("{}") + + setup_vscodium_portable( + vscodium_dir, + [extension_dir], + settings_template, + user_settings_overrides={ + **_BUNDLE_USER_SETTINGS, + **_WATERPROOF_USER_SETTINGS, + }, + ) + + installed_package = json.loads(( + vscodium_dir / "data/extensions" / extension_dir.name / "package.json" + ).read_text()) + editor = installed_package["contributes"]["customEditors"][0] + assert editor["priority"] == "default" + assert "priority" not in json.loads((nested / "package.json").read_text())[ + "contributes" + ]["customEditors"][0] + user_settings = json.loads(( + vscodium_dir / "data/user-data/User/settings.json" + ).read_text()) + assert "workbench.editorAssociations" not in user_settings + assert user_settings["window.autoDetectColorScheme"] is True + assert user_settings["workbench.colorTheme"] == "waterproof-light" + assert ( + user_settings["workbench.preferredLightColorTheme"] + == "waterproof-light" + ) + assert ( + user_settings["workbench.preferredDarkColorTheme"] + == "waterproof-dark" + ) # --------------------------------------------------------------------------- @@ -330,6 +814,49 @@ def test_preserves_all_project_settings(self, tmp_path: Path) -> None: assert result["lean4.input.leader"] == "\\" assert result["lean4.automaticallyBuildDependencies"] is False + def test_waterproof_association_preserves_other_editor_associations( + self, tmp_path: Path + ) -> None: + vscode_dir = tmp_path / ".vscode" + vscode_dir.mkdir() + (vscode_dir / "settings.json").write_text(json.dumps({ + "workbench.editorAssociations": { + "*.md": "vscode.markdown.preview.editor", + "*.lean": "project.otherEditor", + }, + })) + + _patch_workspace_settings(tmp_path, _WATERPROOF_CRITICAL_SETTINGS) + + result = json.loads((vscode_dir / "settings.json").read_text()) + associations = result["workbench.editorAssociations"] + assert associations == { + "*.md": "vscode.markdown.preview.editor", + "*.lean": "waterproofTue.waterproofEditor", + } + + def test_waterproof_theme_settings_are_removed_from_workspace( + self, tmp_path: Path + ) -> None: + vscode_dir = tmp_path / ".vscode" + vscode_dir.mkdir() + project_settings = { + **_WATERPROOF_USER_SETTINGS, + "editor.fontSize": 14, + } + (vscode_dir / "settings.json").write_text(json.dumps(project_settings)) + + _patch_workspace_settings( + tmp_path, + _WATERPROOF_CRITICAL_SETTINGS, + remove_settings=tuple(_WATERPROOF_USER_SETTINGS), + ) + + result = json.loads((vscode_dir / "settings.json").read_text()) + for key in _WATERPROOF_USER_SETTINGS: + assert key not in result + assert result["editor.fontSize"] == 14 + def test_creates_vscode_dir_when_missing(self, tmp_path: Path) -> None: """.vscode/ directory is created if it doesn't exist.""" assert not (tmp_path / ".vscode").exists() @@ -361,6 +888,22 @@ def test_all_critical_settings_present(self) -> None: assert "lean4.alwaysAskBeforeInstallingLeanVersions" in _BUNDLE_CRITICAL_SETTINGS assert "lean4.showSetupWarnings" in _BUNDLE_CRITICAL_SETTINGS assert "security.workspace.trust.enabled" in _BUNDLE_CRITICAL_SETTINGS + assert ( + _BUNDLE_CRITICAL_SETTINGS[ + "workbench.secondarySideBar.defaultVisibility" + ] + == "hidden" + ) + assert _WATERPROOF_CRITICAL_SETTINGS["waterproof.skipLaunchChecks"] == "lean4" + assert _WATERPROOF_CRITICAL_SETTINGS["workbench.editorAssociations"] == { + "*.lean": "waterproofTue.waterproofEditor", + } + assert _WATERPROOF_USER_SETTINGS == { + "window.autoDetectColorScheme": True, + "workbench.colorTheme": "waterproof-light", + "workbench.preferredLightColorTheme": "waterproof-light", + "workbench.preferredDarkColorTheme": "waterproof-dark", + } class TestParseJsonc: @@ -391,34 +934,47 @@ class TestRewriteLakefileLeanDeps: def test_bare_require(self, tmp_path: Path) -> None: lakefile = tmp_path / "lakefile.lean" - lakefile.write_text('require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v1.0"\n') + lakefile.write_text( + 'require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v1.0"\n', + encoding="utf-8", + ) _rewrite_lakefile_lean_deps(tmp_path) - assert lakefile.read_text() == 'require mathlib from ".lake/packages/mathlib"\n' + assert lakefile.read_text(encoding="utf-8") == 'require mathlib from ".lake/packages/mathlib"\n' def test_quoted_require(self, tmp_path: Path) -> None: lakefile = tmp_path / "lakefile.lean" - lakefile.write_text('require "mathlib" from git "https://github.com/leanprover-community/mathlib4" @ "v1.0"\n') + lakefile.write_text( + 'require "mathlib" from git "https://github.com/leanprover-community/mathlib4" @ "v1.0"\n', + encoding="utf-8", + ) _rewrite_lakefile_lean_deps(tmp_path) - assert lakefile.read_text() == 'require "mathlib" from ".lake/packages/mathlib"\n' + assert lakefile.read_text(encoding="utf-8") == 'require "mathlib" from ".lake/packages/mathlib"\n' def test_guillemet_require(self, tmp_path: Path) -> None: lakefile = tmp_path / "lakefile.lean" - lakefile.write_text('require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"\n') + lakefile.write_text( + 'require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"\n', + encoding="utf-8", + ) _rewrite_lakefile_lean_deps(tmp_path) - assert lakefile.read_text() == 'require «doc-gen4» from ".lake/packages/doc-gen4"\n' + assert lakefile.read_text(encoding="utf-8") == 'require «doc-gen4» from ".lake/packages/doc-gen4"\n' def test_no_rev(self, tmp_path: Path) -> None: lakefile = tmp_path / "lakefile.lean" - lakefile.write_text('require mathlib from git "https://github.com/leanprover-community/mathlib4"\n') + lakefile.write_text( + 'require mathlib from git "https://github.com/leanprover-community/mathlib4"\n', + encoding="utf-8", + ) _rewrite_lakefile_lean_deps(tmp_path) - assert lakefile.read_text() == 'require mathlib from ".lake/packages/mathlib"\n' + assert lakefile.read_text(encoding="utf-8") == 'require mathlib from ".lake/packages/mathlib"\n' def test_multiple_deps(self, tmp_path: Path) -> None: lakefile = tmp_path / "lakefile.lean" lakefile.write_text( 'require "mathlib" from git "https://github.com/leanprover-community/mathlib4" @ "v1.0"\n' 'require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"\n' - 'require aesop from git "https://github.com/leanprover-community/aesop"\n' + 'require aesop from git "https://github.com/leanprover-community/aesop"\n', + encoding="utf-8", ) _rewrite_lakefile_lean_deps(tmp_path) expected = ( @@ -426,14 +982,14 @@ def test_multiple_deps(self, tmp_path: Path) -> None: 'require «doc-gen4» from ".lake/packages/doc-gen4"\n' 'require aesop from ".lake/packages/aesop"\n' ) - assert lakefile.read_text() == expected + assert lakefile.read_text(encoding="utf-8") == expected def test_commented_out_require_not_rewritten(self, tmp_path: Path) -> None: lakefile = tmp_path / "lakefile.lean" original = '-- require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v1.0"\n' - lakefile.write_text(original) + lakefile.write_text(original, encoding="utf-8") _rewrite_lakefile_lean_deps(tmp_path) - assert lakefile.read_text() == original + assert lakefile.read_text(encoding="utf-8") == original def test_no_lakefile(self, tmp_path: Path) -> None: """No crash when lakefile.lean doesn't exist.""" diff --git a/tests/test_download.py b/tests/test_download.py new file mode 100644 index 0000000..9872b64 --- /dev/null +++ b/tests/test_download.py @@ -0,0 +1,83 @@ +import json +import zipfile +from pathlib import Path + +import pytest + +import download + + +def test_lean_extraction_replaces_stale_platform( + tmp_path: Path, + monkeypatch: pytest.MonkeyPatch, +) -> None: + extraction = tmp_path / "lean-extract" + stale_lake = extraction / "lean-4.31.0-linux" / "bin" / "lake" + stale_lake.parent.mkdir(parents=True) + stale_lake.write_bytes(b"stale") + + def fake_download(_url: str, destination: Path) -> None: + with zipfile.ZipFile(destination, "w") as archive: + archive.writestr( + "lean-4.31.0-windows/bin/lake.exe", + b"windows lake", + ) + + monkeypatch.setattr(download, "_download", fake_download) + + toolchain = download.download_lean_toolchain( + "v4.31.0", "windows", tmp_path + ) + + assert toolchain == extraction / "lean-4.31.0-windows" + assert (toolchain / "bin" / "lake.exe").is_file() + + +def _write_vsix( + path: Path, + *, + publisher: str = "waterproof-tue", + name: str = "waterproof", + version: str = "1.0.0", + files: dict[str, bytes] | None = None, +) -> None: + package = {"publisher": publisher, "name": name, "version": version} + with zipfile.ZipFile(path, "w") as archive: + archive.writestr("extension/package.json", json.dumps(package)) + for relative, contents in (files or {}).items(): + archive.writestr(f"extension/{relative}", contents) + + +def test_local_waterproof_vsix_replaces_reused_destination(tmp_path: Path) -> None: + source = tmp_path / "local.vsix" + _write_vsix(source, files={"obsolete.js": b"old"}) + + extension_dirs, version = download.install_local_waterproof_vsix( + source, tmp_path + ) + extension = extension_dirs[0] + assert version == "1.0.0" + assert (extension / "obsolete.js").is_file() + + _write_vsix(source, version="2.0.0", files={"current.js": b"new"}) + extension_dirs, version = download.install_local_waterproof_vsix( + source, tmp_path + ) + extension = extension_dirs[0] + + assert version == "2.0.0" + assert not (extension / "obsolete.js").exists() + assert (extension / "current.js").read_bytes() == b"new" + assert source.is_file() + assert not list(tmp_path.glob(".waterproof-local-*.vsix")) + + +def test_local_waterproof_vsix_rejects_wrong_extension(tmp_path: Path) -> None: + source = tmp_path / "unrelated.vsix" + _write_vsix(source, publisher="someone", name="unrelated") + + with pytest.raises(ValueError, match="expected waterproof-tue.waterproof"): + download.install_local_waterproof_vsix(source, tmp_path) + + assert source.is_file() + assert not (tmp_path / "waterproof-tue.waterproof-local").exists() diff --git a/tests/test_git_shim.py b/tests/test_git_shim.py index f81dd95..4509239 100644 --- a/tests/test_git_shim.py +++ b/tests/test_git_shim.py @@ -192,16 +192,8 @@ def test_unknown_subcommand_exits_128( ) -def _have_cross_compiler() -> bool: - """True iff an explicit PE cross-compiler is on PATH.""" - for name in ("x86_64-w64-mingw32-gcc", "x86_64-w64-mingw32-cc", "zig"): - if shutil.which(name): - return True - return False - - class TestBuildGitShim: - """Exercise the download.build_git_shim helper end-to-end.""" + """Exercise the bundled-leanc contract of ``build_git_shim``.""" def test_returns_none_on_non_windows(self, tmp_path: Path) -> None: from download import build_git_shim @@ -209,54 +201,56 @@ def test_returns_none_on_non_windows(self, tmp_path: Path) -> None: assert build_git_shim(tmp_path, "linux-x64") is None assert build_git_shim(tmp_path, "darwin-arm64") is None - def test_builds_for_windows(self, tmp_path: Path) -> None: - """Full build via ``build_git_shim`` — requires either a real PE - cross-compiler (mingw / zig) or a native Windows host. On - macOS/Linux without mingw or zig, the helper correctly refuses - to fall through to native gcc/clang.""" + def test_windows_requires_lean_toolchain(self, tmp_path: Path) -> None: + from download import build_git_shim + + with pytest.raises(RuntimeError, match="requires the Lean toolchain"): + build_git_shim(tmp_path, "windows") + + def test_windows_requires_bundled_leanc(self, tmp_path: Path) -> None: from download import build_git_shim - if not _have_cross_compiler() and sys.platform != "win32": - with pytest.raises(RuntimeError, match="No C compiler found"): - build_git_shim(tmp_path, "windows") - return - - out = build_git_shim(tmp_path, "windows") - assert out is not None - assert out.is_file() - assert out.name == "git.exe" - assert out.stat().st_size > 0 - - # Must be a real PE image — not an ELF/Mach-O wearing a .exe hat. - with open(out, "rb") as f: - dos = f.read(0x40) - assert dos[:2] == b"MZ", f"not a PE (DOS magic): {dos[:4]!r}" - e_lfanew = int.from_bytes(dos[0x3C:0x40], "little") - with open(out, "rb") as f: - f.seek(e_lfanew) - sig = f.read(4) - assert sig == b"PE\x00\x00", f"not a PE (bad PE sig): {sig!r}" - - def test_native_non_windows_compiler_is_rejected( + lean_dir = tmp_path / "lean" + lean_dir.mkdir() + with pytest.raises(RuntimeError, match=r"missing .*leanc\.exe"): + build_git_shim(tmp_path, "windows", lean_dir=lean_dir) + + def test_builds_with_bundled_leanc( self, tmp_path: Path, monkeypatch: pytest.MonkeyPatch ) -> None: - """If someone removes the cross-only guard and a native compiler - produces an ELF/Mach-O binary, the PE signature check should - catch it loudly. Simulate that by patching - ``_find_git_shim_compiler`` to return a native compiler on a - non-Windows host.""" - if sys.platform == "win32": - pytest.skip("native compiler on Windows produces valid PE") - cc = _native_cc() - if cc is None: - pytest.skip("no native compiler to misuse") - import download - monkeypatch.setattr( - download, - "_find_git_shim_compiler", - lambda: (cc, ()), + lean_dir = tmp_path / "lean" + leanc = lean_dir / "bin" / "leanc.exe" + leanc.parent.mkdir(parents=True) + leanc.touch() + calls = [] + + class Result: + returncode = 0 + stdout = "" + stderr = "" + + def fake_run(cmd, **kwargs): + calls.append((cmd, kwargs)) + output = Path(cmd[cmd.index("-o") + 1]) + image = bytearray(0x84) + image[:2] = b"MZ" + image[0x3C:0x40] = (0x80).to_bytes(4, "little") + image[0x80:0x84] = b"PE\x00\x00" + output.write_bytes(image) + return Result() + + monkeypatch.setattr(download.subprocess, "run", fake_run) + + output = download.build_git_shim( + tmp_path, "windows", lean_dir=lean_dir, ) - with pytest.raises(RuntimeError, match="not a PE image"): - download.build_git_shim(tmp_path, "windows") + + assert output == tmp_path / "git-shim" / "git.exe" + assert calls == [ + ([ + str(leanc), "-O2", "-Wall", "-Wextra", "-s", + "-o", str(output), str(SHIM_SOURCE), + ], {"capture_output": True, "text": True}) + ] diff --git a/tests/test_import_closure.py b/tests/test_import_closure.py index 45b143e..9271b29 100644 --- a/tests/test_import_closure.py +++ b/tests/test_import_closure.py @@ -8,6 +8,9 @@ sys.path.insert(0, str(Path(__file__).parent.parent)) from import_closure import ( + _LeanEnvironment, + _src_deps_batch, + _src_deps_one, module_to_relpath, compute_src_deps, find_module_build_artifacts, @@ -27,7 +30,15 @@ def test_dotted(self): class TestComputeSrcDeps: - def test_transitive_walks_src_deps_graph(self, tmp_path, monkeypatch): + @staticmethod + def lean_env(tmp_path: Path) -> _LeanEnvironment: + return _LeanEnvironment( + executable="/toolchain/bin/lean", + process_env={"LEAN_PATH": "/build/lib/lean"}, + src_search_path=(tmp_path,), + ) + + def test_transitive_walks_batched_import_graph(self, tmp_path, monkeypatch): project = tmp_path / "project" project.mkdir() main = project / "Main.lean" @@ -41,25 +52,157 @@ def test_transitive_walks_src_deps_graph(self, tmp_path, monkeypatch): dep_b.write_text("def b := 1\n") outputs = { - str(main.resolve()): f"{dep_a}\n", - str(dep_a.resolve()): f"{dep_b}\n", - str(dep_b.resolve()): "", + main.resolve(): [dep_a.resolve()], + dep_a.resolve(): [dep_b.resolve()], + dep_b.resolve(): [], } + waves = [] + + def fake_batch(lean_files, *args, **kwargs): + waves.append(lean_files) + return [outputs[path] for path in lean_files] + + monkeypatch.setattr( + "import_closure._load_lean_environment", + lambda _project: self.lean_env(tmp_path), + ) + monkeypatch.setattr("import_closure._src_deps_batch", fake_batch) + + deps = compute_src_deps(project) + + assert deps == {dep_a.resolve(), dep_b.resolve()} + assert waves == [[main.resolve()], [dep_a.resolve()], [dep_b.resolve()]] + + def test_reports_per_wave_progress(self, tmp_path, monkeypatch): + project = tmp_path / "project" + project.mkdir() + main = project / "Main.lean" + main.write_text("import A\n") + dep_a = tmp_path / "A.lean" + dep_a.write_text("") + + outputs = { + main.resolve(): [dep_a.resolve()], + dep_a.resolve(): [], + } + monkeypatch.setattr( + "import_closure._load_lean_environment", + lambda _project: self.lean_env(tmp_path), + ) + monkeypatch.setattr( + "import_closure._src_deps_batch", + lambda lean_files, *args, **kwargs: [ + outputs[path] for path in lean_files + ], + ) + events = [] + + compute_src_deps(project, progress=lambda *event: events.append(event)) + + assert events == [ + (1, 0, 1, 0, 0), + (1, 1, 1, 1, 1), + (2, 0, 1, 1, 1), + (2, 1, 1, 2, 1), + ] + + def test_falls_back_to_parallel_src_deps(self, tmp_path, monkeypatch): + project = tmp_path / "project" + project.mkdir() + main = project / "Main.lean" + main.write_text("import A\n") + dep_a = tmp_path / "A.lean" + dep_a.write_text("") + + outputs = { + main.resolve(): [dep_a.resolve()], + dep_a.resolve(): [], + } + lean_env = self.lean_env(tmp_path) + monkeypatch.setattr( + "import_closure._load_lean_environment", + lambda _project: lean_env, + ) + monkeypatch.setattr( + "import_closure._src_deps_batch", + lambda *args, **kwargs: None, + ) + monkeypatch.setattr( + "import_closure._src_deps_one", + lambda source, _project, lean_env=None: outputs[source], + ) + deps = compute_src_deps(project, max_workers=1) + + assert deps == {dep_a.resolve()} + + def test_batch_resolves_json_imports(self, tmp_path, monkeypatch): + project = tmp_path / "project" + project.mkdir() + main = project / "Main.lean" + main.write_text("import A\n") + source_root = tmp_path / "sources" + source_root.mkdir() + dep_a = source_root / "A.lean" + dep_a.write_text("") + lean_env = _LeanEnvironment( + executable="/toolchain/bin/lean", + process_env={"LEAN_PATH": "/build/lib/lean"}, + src_search_path=(source_root,), + ) + calls = [] class FakeResult: - def __init__(self, stdout: str): - self.stdout = stdout - self.stderr = "" - self.returncode = 0 + returncode = 0 + stdout = ( + '{"imports":[{"errors":[],"result":{"imports":' + '[{"module":"A"}],"isModule":false}}]}' + ) - def fake_run(cmd, cwd, capture_output, text, **kwargs): - return FakeResult(outputs[str(Path(cmd[-1]).resolve())]) + def fake_run(cmd, **kwargs): + calls.append((cmd, kwargs)) + return FakeResult() monkeypatch.setattr("import_closure.subprocess.run", fake_run) - deps = compute_src_deps(project) + result = _src_deps_batch([main], project, lean_env) - assert deps == {dep_a.resolve(), dep_b.resolve()} + assert result == [[dep_a.resolve()]] + assert calls[0][0] == [ + "/toolchain/bin/lean", "--deps-json", "--stdin", + ] + assert calls[0][1]["input"] == f"{main}\n" + assert calls[0][1]["env"] is lean_env.process_env + + def test_src_deps_fallback_reuses_loaded_environment( + self, tmp_path, monkeypatch, + ): + project = tmp_path / "project" + project.mkdir() + main = project / "Main.lean" + main.write_text("") + dep = tmp_path / "A.lean" + dep.write_text("") + lean_env = self.lean_env(tmp_path) + calls = [] + + class FakeResult: + returncode = 0 + stderr = "" + stdout = f"{dep}\n" + + def fake_run(cmd, **kwargs): + calls.append((cmd, kwargs)) + return FakeResult() + + monkeypatch.setattr("import_closure.subprocess.run", fake_run) + + result = _src_deps_one(main, project, lean_env=lean_env) + + assert result == [dep.resolve()] + assert calls[0][0] == [ + "/toolchain/bin/lean", "--src-deps", str(main), + ] + assert calls[0][1]["env"] is lean_env.process_env class TestSrcPathsToModuleStems: @@ -87,6 +230,52 @@ def test_includes_dependency_sources(self, tmp_path): assert "Mathlib/Algebra/Group/Basic" in stems assert "Main" in stems # project source also included + def test_resolves_dependency_src_dir_against_build_artifacts(self, tmp_path): + """Verso-style srcDir prefixes must not leak into artifact stems.""" + project = tmp_path / "project" + project.mkdir() + (project / "Main.lean").write_text("") + + package = project / ".lake" / "packages" / "verso" + source = ( + package + / "src" / "verso-manual" + / "VersoManual" / "Html" / "Style.lean" + ) + source.parent.mkdir(parents=True) + source.write_text("") + + artifact = ( + package + / ".lake" / "build" / "lib" / "lean" + / "VersoManual" / "Html" / "Style.olean" + ) + artifact.parent.mkdir(parents=True) + artifact.write_bytes(b"olean") + + stems = src_paths_to_module_stems({source.resolve()}, project) + + assert "VersoManual/Html/Style" in stems + assert "src/verso-manual/VersoManual/Html/Style" not in stems + + def test_resolves_project_src_dir_against_build_artifacts(self, tmp_path): + project = tmp_path / "project" + source = project / "src" / "Course" / "Main.lean" + source.parent.mkdir(parents=True) + source.write_text("") + + artifact = ( + project / ".lake" / "build" / "lib" / "lean" + / "Course" / "Main.olean" + ) + artifact.parent.mkdir(parents=True) + artifact.write_bytes(b"olean") + + stems = src_paths_to_module_stems(set(), project) + + assert "Course/Main" in stems + assert "src/Course/Main" not in stems + def test_ignores_toolchain_sources(self, tmp_path): project = tmp_path / "project" project.mkdir() diff --git a/tests/test_launcher.py b/tests/test_launcher.py index b74f373..3f8a05c 100644 --- a/tests/test_launcher.py +++ b/tests/test_launcher.py @@ -28,8 +28,9 @@ def _create_fake_bundle(root: Path) -> None: / ".lake" / "build" / "lib" / "lean").mkdir(parents=True) # One package WITHOUT a build dir (should NOT appear in LEAN_PATH) (root / "project" / ".lake" / "packages" / "batteries").mkdir(parents=True) - # Dummy VSCodium entries so the script doesn't complain - (root / "vscodium").mkdir(parents=True) + # Dummy VSCodium entries so the script doesn't complain. The portable + # user directory also stores the one-time default-file marker. + (root / "vscodium" / "data" / "user-data" / "User").mkdir(parents=True) def _parse_probe_output(path: Path) -> dict[str, str]: @@ -55,15 +56,19 @@ def _parse_probe_output(path: Path) -> dict[str, str]: ( echo "[LAUNCH_ARG]" echo "$BUNDLE_ROOT/project" + echo "[OPEN_ARG]" + echo "${ARGS[1]-}" ) > "$BUNDLE_ROOT/_test_probe.txt" """ -def _patch_unix_launcher(template: Path, output: Path) -> None: +def _patch_unix_launcher( + template: Path, output: Path, open_file: str = "", +) -> 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("@@OPEN_FILE@@", 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. @@ -92,6 +97,8 @@ def result(self, tmp_path: Path) -> dict[str, str]: if k not in ("ELAN_HOME", "LEAN_PATH") } clean_env["HOME"] = str(tmp_path) + clean_env["VSCODE_IPC_HOOK_CLI"] = "/stale/remote-cli.sock" + clean_env.pop("DONT_PROMPT_WSL_INSTALL", None) subprocess.run( [bash, str(patched)], check=True, @@ -161,6 +168,51 @@ def test_workspace_argument(self, result: dict[str, str]) -> None: root = result["_bundle_root"] assert result["LAUNCH_ARG"] == f"{root}/project" + def test_default_file_is_only_opened_on_first_launch( + self, tmp_path: Path, + ) -> None: + _create_fake_bundle(tmp_path) + relative_file = "Course/Sheet.lean" + lean_file = tmp_path / "project" / relative_file + lean_file.parent.mkdir() + lean_file.write_text("import Init") + patched = tmp_path / "start_lean_test.sh" + _patch_unix_launcher( + TEMPLATES_DIR / "start_lean.sh", patched, relative_file, + ) + clean_env = { + key: value for key, value in os.environ.items() + if key not in ("ELAN_HOME", "LEAN_PATH") + } + clean_env["HOME"] = str(tmp_path) + bash = shutil.which("bash") + assert bash + + subprocess.run( + [bash, str(patched)], + check=True, + timeout=30, + cwd=tmp_path, + env=clean_env, + ) + first = _parse_probe_output(tmp_path / "_test_probe.txt") + marker = ( + tmp_path / "vscodium" / "data" / "user-data" / "User" + / ".lean-bundle-default-opened" + ) + assert first["OPEN_ARG"] == str(lean_file) + assert marker.is_file() + + subprocess.run( + [bash, str(patched)], + check=True, + timeout=30, + cwd=tmp_path, + env=clean_env, + ) + second = _parse_probe_output(tmp_path / "_test_probe.txt") + assert second["OPEN_ARG"] == "" + # --------------------------------------------------------------------------- # Windows launcher tests @@ -171,7 +223,8 @@ def test_workspace_argument(self, result: dict[str, str]) -> None: echo [PATH] echo !PATH! echo [ELAN_HOME] - echo !ELAN_HOME! + if defined ELAN_HOME echo __SET__ + if not defined ELAN_HOME echo __UNSET__ echo [LEAN_PATH] echo !LEAN_PATH! echo [LAUNCH_ARG] @@ -238,13 +291,9 @@ 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}" - ) + # Use an explicit probe marker instead of parsing cmd.exe's localized + # output for `echo` with an empty variable. + assert result.get("ELAN_HOME") == "__UNSET__" def test_path_has_no_elan(self, result: dict[str, str]) -> None: for entry in result["PATH"].split(";"):