fix(Bazel): Setup BB Bazel CI - #729
Merged
Merged
Conversation
@lake_deps was fetched by every bazel command in the workspace, including ones that build no Lean at all -- `bazel build //deep_causality_num:...` and CI's own `bazel test -- //... -//lean/...` both materialized 7.5 GB of Lake/Mathlib before doing anything. Two independent causes: register_toolchains() pointed at @lake_deps//:lean_toolchain_def. Registering a toolchain forces Bazel to fetch the repo the toolchain() target lives in so resolution can evaluate it, which happens for every target in every build. rules_lean declared toolchain() next to the implementation, so there was no cheap repo to register. Adds lean_toolchain_decls: a downloadless repo holding only the declaration, created per Lean version. Resolution reads it for free and the 2.6 GB distribution is fetched lazily, only when the Lean toolchain is actually selected -- the same split rules_rust uses for @rust_toolchains. lean/BUILD.bazel loaded @lake_deps//:packages.bzl. A load() from an external repo forces that repo to be fetched before the loading package can be evaluated, and //... evaluates every package. The list is now generated locally (lean/lake_packages.bzl, from lake-manifest.json); labels in attributes stay lazy where load() cannot. Measured on a cold output base building one Rust crate: lake_deps and lean_dist_4_32_0 both absent, only the 4 KB declaration repo present, build green in 10.6s. `bazel build -- //... -//lean/...` builds 1463 targets in 4.1s with no Lean fetch. Building //lean/... still fetches both, as it must. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Marvin Hansen <marvin.hansen@gmail.com>
The Mathlib closure is set by what these files import, and the cost is invisible at the point of writing an import: Mathlib.Analysis.Quaternion reached 8,639 of 9,450 modules to supply four algebraic laws. Records the rule, and the number, in the header block of all 65 proofs -- import the narrowest module that type-checks, and mirror new imports into cache_roots in //MODULE.bazel, which tree-shakes the olean download to those roots plus their closure. Complex/Quaternion.lean's inline comment is trimmed to the file-specific fact now that its header carries the general rule. All 65 tracked proof files type-check after the edits. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Signed-off-by: Marvin Hansen <marvin.hansen@gmail.com>
Signed-off-by: Marvin Hansen <marvin.hansen@gmail.com>
…flow. Signed-off-by: Marvin Hansen <marvin.hansen@gmail.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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.
Describe your changes
Issue ticket number and link
Code checklist before requesting a review
For details on make, please see BUILD.md
Note: The CI runs all of the above and fixing things before they hit CI speeds
up the review and merge process. Thank you.
Summary by cubic
Set up BuildBuddy Bazel CI and removed the old GitHub “Tests” workflow. Lean builds are now lazy and cache-friendly; non-Lean builds and CI no longer fetch Lake/Mathlib, and Lean uses a content-addressed lock for reproducible, remotely cacheable fetches.
Refactors
rules_leanand split toolchain declarations so@lake_depsand the Lean dist are fetched only when building//lean/...; replaced@lake_deps//:packages.bzlwith locallean/lake_packages.bzl.lean/lake-lock.jsonand generators (build/scripts/lean_lock.sh,build/scripts/lean_packages_bzl.py) to pin Lake/Mathlib to sha256 archives; updatedMODULE.bazelandlean/BUILD.bazel.cache_rootssmall.CI
buildbuddy.yamlto runbazel build/test -- //... -//lean/...with reduced memory/disk..github/workflows/run_tests.ymlin favor of BuildBuddy Bazel CI.Written for commit cfa2be5. Summary will update on new commits.