Repository navigation
Conversation
github-actions
Bot
added
the
toolchain-available
ejgallego
added
the
release-ci
Member
|
Are we missing dynamic linking against libleanshared to shrink the binary sizes? |
Contributor
Author
I'm investigating. Thanks for the tip. |
Contributor
Author
|
Linking against Original build configuration was statically linked, this was done on purpose not to depend on any other toolchain / file. I've improved the build config so we now support both self-contained mode, and shared mode. Thanks again! |
Kha
approved these changes
Oct 14, 2026
| cd tests | ||
| nix develop -c make -C ../build -j$NPROC bench | ||
| if: matrix.test-bench | ||
| - name: Check rebootstrap |
Member
There was a problem hiding this comment.
I think we could also disable this step for releases, it really isn't relevant for them
Member
|
fsanitize failure should be resolved with master merge |
This PR bundles `lean-beam` with release toolchains, providing command-line access to Lean's proof state and speculative elaboration without a separate Beam installation. Build the CLI, daemon, and plugin with the toolchain being packaged and install them using Beam's native toolchain distribution support. Add a package regression covering relocation, runtime startup, speculative elaboration, and rejection of a mismatched project toolchain. Rebuild Beam after rebootstrap changes the compiler. The Beam pin is a local-only validation candidate and must be replaced with a deployed immutable revision before upstream submission.
This PR documents why native release jobs require the Beam executable and other jobs allow the package test to skip when it is absent. Match the explicit build condition with `matrix.release && !matrix.wasm` and use string values `1` and `0` for the shell test. The con-leche and lean4lean package tests skip on missing executables in all jobs, including release jobs.
This PR adds Lean Beam's CLI, MCP server, daemon, and LSP plugin to native release toolchains, built for the containing Lean toolchain. The added distribution files and reference sizes on Linux x86_64 are: | File | Uncompressed size | | --- | ---: | | `bin/lean-beam` | 135.7 MiB | | `bin/lean-beam-mcp` | 259.5 MiB | | `bin/beam-daemon` | 257.6 MiB | | `lib/lean-beam/libbeam_Beam_LSP.so` | 1.1 MiB | | `lib/lean-beam/LICENSE` | 8.9 KiB | | `lib/lean-beam/provenance.json` | 426 bytes | The unstripped payload totals approximately 654.0 MiB and compresses to 122.7 MiB as a standalone `tar.zst` at the release compression level (`zstd -19`). Sizes vary with the platform and compiler; the size increase in the complete Lean archive can differ from this standalone payload. Windows adds `.exe` to the executable names and uses `beam_Beam_LSP.dll`; macOS uses `libbeam_Beam_LSP.dylib`. Use Beam's native build/install interface with the stage being packaged. The bundled MCP server selects the sibling `lean-beam` automatically. Rebuild Beam after rebootstrap changes the compiler. Add a package regression covering relocation, CLI probes, MCP protocol discovery and `lean_sync`, runtime isolation, and rejection of a mismatched project toolchain. Set `LEAN_BEAM_REQUIRED=1` only in native release jobs, matching the explicit Beam build condition `matrix.release && !matrix.wasm`, so a missing Beam executable fails the package test. Allow ordinary and Wasm CI jobs to skip when Beam is absent. The con-leche and lean4lean package tests skip whenever their executables are absent, including in release jobs; Beam's flag adds a stricter presence check for jobs that build it explicitly.
This PR pins the native Lean Beam payload to a public revision that includes the MCP server, fixed toolchain runtime selection, nightly API compatibility, and Windows SDK fixes.
This PR compares bundled Beam artifact paths against the physical toolchain directory so macOS temporary-directory symlinks do not produce a false relocation failure.
This PR pins the Beam leanprover#266 candidate to reuse the shared Lean and Lake libraries shipped in the containing toolchain. Update the package fixture for project-toolchain prefix resolution and document shared-runtime reuse. The Linux x86_64 reference payload adds six files, totals 11.39 MiB uncompressed, and compresses to 1.73 MiB with zstd -19. The pinned revision remains experimental and is not release-quality ready.
ejgallego
force-pushed
the
feat/bundle-lean-beam
branch
from
October 15, 2026 10:02
af2c94d to
8b32c0d
Compare
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds Lean Beam's CLI, MCP server, daemon, and LSP plugin to the native release toolchains.
The Beam executables reuse the toolchain's existing shared Lean and Lake libraries. The added distribution files and reference sizes on Linux x86_64 are:
bin/lean-beambin/lean-beam-mcpbin/beam-daemonlib/lean-beam/libbeam_Beam_LSP.solib/lean-beam/LICENSElib/lean-beam/provenance.jsonThe unstripped payload totals approximately 11.39 MiB and compresses to 1.73 MiB as a standalone
tar.zstat the release compression level (zstd -19). It adds no further copies of Lean or Lake's runtime libraries.The package regression covers relocation, canonical paths, CLI probes, MCP protocol discovery and
lean_sync, runtime isolation, and rejection of a mismatched project toolchain.Native release jobs set
LEAN_BEAM_REQUIRED=1, matching the explicit Beam build conditionmatrix.release && !matrix.wasm, so a missing Beam executable fails the package test. Ordinary builds may skip the test when Beam is absent. In comparison,lean4leanandcon-lecheskip their package tests whenever their binaries are absent, including in release jobs.This remains a draft and is not merge ready, pending further testing.