Conversation
* bazel: BCR-supplied deps + downstream-friendly fixes
Make kepler-formal consumable as a `bazel_dep` from downstream Bzlmod
modules and replace system-installed Boost / TBB / CapnProto / Flex /
ZLIB with BCR-supplied cc_library deps so the binary is reproducible
across hosts that lack the `apt-get install libboost-all-dev libtbb-dev
capnproto libcapnp-dev libfl-dev zlib1g-dev` set the README documents.
Three coordinated changes:
* bazel/deps.bzl — `build_file = "@@//bazel:*.BUILD.bazel"` →
`build_file = Label("//bazel:*.BUILD.bazel")` for glucose, kissat,
naja. The `@@//` apparent-root form resolves to whichever module
is the build root; when kepler-formal is consumed as a non-root
bazel_dep, this becomes `@@//→consumer-root` and the overlay
BUILD files are not found, breaking the glucose / kissat / naja
fetch with `BUILD file not found //bazel:glucose.BUILD.bazel`.
`Label()` resolves in the context of the .bzl file that constructs
it (kepler-formal's own repo) so it works in both root and
bazel_dep configurations. Standard pattern for downstream-friendly
overlay BUILD labels.
* MODULE.bazel + bazel/naja.BUILD.bazel + src/bin/BUILD.bazel +
src/formal/BUILD.bazel — bump every existing BCR dep to latest
(`rules_cc 0.2.18`, `platforms 1.1.0`, `yaml-cpp 0.9.0`,
`googletest 1.17.0.bcr.2`, `zlib 1.3.2`, `spdlog 1.17.0`) and add
BCR `onetbb 2022.3.0`, `capnp-cpp 1.1.0`, `flex 2.6.4.bcr.5`,
`boost.intrusive / boost.dynamic_bitset / boost.unordered 1.90.0.bcr.1`.
The stale "onetbb BCR module is incompatible with Bazel 8/9" comment
is removed — onetbb 2022.3.0 builds on Bazel 8.6. Wire all of those
into `bazel/naja.BUILD.bazel`'s `cmake() deps`, and replace the
binary's `linkopts = ["-lcapnp", "-lkj", "-ltbb", "-ltbbmalloc",
"-lz"]` with cc_library deps on the matching BCR modules.
`src/formal/BUILD.bazel`'s `linkopts = ["-ltbb"]` becomes
`deps = ["@onetbb//:tbb"]`. `CMAKE_DISABLE_FIND_PACKAGE_Boost=TRUE`
is set in naja's cmake() cache_entries so thirdparty/slang falls
back to its vendored `boost_unordered.hpp` instead of looking at
the host /usr/lib/cmake/Boost-*/ tree (which is invisible to
rules_foreign_cc-driven CMake builds). Python3 is left to the host
interpreter — rules_python BCR ships 3.11 by default which doesn't
match the host 3.13, and the upstream CI image installs python3-dev
so host FindPython3 already works.
* rules-foreign-cc-patches/no-leaf-flatten-headers.patch +
single_version_override on rules_foreign_cc 0.15.1 — `_get_headers()`
in `foreign_cc/private/framework.bzl` was placing cc_library headers
whose on-disk paths don't match any include_dir in a per-file
`headers` list that then got leaf-flattened into
`${EXT_BUILD_DEPS}/include/<basename>`. For cc_libraries with
`include_prefix` (like `@capnp-cpp//src/kj`'s `kj/`), this places
`kj/string.h` at BOTH `include/kj/string.h` AND `include/string.h`,
shadowing libc's `<string.h>` and breaking libstdc++'s `<cstring>`
via `using ::memchr`. Without the patch, adding `@capnp-cpp` to
naja's `cmake() deps` makes naja's CMake configure fail. The fix
trusts the include_dirs list. Upstream tracking: rules_foreign_cc
issue #418 (open since 2020). The override only fires when
kepler-formal is the root module; downstream consumers must apply
the same `single_version_override` from their own root MODULE.bazel
(Bzlmod ignores non-root single_version_override).
Tested:
$ bazelisk build //src/bin:kepler-formal
INFO: Build completed successfully, 39 total actions
$ bazel-bin/src/bin/kepler-formal --help
[info] [KeplerFormal.cpp:45] Usage: bazel-bin/src/bin/kepler-formal ...
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* reuse: declare rules-foreign-cc-patches/ under Apache-2.0
Fixes the REUSE Compliance Check failure on PR #136 — the new files
`rules-foreign-cc-patches/BUILD.bazel` and
`rules-foreign-cc-patches/no-leaf-flatten-headers.patch` had no
copyright / license info. Apache-2.0 matches upstream rules_foreign_cc
(the project the patch is targeted at and applies against).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* revert: drop BCR cc-lib wire-up; keep only label fix + version bumps
CI on ubuntu-22.04 failed with a Cap'n Proto version mismatch:
naja_common.capnp.h:10:2: error: #error "Version mismatch between
generated code and library headers. You must use the same version
of the Cap'n Proto compiler and library."
Cause: Ubuntu 22.04 ships capnproto 0.9.1, BCR capnp-cpp is 1.1.0.
naja's `find_package(CapnProto REQUIRED)` finds the 0.9.1 host capnpc
via pkg-config and uses it to compile .capnp schemas; the generated
C++ then `#include`s @capnp-cpp's 1.1.0 headers from EXT_BUILD_DEPS,
trips the version-mismatch guard, fails the build. The same conflict
latently exists for TBB/Boost/Flex, and at link time for the binary
where naja's static archives (built against host 0.9.1) would resolve
against BCR's 1.1.0 ABI.
The full BCR migration needs either a CI base image where host capnp
matches BCR, or naja's CMake taught to ignore host pkg-config — both
out of scope for this PR. Revert everything that depends on
host-version-equals-BCR-version. Keep:
* bazel/deps.bzl — `@@//bazel:*.BUILD.bazel` → `Label(...)` for
downstream `bazel_dep` consumption. Pure label-resolution fix,
no behaviour change for upstream build.
* MODULE.bazel — bump rules_cc / platforms / yaml-cpp / googletest
/ zlib / spdlog to current BCR latest. No new deps, no overrides.
Reverted:
* MODULE.bazel — new bazel_deps for boost/capnp-cpp/flex/onetbb,
plus single_version_override on rules_foreign_cc.
* bazel/naja.BUILD.bazel — cmake() deps additions, CMAKE_DISABLE_
FIND_PACKAGE_Boost cache_entry.
* src/bin/BUILD.bazel + src/formal/BUILD.bazel — linkopts→BCR deps
replacement; restore -lcapnp/-lkj/-ltbb/-ltbbmalloc/-lz and -ltbb.
* rules-foreign-cc-patches/{BUILD.bazel,no-leaf-flatten-headers.patch}
— deleted along with the .reuse/dep5 entry.
Local `bazelisk build //src/bin:kepler-formal` green.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
No description provided.