diff --git a/.bazelignore b/.bazelignore index 1a38d0ff..62b41430 100644 --- a/.bazelignore +++ b/.bazelignore @@ -1,2 +1,4 @@ thirdparty -deps +bazel/registry +# A separate workspace, built from its own directory. +.github/consumer-test diff --git a/.bazelrc b/.bazelrc index 960b5c99..46313ff0 100644 --- a/.bazelrc +++ b/.bazelrc @@ -1,3 +1,24 @@ +# naja's development pin comes from bazel/registry/ (until naja is on +# BCR); versions not on BCR yet come from their open BCR pull requests, +# each pinned to a commit (drop a line once its PR merges); everything +# else from BCR. +common --registry=file://%workspace%/bazel/registry +# bison 3.8.2.bcr.10 bazelbuild/bazel-central-registry#10879 +# sv-lang 11.0.0-20260701-b60d729d.bcr.1 bazelbuild/bazel-central-registry#10882 +# naja-if 0.0.0-20260723-099677d9 bazelbuild/bazel-central-registry#10881 +# naja-verilog 0.0.0-20260909-be6544b1 bazelbuild/bazel-central-registry#10885 +# kissat 4.0.4 bazelbuild/bazel-central-registry#10880 +# cadical 3.0.0 bazelbuild/bazel-central-registry#10883 +# glucose 4.2.1-20251230-674dbba bazelbuild/bazel-central-registry#10884 +common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/bb42d7dc14939aaf578926cf1c93bd987ca9fac7/ +common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/5888fdb942da7cf4a6eecd8d5bc07c777e82c4ee/ +common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/377d10e631e9461794687b9ff1d4bbbde0c9ad1d/ +common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/649d563703219943c013c9e5af8884ea81b2ab19/ +common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/985ff91136fd9c24be49d268c8f8acb416137a01/ +common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/cf30c24de5255b58a523064f8a624848b4bd1bab/ +common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/0dc1d20b35db8595fbaaf762dbf5046fb19ae188/ +common --registry=https://bcr.bazel.build/ + common --enable_platform_specific_config build --cxxopt=-std=c++20 @@ -10,10 +31,5 @@ build --workspace_status_command=tools/workspace_status.sh common:linux --repo_env=BAZEL_DO_NOT_DETECT_CPP_TOOLCHAIN=1 build:linux --dynamic_mode=off -# Force C11 for host tools to work around rules_foreign_cc pkg-config -# bootstrap failure: bundled glib uses 'bool' as a struct field name, -# which is a keyword in GCC 15's default C23 mode. -build --host_conlyopt=-std=c11 - # Recommended: show test output on failure test --test_output=errors diff --git a/.bcr/metadata.template.json b/.bcr/metadata.template.json new file mode 100644 index 00000000..e995a076 --- /dev/null +++ b/.bcr/metadata.template.json @@ -0,0 +1,20 @@ +{ + "homepage": "https://github.com/keplertech/kepler-formal", + "maintainers": [ + { + "github": "xtofalex", + "github_user_id": 3635601, + "name": "Christophe Alexandre" + }, + { + "github": "nanocoh", + "github_user_id": 115838389, + "name": "Noam Cohen" + } + ], + "repository": [ + "github:keplertech/kepler-formal" + ], + "versions": [], + "yanked_versions": {} +} diff --git a/.bcr/presubmit.yml b/.bcr/presubmit.yml new file mode 100644 index 00000000..31eb6ada --- /dev/null +++ b/.bcr/presubmit.yml @@ -0,0 +1,12 @@ +matrix: + platform: ["ubuntu2204", "ubuntu2404"] + bazel: ["8.x"] +tasks: + verify_targets: + name: Verify build targets + platform: ${{ platform }} + bazel: ${{ bazel }} + build_flags: + - "--cxxopt=-std=c++20" + build_targets: + - "@kepler-formal//src/bin:kepler-formal" diff --git a/.bcr/source.template.json b/.bcr/source.template.json new file mode 100644 index 00000000..a3bd62f1 --- /dev/null +++ b/.bcr/source.template.json @@ -0,0 +1,5 @@ +{ + "integrity": "", + "strip_prefix": "{REPO}-{VERSION}", + "url": "https://github.com/{OWNER}/{REPO}/archive/refs/tags/{TAG}.tar.gz" +} diff --git a/.github/consumer-test/.bazelrc b/.github/consumer-test/.bazelrc index ac751990..8e4753e7 100644 --- a/.github/consumer-test/.bazelrc +++ b/.github/consumer-test/.bazelrc @@ -1,10 +1,29 @@ +# Same registries as kepler-formal's .bazelrc. A consumer outside this +# repository lists kepler-formal's bazel/registry/ by URL instead, see +# bazel/registry/README.md. +common --registry=file://%workspace%/../../bazel/registry +# bison 3.8.2.bcr.10 bazelbuild/bazel-central-registry#10879 +# sv-lang 11.0.0-20260701-b60d729d.bcr.1 bazelbuild/bazel-central-registry#10882 +# naja-if 0.0.0-20260723-099677d9 bazelbuild/bazel-central-registry#10881 +# naja-verilog 0.0.0-20260909-be6544b1 bazelbuild/bazel-central-registry#10885 +# kissat 4.0.4 bazelbuild/bazel-central-registry#10880 +# cadical 3.0.0 bazelbuild/bazel-central-registry#10883 +# glucose 4.2.1-20251230-674dbba bazelbuild/bazel-central-registry#10884 +common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/bb42d7dc14939aaf578926cf1c93bd987ca9fac7/ +common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/5888fdb942da7cf4a6eecd8d5bc07c777e82c4ee/ +common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/377d10e631e9461794687b9ff1d4bbbde0c9ad1d/ +common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/649d563703219943c013c9e5af8884ea81b2ab19/ +common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/985ff91136fd9c24be49d268c8f8acb416137a01/ +common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/cf30c24de5255b58a523064f8a624848b4bd1bab/ +common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/0dc1d20b35db8595fbaaf762dbf5046fb19ae188/ +common --registry=https://bcr.bazel.build/ + common --enable_platform_specific_config build --cxxopt=-std=c++20 build --host_cxxopt=-std=c++20 -# Same guards as the root .bazelrc: the hermetic toolchain must win -# resolution, and host tools stay on C11 for the rules_foreign_cc -# pkg-config bootstrap. +# Same guard as the root .bazelrc: the hermetic toolchain must win +# resolution. common:linux --repo_env=BAZEL_DO_NOT_DETECT_CPP_TOOLCHAIN=1 -build --host_conlyopt=-std=c11 +build:linux --dynamic_mode=off diff --git a/.github/consumer-test/MODULE.bazel b/.github/consumer-test/MODULE.bazel index fab1e006..92e0e4a4 100644 --- a/.github/consumer-test/MODULE.bazel +++ b/.github/consumer-test/MODULE.bazel @@ -1,10 +1,12 @@ # Minimal downstream consumer of kepler-formal. # -# Builds the checker exactly the way an external module does: bazel_dep + -# override, no dev_dependencies. This catches breakage that is invisible -# when this repo is the root module, e.g. paths spelled with root-module -# canonical repo names (the repo mapping renames extension repos in a -# consumer context). +# Builds the checker exactly the way an external module does: a plain +# bazel_dep, no dev_dependencies. This catches breakage that is invisible +# when this repo is the root module, e.g. labels that only resolve from +# the root module's repo mapping. +# +# kepler-formal's own registry (bazel/registry) supplies the modules that +# are not on BCR yet; see .bazelrc. # # The root module's hermetic-llvm toolchain *registration* is a # dev_dependency and does not propagate; the toolchain repo itself does. @@ -26,11 +28,3 @@ llvm_toolchains = use_extension("@llvm//extensions:toolchain.bzl", "toolchain") use_repo(llvm_toolchains, "llvm_toolchains") register_toolchains("@llvm_toolchains//:all") - -bazel_dep(name = "rules_foreign_cc", version = "0.15.1") - -register_toolchains( - "@rules_foreign_cc//toolchains:preinstalled_cmake_toolchain", - "@rules_foreign_cc//toolchains:preinstalled_make_toolchain", - "@rules_foreign_cc//toolchains:preinstalled_pkgconfig_toolchain", -) diff --git a/.github/workflows/bazel.yml b/.github/workflows/bazel.yml index fa80fc0f..ba2855f2 100644 --- a/.github/workflows/bazel.yml +++ b/.github/workflows/bazel.yml @@ -13,30 +13,18 @@ jobs: steps: - uses: actions/checkout@v4 - # No submodules needed — Bazel fetches deps via http_archive + # No submodules needed — every dependency is a bazel_dep - name: Cache Bazel outputs uses: actions/cache@v4 with: path: ~/.cache/bazel - key: bazel-${{ runner.os }}-${{ hashFiles('MODULE.bazel', 'bazel/deps.bzl', 'bazel/*.BUILD.bazel') }} + key: bazel-${{ runner.os }}-${{ hashFiles('MODULE.bazel', 'bazel/registry/**') }} restore-keys: | bazel-${{ runner.os }}- - - name: Install system dependencies - run: | - sudo apt-get update - sudo apt-get install -yq \ - build-essential pkg-config \ - bison flex python3-dev - - name: Build kepler-formal run: bazelisk build //src/bin:kepler-formal - - name: Dump rules_foreign_cc CMake log on failure - if: failure() - run: | - find bazel-out -type f -name CMake.log -print -exec sed -n '1,260p' {} \; || true - - name: Run tests run: bazelisk test //test/... diff --git a/.github/workflows/consumer.yml b/.github/workflows/consumer.yml index 2d9b2eda..88f258e3 100644 --- a/.github/workflows/consumer.yml +++ b/.github/workflows/consumer.yml @@ -24,22 +24,11 @@ jobs: uses: actions/cache@v4 with: path: ~/.cache/bazel - key: bazel-consumer-${{ runner.os }}-${{ hashFiles('MODULE.bazel', 'bazel/deps.bzl', 'bazel/*.BUILD.bazel') }} + key: bazel-consumer-${{ runner.os }}-${{ hashFiles('MODULE.bazel', 'bazel/registry/**') }} restore-keys: | bazel-consumer-${{ runner.os }}- - - name: Install system dependencies - run: | - sudo apt-get update - sudo apt-get install -yq \ - build-essential pkg-config \ - bison flex python3-dev - - name: Build kepler-formal as a dependency working-directory: .github/consumer-test run: bazelisk build @kepler-formal//src/bin:kepler-formal - - name: Dump rules_foreign_cc CMake log on failure - if: failure() - run: | - find .github/consumer-test/bazel-out -type f -name CMake.log -print -exec sed -n '1,260p' {} \; || true diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 056a0cde..f2609914 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -26,17 +26,10 @@ jobs: uses: actions/cache@v4 with: path: ~/.cache/bazel - key: bazel-release-${{ runner.os }}-${{ hashFiles('MODULE.bazel', 'bazel/deps.bzl', 'bazel/*.BUILD.bazel') }} + key: bazel-release-${{ runner.os }}-${{ hashFiles('MODULE.bazel', 'bazel/registry/**') }} restore-keys: | bazel-release-${{ runner.os }}- - - name: Install system dependencies - run: | - sudo apt-get update - sudo apt-get install -yq \ - build-essential pkg-config \ - bison flex python3-dev - - name: Build (optimized) run: bazelisk build -c opt //src/bin:kepler-formal @@ -61,18 +54,19 @@ jobs: exit 1 fi - # Bundle TBB (no static libs by design) from the hermetic Bazel - # build — the exact libraries the binary and naja .so files link. - for lib in libtbb.so.12 libtbbmalloc.so.2; do - find -L bazel-bin/ -name "${lib}" -print -quit | xargs -I{} cp -L {} "${DIST}/lib/" - test -f "${DIST}/lib/${lib}" || { echo "missing bundled ${lib}"; exit 1; } - done + # Bundle the hermetic Python runtime the binary embeds (libpython + # and its stdlib) from the binary's runfiles. + PY_RUNTIME=$(find -L bazel-bin/src/bin/kepler-formal.runfiles -maxdepth 1 -name 'rules_python++python+python_3_*' -print -quit) + test -n "${PY_RUNTIME}" || { echo "missing bundled Python runtime"; exit 1; } + cp -RL "${PY_RUNTIME}" "${DIST}/python" - # Create wrapper script that sets LD_LIBRARY_PATH for bundled libs + # Create wrapper script that points the binary at the bundled libs + # and Python runtime. printf '%s\n' \ '#!/usr/bin/env bash' \ 'SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"' \ - 'export LD_LIBRARY_PATH="${SCRIPT_DIR}/lib${LD_LIBRARY_PATH:+:$LD_LIBRARY_PATH}"' \ + 'export LD_LIBRARY_PATH="${SCRIPT_DIR}/lib:${SCRIPT_DIR}/python/lib${LD_LIBRARY_PATH:+:$LD_LIBRARY_PATH}"' \ + 'export PYTHONHOME="${PYTHONHOME:-${SCRIPT_DIR}/python}"' \ 'exec "${SCRIPT_DIR}/bin/kepler-formal" "$@"' \ > "${DIST}/kepler-formal" chmod +x "${DIST}/kepler-formal" diff --git a/.gitignore b/.gitignore index 4ea177a9..5009b16a 100644 --- a/.gitignore +++ b/.gitignore @@ -8,9 +8,6 @@ bazel-* MODULE.bazel.lock .vscode/ -# bazel run //:deps output (hermetic CMake-flow dependencies) -/deps/ - # Optional Python MCP add-on __pycache__/ *.py[cod] diff --git a/.reuse/dep5 b/.reuse/dep5 index d8b216e4..79f19904 100644 --- a/.reuse/dep5 +++ b/.reuse/dep5 @@ -7,7 +7,7 @@ Files: src/* Copyright: 2025 keplertech.io License: Apache-2.0 -Files: examples/* .github/workflows/* .github/consumer-test/* .gitmodules README.md docs/* +Files: examples/* .github/workflows/* .github/consumer-test/* .bcr/* .gitmodules README.md docs/* Copyright: 2025 keplertech.io License: Apache-2.0 @@ -15,7 +15,7 @@ Files: test/* Copyright: 2025 keplertech.io License: Apache-2.0 -Files: BUILD.bazel MODULE.bazel .bazelrc .bazelversion .bazelignore .gitignore +Files: BUILD.bazel MODULE.bazel .bazelrc .bazelversion .bazelignore .gitignore CLAUDE.md AGENTS.md Copyright: 2025 keplertech.io License: Apache-2.0 diff --git a/AGENTS.md b/AGENTS.md new file mode 120000 index 00000000..681311eb --- /dev/null +++ b/AGENTS.md @@ -0,0 +1 @@ +CLAUDE.md \ No newline at end of file diff --git a/BUILD.bazel b/BUILD.bazel index 8b7386e9..a4919d7f 100644 --- a/BUILD.bazel +++ b/BUILD.bazel @@ -1,97 +1,6 @@ # Root BUILD file for kepler-formal -load("//bazel:collect_headers.bzl", "collect_headers") -load("//bazel:toolchain_cmake.bzl", "toolchain_cmake") - -# Full cmake install prefixes (bin/ include/ lib/ lib/cmake/) of the -# hermetic dependency builds, for //:deps export. -filegroup( - name = "capnproto_install", - srcs = ["@capnproto"], - output_group = "gen_dir", -) - -filegroup( - name = "onetbb_install", - srcs = ["@onetbb"], - output_group = "gen_dir", -) - -# Export the hermetic dependency install trees into /deps/ so the -# plain CMake flow needs no system-installed libraries (opt-in): -# -# bazelisk run //:deps -# cmake -B build -DCMAKE_TOOLCHAIN_FILE=$PWD/deps/toolchain.cmake -sh_binary( - name = "deps", - srcs = ["//bazel:export_deps.sh"], - args = [ - "$(rootpath :capnproto_install)", - "$(rootpath :onetbb_install)", - "$(rootpath @boost_headers//:version_hdr)", - "$(rootpath @flex_src//:flexlexer_hdr)", - ] + select({ - # macOS keeps the host toolchain: deps/toolchain.cmake stays - # dependency-resolution-only, no compiler export. - "@platforms//os:macos": ["NONE"], - "//conditions:default": ["$(rootpath :toolchain_fragment_file)"], - }) + [ - "$(rootpaths @zlib//:z)", - "$(rootpaths :zlib_headers)", - ] + select({ - "@platforms//os:macos": [], - "//conditions:default": [ - "$(rootpath @llvm//runtimes/libcxx:libcxx.static)", - "$(rootpath @llvm//runtimes/libcxx:libcxxabi.static)", - "$(rootpath @llvm//runtimes/libunwind:libunwind.static)", - ], - }), - data = [ - ":capnproto_install", - ":onetbb_install", - ":zlib_headers", - "@boost_headers//:headers", - "@boost_headers//:version_hdr", - "@flex_src//:flexlexer_hdr", - "@zlib//:z", - ] + select({ - "@platforms//os:macos": [], - "//conditions:default": [ - ":toolchain_fragment", - ":toolchain_fragment_file", - # Materializes the compiler, resource dir, hermetic glibc/ - # kernel headers, CRT objects and runtime archives in runfiles - # for export into deps/llvm/. - "@bazel_tools//tools/cpp:current_cc_toolchain", - "@llvm//runtimes/libcxx:libcxx.static", - "@llvm//runtimes/libcxx:libcxxabi.static", - "@llvm//runtimes/libunwind:libunwind.static", - ], - }), -) - -toolchain_cmake( - name = "toolchain_fragment", -) - -# Single-file view for $(rootpath); the sh_binary derives the wrapper -# script paths as siblings of the fragment. -filegroup( - name = "toolchain_fragment_file", - srcs = [":toolchain_fragment"], - output_group = "fragment", -) - -# zlib's public headers are not visible as source targets in the BCR repo; -# collect them from CcInfo instead. -collect_headers( - name = "zlib_headers", - basenames = [ - "zconf.h", - "zlib.h", - ], - deps = ["@zlib//:z"], -) +load("@rules_shell//shell:sh_binary.bzl", "sh_binary") sh_binary( name = "release", diff --git a/CLAUDE.md b/CLAUDE.md new file mode 100644 index 00000000..99b6a76d --- /dev/null +++ b/CLAUDE.md @@ -0,0 +1,86 @@ +# kepler-formal — Agent Guide + +Guidance for AI coding agents (Claude Code reads this as `CLAUDE.md`; +Codex reads it as `AGENTS.md` via symlink) working in this repository. + +## Build systems + +CMake (`CMakeLists.txt`, `thirdparty/` git submodules) and Bazel +(`MODULE.bazel`, `BUILD.bazel` files) are independent. The Bazel build +does not use the submodules, and Bazel changes must not touch the CMake +flow. + +## Bazel: a BCR-ready module + +kepler-formal's Bazel build is meant to be published to the Bazel Central +Registry (BCR) and consumed by other modules (e.g. bazel-orfs) with a +plain `bazel_dep`. Keep it that way. Invariants: + +- `MODULE.bazel` contains only `bazel_dep`s, plus the hermetic-llvm + toolchain setup, whose registration is a `dev_dependency`. No + `http_archive`, `git_override`, `archive_override`, module extensions + or repository rules of our own; overrides are ignored for non-root + modules, so they would only hide breakage that consumers then hit. +- Nothing runs cmake/make inside Bazel (no `rules_foreign_cc`), and + nothing is found on the host (`PATH`, pkg-config, system headers or + libraries). CI installs no packages for Bazel. +- Depend on naja's own targets (`@naja//src/dnl:naja_dnl`, …). If naja + (or any dependency) needs a fix, fix it there — in naja itself or in + its registry entry — never by patching its BUILD files from here. +- Load every rule (`@rules_cc//cc:cc_library.bzl`, + `@rules_shell//shell:sh_test.bzl`, …); Bazel 9 has no native ones. + +**Where dependencies come from.** Everything comes from BCR. A module +version not on BCR yet comes from its open bazel-central-registry pull +request (one module per PR): `.bazelrc` lists the PR's commit +(`https://raw.githubusercontent.com//bazel-central-registry//`) +ahead of BCR, and Bazel takes each `name@version` from the first +registry that has it. Drop the line once the PR merges; when a PR needs +a fix, push a new commit (no force-push, pinned commits must stay +reachable) and move the pin. The one exception is naja's development +pin (#457 + #455 merged, `oharboe/naja@kepler-pin`), served from the +in-tree `bazel/registry/` until naja is released and on BCR; bump it with +`bazel/registry/update_source.py naja []`. +Unreleased commits use `--` versions. Never +change a version's contents once something depends on it; add a new +version. + +To try a local naja checkout without touching the registry: +`bazel test //... --override_module=naja=`. Don't commit such +overrides. + +**Publishing to BCR**: one module per bazel-central-registry pull +request, each based on BCR main, so each goes in on its own. Then naja +(publish-to-bcr from a naja release), then kepler-formal itself through +the publish-to-bcr app (`.bcr/` templates; maintainers: xtofalex, +nanocoh). BCR rejects symlinks in entries, so `overlay/MODULE.bazel` is a +copy. See `docs/bcr-roadmap.md`. + +**Known traps** (each already fixed; don't reintroduce): + +- The hermetic-llvm toolchain passes libc headers as early `-isystem` + flags; libraries whose headers must shadow libc's need `-I` (see the + registry's bison). It also exposes headers that a host-toolchain build + silently takes from `/usr/include`. +- `kepler-formal` links naja's `naja_runtime` as a `cc_shared_library` + (`dynamic_deps`), shared with the `naja.so` Python module. Anything it + links that the binary also uses must be exported by `naja_runtime` + (TBB, zlib), and linker inputs must be owned by targets the + `cc_shared_library` graph aspect can see — naja's `python_libs` exists + for libpython. +- The embedded Python is rules_python's hermetic runtime. Its compiled-in + prefix does not exist at run time: `src/bin/CppDriver.cpp` points + `PYTHONHOME` at the runtime in runfiles (Bazel builds only), and the + release tarball bundles it and sets `PYTHONHOME` in its wrapper. +- `.github/consumer-test` is a separate workspace (in `.bazelignore`) + that builds kepler-formal as a dependency, on the newest Bazel. Run it + for any change to `MODULE.bazel`, the registry, or labels that cross + repositories. + +## Build & test + +```bash +bazelisk build //src/bin:kepler-formal +bazelisk test //... +(cd .github/consumer-test && bazelisk build @kepler-formal//src/bin:kepler-formal) +``` diff --git a/MODULE.bazel b/MODULE.bazel index 6a050627..6cf3fd13 100644 --- a/MODULE.bazel +++ b/MODULE.bazel @@ -1,26 +1,31 @@ +"""kepler-formal: formal equivalence checking on naja netlists. + +Every dependency is a plain bazel_dep. Versions that are not on the +Bazel Central Registry yet come from their open BCR pull requests, and +naja's development pin from bazel/registry/; .bazelrc lists both ahead +of BCR. See docs/bcr-roadmap.md. +""" + module( name = "kepler-formal", # Keep in sync with KEPLER_VERSION in src/bin/KeplerVersion.h.in. version = "0.5.0", + bazel_compatibility = [">=8.0.0"], ) -# Infrastructure -bazel_dep(name = "rules_cc", version = "0.2.20") -bazel_dep(name = "rules_foreign_cc", version = "0.15.1") +bazel_dep(name = "cadical", version = "3.0.0") +bazel_dep(name = "glucose", version = "4.2.1-20251230-674dbba") +bazel_dep(name = "kissat", version = "4.0.4") +bazel_dep(name = "naja", version = "0.7.26-20261003-d298a369") +bazel_dep(name = "onetbb", version = "2023.1.0") bazel_dep(name = "platforms", version = "1.1.0") -bazel_dep(name = "bazel_skylib", version = "1.9.0") - -# Direct dependencies from BCR -bazel_dep(name = "yaml-cpp", version = "0.9.0") -bazel_dep(name = "googletest", version = "1.17.0.bcr.2", dev_dependency = True) -bazel_dep(name = "capnp-cpp", version = "1.4.0") -bazel_dep(name = "zlib", version = "1.3.2") -bazel_dep(name = "fmt", version = "12.2.0") +bazel_dep(name = "rules_cc", version = "0.2.25") +bazel_dep(name = "rules_python", version = "1.9.0") +bazel_dep(name = "rules_shell", version = "0.8.0") bazel_dep(name = "spdlog", version = "1.17.0") -# TBB comes from the cmake-built @onetbb repo (bazel/deps.bzl), not the BCR -# onetbb module: Naja's native targets and the kepler-formal binary must -# share a single libtbb.so.12 runtime. The same install tree is exported -# for the plain CMake flow by //:deps. +bazel_dep(name = "yaml-cpp", version = "0.9.0.bcr.1") + +bazel_dep(name = "googletest", version = "1.18.0.bcr.1", dev_dependency = True) # Hermetic zero-sysroot LLVM toolchain (hermetic-llvm): statically linked # clang 22, libc++ linked statically by default, glibc 2.28 floor. No host @@ -31,13 +36,11 @@ bazel_dep(name = "spdlog", version = "1.17.0") # kepler-formal is the root module (its own builds and CI). register_toolchains # from a dependency is global: a module that depends on kepler-formal would # otherwise inherit this toolchain and have its own C++ toolchain selection -# silently replaced. The extension usage itself stays non-dev (its -# extension_metadata reports non-dev root deps, which Bazel rejects if the only -# usage is dev); the guard on register_toolchains is what keeps the toolchain -# out of consumers. The llvm module stays a normal dependency because the binary -# links its static libc++/libc++abi/libunwind archives (see -# //bazel:hermetic_cxx_runtime). -bazel_dep(name = "llvm", version = "0.8.11") +# silently replaced. A consumer that wants the same toolchain registers it +# itself, as .github/consumer-test does. The extension usage itself stays +# non-dev: its extension_metadata reports non-dev root deps, which Bazel +# rejects if the only usage is dev. +bazel_dep(name = "llvm", version = "0.8.24") llvm_toolchains = use_extension("@llvm//extensions:toolchain.bzl", "toolchain") llvm_toolchains.exec( @@ -54,42 +57,3 @@ register_toolchains( "@llvm_toolchains//:all", dev_dependency = True, ) - -# Use preinstalled cmake/make/pkg-config instead of bootstrapping. -# The bundled glib in rules_foreign_cc pkg-config bootstrap fails -# with modern GCC 15 (C23 bool keyword collision in glib source). -register_toolchains( - "@rules_foreign_cc//toolchains:preinstalled_cmake_toolchain", - "@rules_foreign_cc//toolchains:preinstalled_make_toolchain", - "@rules_foreign_cc//toolchains:preinstalled_pkgconfig_toolchain", -) - -# Third-party dependencies fetched via http_archive for BCR compatibility. -# BUILD file overlays live in bazel/*.BUILD.bazel. -# The cmake flow uses git submodules (thirdparty/) directly. -# See docs/bcr-roadmap.md for the full BCR publication plan. -deps = use_extension("//bazel:deps.bzl", "deps") -use_repo( - deps, - "bison_tool", - "boost", - "boost_headers", - "cadical", - "capnproto", - "flex_headers", - "flex_src", - "flex_tool", - "glucose", - "kissat", - "m4_tool", - "naja", - "naja-if", - "naja-verilog", - "naja_git_version", - "onetbb", - "python", - "slang", - "slang_host_prefixes", - "tbb", - "tomlplusplus", -) diff --git a/README.md b/README.md index 81988786..e75f0750 100644 --- a/README.md +++ b/README.md @@ -109,23 +109,20 @@ cmake .. \ -DCMAKE_EXE_LINKER_FLAGS="-flto" ``` -### Bazel (experimental) +### Bazel -On Ubuntu, install the required host tools: - -```bash -sudo apt-get install build-essential pkg-config bison flex python3-dev -``` - -Build and test with Bazelisk: +The Bazel build needs no host packages on Linux (hermetic clang +toolchain; every library and code generator is a Bazel module) and does +not use the `thirdparty/` submodules: ```bash bazelisk build //src/bin:kepler-formal -bazelisk test //test/... +bazelisk test //... ``` -Additional notes and the BCR publication roadmap are tracked in -[docs/bcr-roadmap.md](docs/bcr-roadmap.md). +Dependencies, where modules not yet on the Bazel Central Registry come +from, and how to depend on kepler-formal from another Bazel +module are described in [docs/bcr-roadmap.md](docs/bcr-roadmap.md). ## Usage diff --git a/bazel/BUILD.bazel b/bazel/BUILD.bazel index 57f2d876..9c7967c4 100644 --- a/bazel/BUILD.bazel +++ b/bazel/BUILD.bazel @@ -1,59 +1 @@ -# Package marker for bazel/ overlay directory - -exports_files([ - "export_deps.sh", - "naja_cc_library.bzl", - "naja_ff_scan.patch", - "naja_verilog_bazel9.patch", -]) - -load("@bazel_skylib//rules:common_settings.bzl", "bool_flag") -load("@rules_cc//cc:cc_import.bzl", "cc_import") -load("@rules_cc//cc:cc_library.bzl", "cc_library") - -# When kepler-formal is the root module its hermetic clang toolchain compiles -# the rules_foreign_cc CMake deps (Cap'n Proto, oneTBB, and Slang), so those -# builds must link the hermetic static libc++/libc++abi/libunwind archives. A -# downstream consumer that builds kepler-formal's deps with its own toolchain -# must not get those archives. Consumers set this flag false. -bool_flag( - name = "hermetic_cxx_runtime_enabled", - build_setting_default = True, -) - -config_setting( - name = "hermetic_runtime", - constraint_values = ["@platforms//os:linux"], - flag_values = {":hermetic_cxx_runtime_enabled": "True"}, - visibility = ["//visibility:public"], -) - -# The hermetic-llvm toolchain passes libc++/libc++abi/libunwind to linker -# actions as Bazel link inputs; its -L "library search directories" contain -# deliberate empty stubs so a stray -lc++ is a no-op. CMake builds under -# rules_foreign_cc never see the real archives, so re-export them here and -# let the CMake overlays link them by explicit $EXT_BUILD_DEPS path. -cc_import( - name = "hermetic_libcxx", - static_library = "@llvm//runtimes/libcxx:libcxx.static", -) - -cc_import( - name = "hermetic_libcxxabi", - static_library = "@llvm//runtimes/libcxx:libcxxabi.static", -) - -cc_import( - name = "hermetic_libunwind", - static_library = "@llvm//runtimes/libunwind:libunwind.static", -) - -cc_library( - name = "hermetic_cxx_runtime", - visibility = ["//visibility:public"], - deps = [ - ":hermetic_libcxx", - ":hermetic_libcxxabi", - ":hermetic_libunwind", - ], -) +# Package for the .bzl files in this directory. diff --git a/bazel/boost.BUILD.bazel b/bazel/boost.BUILD.bazel deleted file mode 100644 index 73cf9cf8..00000000 --- a/bazel/boost.BUILD.bazel +++ /dev/null @@ -1,27 +0,0 @@ -load("@rules_cc//cc:cc_library.bzl", "cc_library") - -# Header-only boost slice. A single monolithic archive (not BCR boost.* -# modules) keeps one pin serving both naja's cmake build (one -# Boost_INCLUDE_DIR under $EXT_BUILD_DEPS/include) and Bazel compiles of -# naja public headers (boost/intrusive, boost/dynamic_bitset). -cc_library( - name = "boost", - hdrs = glob(["boost/**"]), - includes = ["."], - visibility = ["//visibility:public"], -) - -# Raw header tree for //:deps export into deps/include/boost. -filegroup( - name = "headers", - srcs = glob(["boost/**"]), - visibility = ["//visibility:public"], -) - -# Single-file sentinel so //:deps can locate the boost root without -# expanding ~16k header paths into argv. -filegroup( - name = "version_hdr", - srcs = ["boost/version.hpp"], - visibility = ["//visibility:public"], -) diff --git a/bazel/cadical.BUILD.bazel b/bazel/cadical.BUILD.bazel deleted file mode 100644 index 378c74e7..00000000 --- a/bazel/cadical.BUILD.bazel +++ /dev/null @@ -1,75 +0,0 @@ -load("@rules_cc//cc:cc_library.bzl", "cc_library") - -CADICAL_KITTEN_SYMBOL_PREFIX_COPTS = [ - "-Dcompletely_backtrack_to_root_level=cadical_completely_backtrack_to_root_level", - "-Dcitten_clause_with_id=cadical_citten_clause_with_id", - "-Dcitten_clause_with_id_and_equivalence=cadical_citten_clause_with_id_and_equivalence", - "-Dcitten_clause_with_id_and_exception=cadical_citten_clause_with_id_and_exception", - "-Dkitten_add_prime_implicant=cadical_kitten_add_prime_implicant", - "-Dkitten_assume=cadical_kitten_assume", - "-Dkitten_assume_signed=cadical_kitten_assume_signed", - "-Dkitten_binary=cadical_kitten_binary", - "-Dkitten_clause=cadical_kitten_clause", - "-Dkitten_clause_with_id_and_exception=cadical_kitten_clause_with_id_and_exception", - "-Dkitten_clear=cadical_kitten_clear", - "-Dkitten_compute_clausal_core=cadical_kitten_compute_clausal_core", - "-Dkitten_compute_prime_implicant=cadical_kitten_compute_prime_implicant", - "-Dkitten_current_ticks=cadical_kitten_current_ticks", - "-Dkitten_failed=cadical_kitten_failed", - "-Dkitten_fixed=cadical_kitten_fixed", - "-Dkitten_fixed_signed=cadical_kitten_fixed_signed", - "-Dkitten_flip_and_implicant_for_signed_literal=cadical_kitten_flip_and_implicant_for_signed_literal", - "-Dkitten_flip_literal=cadical_kitten_flip_literal", - "-Dkitten_flip_phases=cadical_kitten_flip_phases", - "-Dkitten_flip_signed_literal=cadical_kitten_flip_signed_literal", - "-Dkitten_init=cadical_kitten_init", - "-Dkitten_no_terminator=cadical_kitten_no_terminator", - "-Dkitten_no_ticks_limit=cadical_kitten_no_ticks_limit", - "-Dkitten_randomize_phases=cadical_kitten_randomize_phases", - "-Dkitten_release=cadical_kitten_release", - "-Dkitten_set_logging=cadical_kitten_set_logging", - "-Dkitten_set_terminator=cadical_kitten_set_terminator", - "-Dkitten_set_ticks_limit=cadical_kitten_set_ticks_limit", - "-Dkitten_shrink_to_clausal_core=cadical_kitten_shrink_to_clausal_core", - "-Dkitten_shuffle_clauses=cadical_kitten_shuffle_clauses", - "-Dkitten_signed_value=cadical_kitten_signed_value", - "-Dkitten_solve=cadical_kitten_solve", - "-Dkitten_status=cadical_kitten_status", - "-Dkitten_trace_core=cadical_kitten_trace_core", - "-Dkitten_track_antecedents=cadical_kitten_track_antecedents", - "-Dkitten_traverse_core_clauses=cadical_kitten_traverse_core_clauses", - "-Dkitten_traverse_core_clauses_with_id=cadical_kitten_traverse_core_clauses_with_id", - "-Dkitten_traverse_core_ids=cadical_kitten_traverse_core_ids", - "-Dkitten_unit=cadical_kitten_unit", - "-Dkitten_value=cadical_kitten_value", - "-Dnew_learned_klause=cadical_new_learned_klause", -] - -cc_library( - name = "cadical", - srcs = glob( - ["src/*.cpp"], - exclude = [ - "src/cadical.cpp", - "src/mobical.cpp", - ], - ) + glob(["src/*.c"]) + [ - "contrib/craigtracer.cpp", - ], - hdrs = glob([ - "src/*.h", - "src/*.hpp", - ]) + glob(["contrib/*.hpp"]), - copts = [ - "-DNBUILD", - "-DNDEBUG", - "-DNTRACING", - "-DQUIET", - "-DNCLOSEFROM", - ] + CADICAL_KITTEN_SYMBOL_PREFIX_COPTS, - includes = [ - "src", - "contrib", - ], - visibility = ["//visibility:public"], -) diff --git a/bazel/capnproto.BUILD.bazel b/bazel/capnproto.BUILD.bazel deleted file mode 100644 index c3c79d5f..00000000 --- a/bazel/capnproto.BUILD.bazel +++ /dev/null @@ -1,64 +0,0 @@ -load("@rules_foreign_cc//foreign_cc:defs.bzl", "cmake") - -filegroup( - name = "all_srcs", - srcs = glob(["**"]), -) - -# Cap'n Proto built once via cmake so that naja's find_package(CapnProto) -# gets a real CMake package (lib/cmake/CapnProto/*.cmake) plus the capnp -# compiler binaries, and the final link gets the same libcapnp.a/libkj.a -# through CcInfo — the schema-compiler and link-time versions can never skew. -CAPNPROTO_CMAKE_CACHE_ENTRIES = { - "BUILD_TESTING": "OFF", - "BUILD_SHARED_LIBS": "OFF", - "CMAKE_BUILD_TYPE": "Release", - # Static archives end up in a PIE binary and in naja test executables. - "CMAKE_POSITION_INDEPENDENT_CODE": "ON", - "WITH_OPENSSL": "OFF", - "WITH_ZLIB": "OFF", -} - -cmake( - name = "capnproto", - cache_entries = select({ - # rules_foreign_cc links executables with the C driver; the host - # (Xcode) toolchain needs the C++ runtime spelled out. The hermetic - # Linux toolchain links its own static libc++ and must not see - # -lstdc++. - "@platforms//os:macos": CAPNPROTO_CMAKE_CACHE_ENTRIES | { - "CMAKE_EXE_LINKER_FLAGS": "-lstdc++ -lm", - }, - # See naja.BUILD.bazel: the hermetic toolchain's C++ runtime - # archives are Bazel link inputs rules_foreign_cc doesn't capture, - # and the -L'd search directories contain deliberate stubs. - "@kepler-formal//bazel:hermetic_runtime": CAPNPROTO_CMAKE_CACHE_ENTRIES | { - "CMAKE_CXX_STANDARD_LIBRARIES": " ".join([ - "$${EXT_BUILD_DEPS}/lib/liblibcxx.static.a", - "$${EXT_BUILD_DEPS}/lib/liblibcxxabi.static.a", - "$${EXT_BUILD_DEPS}/lib/liblibunwind.static.a", - "-lm", - ]), - }, - # Consumer toolchain (hermetic_cxx_runtime_enabled=False): use the - # consumer's own libc++; no hermetic archives. - "//conditions:default": CAPNPROTO_CMAKE_CACHE_ENTRIES, - }), - build_args = ["-j4"], - deps = select({ - "@platforms//os:macos": [], - "@kepler-formal//bazel:hermetic_runtime": ["@kepler-formal//bazel:hermetic_cxx_runtime"], - "//conditions:default": [], - }), - lib_source = ":all_srcs", - out_binaries = [ - "capnp", - "capnpc-c++", - ], - # Link order: capnp before kj. - out_static_libs = [ - "libcapnp.a", - "libkj.a", - ], - visibility = ["//visibility:public"], -) diff --git a/bazel/collect_headers.bzl b/bazel/collect_headers.bzl deleted file mode 100644 index 2376e3b3..00000000 --- a/bazel/collect_headers.bzl +++ /dev/null @@ -1,23 +0,0 @@ -"""Collect public headers of cc_library targets as plain files. - -Used by //:deps to export headers of external cc_library targets (e.g. BCR -zlib) whose header files are not visible as source targets. -""" - -def _collect_headers_impl(ctx): - headers = [] - for dep in ctx.attr.deps: - for hdr in dep[CcInfo].compilation_context.direct_public_headers: - if not ctx.attr.basenames or hdr.basename in ctx.attr.basenames: - headers.append(hdr) - return [DefaultInfo(files = depset(headers))] - -collect_headers = rule( - implementation = _collect_headers_impl, - attrs = { - "basenames": attr.string_list( - doc = "If set, only headers with these basenames are collected.", - ), - "deps": attr.label_list(providers = [CcInfo]), - }, -) diff --git a/bazel/deps.bzl b/bazel/deps.bzl deleted file mode 100644 index ed65439b..00000000 --- a/bazel/deps.bzl +++ /dev/null @@ -1,168 +0,0 @@ -"""Module extension that fetches third-party dependencies via http_archive. - -For BCR compatibility, dependencies are fetched as source archives from -GitHub rather than relying on git submodules. The cmake flow continues -to use submodules directly (thirdparty/). - -When a dependency gains native Bazel support or is published to BCR, -replace the corresponding http_archive with a bazel_dep in MODULE.bazel. -""" - -load("@bazel_tools//tools/build_defs/repo:http.bzl", "http_archive") -load( - "//bazel:naja_repositories.bzl", - "alias_repository", - "host_prefixes_repository", - "naja_version_repository", - "python_repository", - "system_tool_repository", -) - -# Pinned dependency versions. -# To update: change the commit, run `bazel fetch @cadical @glucose @kissat @naja` -# to verify, then update the sha256 hashes. -# Hermetic library dependencies (previously system packages). -# capnproto and oneTBB retain CMake install trees for //:deps; the native -# Naja targets consume BCR capnp-cpp and the same oneTBB CcInfo directly. -# Boost and FlexLexer.h are header-only. -_CAPNPROTO_VERSION = "1.4.0" -_ONETBB_VERSION = "2022.3.0" -_BOOST_VERSION = "1_89_0" -_FLEX_VERSION = "2.6.4" - -_CADICAL_COMMIT = "7b99c07f0bcab5824a5a3ce62c7066554017f641" -_GLUCOSE_COMMIT = "7f887abba7cf13636a5ac2d28653668a20a91b25" -_KISSAT_COMMIT = "8af8e56f174b778aef3aa45af9f739b2a5f492c2" -_NAJA_COMMIT = "6331960cb372ef6d332d07a42fb449d0bea01bbe" -_NAJA_VERILOG_COMMIT = "be6544b128e229ce2aee814e795c1e49b02caf5c" -_NAJA_IF_COMMIT = "099677d9f52c0db11b12c08d03e32543eebc7888" -_SLANG_COMMIT = "b60d729d66b9cdeec158b800f898461a138d505e" -_TOMLPLUSPLUS_COMMIT = "30172438cee64926dc41fdd9c11fb3ba5b2ba9de" - -def _deps_impl(_module_ctx): - http_archive( - name = "capnproto", - url = "https://capnproto.org/capnproto-c++-{}.tar.gz".format(_CAPNPROTO_VERSION), - sha256 = "fa02378ad522b318916b9ad928d1372fc9abd43dd1f4f0392e50450f5c87828f", - strip_prefix = "capnproto-c++-{}".format(_CAPNPROTO_VERSION), - build_file = Label("//bazel:capnproto.BUILD.bazel"), - ) - - http_archive( - name = "onetbb", - url = "https://github.com/uxlfoundation/oneTBB/archive/refs/tags/v{}.tar.gz".format(_ONETBB_VERSION), - sha256 = "01598a46c1162c27253a0de0236f520fd8ee8166e9ebb84a4243574f88e6e50a", - strip_prefix = "oneTBB-{}".format(_ONETBB_VERSION), - build_file = Label("//bazel:onetbb.BUILD.bazel"), - ) - - http_archive( - name = "boost_headers", - url = "https://archives.boost.io/release/{}/source/boost_{}.tar.gz".format(_BOOST_VERSION.replace("_", "."), _BOOST_VERSION), - sha256 = "9de758db755e8330a01d995b0a24d09798048400ac25c03fc5ea9be364b13c93", - strip_prefix = "boost_{}".format(_BOOST_VERSION), - build_file = Label("//bazel:boost.BUILD.bazel"), - ) - - http_archive( - name = "flex_src", - url = "https://github.com/westes/flex/releases/download/v{v}/flex-{v}.tar.gz".format(v = _FLEX_VERSION), - sha256 = "e87aae032bf07c26f85ac0ed3250998c37621d95f8bd748b31f15b33c45ee995", - strip_prefix = "flex-{}".format(_FLEX_VERSION), - build_file = Label("//bazel:flexlexer.BUILD.bazel"), - ) - - http_archive( - name = "cadical", - url = "https://github.com/arminbiere/cadical/archive/{}.tar.gz".format(_CADICAL_COMMIT), - sha256 = "d89bad4091f2203980ab30fdac14be874a4aca9b716cbcc132f5c7283b6fd987", - strip_prefix = "cadical-{}".format(_CADICAL_COMMIT), - build_file = Label("//bazel:cadical.BUILD.bazel"), - ) - - http_archive( - name = "glucose", - url = "https://github.com/audemard/glucose/archive/{}.tar.gz".format(_GLUCOSE_COMMIT), - sha256 = "3033a27047f35653f63559e4f31d664cb8b57a7dcdab9d90233be1d1f52f4eda", - strip_prefix = "glucose-{}".format(_GLUCOSE_COMMIT), - build_file = Label("//bazel:glucose.BUILD.bazel"), - ) - - http_archive( - name = "kissat", - url = "https://github.com/arminbiere/kissat/archive/{}.tar.gz".format(_KISSAT_COMMIT), - sha256 = "9268b6daaf76ea34ea9da503338beddc5539eb783d1a83a37a7af2a028f3b236", - strip_prefix = "kissat-{}".format(_KISSAT_COMMIT), - build_file = Label("//bazel:kissat.BUILD.bazel"), - ) - - alias_repository( - name = "boost", - aliases = {"headers": "@boost_headers//:boost"}, - ) - - alias_repository( - name = "tbb", - aliases = { - "tbb": "@onetbb//:onetbb", - "tbbmalloc": "@onetbb//:onetbb", - }, - ) - - alias_repository( - name = "flex_headers", - aliases = {"headers": "@flex_src//:flexlexer"}, - ) - - system_tool_repository(name = "bison_tool", tool = "bison") - system_tool_repository(name = "flex_tool", tool = "flex") - system_tool_repository(name = "m4_tool", tool = "m4") - python_repository(name = "python") - host_prefixes_repository(name = "slang_host_prefixes") - naja_version_repository(name = "naja_git_version", git_hash = _NAJA_COMMIT[:8]) - - http_archive( - name = "naja-if", - url = "https://github.com/najaeda/naja-if/archive/{}.tar.gz".format(_NAJA_IF_COMMIT), - sha256 = "0a980530cc12a19a7df5702012cb096c0186b96fe93328bfb250415834fadd1a", - strip_prefix = "naja-if-{}".format(_NAJA_IF_COMMIT), - ) - - http_archive( - name = "naja-verilog", - url = "https://github.com/najaeda/naja-verilog/archive/{}.tar.gz".format(_NAJA_VERILOG_COMMIT), - sha256 = "f6fa913e9af19a589fe656bd503f9e1acb1fab11db8a563457513e76113bb003", - strip_prefix = "naja-verilog-{}".format(_NAJA_VERILOG_COMMIT), - patch_args = ["-p0", "-f"], - patches = [Label("//bazel:naja_verilog_bazel9.patch")], - ) - - http_archive( - name = "tomlplusplus", - url = "https://github.com/marzer/tomlplusplus/archive/{}.tar.gz".format(_TOMLPLUSPLUS_COMMIT), - sha256 = "291254ffe7f2433f90deef878d0d9335534a350a958ea23ecf511b7b2277bf7f", - strip_prefix = "tomlplusplus-{}".format(_TOMLPLUSPLUS_COMMIT), - build_file = Label("//bazel:tomlplusplus.BUILD.bazel"), - ) - - http_archive( - name = "slang", - url = "https://github.com/MikePopoloski/slang/archive/{}.tar.gz".format(_SLANG_COMMIT), - sha256 = "a9f65590ccf4ff2083b49f0f4352aac53e6458b04b2f1a65e24814aba3a05bc2", - strip_prefix = "slang-{}".format(_SLANG_COMMIT), - build_file = Label("//bazel:slang.BUILD.bazel"), - ) - - http_archive( - name = "naja", - url = "https://github.com/nanocoh/naja/archive/{}.tar.gz".format(_NAJA_COMMIT), - sha256 = "29fb32c3bb91d777bfd1458b5a90858f4979bc075fd2e79fcac63cf16a97c1b2", - strip_prefix = "naja-{}".format(_NAJA_COMMIT), - build_file = Label("//bazel:naja.BUILD.bazel"), - patch_args = ["-p0", "-f"], - patches = [Label("//bazel:naja_ff_scan.patch")], - ) - -deps = module_extension( - implementation = _deps_impl, -) diff --git a/bazel/export_deps.sh b/bazel/export_deps.sh deleted file mode 100755 index c615ad11..00000000 --- a/bazel/export_deps.sh +++ /dev/null @@ -1,116 +0,0 @@ -#!/usr/bin/env bash -# Export the hermetic dependency install trees into /deps/ so the -# plain CMake flow can build without system-installed libraries: -# -# bazelisk run //:deps -# cmake -B build -DCMAKE_TOOLCHAIN_FILE=$PWD/deps/toolchain.cmake -# -# Strictly opt-in: the CMake-with-system-packages flow is unaffected unless -# the toolchain file is passed. deps/ is git- and bazel-ignored and fully -# regenerated on every run (safe to delete at any time). -set -euo pipefail - -if [[ -z ${BUILD_WORKSPACE_DIRECTORY:-} ]]; then - echo >&2 "error: must be invoked via 'bazel run //:deps'" - exit 1 -fi - -CAPNPROTO_PREFIX=$1 -ONETBB_PREFIX=$2 -BOOST_VERSION_HPP=$3 # sentinel file; boost root is two levels up -FLEXLEXER_H=$4 -TOOLCHAIN_FRAGMENT=$5 # generated compiler settings, or NONE (macOS) -shift 5 # remaining: zlib outputs + headers + hermetic runtime archives - -DEST="${BUILD_WORKSPACE_DIRECTORY}/deps" -STAGE="${DEST}.tmp" -# A stale stage from an interrupted run may carry read-only bits. -[ -d "${STAGE}" ] && chmod -R u+w "${STAGE}" -rm -rf "${STAGE}" -mkdir -p "${STAGE}/include" "${STAGE}/lib" - -# Merge the cmake install prefixes (bin/ include/ lib/ lib/cmake/) into one -# CMake prefix. -L dereferences tree-artifact symlink chains (libtbb.so.12, -# capnpc) so deps/ survives 'bazel clean'. The CapnProto/TBB package configs -# stay valid after copying: they compute _IMPORT_PREFIX relative to their own -# location. -# Preserve mode (execute bits on bin/capnp etc.); bazel outputs are -# read-only, so restore user-write between the merges. -cp -RL --no-preserve=timestamps "${CAPNPROTO_PREFIX}"/. "${STAGE}/" -chmod -R u+w "${STAGE}" -cp -RL --no-preserve=timestamps "${ONETBB_PREFIX}"/. "${STAGE}/" -chmod -R u+w "${STAGE}" - -# Header-only and single-file deps. -cp -RL --no-preserve=mode,timestamps "$(dirname "$(dirname "${BOOST_VERSION_HPP}")")/boost" "${STAGE}/include/boost" -cp -L --no-preserve=mode,timestamps "${FLEXLEXER_H}" "${STAGE}/include/" -# zlib static archive + public headers, and (on Linux) the hermetic C++ -# runtime archives referenced by toolchain.cmake. libz.so is skipped — -# CMake consumers should link the static archive, and a solib copy would -# dangle. -for f in "$@"; do - case "${f}" in - *.a) cp -L --no-preserve=mode,timestamps "${f}" "${STAGE}/lib/" ;; - *.h) cp -L --no-preserve=mode,timestamps "${f}" "${STAGE}/include/" ;; - esac -done - -# Hermetic compiler export: materialize the cc_toolchain's runfiles -# (clang dist, resource dir, hermetic glibc/kernel headers, CRT objects) -# under deps/llvm// — the layout toolchain.cmake's rewritten paths -# expect. cwd is the runfiles _main directory under 'bazel run', so the -# repo directories live one level up. -if [[ ${TOOLCHAIN_FRAGMENT} != NONE ]]; then - mkdir -p "${STAGE}/llvm" - for d in ../llvm+ ../llvm++*; do - [[ -d ${d} ]] || continue - # Keep mode (execute bits on the tools); the stage-wide chmod below - # restores user-write. - cp -RL --no-preserve=timestamps "${d}" "${STAGE}/llvm/$(basename "${d}")" - done - # The clang dist is busybox-style (clang, lld, llvm-ar, ... are all - # symlinks to one ~200MB multi-call binary); dereferencing copies made - # each a full copy. Re-share identical large files via hardlinks. - canonical="" - prev_size="" - while IFS= read -r line; do - size=${line%% *} - f=${line#* } - if [[ ${size} == "${prev_size}" ]] && cmp -s "${canonical}" "${f}"; then - ln -f "${canonical}" "${f}" - else - canonical=${f} - prev_size=${size} - fi - done < <(find "${STAGE}/llvm" -type f -size +10M -printf '%s %p\n' | sort -n) -fi - -# Dependency resolution block; on Linux the hermetic compiler settings -# (generated from the Bazel cc_toolchain) are appended so the CMake flow -# needs no host compiler and is ABI-identical to the Bazel flow. -cat > "${STAGE}/toolchain.cmake" <<'EOF' -# Generated by 'bazel run //:deps' — do not edit. -get_filename_component(_KF_DEPS "${CMAKE_CURRENT_LIST_DIR}" ABSOLUTE) -list(APPEND CMAKE_PREFIX_PATH "${_KF_DEPS}") -set(Boost_INCLUDE_DIR "${_KF_DEPS}/include" CACHE PATH "") -set(FLEX_INCLUDE_DIR "${_KF_DEPS}/include" CACHE PATH "") -set(ZLIB_ROOT "${_KF_DEPS}" CACHE PATH "") -EOF -if [[ ${TOOLCHAIN_FRAGMENT} != NONE ]]; then - cat "${TOOLCHAIN_FRAGMENT}" >> "${STAGE}/toolchain.cmake" - # Compiler wrapper scripts generated alongside the fragment. - for w in hermetic-cc hermetic-cxx; do - cp -L --no-preserve=timestamps "$(dirname "${TOOLCHAIN_FRAGMENT}")/${w}" "${STAGE}/bin/${w}" - chmod +x "${STAGE}/bin/${w}" - done -fi - -# Belt and braces on top of the repo .gitignore/.bazelignore entries. -printf '*\n' > "${STAGE}/.gitignore" - -chmod -R u+w "${STAGE}" -rm -rf "${DEST}" -mv "${STAGE}" "${DEST}" - -echo "Hermetic dependencies exported to ${DEST}" -echo "Use with: cmake -B build -DCMAKE_TOOLCHAIN_FILE=${DEST}/toolchain.cmake" diff --git a/bazel/flexlexer.BUILD.bazel b/bazel/flexlexer.BUILD.bazel deleted file mode 100644 index 7cce1e03..00000000 --- a/bazel/flexlexer.BUILD.bazel +++ /dev/null @@ -1,20 +0,0 @@ -load("@rules_cc//cc:cc_library.bzl", "cc_library") - -# FlexLexer.h only (the flex *binary* stays a host tool). naja-verilog's -# scanner does '#include ' and FindFLEX would otherwise add -# -I/usr/include for it — hoisting the entire host header tree ahead of -# hermetic headers. Pinned to flex 2.6.4 to match the ubuntu/homebrew flex -# that generates the scanner source. -cc_library( - name = "flexlexer", - hdrs = ["src/FlexLexer.h"], - strip_include_prefix = "src", - visibility = ["//visibility:public"], -) - -# For //:deps export into deps/include. -filegroup( - name = "flexlexer_hdr", - srcs = ["src/FlexLexer.h"], - visibility = ["//visibility:public"], -) diff --git a/bazel/glucose.BUILD.bazel b/bazel/glucose.BUILD.bazel deleted file mode 100644 index b8f16818..00000000 --- a/bazel/glucose.BUILD.bazel +++ /dev/null @@ -1,26 +0,0 @@ -load("@rules_cc//cc:cc_library.bzl", "cc_library") - -cc_library( - name = "glucose", - srcs = [ - "core/Solver.cc", - "core/lcm.cc", - "simp/SimpSolver.cc", - "utils/Options.cc", - "utils/System.cc", - ], - hdrs = glob([ - "core/*.h", - "mtl/*.h", - "simp/*.h", - "utils/*.h", - ]), - copts = [ - "-std=c++11", - "-Wno-parentheses", - ], - includes = ["."], - linkopts = ["-lpthread"], - visibility = ["//visibility:public"], - deps = ["@zlib"], -) diff --git a/bazel/kissat.BUILD.bazel b/bazel/kissat.BUILD.bazel deleted file mode 100644 index a18d4737..00000000 --- a/bazel/kissat.BUILD.bazel +++ /dev/null @@ -1,51 +0,0 @@ -load("@rules_cc//cc:cc_library.bzl", "cc_library") - -# Generate build.h with version info (replaces scripts/generate-build-header.sh) -genrule( - name = "build_header", - srcs = ["VERSION"], - outs = ["src/build.h"], - cmd = """ - VERSION=$$(cat $(location VERSION)) - cat > $@ <
++deps+naja — a hardcoded path dangles there, quoted -includes fall through to the transitive system paths, and a host-installed -Naja can be selected instead. -""" - -_NAJA_ROOT = Label("@naja//:BUILD").workspace_root - -_NAJA_QUOTE_INCLUDE_DIRS = [ - "src/dnl", - "src/nl/netlist/core", - "src/nl/netlist/snl", - "src/core", - "src/bne", - "src/metrics", - "src/nl/netlist/decorators", - "src/nl/netlist/pnl", - "src/nl/netlist/visual", - "src/nl/netlist/serialization/capnp", - "src/nl/formats/hdl", - "src/nl/formats/lefdef", - "src/nl/formats/liberty", - "src/nl/formats/systemverilog/frontend", - "src/nl/formats/verilog/backend", - "src/nl/formats/verilog/frontend", - "src/nl/formats/vhdl", - "src/nl/python/pyloader", - "src/optimization", - "thirdparty/yosys-liberty/src", - "thirdparty/lefdef/src/def/def", -] - -NAJA_HEADER_COPTS = [ - # Kepler and Naja's headers require C++20. The root module sets this via - # .bazelrc (--cxxopt=-std=c++20), but that does not reach a downstream - # consumer, so set it on the targets themselves. - "-std=c++20", -] + [ - "-iquote%s/%s" % (_NAJA_ROOT, d) - for d in _NAJA_QUOTE_INCLUDE_DIRS -] diff --git a/bazel/naja_repositories.bzl b/bazel/naja_repositories.bzl deleted file mode 100644 index 6fba75a2..00000000 --- a/bazel/naja_repositories.bzl +++ /dev/null @@ -1,155 +0,0 @@ -"""Repository adapters needed by Naja's native Bazel targets.""" - -def _find_tool(repository_ctx, tool): - for prefix in ["/opt/homebrew/opt", "/usr/local/opt"]: - candidate = repository_ctx.path("{}/{}/bin/{}".format(prefix, tool, tool)) - if candidate.exists: - return candidate - return repository_ctx.which(tool) - -def _alias_repository_impl(repository_ctx): - lines = ["package(default_visibility = [\"//visibility:public\"])", ""] - for name, actual in sorted(repository_ctx.attr.aliases.items()): - lines.extend([ - "alias(", - " name = \"{}\",".format(name), - " actual = \"{}\",".format(actual), - ")", - "", - ]) - repository_ctx.file("BUILD.bazel", "\n".join(lines)) - -alias_repository = repository_rule( - implementation = _alias_repository_impl, - attrs = {"aliases": attr.string_dict(mandatory = True)}, -) - -def _system_tool_repository_impl(repository_ctx): - tool = repository_ctx.attr.tool - found = _find_tool(repository_ctx, tool) - if not found: - fail("{} not found on PATH; required to build Naja".format(tool)) - repository_ctx.symlink(found, tool) - repository_ctx.file( - "BUILD.bazel", - 'exports_files(["{}"], visibility = ["//visibility:public"])\n'.format(tool), - ) - -system_tool_repository = repository_rule( - implementation = _system_tool_repository_impl, - attrs = {"tool": attr.string(mandatory = True)}, - local = True, -) - -def _python_repository_impl(repository_ctx): - python_config = repository_ctx.which("python3-config") - if not python_config: - fail("python3-config not found on PATH; required to build Naja") - - def run(args): - result = repository_ctx.execute([python_config] + args) - if result.return_code != 0: - fail("python3-config {} failed: {}".format(" ".join(args), result.stderr)) - return result.stdout.strip().split(" ") - - include_dirs = [arg[2:] for arg in run(["--includes"]) if arg.startswith("-I")] - if not include_dirs: - fail("python3-config --includes returned no include directories") - for index, include_dir in enumerate(include_dirs): - repository_ctx.symlink(include_dir, "include{}".format(index)) - - # Debian's pyconfig.h forwards to a multiarch include directory that - # python3-config --includes does not report. - python = repository_ctx.which("python3") - if not python: - fail("python3 not found on PATH; required to build Naja") - multiarch_result = repository_ctx.execute([ - python, - "-c", - "import sysconfig; print(sysconfig.get_config_var('MULTIARCH') or '')", - ]) - if multiarch_result.return_code != 0: - fail("python3 sysconfig query failed: {}".format(multiarch_result.stderr)) - - platform_include_roots = [] - multiarch = multiarch_result.stdout.strip() - if multiarch: - for index, include_dir in enumerate(include_dirs): - include_path = repository_ctx.path(include_dir) - platform_root = include_path.dirname.get_child(multiarch) - platform_include = platform_root.get_child(include_path.basename) - if platform_include.exists: - root = "platform_include{}".format(index) - repository_ctx.symlink( - platform_include, - "{}/{}/{}".format(root, multiarch, include_path.basename), - ) - platform_include_roots.append(root) - - ldflags = run(["--ldflags", "--embed"]) - linkopts = [arg for arg in ldflags if arg] - includes = [ - "include{}".format(index) - for index in range(len(include_dirs)) - ] + platform_include_roots - header_globs = [ - "include{}/**/*.h".format(index) - for index in range(len(include_dirs)) - ] + [ - root + "/**/*.h" - for root in platform_include_roots - ] - repository_ctx.file( - "BUILD.bazel", - """\ -load("@rules_cc//cc:cc_library.bzl", "cc_library") - -package(default_visibility = ["//visibility:public"]) - -cc_library( - name = "headers", - hdrs = glob({header_globs}), - includes = {includes}, -) - -cc_library( - name = "embed", - hdrs = glob({header_globs}), - includes = {includes}, - linkopts = {linkopts}, -) -""".format( - header_globs = repr(header_globs), - includes = repr(includes), - linkopts = repr(linkopts), - ), - ) - -python_repository = repository_rule( - implementation = _python_repository_impl, - local = True, -) - -def _host_prefixes_repository_impl(repository_ctx): - repository_ctx.file( - "prefixes.bzl", - 'CMAKE_PREFIX_PATH = ""\n', - ) - repository_ctx.file("BUILD.bazel", "") - -host_prefixes_repository = repository_rule( - implementation = _host_prefixes_repository_impl, - local = True, -) - -def _naja_version_repository_impl(repository_ctx): - repository_ctx.file( - "git_version.bzl", - 'NAJA_GIT_HASH = "{}"\n'.format(repository_ctx.attr.git_hash), - ) - repository_ctx.file("BUILD.bazel", "") - -naja_version_repository = repository_rule( - implementation = _naja_version_repository_impl, - attrs = {"git_hash": attr.string(mandatory = True)}, -) diff --git a/bazel/naja_verilog_bazel9.patch b/bazel/naja_verilog_bazel9.patch deleted file mode 100644 index 079baf83..00000000 --- a/bazel/naja_verilog_bazel9.patch +++ /dev/null @@ -1,11 +0,0 @@ ---- BUILD.bazel -+++ BUILD.bazel -@@ -3,3 +3,7 @@ - # SPDX-License-Identifier: Apache-2.0 -- -+ -+load("@rules_cc//cc:cc_binary.bzl", "cc_binary") -+load("@rules_cc//cc:cc_library.bzl", "cc_library") -+load("@rules_cc//cc:cc_test.bzl", "cc_test") -+ - # Core naja-verilog library and executable targets. diff --git a/bazel/onetbb.BUILD.bazel b/bazel/onetbb.BUILD.bazel deleted file mode 100644 index 7c15172f..00000000 --- a/bazel/onetbb.BUILD.bazel +++ /dev/null @@ -1,64 +0,0 @@ -load("@rules_foreign_cc//foreign_cc:defs.bzl", "cmake") - -filegroup( - name = "all_srcs", - srcs = glob(["**"]), -) - -# oneTBB built via cmake (not the BCR onetbb module) so that naja's -# find_package(TBB) gets TBBConfig.cmake and — crucially — the naja shared -# libraries and the kepler-formal binary share one libtbb.so.12 runtime -# (TBB scheduler singletons; two runtimes in one process is a bug). -# TBB is shared by design (no static libs); bundled in the release tarball. -ONETBB_CMAKE_CACHE_ENTRIES = { - "CMAKE_BUILD_TYPE": "Release", - # Don't let -Werror break builds under newer compilers. - "TBB_STRICT": "OFF", - "TBB_TEST": "OFF", - "TBB_EXAMPLES": "OFF", -} - -cmake( - name = "onetbb", - cache_entries = select({ - "@platforms//os:macos": ONETBB_CMAKE_CACHE_ENTRIES, - # tbbmalloc's linker version script assigns symbols that are only - # defined when ITT is enabled; GNU ld ignores that, ld.lld (the - # hermetic toolchain's linker) errors without --undefined-version. - "@kepler-formal//bazel:hermetic_runtime": ONETBB_CMAKE_CACHE_ENTRIES | { - "CMAKE_SHARED_LINKER_FLAGS": "-Wl,--undefined-version", - # See naja.BUILD.bazel: link the hermetic C++ runtime into the - # shared libraries so their libc++ symbols resolve at load time. - "CMAKE_CXX_STANDARD_LIBRARIES": " ".join([ - "$${EXT_BUILD_DEPS}/lib/liblibcxx.static.a", - "$${EXT_BUILD_DEPS}/lib/liblibcxxabi.static.a", - "$${EXT_BUILD_DEPS}/lib/liblibunwind.static.a", - "-lm", - ]), - }, - # Consumer toolchain (hermetic_cxx_runtime_enabled=False): the consumer's - # own libc++ is used; do not inject the hermetic archives. Keep - # --undefined-version (ld.lld, incl. consumers using lld). - "//conditions:default": ONETBB_CMAKE_CACHE_ENTRIES | { - "CMAKE_SHARED_LINKER_FLAGS": "-Wl,--undefined-version", - }, - }), - deps = select({ - "@platforms//os:macos": [], - "@kepler-formal//bazel:hermetic_runtime": ["@kepler-formal//bazel:hermetic_cxx_runtime"], - "//conditions:default": [], - }), - build_args = ["-j4"], - lib_source = ":all_srcs", - out_shared_libs = select({ - "@platforms//os:macos": [ - "libtbb.12.dylib", - "libtbbmalloc.2.dylib", - ], - "//conditions:default": [ - "libtbb.so.12", - "libtbbmalloc.so.2", - ], - }), - visibility = ["//visibility:public"], -) diff --git a/bazel/registry/README.md b/bazel/registry/README.md new file mode 100644 index 00000000..9b47af78 --- /dev/null +++ b/bazel/registry/README.md @@ -0,0 +1,36 @@ +# In-tree Bazel registry + +This registry holds one module: `naja`, at the development pin +kepler-formal is tested against (najaeda/naja#457 merged with #455, +`oharboe/naja@kepler-pin`), until naja is released and on the +[Bazel Central Registry](https://registry.bazel.build/). Then it goes away. + +Every other module that is not on BCR yet comes from its open +bazel-central-registry pull request; `.bazelrc` lists those by commit, +after this registry and ahead of BCR. + +The layout is BCR's (`modules/naja/metadata.json`, +`modules/naja//{MODULE.bazel,source.json,presubmit.yml,overlay/}`). +`overlay/MODULE.bazel` is a copy of the version's `MODULE.bazel`; BCR +rejects symlinks. + +## Bumping naja + +1. Add `modules/naja//`, versioned `0.7.26--`, + with naja's `MODULE.bazel` at that commit (its `module(version = ...)` + set to the directory name), copied to `overlay/MODULE.bazel`. +2. Put the version in `modules/naja/metadata.json`. +3. `bazel/registry/update_source.py naja https://github.com//naja/archive/.tar.gz naja-` +4. Point the `bazel_dep` in `MODULE.bazel` at it, and add any new BCR + pull request registries naja's `.bazelrc` lists. + +## Depending on kepler-formal from another module + +List this registry by a pinned URL, then the BCR pull request registries +from kepler-formal's `.bazelrc`, then BCR: + +``` +common --registry=https://raw.githubusercontent.com/keplertech/kepler-formal//bazel/registry/ +common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry// # one per BCR PR +common --registry=https://bcr.bazel.build/ +``` diff --git a/bazel/registry/bazel_registry.json b/bazel/registry/bazel_registry.json new file mode 100644 index 00000000..0967ef42 --- /dev/null +++ b/bazel/registry/bazel_registry.json @@ -0,0 +1 @@ +{} diff --git a/bazel/registry/modules/naja/0.7.26-20261003-d298a369/MODULE.bazel b/bazel/registry/modules/naja/0.7.26-20261003-d298a369/MODULE.bazel new file mode 100644 index 00000000..cbfccca6 --- /dev/null +++ b/bazel/registry/modules/naja/0.7.26-20261003-d298a369/MODULE.bazel @@ -0,0 +1,38 @@ +# SPDX-FileCopyrightText: 2023 The Naja authors +# +# SPDX-License-Identifier: Apache-2.0 + +"""Bazel module for naja. + +Every dependency is a plain bazel_dep. Versions that are not on the +Bazel Central Registry yet come from their open BCR pull requests, +which .bazelrc lists ahead of BCR. +""" + +module( + name = "naja", + version = "0.7.26-20261003-d298a369", + bazel_compatibility = [">=8.0.0"], +) + +bazel_dep(name = "bazel_skylib", version = "1.9.2") +bazel_dep(name = "bison", version = "3.8.2.bcr.10") +bazel_dep(name = "boost.asio", version = "1.90.0.bcr.1") +bazel_dep(name = "boost.dynamic_bitset", version = "1.90.0.bcr.1") +bazel_dep(name = "boost.intrusive", version = "1.90.0.bcr.1") +bazel_dep(name = "boost.multiprecision", version = "1.90.0.bcr.1") +bazel_dep(name = "capnp-cpp", version = "1.5.0") +bazel_dep(name = "fmt", version = "12.2.0") +bazel_dep(name = "naja-if", version = "0.0.0-20260723-099677d9") +bazel_dep(name = "naja-verilog", version = "0.0.0-20260909-be6544b1") +bazel_dep(name = "onetbb", version = "2023.1.0") +bazel_dep(name = "platforms", version = "1.1.0") +bazel_dep(name = "rules_cc", version = "0.2.25") +bazel_dep(name = "rules_python", version = "1.9.0") +bazel_dep(name = "rules_shell", version = "0.8.0") +bazel_dep(name = "spdlog", version = "1.17.0") +bazel_dep(name = "sv-lang", version = "11.0.0-20260701-b60d729d.bcr.1") +bazel_dep(name = "zlib", version = "1.3.2.bcr.1") + +bazel_dep(name = "google_benchmark", version = "1.9.5", dev_dependency = True) +bazel_dep(name = "googletest", version = "1.18.0.bcr.1", dev_dependency = True) diff --git a/bazel/registry/modules/naja/0.7.26-20261003-d298a369/overlay/MODULE.bazel b/bazel/registry/modules/naja/0.7.26-20261003-d298a369/overlay/MODULE.bazel new file mode 100644 index 00000000..cbfccca6 --- /dev/null +++ b/bazel/registry/modules/naja/0.7.26-20261003-d298a369/overlay/MODULE.bazel @@ -0,0 +1,38 @@ +# SPDX-FileCopyrightText: 2023 The Naja authors +# +# SPDX-License-Identifier: Apache-2.0 + +"""Bazel module for naja. + +Every dependency is a plain bazel_dep. Versions that are not on the +Bazel Central Registry yet come from their open BCR pull requests, +which .bazelrc lists ahead of BCR. +""" + +module( + name = "naja", + version = "0.7.26-20261003-d298a369", + bazel_compatibility = [">=8.0.0"], +) + +bazel_dep(name = "bazel_skylib", version = "1.9.2") +bazel_dep(name = "bison", version = "3.8.2.bcr.10") +bazel_dep(name = "boost.asio", version = "1.90.0.bcr.1") +bazel_dep(name = "boost.dynamic_bitset", version = "1.90.0.bcr.1") +bazel_dep(name = "boost.intrusive", version = "1.90.0.bcr.1") +bazel_dep(name = "boost.multiprecision", version = "1.90.0.bcr.1") +bazel_dep(name = "capnp-cpp", version = "1.5.0") +bazel_dep(name = "fmt", version = "12.2.0") +bazel_dep(name = "naja-if", version = "0.0.0-20260723-099677d9") +bazel_dep(name = "naja-verilog", version = "0.0.0-20260909-be6544b1") +bazel_dep(name = "onetbb", version = "2023.1.0") +bazel_dep(name = "platforms", version = "1.1.0") +bazel_dep(name = "rules_cc", version = "0.2.25") +bazel_dep(name = "rules_python", version = "1.9.0") +bazel_dep(name = "rules_shell", version = "0.8.0") +bazel_dep(name = "spdlog", version = "1.17.0") +bazel_dep(name = "sv-lang", version = "11.0.0-20260701-b60d729d.bcr.1") +bazel_dep(name = "zlib", version = "1.3.2.bcr.1") + +bazel_dep(name = "google_benchmark", version = "1.9.5", dev_dependency = True) +bazel_dep(name = "googletest", version = "1.18.0.bcr.1", dev_dependency = True) diff --git a/bazel/registry/modules/naja/0.7.26-20261003-d298a369/presubmit.yml b/bazel/registry/modules/naja/0.7.26-20261003-d298a369/presubmit.yml new file mode 100644 index 00000000..e6f3922e --- /dev/null +++ b/bazel/registry/modules/naja/0.7.26-20261003-d298a369/presubmit.yml @@ -0,0 +1,17 @@ +matrix: + platform: ["ubuntu2204", "ubuntu2404", "macos_arm64"] + bazel: ["8.x"] +tasks: + verify_targets: + name: Verify build targets + platform: ${{ platform }} + bazel: ${{ bazel }} + build_flags: + - "--cxxopt=-std=c++20" + build_targets: + - "@naja//src/dnl:naja_dnl" + - "@naja//src/nl/formats/systemverilog:naja_snl_systemverilog" + - "@naja//src/nl/formats/verilog:naja_snl_verilog" + - "@naja//src/nl/netlist/serialization/capnp:naja_nl_dump" + - "@naja//src/nl/python/pyloader:naja_snl_pyloader" + - "@naja//src/optimization:naja_opt" diff --git a/bazel/registry/modules/naja/0.7.26-20261003-d298a369/source.json b/bazel/registry/modules/naja/0.7.26-20261003-d298a369/source.json new file mode 100644 index 00000000..944f84a2 --- /dev/null +++ b/bazel/registry/modules/naja/0.7.26-20261003-d298a369/source.json @@ -0,0 +1,8 @@ +{ + "url": "https://github.com/oharboe/naja/archive/d298a369a3339d606e54aff5f2e42ee6b37ba73c.tar.gz", + "integrity": "sha256-0ct4zJM18PCv3cx71LQVM65cLbnu/pH/dXzhsc/T+u0=", + "strip_prefix": "naja-d298a369a3339d606e54aff5f2e42ee6b37ba73c", + "overlay": { + "MODULE.bazel": "sha256-D8/twMbwG2t0v4yPHwst3EZ43aD/IzhPEcFxWrJBGfw=" + } +} diff --git a/bazel/registry/modules/naja/metadata.json b/bazel/registry/modules/naja/metadata.json new file mode 100644 index 00000000..2b1b2a59 --- /dev/null +++ b/bazel/registry/modules/naja/metadata.json @@ -0,0 +1,23 @@ +{ + "homepage": "https://github.com/najaeda/naja", + "maintainers": [ + { + "github": "xtofalex", + "github_user_id": 3635601, + "name": "Christophe Alexandre" + }, + { + "github": "nanocoh", + "github_user_id": 115838389, + "name": "Noam Cohen" + } + ], + "repository": [ + "github:najaeda/naja", + "github:oharboe/naja" + ], + "versions": [ + "0.7.26-20261003-d298a369" + ], + "yanked_versions": {} +} diff --git a/bazel/registry/update_source.py b/bazel/registry/update_source.py new file mode 100755 index 00000000..c55e9968 --- /dev/null +++ b/bazel/registry/update_source.py @@ -0,0 +1,61 @@ +#!/usr/bin/env python3 +# SPDX-FileCopyrightText: 2026 keplertech.io +# +# SPDX-License-Identifier: Apache-2.0 +"""(Re)write source.json for one module version in this registry. + +Usage: + update_source.py [] + +Downloads , records its integrity, and records the integrity of +every file under the version's overlay/ and patches/ directories, so +the entry stays valid after editing an overlay or patch. The layout is +the Bazel Central Registry's, so a finished entry can be copied +verbatim into a bazel-central-registry pull request. +""" + +import base64 +import hashlib +import json +import pathlib +import sys +import urllib.request + + +def integrity(data): + return "sha256-" + base64.b64encode(hashlib.sha256(data).digest()).decode() + + +def main(argv): + if len(argv) not in (4, 5): + sys.exit(__doc__) + module, version, url = argv[1:4] + strip_prefix = argv[4] if len(argv) == 5 else "" + root = pathlib.Path(__file__).resolve().parent / "modules" / module / version + if not (root / "MODULE.bazel").is_file(): + sys.exit("{}/MODULE.bazel not found".format(root)) + + # Keep fields this script does not compute (mirror_urls, patch_strip). + source_json = root / "source.json" + source = json.loads(source_json.read_text()) if source_json.is_file() else {} + with urllib.request.urlopen(url) as response: + source.update(url=url, integrity=integrity(response.read())) + if strip_prefix: + source["strip_prefix"] = strip_prefix + + for kind in ("overlay", "patches"): + directory = root / kind + if directory.is_dir(): + source[kind] = { + str(path.relative_to(directory)): integrity(path.read_bytes()) + for path in sorted(directory.rglob("*")) + if path.is_file() + } + if "patches" in source: + source.setdefault("patch_strip", 1) + + source_json.write_text(json.dumps(source, indent=4) + "\n") + + +if __name__ == "__main__": + main(sys.argv) diff --git a/bazel/slang.BUILD.bazel b/bazel/slang.BUILD.bazel deleted file mode 100644 index 8649445f..00000000 --- a/bazel/slang.BUILD.bazel +++ /dev/null @@ -1,137 +0,0 @@ -load("@rules_cc//cc:cc_library.bzl", "cc_library") - -# Generated syntax files -genrule( - name = "gen_syntax", - srcs = [ - "scripts/syntax.txt", - "scripts/tokenkinds.txt", - "scripts/triviakinds.txt", - "scripts/systemnames.txt", - "scripts/syntax_gen.py", - ], - outs = [ - "slang/syntax/AllSyntax.h", - "AllSyntax.cpp", - "SyntaxClone.cpp", - "slang/syntax/SyntaxKind.h", - "slang/syntax/SyntaxFwd.h", - "slang/syntax/CSTJsonVisitorGen.h", - "slang/parsing/TokenKind.h", - "slang/parsing/KnownSystemName.h", - "TokenKind.cpp", - "KnownSystemName.cpp", - ], - cmd = "python3 $(location scripts/syntax_gen.py) --dir $(@D) --syntax $(location scripts/syntax.txt)", -) - -# Generated diagnostic files -genrule( - name = "gen_diagnostics", - srcs = [ - "scripts/diagnostics.txt", - "scripts/diagnostic_gen.py", - "source/CMakeLists.txt", - "include/slang/util/Util.h", - ], - outs = [ - "slang/diagnostics/AllDiags.h", - "slang/diagnostics/AnalysisDiags.h", - "slang/diagnostics/CompilationDiags.h", - "slang/diagnostics/ConstEvalDiags.h", - "slang/diagnostics/DeclarationsDiags.h", - "slang/diagnostics/DriverDiags.h", - "slang/diagnostics/ExpressionsDiags.h", - "slang/diagnostics/GeneralDiags.h", - "slang/diagnostics/LexerDiags.h", - "slang/diagnostics/LookupDiags.h", - "slang/diagnostics/MetaDiags.h", - "slang/diagnostics/NumericDiags.h", - "slang/diagnostics/ParserDiags.h", - "slang/diagnostics/PreprocessorDiags.h", - "slang/diagnostics/StatementsDiags.h", - "slang/diagnostics/SysFuncsDiags.h", - "slang/diagnostics/TypesDiags.h", - "DiagCode.cpp", - ], - cmd = "python3 $(location scripts/diagnostic_gen.py) --outDir $(@D) --diagnostics $(location scripts/diagnostics.txt) --srcDir $$(dirname $(location source/CMakeLists.txt)) --incDir $$(dirname $(location include/slang/util/Util.h))/..", -) - -# Generated VersionInfo.cpp -genrule( - name = "gen_version_info", - srcs = ["source/util/VersionInfo.cpp.in"], - outs = ["VersionInfo.cpp"], - cmd = "sed -e 's/@SLANG_VERSION_MAJOR@/11/g' -e 's/@SLANG_VERSION_MINOR@/0/g' -e 's/@SLANG_VERSION_PATCH@/0/g' -e 's/@SLANG_VERSION_VERSION@/11.0.0/g' $< > $@", -) - -# Generated slang_export.h -genrule( - name = "gen_slang_export", - outs = ["slang/slang_export.h"], - cmd = "echo '#ifndef SLANG_EXPORT_H' > $@ && echo '#define SLANG_EXPORT_H' >> $@ && echo '#define SLANG_EXPORT' >> $@ && echo '#define SLANG_NO_EXPORT' >> $@ && echo '#endif' >> $@", -) - -cc_library( - name = "slang_boost_shims", - hdrs = [ - "external/boost_concurrent.hpp", - "external/boost_unordered.hpp", - ], - includes = ["external"], -) - -cc_library( - name = "slang", - srcs = [ - ":gen_diagnostics", - ":gen_syntax", - ":gen_version_info", - ] + glob([ - "source/**/*.cpp", - ]), - hdrs = [ - ":gen_diagnostics", - ":gen_syntax", - ":gen_slang_export", - ] + glob([ - "include/**/*.h", - "external/**/*.h", - "external/**/*.hpp", - "source/**/*.h", - ]), - copts = [ - "-std=c++20", - "-fPIC", - "-fvisibility=hidden", - "-fvisibility-inlines-hidden", - "-Wno-unknown-warning-option", - ], - defines = [ - "SLANG_STATIC_DEFINE", - "SLANG_USE_THREADS", - ], - includes = [ - ".", - "external", - "include", - "source", - "source/analysis", - "source/ast", - "source/diagnostics", - "source/driver", - "source/numeric", - "source/parsing", - "source/syntax", - "source/text", - "source/util", - "$(GENDIR)/external/slang", - ], - visibility = ["//visibility:public"], - deps = [ - ":slang_boost_shims", - "@boost_headers//:boost", - "@fmt//:fmt", - "@tomlplusplus//:tomlplusplus", - ], -) diff --git a/bazel/tbb.bzl b/bazel/tbb.bzl deleted file mode 100644 index ac92e736..00000000 --- a/bazel/tbb.bzl +++ /dev/null @@ -1,4 +0,0 @@ -# oneTBB is provided hermetically by the cmake-built @onetbb repo on all -# platforms (headers + shared libtbb/libtbbmalloc via CcInfo). No system -# link flags: the libraries travel through Bazel's solib mechanism. -TBB_DEPS = ["@onetbb"] diff --git a/bazel/tomlplusplus.BUILD.bazel b/bazel/tomlplusplus.BUILD.bazel deleted file mode 100644 index 7d1fe7e8..00000000 --- a/bazel/tomlplusplus.BUILD.bazel +++ /dev/null @@ -1,9 +0,0 @@ -load("@rules_cc//cc:cc_library.bzl", "cc_library") - -cc_library( - name = "tomlplusplus", - srcs = ["src/toml.cpp"], - hdrs = glob(["include/toml++/**"]), - includes = ["include"], - visibility = ["//visibility:public"], -) diff --git a/bazel/toolchain_cmake.bzl b/bazel/toolchain_cmake.bzl deleted file mode 100644 index d0d60088..00000000 --- a/bazel/toolchain_cmake.bzl +++ /dev/null @@ -1,168 +0,0 @@ -"""Generate CMake toolchain settings from the resolved cc_toolchain. - -Used by //:deps to export the hermetic compiler for the plain CMake flow. -Emits three files: - -- toolchain_fragment.cmake — appended to deps/toolchain.cmake; points - CMAKE_{C,CXX}_COMPILER at the wrapper scripts and carries the link-time - settings (linker flags, C++ runtime archives, ar). -- hermetic-cc / hermetic-cxx — POSIX sh wrappers exec'ing the exported - clang with the zero-sysroot compile flags baked in. Flags live in the - wrappers rather than CMAKE__FLAGS_INIT because third-party - CMakeLists routinely stomp the flag variables (e.g. glucose's - set(CMAKE_CXX_FLAGS "-std=c++11")), which would silently fall back to - host headers and produce objects that cannot link against the hermetic - glibc stubs. - -Reuses rules_foreign_cc's toolchain capture (the same code that generates -the crosstool for the @naja/@capnproto/@onetbb cmake builds), so the CMake -flow compiles with the same flags as the Bazel flow. The load path is -private to rules_foreign_cc — pinned in MODULE.bazel; revisit on upgrades. -""" - -load( - "@rules_foreign_cc//foreign_cc/private:cc_toolchain_util.bzl", - "get_flags_info", - "get_tools_info", -) - -def _rewrite(s, bin_external, root): - """Rewrite execroot-relative external paths to //...""" - s = s.replace(bin_external, root + "/") - if s.startswith("external/"): - s = root + "/" + s[len("external/"):] - return s.replace("=external/", "=" + root + "/") - -def _cmake_join(flag_list, bin_external): - return " ".join([ - _rewrite(f, bin_external, "${_KF_LLVM}").replace('"', '\\"') - for f in flag_list - ]) - -def _keep_for_wrapper(flag): - """Drop Bazel's style/diagnostic preferences from the exported wrapper. - - The wrapper's job is hermeticity (sysroot, headers, target), not - imposing warning policy on third-party builds — cadical's configure, - for one, fails its test compile when -Wall produces output. -Wno-* - suppressions stay; warning-enabling -W* (incl. -Werror=*) go. - """ - if flag == "-fcolor-diagnostics": - return False - return not flag.startswith("-W") or flag.startswith("-Wno-") - -def _sh_join(flag_list, bin_external): - # Double-quote each flag so the wrapper's $D expands; escape embedded - # double quotes (e.g. -D__DATE__="redacted"). - return " ".join([ - '"%s"' % _rewrite(f, bin_external, "$D/llvm").replace('"', '\\"') - for f in flag_list - if _keep_for_wrapper(f) - ]) - -_WRAPPER = """#!/bin/sh -# Generated by //bazel:toolchain_cmake.bzl — do not edit. -# Hermetic zero-sysroot {lang} compiler for the CMake flow; flags are baked -# in so projects that overwrite CMAKE_{lang_upper}_FLAGS cannot lose them -# (and so configure scripts that invoke $CC/$CXX directly, like cadical's -# and kissat's, compile AND link hermetically). -# -Qunused-arguments: compile-only flags are silently ignored at link. -# -idirafter ranks below all hermetic -isystem headers; needed only for -# the system Python3 (Debian multiarch pyconfig.h), the one deliberate -# host dependency. -D=$(CDPATH='' cd -- "$(dirname -- "$0")/.." && pwd) -link=1 -for a in "$@"; do - case "$a" in - -c|-S|-E|-M|-MM|-###|--version|-dumpversion|-dumpmachine|--help|-print-*) link=0 ;; - esac -done -if [ "$link" = 1 ]; then - # Linking: add the toolchain's linker flags, and the C++ runtime - # archives after the user inputs (archive order matters). - exec "$D/llvm/{compiler}" -Qunused-arguments {flags} -idirafter /usr/include {link_flags} "$@" {post_libs} -fi -exec "$D/llvm/{compiler}" -Qunused-arguments {flags} -idirafter /usr/include "$@" -""" - -def _toolchain_cmake_impl(ctx): - tools = get_tools_info(ctx) - flags = get_flags_info(ctx) - bin_external = ctx.bin_dir.path + "/external/" - - cc_rel = _rewrite(tools.cc, bin_external, "") - if cc_rel.startswith("/"): - cc_rel = cc_rel[1:] - - # The hermetic toolchain drives C and C++ through the clang binary; - # use the clang++ driver name for C++ (mirrors rules_foreign_cc). - cxx_rel = _rewrite(tools.cxx, bin_external, "") - if cxx_rel.startswith("/"): - cxx_rel = cxx_rel[1:] - if cxx_rel.endswith("/clang"): - cxx_rel += "++" - - ar = _rewrite(tools.cxx_linker_static, bin_external, "${_KF_LLVM}") - - link_flags = _sh_join(flags.cxx_linker_executable, bin_external) - cxx_runtime = " ".join([ - '"$D/lib/liblibcxx.static.a"', - '"$D/lib/liblibcxxabi.static.a"', - '"$D/lib/liblibunwind.static.a"', - ]) - - cc_wrapper = ctx.actions.declare_file("hermetic-cc") - ctx.actions.write(cc_wrapper, _WRAPPER.format( - lang = "C", - lang_upper = "C", - compiler = cc_rel, - flags = _sh_join(flags.cc, bin_external), - link_flags = link_flags, - post_libs = "-lm", - ), is_executable = True) - - cxx_wrapper = ctx.actions.declare_file("hermetic-cxx") - ctx.actions.write(cxx_wrapper, _WRAPPER.format( - lang = "C++", - lang_upper = "CXX", - compiler = cxx_rel, - flags = _sh_join(flags.cxx, bin_external), - link_flags = link_flags, - post_libs = cxx_runtime + " -lm", - ), is_executable = True) - - fragment = ctx.actions.declare_file("toolchain_fragment.cmake") - ctx.actions.write(fragment, """# Hermetic compiler settings (generated from the Bazel cc_toolchain -# by //bazel:toolchain_cmake.bzl — do not edit). -set(_KF_LLVM "${{_KF_DEPS}}/llvm") -set(CMAKE_C_COMPILER "${{_KF_DEPS}}/bin/hermetic-cc") -set(CMAKE_CXX_COMPILER "${{_KF_DEPS}}/bin/hermetic-cxx") -set(CMAKE_AR "{ar}" CACHE FILEPATH "Archiver") -# llvm-ar writes the symbol index itself; ':' is CMake's no-op ranlib. -set(CMAKE_RANLIB ":") -set(CMAKE_EXE_LINKER_FLAGS_INIT "{exe_link_flags}") -set(CMAKE_SHARED_LINKER_FLAGS_INIT "{shared_link_flags}") -# The C++ runtime archives are Bazel link inputs, not driver defaults -# (see bazel/naja.BUILD.bazel); exported into deps/lib by //:deps. -set(CMAKE_CXX_STANDARD_LIBRARIES_INIT "${{_KF_DEPS}}/lib/liblibcxx.static.a ${{_KF_DEPS}}/lib/liblibcxxabi.static.a ${{_KF_DEPS}}/lib/liblibunwind.static.a -lm") -""".format( - ar = ar, - exe_link_flags = _cmake_join(flags.cxx_linker_executable, bin_external), - shared_link_flags = _cmake_join(flags.cxx_linker_shared, bin_external), - )) - - return [ - DefaultInfo(files = depset([fragment, cc_wrapper, cxx_wrapper])), - OutputGroupInfo(fragment = depset([fragment])), - ] - -toolchain_cmake = rule( - implementation = _toolchain_cmake_impl, - attrs = { - "_cc_toolchain": attr.label( - default = Label("@bazel_tools//tools/cpp:current_cc_toolchain"), - ), - }, - fragments = ["cpp"], - toolchains = ["@bazel_tools//tools/cpp:toolchain_type"], -) diff --git a/docs/bcr-roadmap.md b/docs/bcr-roadmap.md index 4aae2281..a20579c7 100644 --- a/docs/bcr-roadmap.md +++ b/docs/bcr-roadmap.md @@ -1,167 +1,88 @@ -# Bazel Central Registry (BCR) Roadmap +# Bazel and the Bazel Central Registry (BCR) -This document tracks the plan to publish kepler-formal to the -[Bazel Central Registry](https://registry.bazel.build/) so that -downstream projects like [bazel-orfs](https://github.com/The-OpenROAD-Project/bazel-orfs) -can depend on it with a simple `bazel_dep()`. +kepler-formal's Bazel build is a plain bzlmod module, ready to be +published to the [Bazel Central Registry](https://registry.bazel.build/) +so that downstream projects like +[bazel-orfs](https://github.com/The-OpenROAD-Project/bazel-orfs) can +depend on it with a single `bazel_dep()`. -## Build systems +The Bazel build is independent of the CMake flow: it does not use the +`thirdparty/` git submodules, and it never runs cmake. -kepler-formal supports two build systems: - -- **CMake** (primary): Uses git submodules in `thirdparty/` directly. - This is the established flow and remains a first-class citizen. -- **Bazel** (new): Uses `http_archive` to fetch the same dependencies - as source archives from GitHub. This avoids requiring git submodules - and is compatible with BCR distribution. - -Both build systems use the same source code and overlay BUILD files -(in `bazel/`). The cmake flow is unaffected by Bazel changes. - -### Current Bazel usage - -Bazel build support is available alongside CMake. It uses [bzlmod](https://bazel.build/external/overview#bzlmod) (`MODULE.bazel`) and pulls most dependencies from the [Bazel Central Registry](https://registry.bazel.build/). - -Build with Bazel: - -```bash -git clone --recurse-submodules https://github.com/keplertech/kepler-formal.git -cd kepler-formal -bazel build //src/bin:kepler-formal -``` - -Run tests: +## Build ```bash -bazel test //test/... +bazelisk build //src/bin:kepler-formal +bazelisk test //... ``` -### Dependency strategy - -- **BCR**: `yaml-cpp`, `googletest`, `zlib`, `spdlog` -- **Native BUILD files**: `kissat`, `glucose`, `boost` (headers), - `FlexLexer.h` -- **`rules_foreign_cc`**: `naja` and its nested sources, `capnproto`, - `onetbb` (cmake package trees consumed by naja's `find_package`) -- **System packages still required**: build tools only (cmake, make, - bison, flex) and Python 3 headers — see the hermeticity inventory below +No host packages are needed on Linux: the C++ toolchain (hermetic-llvm), +every library, and every code generator (bison, flex, the capnp compiler, +slang's Python generators) come from Bazel modules. -### Future work: bazel-orfs integration +## Dependencies -Once kepler-formal is fully buildable with Bazel, it can be consumed directly by [bazel-orfs](https://github.com/The-OpenROAD-Project/bazel-orfs) as a proper Bazel dependency instead of the current `$PATH`-based wrapper -([bazel-orfs#523](https://github.com/The-OpenROAD-Project/bazel-orfs/pull/523)). -This enables: +`MODULE.bazel` contains only `bazel_dep`s. Everything on BCR comes from +BCR: `onetbb`, `spdlog`, `yaml-cpp`, `googletest`, and, through naja, +`capnp-cpp`, `boost.*`, `fmt`, `bison`, `flex`, `rules_python`, and +others. -- **`bazel_dep` or `git_override`** in bazel-orfs `MODULE.bazel` to pin kepler-formal to a specific version or commit -- **Hermetic LEC tests** in bazel-orfs CI without requiring a pre-installed kepler-formal binary -- **Remote caching** of kepler-formal build artifacts shared across bazel-orfs users -- **Eventual BCR publication** of kepler-formal as a first-class Bazel module +What is not on BCR yet comes from its open bazel-central-registry pull +request, which `.bazelrc` lists by commit ahead of BCR: -## Phases +| Module | BCR pull request | +|---|---| +| `bison` 3.8.2.bcr.10 | bazelbuild/bazel-central-registry#10879 | +| `sv-lang` 11.0.0-20260701-b60d729d.bcr.1 | bazelbuild/bazel-central-registry#10882 | +| `naja-if` | bazelbuild/bazel-central-registry#10881 | +| `naja-verilog` | bazelbuild/bazel-central-registry#10885 | +| `kissat` 4.0.4 | bazelbuild/bazel-central-registry#10880 | +| `cadical` 3.0.0 | bazelbuild/bazel-central-registry#10883 | +| `glucose` 4.2.1-20251230-674dbba | bazelbuild/bazel-central-registry#10884 | -### Phase 1: http_archive deps (done) +`naja` itself is served from the in-tree +[`bazel/registry/`](../bazel/registry/README.md) until it is released and +on BCR. -The Bazel build fetches glucose, kissat, and naja via `http_archive` -instead of `new_local_repository`. This means `bazel build` works -from a source tarball without `git submodule init`. +## Depending on kepler-formal -Dependency versions are pinned in `bazel/deps.bzl` by commit SHA. +Until kepler-formal and the modules above are on BCR, a downstream +module lists the same registries as kepler-formal's `.bazelrc`, with +kepler-formal's `bazel/registry/` by pinned URL: -### Phase 2: git_override (next) - -Downstream projects can depend on kepler-formal via `git_override` -in their `MODULE.bazel`: +``` +# .bazelrc +common --registry=https://raw.githubusercontent.com/keplertech/kepler-formal//bazel/registry/ +# ...the BCR pull request registries from kepler-formal's .bazelrc... +common --registry=https://bcr.bazel.build/ +build --cxxopt=-std=c++20 +``` ```python -bazel_dep(name = "kepler-formal", version = "1.0.0") - +# MODULE.bazel +bazel_dep(name = "kepler-formal", version = "0.5.0") git_override( module_name = "kepler-formal", remote = "https://github.com/keplertech/kepler-formal.git", - commit = "", + commit = "", ) ``` -This works today — no BCR submission required. - -### Phase 2.5: Binary releases (done) - -Pre-built binaries are published as GitHub Releases. Run -`bazelisk run //:release` to tag and push; CI builds an optimized binary -and uploads it. See `docs/releasing.md` for full instructions. +`.github/consumer-test` is such a consumer and runs in CI. -Cap'n Proto is statically linked. Naja shared libraries and TBB -(which has no static libs) are bundled in the tarball with a wrapper -script. +## Publishing to BCR -Downstream projects can fetch the tarball via `http_archive` for fast -CI without building from source. +1. Get the BCR pull requests above merged, dropping each `.bazelrc` + line as it lands, then naja (released, via publish-to-bcr), deleting + it from `bazel/registry/`. +2. Ensure the version in `MODULE.bazel` matches + `src/bin/KeplerVersion.h.in`, and tag a release with + `bazelisk run //:release` (see `docs/releasing.md`). +3. Submit kepler-formal with the + [publish-to-bcr](https://github.com/bazel-contrib/publish-to-bcr) + GitHub App, which uses the templates in `.bcr/`. -### Phase 3: BCR publication - -To publish to BCR: - -1. Ensure the version in `MODULE.bazel` follows semver and matches `src/bin/KeplerVersion.h.in` (currently `0.5.0`). -2. Create a GitHub release/tag matching the version (e.g. `v1.0.0`) — - this now happens automatically via `bazelisk run //:release`. -3. Submit to BCR via the - [publish-to-bcr](https://github.com/bazel-contrib/publish-to-bcr) GitHub App - or manual PR to [bazel-central-registry](https://github.com/bazelbuild/bazel-central-registry). -4. Once published, downstream projects use plain `bazel_dep` with no override. - -## Updating pinned dependencies - -Dependency commit SHAs are pinned in `bazel/deps.bzl`. To update: - -1. Update the `_*_COMMIT` constants to the new commit SHA. -2. Run `bazel fetch @glucose @kissat @naja` — it will fail with a SHA - mismatch and print the correct `sha256`. Update the hash. -3. Verify: `bazel build //src/bin:kepler-formal && bazel test //test/...` - -The cmake flow uses whatever submodule commit is checked out in -`thirdparty/`. Keep the Bazel pins in sync with the submodule SHAs -when updating submodules. - -## Hermeticity: local-system dependency inventory - -All C/C++ *libraries* are now provided through Bazel; what remains from the -host is build *tools*. Full inventory with per-item status: - -| Dependency | Where used | Status / hermetic path | -|---|---|---| -| libcapnp/libkj + capnp compiler | src/bin, tests, naja cmake | **hermetic**: cmake-built `@capnproto` 1.4.0 (`bazel/capnproto.BUILD.bazel`) | -| libtbb/libtbbmalloc | src/bin, tests, naja cmake, release bundle | **hermetic**: cmake-built `@onetbb` 2022.3.0 — naja's `.so`s and the binary share one `libtbb.so.12` | -| zlib | src/bin, tests, naja cmake, glucose | **hermetic**: BCR `@zlib` everywhere | -| Boost headers | naja cmake + kepler compiles (via naja headers) | **hermetic**: `@boost_headers` 1.89.0 | -| FlexLexer.h (was libfl-dev) | naja-verilog scanner (previously leaked `-I/usr/include` via FindFLEX) | **hermetic**: `@flex_src//:flexlexer` + `FLEX_INCLUDE_DIR` cache entry | -| Host C++ toolchain | whole Bazel build | **hermetic** (Linux): hermetic-llvm (BCR `llvm`, zero-sysroot clang 22/libc++, glibc 2.28 floor) — see OpenROAD PR 10812. macOS still uses the host Xcode toolchain | -| Python3 interpreter + dev headers | naja cmake `find_package(Python3 ... Development.Embed REQUIRED)` runs even with `BUILD_NAJA_PYTHON=OFF`; `libnaja_python.so` links system libpython | future: rules_python / python-build-standalone + `Python3_ROOT_DIR`, or an upstream naja option to skip the probe | -| bison/flex executables | naja-verilog codegen (Homebrew paths hardcoded on macOS) | future: BCR `bison`/`flex`/`m4` modules fed via `BISON_EXECUTABLE`/`FLEX_EXECUTABLE` | -| cmake/make/pkg-config binaries | rules_foreign_cc preinstalled toolchains | future: rules_foreign_cc built/prebuilt toolchains (built pkg-config currently trips over a glib C23 issue with GCC 15) | -| Network during naja build | slang FetchContent (fmt) — the `requires-network` tag on `@naja` | future: pre-fetch in `naja_repo`, set `FETCHCONTENT_SOURCE_DIR_FMT` | -| macOS host toolchain | macOS Bazel build | future: hermetic-llvm macOS (SDK subset; CLI defaults suffice) | -| clang-tidy | not wired | future: `@llvm//tools:clang-tidy` lint aspect | - -The BCR `onetbb` module is Bazel-8-compatible nowadays; the cmake-built -`@onetbb` is used instead because naja's `find_package(TBB)` needs -`TBBConfig.cmake` and both naja and the binary must share a single TBB -runtime. - -### Hermetic dependencies for the CMake flow: `bazelisk run //:deps` - -The same install trees serve the plain CMake flow, opt-in: - -```bash -bazelisk run //:deps -cmake -B build -DCMAKE_TOOLCHAIN_FILE=$PWD/deps/toolchain.cmake -``` +## Binary releases -This exports capnproto, oneTBB, boost, zlib and FlexLexer.h into `deps/` -(git- and bazel-ignored) with a generated `toolchain.cmake`, replacing the -platform-specific apt/homebrew install step. On Linux the hermetic -compiler is exported too (`deps/llvm/`, with `toolchain.cmake` generated -from the resolved Bazel cc_toolchain by `bazel/toolchain_cmake.bzl`), so -the CMake flow compiles with the identical clang/libc++ as the Bazel flow -and needs no host compiler at all. The system-package CMake flow keeps -working unchanged. Host tools still required: cmake, make, bison, flex, -python3 (dev headers). +`bazelisk run //:release` tags a version; CI builds an optimized binary +and publishes it as a GitHub Release. See `docs/releasing.md`. diff --git a/docs/releasing.md b/docs/releasing.md index f38a86a9..953dbcf5 100644 --- a/docs/releasing.md +++ b/docs/releasing.md @@ -120,15 +120,9 @@ http_archive( ### Bazel (build from source) -```python -bazel_dep(name = "kepler-formal", version = "1.0.0") - -git_override( - module_name = "kepler-formal", - remote = "https://github.com/keplertech/kepler-formal.git", - commit = "", -) -``` +See [Depending on kepler-formal](bcr-roadmap.md#depending-on-kepler-formal): +until kepler-formal is on the Bazel Central Registry, a consumer also +lists kepler-formal's registry in its `.bazelrc`. ## Troubleshooting @@ -140,6 +134,6 @@ Bump the version to a new number and retry. **"Working tree is dirty" error**: Commit or stash all changes first. -**Release workflow fails**: Check the Actions tab for logs. The most -common issue is a stale dependency hash in `bazel/deps.bzl` — update -per the instructions in `docs/bcr-roadmap.md`. +**Release workflow fails**: Check the Actions tab for logs. A stale +`source.json` integrity hash in `bazel/registry/` is fixed by rerunning +`bazel/registry/update_source.py` (see `bazel/registry/README.md`). diff --git a/src/bin/BUILD.bazel b/src/bin/BUILD.bazel index 9e3ea3a6..bff1f751 100644 --- a/src/bin/BUILD.bazel +++ b/src/bin/BUILD.bazel @@ -1,7 +1,6 @@ load("@rules_cc//cc:cc_binary.bzl", "cc_binary") load("@rules_cc//cc:cc_library.bzl", "cc_library") load("//bazel:kepler_version.bzl", "kepler_version") -load("//bazel:naja_includes.bzl", "NAJA_HEADER_COPTS") exports_files(["KeplerVersion.h.in"]) @@ -37,13 +36,15 @@ cc_binary( "RunResult.h", "RunResult.cpp", ], - copts = NAJA_HEADER_COPTS, - data = [":naja_python_module"], + # The embedded Python's runtime (stdlib), located through runfiles by + # CppDriver.cpp. + data = [ + ":naja_python_module", + "@rules_python//python:current_py_toolchain", + ], dynamic_deps = ["@naja//src/nl/python/naja_wrapping:naja_runtime"], - # capnp/kj (static), TBB (shared, bundled in the release tarball) and - # zlib arrive transitively through @naja's cmake deps — no system -l - # flags. The hermetic toolchain links libc++ statically by default, - # which supersedes the former -static-libstdc++/-static-libgcc. + local_defines = ['KEPLER_PYTHON3_ROOTPATH=\\"$(PYTHON3_ROOTPATH)\\"'], + toolchains = ["@rules_python//python:current_py_toolchain"], visibility = ["//visibility:public"], deps = [ ":kepler_version", @@ -53,8 +54,15 @@ cc_binary( "//src/strategies:formal_strategies", "//src/utils:kepler_formal_utils", "@kissat", - "@naja", - "@naja//:naja_extra_headers", + "@naja//src/core:naja_core", + "@naja//src/dnl:naja_dnl", + "@naja//src/nl/formats/liberty:naja_snl_liberty", + "@naja//src/nl/formats/systemverilog:naja_snl_systemverilog", + "@naja//src/nl/formats/verilog:naja_snl_verilog", + "@naja//src/nl/netlist:naja_nl", + "@naja//src/nl/netlist/serialization/capnp:naja_nl_dump", + "@naja//src/nl/python/pyloader:naja_snl_pyloader", + "@rules_cc//cc/runfiles", "@spdlog", "@yaml-cpp", ], diff --git a/src/bin/CppDriver.cpp b/src/bin/CppDriver.cpp index 6a501806..47446f35 100644 --- a/src/bin/CppDriver.cpp +++ b/src/bin/CppDriver.cpp @@ -5,11 +5,48 @@ #include "SNLPyLoader.h" #include +#include #include #include +#ifdef KEPLER_PYTHON3_ROOTPATH +#include "rules_cc/cc/runfiles/runfiles.h" +#endif + namespace { +#ifdef KEPLER_PYTHON3_ROOTPATH +// Bazel builds embed the toolchain's hermetic Python, whose compiled-in +// prefix does not exist at run time. Point it at the runtime that ships in +// this binary's runfiles, unless the caller chose a PYTHONHOME (the release +// tarball's wrapper script does). +static void setBundledPythonHome(const char* argv0) { + if (std::getenv("PYTHONHOME")) { + return; + } + std::string error; + std::unique_ptr runfiles( + rules_cc::cc::runfiles::Runfiles::Create(argv0, BAZEL_CURRENT_REPOSITORY, &error)); + if (!runfiles) { + return; + } + // $(PYTHON3_ROOTPATH) of an external repository is "..//bin/python3"; + // its runfiles location drops the "../". + std::string rootpath(KEPLER_PYTHON3_ROOTPATH); + const std::string rlocation = + rootpath.rfind("../", 0) == 0 ? rootpath.substr(3) : "_main/" + rootpath; + const std::filesystem::path interpreter(runfiles->Rlocation(rlocation)); + std::error_code ec; + if (interpreter.empty() || !std::filesystem::exists(interpreter, ec)) { + return; + } + const auto home = interpreter.parent_path().parent_path(); + if (setenv("PYTHONHOME", home.string().c_str(), 1) != 0) { + throw std::runtime_error("Cannot configure PYTHONHOME for Naja primitives"); // LCOV_EXCL_LINE + } +} +#endif + static void addNajaPythonPath(const char* argv0) { if (!argv0 || !*argv0) { return; @@ -63,6 +100,9 @@ static void addNajaPythonPath(const char* argv0) { class StandalonePrimitiveLoader final : public KEPLER_FORMAL::PrimitiveLibraryLoader { public: void prepare(const char* executable) const override { +#ifdef KEPLER_PYTHON3_ROOTPATH + setBundledPythonHome(executable); +#endif addNajaPythonPath(executable); } void load(naja::NL::NLLibrary* library, diff --git a/src/clauses/BUILD.bazel b/src/clauses/BUILD.bazel index 4414a767..af6defb3 100644 --- a/src/clauses/BUILD.bazel +++ b/src/clauses/BUILD.bazel @@ -1,6 +1,4 @@ load("@rules_cc//cc:cc_library.bzl", "cc_library") -load("//bazel:naja_includes.bzl", "NAJA_HEADER_COPTS") -load("//bazel:tbb.bzl", "TBB_DEPS") cc_library( name = "kepler_clauses", @@ -14,13 +12,14 @@ cc_library( "SNLTruthTableTree.h", "Tree2BoolExpr.h", ], - copts = NAJA_HEADER_COPTS, includes = ["."], visibility = ["//visibility:public"], - deps = TBB_DEPS + [ + deps = [ + "@onetbb//:tbb", "//src/config:kepler_config", "//src/formal:formal_structures", - "@naja", - "@naja//:naja_extra_headers", + "@naja//src/core:naja_core", + "@naja//src/nl/netlist:naja_nl", + "@naja//src/dnl:naja_dnl", ], ) diff --git a/src/clocks/BUILD.bazel b/src/clocks/BUILD.bazel index 7d42db25..edb5de62 100644 --- a/src/clocks/BUILD.bazel +++ b/src/clocks/BUILD.bazel @@ -1,5 +1,4 @@ load("@rules_cc//cc:cc_library.bzl", "cc_library") -load("//bazel:naja_includes.bzl", "NAJA_HEADER_COPTS") cc_library( name = "kepler_clocks", @@ -14,7 +13,6 @@ cc_library( "../formal", "../sec", ], - copts = NAJA_HEADER_COPTS, visibility = ["//visibility:public"], deps = [ "//src/formal:formal_structures", diff --git a/src/formal/BUILD.bazel b/src/formal/BUILD.bazel index 605a1f4d..3360a1a7 100644 --- a/src/formal/BUILD.bazel +++ b/src/formal/BUILD.bazel @@ -1,5 +1,4 @@ load("@rules_cc//cc:cc_library.bzl", "cc_library") -load("//bazel:tbb.bzl", "TBB_DEPS") cc_library( name = "formal_structures", @@ -17,5 +16,5 @@ cc_library( ], includes = ["."], visibility = ["//visibility:public"], - deps = TBB_DEPS, + deps = ["@onetbb//:tbb"], ) diff --git a/src/scope/BUILD.bazel b/src/scope/BUILD.bazel index 4e1df9a8..f6cd7e37 100644 --- a/src/scope/BUILD.bazel +++ b/src/scope/BUILD.bazel @@ -1,17 +1,16 @@ load("@rules_cc//cc:cc_library.bzl", "cc_library") -load("//bazel:naja_includes.bzl", "NAJA_HEADER_COPTS") -load("//bazel:tbb.bzl", "TBB_DEPS") cc_library( name = "scope_extraction", srcs = ["ScopeExtraction.cpp"], hdrs = ["ScopeExtraction.h"], - copts = NAJA_HEADER_COPTS, includes = ["."], visibility = ["//visibility:public"], - deps = TBB_DEPS + [ + deps = [ + "@onetbb//:tbb", "//src/utils:kepler_formal_utils", - "@naja", - "@naja//:naja_extra_headers", + "@naja//src/nl/netlist:naja_nl", + "@naja//src/dnl:naja_dnl", + "@naja//src/optimization:naja_opt", ], ) diff --git a/src/sec/BUILD.bazel b/src/sec/BUILD.bazel index b8edd183..9d7439d0 100644 --- a/src/sec/BUILD.bazel +++ b/src/sec/BUILD.bazel @@ -1,6 +1,4 @@ load("@rules_cc//cc:cc_library.bzl", "cc_library") -load("//bazel:naja_includes.bzl", "NAJA_HEADER_COPTS") -load("//bazel:tbb.bzl", "TBB_DEPS") cc_library( name = "sec_common_headers", @@ -70,9 +68,9 @@ cc_library( ".", "..", ], - copts = NAJA_HEADER_COPTS, visibility = ["//visibility:public"], - deps = TBB_DEPS + [ + deps = [ + "@onetbb//:tbb", "//src/clauses:kepler_clauses", "//src/config:kepler_config", "//src/clocks:kepler_clocks", @@ -80,8 +78,8 @@ cc_library( "//src/sat:sat_solver_wrapper", ":sec_common_headers", "//src/strategies:formal_strategies", - "@naja", - "@naja//:naja_extra_headers", + "@naja//src/nl/netlist:naja_nl", + "@naja//src/dnl:naja_dnl", "@kissat", ], ) diff --git a/src/strategies/BUILD.bazel b/src/strategies/BUILD.bazel index f2aeaf5f..3c700b92 100644 --- a/src/strategies/BUILD.bazel +++ b/src/strategies/BUILD.bazel @@ -1,6 +1,4 @@ load("@rules_cc//cc:cc_library.bzl", "cc_library") -load("//bazel:naja_includes.bzl", "NAJA_HEADER_COPTS") -load("//bazel:tbb.bzl", "TBB_DEPS") cc_library( name = "formal_strategies", @@ -16,9 +14,9 @@ cc_library( "miter", "..", # for ../sat/SATSolverWrapper.h relative includes ], - copts = NAJA_HEADER_COPTS, visibility = ["//visibility:public"], - deps = TBB_DEPS + [ + deps = [ + "@onetbb//:tbb", "//src/clauses:kepler_clauses", "//src/config:kepler_config", "//src/formal:formal_structures", @@ -26,8 +24,9 @@ cc_library( "//src/sat:sat_solver_wrapper", "@glucose", "@kissat", - "@naja", - "@naja//:naja_extra_headers", + "@naja//src/core:naja_core", + "@naja//src/nl/netlist:naja_nl", + "@naja//src/dnl:naja_dnl", "@spdlog", ], ) diff --git a/src/utils/BUILD.bazel b/src/utils/BUILD.bazel index 78bec20d..eaa0fadf 100644 --- a/src/utils/BUILD.bazel +++ b/src/utils/BUILD.bazel @@ -1,6 +1,4 @@ load("@rules_cc//cc:cc_library.bzl", "cc_library") -load("//bazel:naja_includes.bzl", "NAJA_HEADER_COPTS") -load("//bazel:tbb.bzl", "TBB_DEPS") cc_library( name = "kepler_formal_utils", @@ -12,12 +10,12 @@ cc_library( "DesignBoundary.h", "SNLLogicCone.h", ], - copts = NAJA_HEADER_COPTS, includes = ["."], visibility = ["//visibility:public"], - deps = TBB_DEPS + [ + deps = [ + "@onetbb//:tbb", "//src/formal:formal_structures", - "@naja", - "@naja//:naja_extra_headers", + "@naja//src/nl/netlist:naja_nl", + "@naja//src/dnl:naja_dnl", ], ) diff --git a/test/BUILD.bazel b/test/BUILD.bazel index 2ec798db..7127b75d 100644 --- a/test/BUILD.bazel +++ b/test/BUILD.bazel @@ -1,4 +1,4 @@ -# Package marker for test directory +load("@rules_shell//shell:sh_test.bzl", "sh_test") sh_test( name = "VersionCliTest", diff --git a/test/scope/BUILD.bazel b/test/scope/BUILD.bazel index aa749a06..c4e78fed 100644 --- a/test/scope/BUILD.bazel +++ b/test/scope/BUILD.bazel @@ -1,17 +1,14 @@ load("@rules_cc//cc:cc_test.bzl", "cc_test") -load("//bazel:naja_includes.bzl", "NAJA_HEADER_COPTS") cc_test( name = "ScopeExtractionTests", srcs = ["ScopeExtractionTests.cpp"], - copts = NAJA_HEADER_COPTS, deps = [ "//src/clauses:kepler_clauses", "//src/formal:formal_structures", "//src/scope:scope_extraction", "//src/strategies:formal_strategies", - "@naja", - "@naja//:naja_extra_headers", - "@googletest//:gtest_main", + "@naja//src/nl/netlist:naja_nl", + "@googletest//:gtest", ], ) diff --git a/test/sec/BUILD.bazel b/test/sec/BUILD.bazel index 26983f4c..b704008e 100644 --- a/test/sec/BUILD.bazel +++ b/test/sec/BUILD.bazel @@ -1,16 +1,14 @@ load("@rules_cc//cc:cc_test.bzl", "cc_test") -load("//bazel:naja_includes.bzl", "NAJA_HEADER_COPTS") cc_test( name = "BoundaryEquivalenceTests", srcs = ["BoundaryEquivalenceTests.cpp"], - copts = NAJA_HEADER_COPTS, deps = [ "//src/sec:kepler_sec", "//src/utils:kepler_formal_utils", "//src/clauses:kepler_clauses", - "@naja", - "@naja//:naja_extra_headers", + "@naja//src/nl/netlist:naja_nl", + "@naja//src/dnl:naja_dnl", "@googletest//:gtest_main", ], ) @@ -21,7 +19,6 @@ cc_test( "SecBtor2ExporterTests.cpp", "SecBtor2ExportValidationTests.cpp", ], - copts = NAJA_HEADER_COPTS, deps = ["//src/sec:kepler_sec", "//src/formal:formal_structures", "@googletest//:gtest_main"], ) @@ -34,21 +31,22 @@ cc_test( ], data = [ "//examples:testdata", - "@naja//:ff_scan_lib", + "@naja//test/nl/formats/liberty:benchmarks/tests/FF_scan.lib", ], env = { - "NAJA_FF_SCAN_LIB": "$(rootpath @naja//:ff_scan_lib)", + "NAJA_FF_SCAN_LIB": "$(rootpath @naja//test/nl/formats/liberty:benchmarks/tests/FF_scan.lib)", "TEST_DATA_PREFIX": "", }, size = "large", timeout = "long", - copts = NAJA_HEADER_COPTS, deps = [ "//src/config:kepler_config", "//src/sec:kepler_sec", "//src/strategies:formal_strategies", - "@naja", - "@naja//:naja_extra_headers", + "@naja//src/nl/netlist:naja_nl", + "@naja//src/dnl:naja_dnl", + "@naja//src/nl/formats/liberty:naja_snl_liberty", + "@naja//src/nl/formats/systemverilog:naja_snl_systemverilog", "@googletest//:gtest_main", ], ) diff --git a/test/strategies/miter/BUILD.bazel b/test/strategies/miter/BUILD.bazel index 2fb4ed33..409c8bb6 100644 --- a/test/strategies/miter/BUILD.bazel +++ b/test/strategies/miter/BUILD.bazel @@ -1,5 +1,5 @@ load("@rules_cc//cc:cc_test.bzl", "cc_test") -load("//bazel:naja_includes.bzl", "NAJA_HEADER_COPTS") +load("@rules_shell//shell:sh_test.bzl", "sh_test") sh_test( name = "BazelPythonPrimitivesTest", @@ -21,14 +21,19 @@ cc_test( "KEPLER_BIN": "$(rootpath //src/bin:kepler-formal)", "TEST_DATA_PREFIX": "", }, - copts = NAJA_HEADER_COPTS, deps = [ "//src/clauses:kepler_clauses", "//src/config:kepler_config", "//src/formal:formal_structures", "//src/strategies:formal_strategies", - "@naja", - "@naja//:naja_extra_headers", - "@googletest//:gtest_main", + "@naja//src/core:naja_core", + "@naja//src/nl/netlist:naja_nl", + "@naja//src/nl/netlist:naja_snl_visual", + "@naja//src/dnl:naja_dnl", + "@naja//src/optimization:naja_opt", + "@naja//src/nl/formats/liberty:naja_snl_liberty", + "@naja//src/nl/formats/verilog:naja_snl_verilog", + "@naja//src/nl/netlist/serialization/capnp:naja_nl_dump", + "@googletest//:gtest", ], ) diff --git a/test/utils/BUILD.bazel b/test/utils/BUILD.bazel index 07f0808c..fa19a079 100644 --- a/test/utils/BUILD.bazel +++ b/test/utils/BUILD.bazel @@ -1,5 +1,4 @@ load("@rules_cc//cc:cc_test.bzl", "cc_test") -load("//bazel:naja_includes.bzl", "NAJA_HEADER_COPTS") cc_test( name = "Btor2WriterTests", @@ -10,12 +9,11 @@ cc_test( cc_test( name = "SNLTruthTableTreeTests", srcs = ["SNLTruthTableTreeTests.cpp"], - copts = NAJA_HEADER_COPTS, deps = [ "//src/clauses:kepler_clauses", "//src/formal:formal_structures", "//src/strategies:formal_strategies", - "@googletest//:gtest_main", + "@googletest//:gtest", ], ) @@ -31,7 +29,6 @@ cc_test( cc_test( name = "DesignBoundaryTests", srcs = ["DesignBoundaryTests.cpp"], - copts = NAJA_HEADER_COPTS, deps = [ "//src/utils:kepler_formal_utils", "@googletest//:gtest_main",