Skip to content

feat: add Waterproof bundle support - #47

Closed
GitLuckier wants to merge 1 commit into
leanprover-community:mainfrom
impermeable:add-waterproof-bundle-option
Closed

GitLuckier wants to merge 1 commit into
leanprover-community:mainfrom
impermeable:add-waterproof-bundle-option

Conversation

@GitLuckier

Copy link
Copy Markdown

This PR ended up somewhat larger than I originally expected, sorry about that.
Getting Waterproof bundles working exposed a few more general issues with building on Windows and computing import-closure, so I fixed those along the way.

  • Adds the --waterproof option.
  • Supports downloading the published Waterproof extension from Open VSX or
    injecting a local VSIX build with --waterproof-vsix.
  • Adds version pinning through --waterproof-version.
  • Configures the bundled editor and launcher for Waterproof projects.
  • Adds --allow-unsolved for proof-sheet with incomplete exercises.
  • Uses the downloaded Lean toolchain to build the project, so Lean and elan no
    longer need to be installed on the build machine.
  • Makes bundle builds native-only and updates the Windows and macOS ARM64 CI
    builds to run on their respective platforms.
  • Uses the downloaded toolchain's leanc.exe to compile the Windows git shim,
    so no separate C compiler is needed.
  • Improves import-closure computation by making it more than 20x faster in my
    testing and adding a progress indicator.
  • Adds a few related improvements for proof-sheet builds, including commit
    hashes in --ref, safer work-directory cleanup through --clean-work-dir,
    and better handling of Windows paths.
  • Changes --open-file so that an explicitly selected file is opened only on
    the first launch. When it is omitted, only the workspace is opened.
  • Documents installation, Waterproof usage, proof-sheet bundle commands, and
    the current limitations.
  • Adds tests for the new options, Waterproof configuration, extension
    installation, and import-closure implementation.

Validation

  • I built a Waterproof bundle inside a Fedora container and opened it on a
    fresh Linux Mint virtual machine.
  • I tested the Windows flow on my Windows 11 machine with no Lean installation.

Trying it

On the operating system you want to target, run
python3 bundle.py https://github.com/impermeable/introduction-to-proof-sheets-lean --ref e62b9166113d3f48b82a09bd5e728fbd779608cc --vscodium-version 1.126.04524 --waterproof-version 0.12.0 --allow-unsolved.
Then unzip the generated bundle and launch Start_Lean. Omit the three version
pins to use the latest versions, or replace --waterproof-version with
--waterproof-vsix PATH to test a local extension build.

Known limitations

  • Windows Waterproof bundles cannot reliably auto-open a .lean file in the
    Waterproof editor on first launch. On a cold start, VSCodium instead opens
    the file in the normal text editor. The CLI therefore rejects the combination
    of --waterproof, --platform windows, and --open-file. This appears to be
    related to VS Code issue #325506.
  • There is not yet a dedicated end-to-end Waterproof test in CI.
  • Building a bundle still takes quite a long time because downloads and build
    results are not cached yet. In hindsight, implementing caching earlier would
    have saved me quite a few lengthy rebuilds.

Notes on AI use

Like the original bundle, this was developed with the assistance of LLMs. I
reviewed the resulting diff and manually tested the scenarios described above,
but I have not "re-derived" every implementation-detail.

@GitLuckier GitLuckier closed this Sep 3, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant