Skip to content

bazel: plain bazel_deps via an in-tree registry - #262

Merged
nanocoh merged 6 commits into
keplertech:mainfrom
oharboe:bazel-registry-no-cmake
Oct 3, 2026
Merged

nanocoh merged 6 commits into
keplertech:mainfrom
oharboe:bazel-registry-no-cmake

Conversation

@oharboe

@oharboe oharboe commented Oct 2, 2026 •

Copy link
Copy Markdown
Contributor

Makes kepler-formal's Bazel build idiomatic, so it can be published as a Bazel Central Registry module: MODULE.bazel contains only bazel_deps, rules_foreign_cc is gone from the module graph, and nothing is probed on the host.

Ready to merge once CI is green. Bazel-only change.

BCR pull requests, for now. Modules not on BCR yet come from their BCR pull requests, pinned by commit in .bazelrc, until those merge. Each .bazelrc line is replaced by the proper BCR module as it lands. Meanwhile, a root MODULE.bazel project depending on this one has to carry the same .bazelrc registry lines (plus kepler-formal's bazel/registry/ for naja, by pinned URL; see docs/bcr-roadmap.md).

What changed

  • Removed: bazel/deps.bzl and every overlay, patch and repository rule:

    • rules_foreign_cc builds of capnproto, oneTBB and slang
    • host bison/flex/m4 and python3-config
    • vendored Boost, tomlplusplus and FlexLexer.h
    • the naja BUILD-file patches, and the naja_cc_library/-iquote wrappers
  • Pruned the unused //:deps experimental feature; it got no traction.

  • Dependencies: BCR modules (onetbb, spdlog, yaml-cpp, googletest, rules_python, …) plus naja's own targets instead of an aggregate @naja library.

  • Modules not on BCR yet come from their BCR pull requests, one module each, which .bazelrc lists by commit ahead of BCR. Drop a line as its PR merges.

    Module BCR PR
    kissat 4.0.4 kissat@4.0.4 bazelbuild/bazel-central-registry#10880
    cadical 3.0.0 cadical@3.0.0 bazelbuild/bazel-central-registry#10883
    glucose 4.2.1-20251230-674dbba glucose@4.2.1-20251230-674dbba bazelbuild/bazel-central-registry#10884. Upstream master; the only change since the old pin wraps a stray printf in if (verbosity > 0), which SATSolverWrapper already asks for with verbosity = -1
    naja-if, naja-verilog naja-if@0.0.0-20260723-099677d9 bazelbuild/bazel-central-registry#10881, #10885
    sv-lang, bison sv-lang@11.0.0-20260701-b60d729d.bcr.1 bazelbuild/bazel-central-registry#10882, #10879

    bazel/registry/ keeps only naja: bazel: plain bazel_deps from BCR, no host tools najaeda/naja#457 merged with #455 (oharboe/naja@kepler-pin), until naja is released and on BCR.

  • Embedded Python is the rules_python hermetic runtime. CppDriver.cpp points PYTHONHOME at it in runfiles, in the Bazel build only. The release tarball bundles it, and its wrapper sets PYTHONHOME. TBB is now linked statically into libnaja_runtime.so, so it's no longer bundled separately.

  • Also:

    • .bcr/ templates for publish-to-bcr.
    • llvm 0.8.24.
    • Tests with their own main() use gtest (googletest 1.18's gtest_main would add a second main).
  • CI: Bazel workflows install no packages. The consumer smoke test uses the same registries and no rules_foreign_cc.

Testing

  • bazel test //... (Bazel 8.6, hermetic-llvm): 11/11 pass, including the Python-primitives test.
  • .github/consumer-test builds on Bazel 9.2.
  • bazel mod graph has no rules_foreign_cc.
  • The release packaging script, run locally: the tarball's wrapper runs the Xilinx Python-primitives example with no host Python. The tarball is ~90 MB because it now includes the Python runtime.

Notes

🤖 Generated with Claude Code

Make kepler-formal's Bazel build ready to be a Bazel Central Registry
module: MODULE.bazel contains only bazel_deps, and nothing in the build
runs cmake or probes the host.

- Delete bazel/deps.bzl and every overlay, patch and repository rule:
  rules_foreign_cc builds of capnproto, oneTBB and slang; host bison,
  flex, m4 and python3-config; vendored Boost, tomlplusplus and
  FlexLexer.h; the naja BUILD-file patches and the naja_cc_library and
  -iquote include wrappers.
- Retire //:deps, which only existed to hand cmake-built install trees to
  the CMake flow.
- Depend on BCR modules (onetbb, spdlog, yaml-cpp, googletest,
  rules_python, ...) and on naja's own targets instead of an aggregate
  @naja library.
- bazel/registry/: a file registry in BCR's layout for what is not on
  BCR yet (kissat 4.0.4, cadical 3.0.0, glucose 4.2.1 at upstream
  master, naja, and naja's naja-if, naja-verilog, sv-lang and bison
  entries), listed ahead of BCR in .bazelrc. Publishing a module is
  copying its directory into a BCR pull request.
- Embedded Python is the rules_python hermetic runtime; the driver finds
  it in runfiles, and the release tarball bundles it.
- .bcr/ templates for publish-to-bcr.
- llvm 0.8.24; tests with their own main() use gtest, not gtest_main.

CI installs no host packages for Bazel. CMake and the thirdparty/
submodules are unchanged.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@codecov

codecov Bot commented Oct 2, 2026

Copy link
Copy Markdown

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!

So agents (and people) keep the Bazel build BCR-ready: what may go in
MODULE.bazel, how the in-tree registry relates to naja's, how to publish
to BCR, and the toolchain, linking and embedded-Python traps already hit
once.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@oharboe oharboe changed the title bazel: plain bazel_deps via an in-tree registry, no cmake bazel: plain bazel_deps via an in-tree registry Oct 3, 2026
oharboe and others added 4 commits October 3, 2026 10:27
…orms

- .bcr/metadata.template.json lists xtofalex and nanocoh as the
  kepler-formal module's BCR maintainers.
- overlay/MODULE.bazel files are copies, not symlinks: BCR rejects
  symlinks in registry entries. Contents (and source.json) unchanged.
- kissat, cadical, glucose presubmit: debian13, ubuntu2204, ubuntu2404,
  macos_arm64 on Bazel 8.x and 9.x (debian11 is past end of life).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Synced from naja's registry: naja-if and naja-verilog list xtofalex and
nanocoh as BCR maintainers, and presubmit on debian13, ubuntu2204,
ubuntu2404 and macos_arm64 with Bazel 8.x and 9.x. CLAUDE.md notes the
maintainers and that registry entries hold no symlinks.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Synced from naja's registry. naja still asks for bcr.10, which the
hermetic llvm toolchain needs, and the highest version wins.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
bison, sv-lang, naja-if, naja-verilog, kissat, cadical and glucose are
submitted to BCR, one pull request each (bazelbuild/
bazel-central-registry#10879-#10885). .bazelrc (and the consumer test's)
lists each PR's commit as a registry ahead of BCR; drop a line as its PR
merges. bazel/registry/ keeps only naja's development pin, bumped to
naja#457's current head merged with #455 (d298a369), which takes
sv-lang 11.0.0-20260701-b60d729d.bcr.1.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@oharboe

oharboe commented Oct 3, 2026

Copy link
Copy Markdown
Contributor Author

@nanocoh @xtofalex Ready to merge when CI goes green

@nanocoh
nanocoh merged commit 90ac044 into keplertech:main Oct 3, 2026
209 checks passed
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.

2 participants