From 13799563f0b673abc55aeb9e07a8d8b2ce6b19db Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C3=98yvind=20Harboe?= Date: Fri, 2 Oct 2026 10:41:54 +0200 Subject: [PATCH 1/6] bazel: plain bazel_deps via an in-tree registry, no cmake Make kepler-formal's Bazel build ready to be a Bazel Central Registry module: MODULE.bazel contains only bazel_deps, and nothing in the build runs cmake or probes the host. - Delete bazel/deps.bzl and every overlay, patch and repository rule: rules_foreign_cc builds of capnproto, oneTBB and slang; host bison, flex, m4 and python3-config; vendored Boost, tomlplusplus and FlexLexer.h; the naja BUILD-file patches and the naja_cc_library and -iquote include wrappers. - Retire //:deps, which only existed to hand cmake-built install trees to the CMake flow. - Depend on BCR modules (onetbb, spdlog, yaml-cpp, googletest, rules_python, ...) and on naja's own targets instead of an aggregate @naja library. - bazel/registry/: a file registry in BCR's layout for what is not on BCR yet (kissat 4.0.4, cadical 3.0.0, glucose 4.2.1 at upstream master, naja, and naja's naja-if, naja-verilog, sv-lang and bison entries), listed ahead of BCR in .bazelrc. Publishing a module is copying its directory into a BCR pull request. - Embedded Python is the rules_python hermetic runtime; the driver finds it in runfiles, and the release tarball bundles it. - .bcr/ templates for publish-to-bcr. - llvm 0.8.24; tests with their own main() use gtest, not gtest_main. CI installs no host packages for Bazel. CMake and the thirdparty/ submodules are unchanged. Co-Authored-By: Claude Opus 5.5 --- .bazelignore | 4 +- .bazelrc | 10 +- .bcr/metadata.template.json | 9 + .bcr/presubmit.yml | 12 + .bcr/source.template.json | 5 + .github/consumer-test/.bazelrc | 13 +- .github/consumer-test/MODULE.bazel | 20 +- .github/workflows/bazel.yml | 16 +- .github/workflows/consumer.yml | 13 +- .github/workflows/release.yml | 26 +- .gitignore | 3 - .reuse/dep5 | 2 +- BUILD.bazel | 93 +- MODULE.bazel | 86 +- README.md | 19 +- bazel/BUILD.bazel | 60 +- bazel/boost.BUILD.bazel | 27 - bazel/capnproto.BUILD.bazel | 64 - bazel/collect_headers.bzl | 23 - bazel/deps.bzl | 168 --- bazel/export_deps.sh | 116 -- bazel/flexlexer.BUILD.bazel | 20 - bazel/naja.BUILD.bazel | 31 - bazel/naja_cc_library.bzl | 8 - bazel/naja_ff_scan.patch | 175 --- bazel/naja_includes.bzl | 49 - bazel/naja_repositories.bzl | 155 --- bazel/naja_verilog_bazel9.patch | 11 - bazel/onetbb.BUILD.bazel | 64 - bazel/registry/README.md | 57 + bazel/registry/bazel_registry.json | 1 + .../modules/bison/3.8.2.bcr.10/MODULE.bazel | 13 + .../bison/3.8.2.bcr.10/overlay/BUILD.bazel | 1108 +++++++++++++++++ .../bison/3.8.2.bcr.10/overlay/MODULE.bazel | 1 + .../bison/3.8.2.bcr.10/overlay/bison.bzl | 131 ++ .../3.8.2.bcr.10/overlay/examples/BUILD.bazel | 47 + .../overlay/examples/bison_test.bzl | 59 + .../overlay/src/bazel_runfiles.cc | 125 ++ .../3.8.2.bcr.10/patches/bison_runfiles.patch | 29 + .../patches/bison_runfiles_main.patch | 12 + .../3.8.2.bcr.10/patches/rpcalc_stdlib.patch | 10 + .../3.8.2.bcr.10/patches/stdint_comment.patch | 12 + .../patches/string_free_decl.patch | 15 + .../patches/wchar_free_decl.patch | 15 + .../patches/xstrndup_strndup_decl.patch | 17 + .../modules/bison/3.8.2.bcr.10/presubmit.yml | 20 + .../modules/bison/3.8.2.bcr.10/source.json | 27 + bazel/registry/modules/bison/metadata.json | 21 + .../modules/cadical/3.0.0/MODULE.bazel | 7 + .../cadical/3.0.0/overlay/BUILD.bazel} | 7 +- .../cadical/3.0.0/overlay/MODULE.bazel | 1 + .../modules/cadical/3.0.0/presubmit.yml | 10 + .../modules/cadical/3.0.0/source.json | 9 + bazel/registry/modules/cadical/metadata.json | 11 + .../4.2.1-20251230-674dbba/MODULE.bazel | 8 + .../overlay/BUILD.bazel} | 2 + .../overlay/MODULE.bazel | 1 + .../4.2.1-20251230-674dbba/presubmit.yml | 10 + .../4.2.1-20251230-674dbba/source.json | 9 + bazel/registry/modules/glucose/metadata.json | 11 + .../modules/kissat/4.0.4/MODULE.bazel | 7 + .../modules/kissat/4.0.4/overlay/BUILD.bazel} | 29 +- .../modules/kissat/4.0.4/overlay/MODULE.bazel | 1 + .../modules/kissat/4.0.4/presubmit.yml | 10 + .../registry/modules/kissat/4.0.4/source.json | 9 + bazel/registry/modules/kissat/metadata.json | 11 + .../0.0.0-20260723-099677d9/MODULE.bazel | 7 + .../overlay/MODULE.bazel | 1 + .../0.0.0-20260723-099677d9/presubmit.yml | 12 + .../0.0.0-20260723-099677d9/source.json | 8 + bazel/registry/modules/naja-if/metadata.json | 11 + .../0.0.0-20260909-be6544b1/MODULE.bazel | 9 + .../overlay/BUILD.bazel | 60 + .../overlay/MODULE.bazel | 1 + .../0.0.0-20260909-be6544b1/presubmit.yml | 10 + .../0.0.0-20260909-be6544b1/source.json | 9 + .../modules/naja-verilog/metadata.json | 11 + .../0.7.26-20261002-3ab09cb2/MODULE.bazel | 40 + .../overlay/MODULE.bazel | 1 + .../0.7.26-20261002-3ab09cb2/presubmit.yml | 17 + .../naja/0.7.26-20261002-3ab09cb2/source.json | 8 + bazel/registry/modules/naja/metadata.json | 12 + .../11.0.0-20260701-b60d729d/MODULE.bazel | 26 + .../overlay/BUILD.bazel | 514 ++++++++ .../overlay/MODULE.bazel | 1 + .../private/slang/export_headers/BUILD.bazel | 35 + .../overlay/private/tests/BUILD.bazel | 19 + .../overlay/private/tests/pyslang/BUILD.bazel | 11 + .../overlay/private/tests/pyslang/test.py | 21 + .../private/tests/pyslang/test_module.sv | 12 + .../overlay/pyslang/BUILD.bazel | 59 + .../overlay/pyslang/__init__.py | 1 + .../patches/toml_single_header.patch | 15 + .../11.0.0-20260701-b60d729d/presubmit.yml | 60 + .../11.0.0-20260701-b60d729d/source.json | 19 + bazel/registry/modules/sv-lang/metadata.json | 24 + bazel/registry/update_source.py | 61 + bazel/slang.BUILD.bazel | 137 -- bazel/tbb.bzl | 4 - bazel/tomlplusplus.BUILD.bazel | 9 - bazel/toolchain_cmake.bzl | 168 --- docs/bcr-roadmap.md | 197 +-- docs/releasing.md | 18 +- src/bin/BUILD.bazel | 26 +- src/bin/CppDriver.cpp | 40 + src/clauses/BUILD.bazel | 11 +- src/clocks/BUILD.bazel | 2 - src/formal/BUILD.bazel | 3 +- src/scope/BUILD.bazel | 11 +- src/sec/BUILD.bazel | 10 +- src/strategies/BUILD.bazel | 11 +- src/utils/BUILD.bazel | 10 +- test/BUILD.bazel | 2 +- test/scope/BUILD.bazel | 7 +- test/sec/BUILD.bazel | 18 +- test/strategies/miter/BUILD.bazel | 15 +- test/utils/BUILD.bazel | 5 +- 117 files changed, 3218 insertions(+), 1756 deletions(-) create mode 100644 .bcr/metadata.template.json create mode 100644 .bcr/presubmit.yml create mode 100644 .bcr/source.template.json delete mode 100644 bazel/boost.BUILD.bazel delete mode 100644 bazel/capnproto.BUILD.bazel delete mode 100644 bazel/collect_headers.bzl delete mode 100644 bazel/deps.bzl delete mode 100755 bazel/export_deps.sh delete mode 100644 bazel/flexlexer.BUILD.bazel delete mode 100644 bazel/naja.BUILD.bazel delete mode 100644 bazel/naja_cc_library.bzl delete mode 100644 bazel/naja_ff_scan.patch delete mode 100644 bazel/naja_includes.bzl delete mode 100644 bazel/naja_repositories.bzl delete mode 100644 bazel/naja_verilog_bazel9.patch delete mode 100644 bazel/onetbb.BUILD.bazel create mode 100644 bazel/registry/README.md create mode 100644 bazel/registry/bazel_registry.json create mode 100644 bazel/registry/modules/bison/3.8.2.bcr.10/MODULE.bazel create mode 100644 bazel/registry/modules/bison/3.8.2.bcr.10/overlay/BUILD.bazel create mode 120000 bazel/registry/modules/bison/3.8.2.bcr.10/overlay/MODULE.bazel create mode 100644 bazel/registry/modules/bison/3.8.2.bcr.10/overlay/bison.bzl create mode 100644 bazel/registry/modules/bison/3.8.2.bcr.10/overlay/examples/BUILD.bazel create mode 100644 bazel/registry/modules/bison/3.8.2.bcr.10/overlay/examples/bison_test.bzl create mode 100644 bazel/registry/modules/bison/3.8.2.bcr.10/overlay/src/bazel_runfiles.cc create mode 100644 bazel/registry/modules/bison/3.8.2.bcr.10/patches/bison_runfiles.patch create mode 100644 bazel/registry/modules/bison/3.8.2.bcr.10/patches/bison_runfiles_main.patch create mode 100644 bazel/registry/modules/bison/3.8.2.bcr.10/patches/rpcalc_stdlib.patch create mode 100644 bazel/registry/modules/bison/3.8.2.bcr.10/patches/stdint_comment.patch create mode 100644 bazel/registry/modules/bison/3.8.2.bcr.10/patches/string_free_decl.patch create mode 100644 bazel/registry/modules/bison/3.8.2.bcr.10/patches/wchar_free_decl.patch create mode 100644 bazel/registry/modules/bison/3.8.2.bcr.10/patches/xstrndup_strndup_decl.patch create mode 100644 bazel/registry/modules/bison/3.8.2.bcr.10/presubmit.yml create mode 100644 bazel/registry/modules/bison/3.8.2.bcr.10/source.json create mode 100644 bazel/registry/modules/bison/metadata.json create mode 100644 bazel/registry/modules/cadical/3.0.0/MODULE.bazel rename bazel/{cadical.BUILD.bazel => registry/modules/cadical/3.0.0/overlay/BUILD.bazel} (93%) create mode 120000 bazel/registry/modules/cadical/3.0.0/overlay/MODULE.bazel create mode 100644 bazel/registry/modules/cadical/3.0.0/presubmit.yml create mode 100644 bazel/registry/modules/cadical/3.0.0/source.json create mode 100644 bazel/registry/modules/cadical/metadata.json create mode 100644 bazel/registry/modules/glucose/4.2.1-20251230-674dbba/MODULE.bazel rename bazel/{glucose.BUILD.bazel => registry/modules/glucose/4.2.1-20251230-674dbba/overlay/BUILD.bazel} (82%) create mode 120000 bazel/registry/modules/glucose/4.2.1-20251230-674dbba/overlay/MODULE.bazel create mode 100644 bazel/registry/modules/glucose/4.2.1-20251230-674dbba/presubmit.yml create mode 100644 bazel/registry/modules/glucose/4.2.1-20251230-674dbba/source.json create mode 100644 bazel/registry/modules/glucose/metadata.json create mode 100644 bazel/registry/modules/kissat/4.0.4/MODULE.bazel rename bazel/{kissat.BUILD.bazel => registry/modules/kissat/4.0.4/overlay/BUILD.bazel} (58%) create mode 120000 bazel/registry/modules/kissat/4.0.4/overlay/MODULE.bazel create mode 100644 bazel/registry/modules/kissat/4.0.4/presubmit.yml create mode 100644 bazel/registry/modules/kissat/4.0.4/source.json create mode 100644 bazel/registry/modules/kissat/metadata.json create mode 100644 bazel/registry/modules/naja-if/0.0.0-20260723-099677d9/MODULE.bazel create mode 120000 bazel/registry/modules/naja-if/0.0.0-20260723-099677d9/overlay/MODULE.bazel create mode 100644 bazel/registry/modules/naja-if/0.0.0-20260723-099677d9/presubmit.yml create mode 100644 bazel/registry/modules/naja-if/0.0.0-20260723-099677d9/source.json create mode 100644 bazel/registry/modules/naja-if/metadata.json create mode 100644 bazel/registry/modules/naja-verilog/0.0.0-20260909-be6544b1/MODULE.bazel create mode 100644 bazel/registry/modules/naja-verilog/0.0.0-20260909-be6544b1/overlay/BUILD.bazel create mode 120000 bazel/registry/modules/naja-verilog/0.0.0-20260909-be6544b1/overlay/MODULE.bazel create mode 100644 bazel/registry/modules/naja-verilog/0.0.0-20260909-be6544b1/presubmit.yml create mode 100644 bazel/registry/modules/naja-verilog/0.0.0-20260909-be6544b1/source.json create mode 100644 bazel/registry/modules/naja-verilog/metadata.json create mode 100644 bazel/registry/modules/naja/0.7.26-20261002-3ab09cb2/MODULE.bazel create mode 120000 bazel/registry/modules/naja/0.7.26-20261002-3ab09cb2/overlay/MODULE.bazel create mode 100644 bazel/registry/modules/naja/0.7.26-20261002-3ab09cb2/presubmit.yml create mode 100644 bazel/registry/modules/naja/0.7.26-20261002-3ab09cb2/source.json create mode 100644 bazel/registry/modules/naja/metadata.json create mode 100644 bazel/registry/modules/sv-lang/11.0.0-20260701-b60d729d/MODULE.bazel create mode 100644 bazel/registry/modules/sv-lang/11.0.0-20260701-b60d729d/overlay/BUILD.bazel create mode 120000 bazel/registry/modules/sv-lang/11.0.0-20260701-b60d729d/overlay/MODULE.bazel create mode 100644 bazel/registry/modules/sv-lang/11.0.0-20260701-b60d729d/overlay/private/slang/export_headers/BUILD.bazel create mode 100644 bazel/registry/modules/sv-lang/11.0.0-20260701-b60d729d/overlay/private/tests/BUILD.bazel create mode 100644 bazel/registry/modules/sv-lang/11.0.0-20260701-b60d729d/overlay/private/tests/pyslang/BUILD.bazel create mode 100644 bazel/registry/modules/sv-lang/11.0.0-20260701-b60d729d/overlay/private/tests/pyslang/test.py create mode 100644 bazel/registry/modules/sv-lang/11.0.0-20260701-b60d729d/overlay/private/tests/pyslang/test_module.sv create mode 100644 bazel/registry/modules/sv-lang/11.0.0-20260701-b60d729d/overlay/pyslang/BUILD.bazel create mode 100644 bazel/registry/modules/sv-lang/11.0.0-20260701-b60d729d/overlay/pyslang/__init__.py create mode 100644 bazel/registry/modules/sv-lang/11.0.0-20260701-b60d729d/patches/toml_single_header.patch create mode 100644 bazel/registry/modules/sv-lang/11.0.0-20260701-b60d729d/presubmit.yml create mode 100644 bazel/registry/modules/sv-lang/11.0.0-20260701-b60d729d/source.json create mode 100644 bazel/registry/modules/sv-lang/metadata.json create mode 100755 bazel/registry/update_source.py delete mode 100644 bazel/slang.BUILD.bazel delete mode 100644 bazel/tbb.bzl delete mode 100644 bazel/tomlplusplus.BUILD.bazel delete mode 100644 bazel/toolchain_cmake.bzl 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..55ae9b5e 100644 --- a/.bazelrc +++ b/.bazelrc @@ -1,3 +1,8 @@ +# Modules not yet on the Bazel Central Registry come from the in-tree +# registry (see bazel/registry/README.md); everything else from BCR. +common --registry=file://%workspace%/bazel/registry +common --registry=https://bcr.bazel.build/ + common --enable_platform_specific_config build --cxxopt=-std=c++20 @@ -10,10 +15,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..4e669fee --- /dev/null +++ b/.bcr/metadata.template.json @@ -0,0 +1,9 @@ +{ + "homepage": "https://github.com/keplertech/kepler-formal", + "maintainers": [], + "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..8b22f1c3 100644 --- a/.github/consumer-test/.bazelrc +++ b/.github/consumer-test/.bazelrc @@ -1,10 +1,15 @@ +# kepler-formal's registry for modules not yet on BCR, then BCR. A +# consumer outside this repository lists the same registry by URL, see +# bazel/registry/README.md. +common --registry=file://%workspace%/../../bazel/registry +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..697e17cc 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 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/MODULE.bazel b/MODULE.bazel index 6a050627..21ff5cad 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. Modules that are not yet on the +Bazel Central Registry (kissat, glucose, cadical, naja and naja's own +non-BCR dependencies) are served by the registry in bazel/registry/, +which .bazelrc lists ahead of BCR. See bazel/registry/README.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-20261002-3ab09cb2") +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..21e02c79 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, the in-tree registry for modules not yet on the Bazel +Central Registry, 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/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/naja.BUILD.bazel b/bazel/naja.BUILD.bazel deleted file mode 100644 index 9555c85c..00000000 --- a/bazel/naja.BUILD.bazel +++ /dev/null @@ -1,31 +0,0 @@ -load("@rules_cc//cc:cc_library.bzl", "cc_library") - -# Compatibility target for Kepler's existing @naja dependency. The actual -# implementation is Naja's native Bazel target graph. -cc_library( - name = "naja", - visibility = ["//visibility:public"], - deps = [ - "//src/dnl:naja_dnl", - "//src/nl/formats/liberty:naja_snl_liberty", - "//src/nl/formats/systemverilog:naja_snl_systemverilog", - "//src/nl/formats/verilog:naja_snl_verilog", - "//src/nl/netlist:naja_nl", - "//src/nl/netlist:naja_snl_visual", - "//src/nl/netlist/serialization/capnp:naja_nl_dump", - "//src/nl/python/pyloader:naja_snl_pyloader", - "//src/optimization:naja_opt", - ], -) - -alias( - name = "naja_extra_headers", - actual = ":naja", - visibility = ["//visibility:public"], -) - -filegroup( - name = "ff_scan_lib", - srcs = ["//test/nl/formats/liberty:benchmarks/tests/FF_scan.lib"], - visibility = ["//visibility:public"], -) diff --git a/bazel/naja_cc_library.bzl b/bazel/naja_cc_library.bzl deleted file mode 100644 index 5d27fe82..00000000 --- a/bazel/naja_cc_library.bzl +++ /dev/null @@ -1,8 +0,0 @@ -"""C++ rule wrapper that keeps fetched Naja headers ahead of host installs.""" - -load("@rules_cc//cc:cc_library.bzl", _cc_library = "cc_library") -load("//bazel:naja_includes.bzl", "NAJA_HEADER_COPTS") - -def cc_library(**kwargs): - kwargs["copts"] = kwargs.get("copts", []) + NAJA_HEADER_COPTS - _cc_library(**kwargs) diff --git a/bazel/naja_ff_scan.patch b/bazel/naja_ff_scan.patch deleted file mode 100644 index 915dfbb5..00000000 --- a/bazel/naja_ff_scan.patch +++ /dev/null @@ -1,175 +0,0 @@ ---- test/nl/formats/liberty/BUILD.bazel -+++ test/nl/formats/liberty/BUILD.bazel -@@ -18,0 +19,5 @@ -+exports_files( -+ ["benchmarks/tests/FF_scan.lib"], -+ visibility = ["//visibility:public"], -+) -+ ---- src/core/BUILD.bazel -+++ src/core/BUILD.bazel -@@ -3,3 +3,5 @@ - # SPDX-License-Identifier: Apache-2.0 -- -+ -+load("@kepler-formal//bazel:naja_cc_library.bzl", "cc_library") -+ - # Mirrors this directory's own CMakeLists.txt: builds the `naja_core` ---- src/dnl/BUILD.bazel -+++ src/dnl/BUILD.bazel -@@ -3,3 +3,5 @@ - # SPDX-License-Identifier: Apache-2.0 -- -+ -+load("@kepler-formal//bazel:naja_cc_library.bzl", "cc_library") -+ - # Mirrors this directory's own CMakeLists.txt: builds the `naja_dnl` ---- src/metrics/BUILD.bazel -+++ src/metrics/BUILD.bazel -@@ -3,3 +3,5 @@ - # SPDX-License-Identifier: Apache-2.0 -- -+ -+load("@kepler-formal//bazel:naja_cc_library.bzl", "cc_library") -+ - # Mirrors this directory's own CMakeLists.txt: builds the `naja_metrics` ---- src/bne/BUILD.bazel -+++ src/bne/BUILD.bazel -@@ -3,3 +3,5 @@ - # SPDX-License-Identifier: Apache-2.0 -- -+ -+load("@kepler-formal//bazel:naja_cc_library.bzl", "cc_library") -+ - # Mirrors this directory's own CMakeLists.txt: builds the `naja_bne` ---- src/nl/netlist/BUILD.bazel -+++ src/nl/netlist/BUILD.bazel -@@ -3,3 +3,5 @@ - # SPDX-License-Identifier: Apache-2.0 -- -+ -+load("@kepler-formal//bazel:naja_cc_library.bzl", "cc_library") -+ - # Mirrors this directory's own CMakeLists.txt: builds the `naja_nl` ---- src/optimization/BUILD.bazel -+++ src/optimization/BUILD.bazel -@@ -3,3 +3,5 @@ - # SPDX-License-Identifier: Apache-2.0 -- -+ -+load("@kepler-formal//bazel:naja_cc_library.bzl", "cc_library") -+ - # Mirrors this directory's own CMakeLists.txt: builds the `naja_opt` ---- src/nl/python/naja_wrapping/BUILD.bazel -+++ src/nl/python/naja_wrapping/BUILD.bazel -@@ -7,1 +7,5 @@ --# Mirrors this directory's own CMakeLists.txt: builds `naja_python` (the -+load("@kepler-formal//bazel:naja_cc_library.bzl", "cc_library") -+load("@kepler-formal//bazel:naja_includes.bzl", "NAJA_HEADER_COPTS") -+load("@rules_cc//cc:cc_binary.bzl", "cc_binary") -+ -+# Mirrors this directory's own CMakeLists.txt: builds `naja_python` (the -@@ -110,5 +114,8 @@ - exports_filter = [ - "//src:__subpackages__", - "@fmt//:fmt", -+ "@kepler-formal//bazel:hermetic_libcxx", -+ "@kepler-formal//bazel:hermetic_libcxxabi", -+ "@kepler-formal//bazel:hermetic_libunwind", - "@zlib//:z", - ], -@@ -122,6 +129,7 @@ - cc_binary( - name = "naja.so", - srcs = ["PyNaja.cpp"], -+ copts = NAJA_HEADER_COPTS, - dynamic_deps = [":naja_runtime"], - linkopts = select({ - # cc_binary's linkshared=True already implies -dynamiclib on ---- src/nl/python/pyloader/BUILD.bazel -+++ src/nl/python/pyloader/BUILD.bazel -@@ -3,3 +3,5 @@ - # SPDX-License-Identifier: Apache-2.0 -- -+ -+load("@kepler-formal//bazel:naja_cc_library.bzl", "cc_library") -+ - # Mirrors this directory's own CMakeLists.txt: builds `naja_snl_pyloader`. ---- src/nl/netlist/serialization/capnp/BUILD.bazel -+++ src/nl/netlist/serialization/capnp/BUILD.bazel -@@ -3,3 +3,5 @@ - # SPDX-License-Identifier: Apache-2.0 -- -+ -+load("@kepler-formal//bazel:naja_cc_library.bzl", "cc_library") -+ - # Mirrors this directory's own CMakeLists.txt: builds the `naja_nl_dump` ---- src/nl/formats/verilog/BUILD.bazel -+++ src/nl/formats/verilog/BUILD.bazel -@@ -3,3 +3,5 @@ - # SPDX-License-Identifier: Apache-2.0 -- -+ -+load("@kepler-formal//bazel:naja_cc_library.bzl", "cc_library") -+ - # Mirrors this directory's own CMakeLists.txt: builds the `naja_snl_verilog` ---- src/nl/formats/liberty/BUILD.bazel -+++ src/nl/formats/liberty/BUILD.bazel -@@ -3,3 +3,5 @@ - # SPDX-License-Identifier: Apache-2.0 -- -+ -+load("@kepler-formal//bazel:naja_cc_library.bzl", "cc_library") -+ - # Mirrors this directory's own CMakeLists.txt: builds the ---- src/nl/formats/systemverilog/BUILD.bazel -+++ src/nl/formats/systemverilog/BUILD.bazel -@@ -3,3 +3,5 @@ - # SPDX-License-Identifier: Apache-2.0 -- -+ -+load("@kepler-formal//bazel:naja_cc_library.bzl", "cc_library") -+ - # Mirrors this directory's own CMakeLists.txt: builds the ---- thirdparty/yosys-liberty/src/BUILD.bazel -+++ thirdparty/yosys-liberty/src/BUILD.bazel -@@ -3,3 +3,5 @@ - # SPDX-License-Identifier: Apache-2.0 -- -+ -+load("@rules_cc//cc:cc_library.bzl", "cc_library") -+ - # Mirrors this directory's own CMakeLists.txt. YosysLibertyParser is a ---- thirdparty/spdlog-1.17.0/BUILD.bazel -+++ thirdparty/spdlog-1.17.0/BUILD.bazel -@@ -3,3 +3,5 @@ - # SPDX-License-Identifier: Apache-2.0 -- -+ -+load("@rules_cc//cc:cc_library.bzl", "cc_library") -+ - # Vendored directly in this repo (not a submodule). naja only ever uses ---- src/nl/formats/hdl/BUILD.bazel -+++ src/nl/formats/hdl/BUILD.bazel -@@ -1,3 +1,5 @@ - # SPDX-License-Identifier: Apache-2.0 - -+load("@kepler-formal//bazel:naja_cc_library.bzl", "cc_library") -+ - cc_library( ---- src/nl/formats/vhdl/BUILD.bazel -+++ src/nl/formats/vhdl/BUILD.bazel -@@ -1,3 +1,5 @@ - # SPDX-License-Identifier: Apache-2.0 - -+load("@kepler-formal//bazel:naja_cc_library.bzl", "cc_library") -+ - cc_library( ---- src/vhdl/BUILD.bazel -+++ src/vhdl/BUILD.bazel -@@ -1,3 +1,5 @@ - # SPDX-License-Identifier: Apache-2.0 - -+load("@kepler-formal//bazel:naja_cc_library.bzl", "cc_library") -+ - cc_library( diff --git a/bazel/naja_includes.bzl b/bazel/naja_includes.bzl deleted file mode 100644 index 8b69188b..00000000 --- a/bazel/naja_includes.bzl +++ /dev/null @@ -1,49 +0,0 @@ -"""Include flags for compiling Kepler targets against Bazel-fetched Naja. - -Bazel's transitive `includes` are emitted as system include paths. On macOS a -host-installed Naja under /usr/local/include can otherwise win the short -`#include "DNL.h"` lookup before the fetched @naja headers are considered. - -The -iquote prefix is derived from @naja's repo mapping instead of a -hardcoded canonical repo name: as the root module the repo materializes at -external/+deps+naja, but in a downstream consumer it is -external/++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..af21ddfa --- /dev/null +++ b/bazel/registry/README.md @@ -0,0 +1,57 @@ +# In-tree Bazel registry + +kepler-formal's `MODULE.bazel` contains only `bazel_dep`s. Modules that +are not (yet) on the [Bazel Central Registry](https://registry.bazel.build/) +are served from this directory, which `.bazelrc` lists ahead of BCR: + +``` +common --registry=file://%workspace%/bazel/registry +common --registry=https://bcr.bazel.build/ +``` + +| Module | Why it is here | +|---|---| +| `cadical`, `glucose`, `kissat` | not on BCR; upstream has no Bazel build, so the entries carry `overlay/BUILD.bazel` | +| `naja` | not on BCR | +| `naja-if`, `naja-verilog`, `sv-lang`, `bison` | naja's dependencies, copied from naja's own `bazel/registry/` (`bison` 3.8.2.bcr.10 is BCR's bcr.9 with a fix for hermetic-llvm, see naja's README) | + +The layout is exactly BCR's (`modules//metadata.json`, +`modules///{MODULE.bazel,source.json,presubmit.yml,overlay/,patches/}`), +so publishing a module is a matter of copying its directory into a +[bazel-central-registry](https://github.com/bazelbuild/bazel-central-registry) +pull request, then deleting it here. As in BCR, `overlay/MODULE.bazel` is +a symlink to the version's `MODULE.bazel`. + +Unreleased commits use BCR's `--` version +scheme, e.g. `4.2.1-20251230-674dbba`. + +## Updating a module + +1. Add `modules///` with a `MODULE.bazel` whose + `module(version = ...)` matches the directory name, plus any + `overlay/` files or `patches/` (applied with `-p1`). +2. Add the version to `modules//metadata.json`. +3. Write `source.json`: + + ``` + bazel/registry/update_source.py [] + ``` + + Rerun it after editing an overlay file or patch; it records their + integrity hashes too. +4. Point the `bazel_dep` in `MODULE.bazel` at the new version. + +When bumping naja, also copy over any `naja-if`, `naja-verilog` or +`sv-lang` versions its `MODULE.bazel` now asks for from naja's +`bazel/registry/modules/`. + +## Depending on kepler-formal from another module + +A module that depends on kepler-formal needs these registry entries too. +Either copy `modules/` into its own registry, or list this one by a +pinned URL, as `.github/consumer-test` does with a local path: + +``` +common --registry=https://raw.githubusercontent.com/keplertech/kepler-formal//bazel/registry/ +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/bison/3.8.2.bcr.10/MODULE.bazel b/bazel/registry/modules/bison/3.8.2.bcr.10/MODULE.bazel new file mode 100644 index 00000000..ffdf008f --- /dev/null +++ b/bazel/registry/modules/bison/3.8.2.bcr.10/MODULE.bazel @@ -0,0 +1,13 @@ +"""https://www.gnu.org/software/bison/""" + +module( + name = "bison", + version = "3.8.2.bcr.10", + bazel_compatibility = [">=7.2.1"], +) + +bazel_dep(name = "bazel_skylib", version = "1.8.2") +bazel_dep(name = "platforms", version = "1.0.0") +bazel_dep(name = "rules_cc_autoconf", version = "0.19.0") +bazel_dep(name = "rules_cc", version = "0.2.4") +bazel_dep(name = "m4", version = "1.4.21.bcr.4") diff --git a/bazel/registry/modules/bison/3.8.2.bcr.10/overlay/BUILD.bazel b/bazel/registry/modules/bison/3.8.2.bcr.10/overlay/BUILD.bazel new file mode 100644 index 00000000..2d6016ab --- /dev/null +++ b/bazel/registry/modules/bison/3.8.2.bcr.10/overlay/BUILD.bazel @@ -0,0 +1,1108 @@ +load("@bazel_skylib//rules:write_file.bzl", "write_file") +load("@rules_cc//cc:cc_binary.bzl", "cc_binary") +load("@rules_cc//cc:cc_library.bzl", "cc_library") +load("@rules_cc_autoconf//autoconf:autoconf.bzl", "autoconf") +load("@rules_cc_autoconf//autoconf:autoconf_hdr.bzl", "autoconf_hdr") +load("@rules_cc_autoconf//autoconf:autoconf_srcs.bzl", "autoconf_srcs") +load("@rules_cc_autoconf//autoconf:checks.bzl", "checks") +load("@rules_cc_autoconf//autoconf:package_info.bzl", "package_info") + +LOCAL_DEFINES = [ + "HAVE_CONFIG_H", +] + select({ + "@platforms//os:macos": [ + "_DARWIN_C_SOURCE", + ], + "//conditions:default": [], +}) + +GENERATED_SRCS = { + "lib/alloca.h": "lib/alloca.in.h", + "lib/fcntl.h": "lib/fcntl.in.h", + "lib/getopt-cdefs.h": "lib/getopt-cdefs.in.h", + "lib/getopt.h": "lib/getopt.in.h", + "lib/iconv.h": "lib/iconv.in.h", + "lib/inttypes.h": "lib/inttypes.in.h", + "lib/limits.h": "lib/limits.in.h", + "lib/locale.h": "lib/locale.in.h", + "lib/malloc/scratch_buffer.gl.h": "lib/malloc/scratch_buffer.h", + "lib/math.h": "lib/math.in.h", + "lib/sched.h": "lib/sched.in.h", + "lib/signal.h": "lib/signal.in.h", + "lib/spawn.h": "lib/spawn.in.h", + "lib/stdalign.h": "lib/stdalign.in.h", + "lib/stddef.h": "lib/stddef.in.h", + "lib/stdint.h": "lib/stdint.in.h", + "lib/stdio.h": "lib/stdio.in.h", + "lib/stdlib.h": "lib/stdlib.in.h", + "lib/string.h": "lib/string.in.h", + "lib/strings.h": "lib/strings.in.h", + "lib/sys/ioctl.h": "lib/sys_ioctl.in.h", + "lib/sys/resource.h": "lib/sys_resource.in.h", + "lib/sys/stat.h": "lib/sys_stat.in.h", + "lib/sys/time.h": "lib/sys_time.in.h", + "lib/sys/times.h": "lib/sys_times.in.h", + "lib/sys/types.h": "lib/sys_types.in.h", + "lib/sys/wait.h": "lib/sys_wait.in.h", + "lib/termios.h": "lib/termios.in.h", + "lib/textstyle.h": "lib/textstyle.in.h", + "lib/time.h": "lib/time.in.h", + "lib/unistd.h": "lib/unistd.in.h", + "lib/unistr.h": "lib/unistr.in.h", + "lib/unitypes.h": "lib/unitypes.in.h", + "lib/uniwidth.h": "lib/uniwidth.in.h", + "lib/wchar.h": "lib/wchar.in.h", + "lib/wctype.h": "lib/wctype.in.h", +} + +BISON_UNIQUE_M4_FILES = [ + "m4/bison-check-compiler-flag.m4", + "m4/bison-cxx-std.m4", + "m4/c-working.m4", + "m4/cxx.m4", + "m4/flex.m4", + "m4/gnulib-comp.m4", + "m4/m4.m4", + "m4/printf-posix-rpl.m4", + "m4/wchar_t.m4", + "m4/year2038.m4", +] + +# Gnulib m4 modules used by bison (from m4/gnulib-comp.m4) +# Note: 00gnulib is required for proper template processing +GNULIB_M4_DEPS = [ + "@rules_cc_autoconf//gnulib/m4/{}".format(file[len("m4/"):-len(".m4")]) + for file in glob( + include = ["m4/*.m4"], + exclude = BISON_UNIQUE_M4_FILES, + ) +] + +# Package information from configure.ac +package_info( + name = "bison_package_info", + package_name = "GNU Bison", + aliases = { + "VERSION": "PACKAGE_VERSION", + }, + module_bazel = "MODULE.bazel", + package_bugreport = "bug-bison@gnu.org", + package_url = "https://www.gnu.org/software/bison/", + strip_bcr_version = True, +) + +autoconf( + name = "m4_bison-check-compiler-flag", + checks = [], +) + +autoconf( + name = "m4_bison-cxx-std", + checks = [ + # BISON_CXXSTD from m4/bison-cxx-std.m4 (configure.ac lines 77-83) + # Tests compiler flags and AC_SUBSTs CXX_CXXFLAGS + # In Bazel, C++ standard is set via toolchain, but we provide flags for Makefile compatibility + checks.AC_SUBST("CXX98_CXXFLAGS", "-std=c++98"), + checks.AC_SUBST("CXX03_CXXFLAGS", "-std=c++03"), + checks.AC_SUBST("CXX11_CXXFLAGS", "-std=c++11"), + checks.AC_SUBST("CXX14_CXXFLAGS", "-std=c++14"), + checks.AC_SUBST("CXX17_CXXFLAGS", "-std=c++17"), + checks.AC_SUBST("CXX20_CXXFLAGS", "-std=c++20"), + checks.AC_SUBST("CXX2B_CXXFLAGS", "-std=c++2b"), + ], +) + +# Checks from m4/c-working.m4 +# BISON_TEST_FOR_WORKING_C_COMPILER - line 233 +# BISON_C_COMPILER_POSIXLY_CORRECT - line 234 +autoconf( + name = "m4_c-working", + checks = [ + # BISON_TEST_FOR_WORKING_C_COMPILER + # Test that C compiler can compile a simple program + # AC_SUBST BISON_C_WORKS to ":" (colon means true in shell) + checks.AC_SUBST("BISON_C_WORKS", ":"), + # BISON_C_COMPILER_POSIXLY_CORRECT + # Check if C compiler supports -g in POSIXLY_CORRECT mode + # AC_SUBST C_COMPILER_POSIXLY_CORRECT to "true" or "false" + checks.AC_SUBST("C_COMPILER_POSIXLY_CORRECT", "true"), + ], +) + +# Checks from m4/cxx.m4 +# BISON_TEST_FOR_WORKING_CXX_COMPILER - line 235 +# BISON_CXX_COMPILER_POSIXLY_CORRECT - line 236 +autoconf( + name = "m4_cxx", + checks = [ + # BISON_TEST_FOR_WORKING_CXX_COMPILER + # Test that C++ compiler can compile and link a simple program + # AC_SUBST BISON_CXX_WORKS to ":" (if works), "false" (if doesn't), or ":" (if cross-compiling) + checks.AC_SUBST("BISON_CXX_WORKS", ":"), + # BISON_CXX_COMPILER_POSIXLY_CORRECT + # Check if C++ compiler supports -g in POSIXLY_CORRECT mode + # AC_SUBST CXX_COMPILER_POSIXLY_CORRECT to "true" or "false" + checks.AC_SUBST("CXX_COMPILER_POSIXLY_CORRECT", "true"), + ], +) + +# Note: m4_bison_cxx_std checks are now in m4_bison-cxx-std (the canonical target name) + +# Checks from m4/flex.m4 +# AC_PROG_LEX - line 258 +autoconf( + name = "m4_flex", + checks = [ + # Look for flex or lex program + # AC_SUBST LEX - path to lex/flex program + checks.AC_SUBST("LEX", "flex"), + # AC_SUBST LEX_IS_FLEX - true or false + checks.AC_SUBST("LEX_IS_FLEX", "true"), + # AC_SUBST FLEX_SUPPORTS_HEADER_OPT - true or false + checks.AC_SUBST("FLEX_SUPPORTS_HEADER_OPT", "true"), + # AC_SUBST LEX_OUTPUT_ROOT - lex.yy or lexyy + checks.AC_SUBST("LEX_OUTPUT_ROOT", "lex.yy"), + # AC_SUBST LEXLIB - -lfl, -ll, or empty + checks.AC_SUBST("LEXLIB", ""), + # AC_DEFINE YYTEXT_POINTER if yytext is a pointer + checks.AC_DEFINE("YYTEXT_POINTER", "1"), + ], +) + +autoconf( + name = "m4_gnulib-comp", + checks = [ + checks.AC_DEFINE( + "GNULIB_XALLOC", + 1, + subst = True, + ), + checks.AC_DEFINE( + "GNULIB_XALLOC_DIE", + 1, + subst = True, + ), + checks.AC_DEFINE( + "GNULIB_STDIO_SINGLE_THREAD", + 1, + subst = True, + ), + checks.AC_DEFINE( + "USE_UNLOCKED_IO", + "GNULIB_STDIO_SINGLE_THREAD", + ), + # ====================================================================== + # Module indicators from gnulib-comp.m4 + # These override the defaults (0) set by upstream header modules to + # activate gnulib module functionality in generated replacement headers. + # ====================================================================== + + # --- gl_MODULE_INDICATOR (AC_DEFINE in config.h) --- + checks.AC_DEFINE("GNULIB_CANONICALIZE", 1), + checks.AC_DEFINE("GNULIB_CANONICALIZE_LGPL", 1), + checks.AC_DEFINE("GNULIB_CLOEXEC", 1), + checks.AC_DEFINE("GNULIB_CLOSE_STREAM", 1), + checks.AC_DEFINE("GNULIB_DIRNAME", 1), + checks.AC_DEFINE("GNULIB_FD_SAFER_FLAG", 1), + checks.AC_DEFINE("GNULIB_FOPEN_GNU", 1), + checks.AC_DEFINE("GNULIB_FOPEN_SAFER", 1), + checks.AC_DEFINE("GNULIB_GETCWD", 1), + checks.AC_DEFINE("GNULIB_LOCK", 1), + checks.AC_DEFINE("GNULIB_MSVC_NOTHROW", 1), + checks.AC_DEFINE("GNULIB_OPENAT", 1), + checks.AC_DEFINE("GNULIB_PIPE2_SAFER", 1), + checks.AC_DEFINE("GNULIB_REALLOCARRAY", 1), + checks.AC_DEFINE("GNULIB_SNPRINTF", 1), + checks.AC_DEFINE("GNULIB_STRERROR", 1), + checks.AC_DEFINE("GNULIB_STRERROR_R_POSIX", 1), + checks.AC_DEFINE("GNULIB_UNISTR_U8_MBTOUCR", 1), + checks.AC_DEFINE("GNULIB_UNISTR_U8_UCTOMB", 1), + checks.AC_DEFINE("GNULIB_FSCANF", 1), + checks.AC_DEFINE("GNULIB_SCANF", 1), + checks.AC_DEFINE("GNULIB_VFPRINTF_POSIX", 1), + checks.AC_DEFINE("GNULIB_FDOPENDIR", 1), + + # --- gl_STDIO_MODULE_INDICATOR (AC_SUBST for stdio.in.h) --- + checks.AC_SUBST("GNULIB_FOPEN", 1), + checks.AC_SUBST("GNULIB_FPRINTF", 1), + checks.AC_SUBST("GNULIB_FPRINTF_POSIX", 1), + checks.AC_SUBST("GNULIB_FGETC", 1), + checks.AC_SUBST("GNULIB_FGETS", 1), + checks.AC_SUBST("GNULIB_FPUTC", 1), + checks.AC_SUBST("GNULIB_FPUTS", 1), + checks.AC_SUBST("GNULIB_FREAD", 1), + checks.AC_SUBST("GNULIB_FSCANF", 1), + checks.AC_SUBST("GNULIB_FWRITE", 1), + checks.AC_SUBST("GNULIB_GETC", 1), + checks.AC_SUBST("GNULIB_GETCHAR", 1), + checks.AC_SUBST("GNULIB_GETDELIM", 1), + checks.AC_SUBST("GNULIB_GETLINE", 1), + checks.AC_SUBST("GNULIB_OBSTACK_PRINTF", 1), + checks.AC_SUBST("GNULIB_PERROR", 1), + checks.AC_SUBST("GNULIB_PRINTF", 1), + checks.AC_SUBST("GNULIB_PRINTF_POSIX", 1), + checks.AC_SUBST("GNULIB_PUTC", 1), + checks.AC_SUBST("GNULIB_PUTCHAR", 1), + checks.AC_SUBST("GNULIB_PUTS", 1), + checks.AC_SUBST("GNULIB_RENAME", 1), + checks.AC_SUBST("GNULIB_SCANF", 1), + checks.AC_SUBST("GNULIB_SNPRINTF", 1), + checks.AC_SUBST("GNULIB_SPRINTF_POSIX", 1), + checks.AC_SUBST("GNULIB_VASPRINTF", 1), + checks.AC_SUBST("GNULIB_VFPRINTF", 1), + checks.AC_SUBST("GNULIB_VFPRINTF_POSIX", 1), + checks.AC_SUBST("GNULIB_VPRINTF", 1), + checks.AC_SUBST("GNULIB_VSNPRINTF", 1), + checks.AC_SUBST("GNULIB_VSPRINTF_POSIX", 1), + + # --- gl_UNISTD_MODULE_INDICATOR (AC_SUBST for unistd.in.h) --- + # Note: GNULIB_ACCESS is set only for Windows (see select below) + # because MSVC's _access() doesn't support X_OK (mode=1), returning + # EINVAL. The gnulib access replacement (lib/access.c) converts + # X_OK to R_OK. On macOS/Linux the system access() works fine, and + # leaving GNULIB_ACCESS=0 avoids an rpl_access redirect conflict. + checks.AC_SUBST("GNULIB_CHDIR", 1), + checks.AC_SUBST("GNULIB_CLOSE", 1), + checks.AC_SUBST("GNULIB_DUP2", 1), + checks.AC_SUBST("GNULIB_ENVIRON", 1), + checks.AC_SUBST("GNULIB_FCHDIR", 1), + checks.AC_SUBST("GNULIB_FSYNC", 1), + checks.AC_SUBST("GNULIB_GETCWD", 1), + checks.AC_SUBST("GNULIB_GETDTABLESIZE", 1), + checks.AC_SUBST("GNULIB_GETOPT_POSIX", 1), + checks.AC_SUBST("GNULIB_PIPE", 1), + checks.AC_SUBST("GNULIB_PIPE2", 1), + checks.AC_SUBST("GNULIB_READLINK", 1), + checks.AC_SUBST("GNULIB_RMDIR", 1), + checks.AC_SUBST("GNULIB_UNLINK", 1), + checks.AC_SUBST("GNULIB_UNISTD_H_GETOPT", 1), + + # --- gl_STDLIB_MODULE_INDICATOR (AC_SUBST for stdlib.in.h) --- + checks.AC_SUBST("GNULIB_CALLOC_POSIX", 1), + checks.AC_SUBST("GNULIB_CANONICALIZE_FILE_NAME", 1), + checks.AC_SUBST("GNULIB_FREE_POSIX", 1), + checks.AC_SUBST("GNULIB_MALLOC_POSIX", 1), + checks.AC_SUBST("GNULIB_REALLOCARRAY", 1), + checks.AC_SUBST("GNULIB_REALLOC_POSIX", 1), + checks.AC_SUBST("GNULIB_REALPATH", 1), + checks.AC_SUBST("GNULIB_STRTOD", 1), + checks.AC_SUBST("GNULIB_UNSETENV", 1), + + # --- gl_STRING_MODULE_INDICATOR (AC_SUBST for string.in.h) --- + checks.AC_SUBST("GNULIB_FFSL", 1), + checks.AC_SUBST("GNULIB_MEMCHR", 1), + checks.AC_SUBST("GNULIB_MEMPCPY", 1), + checks.AC_SUBST("GNULIB_MEMRCHR", 1), + checks.AC_SUBST("GNULIB_RAWMEMCHR", 1), + checks.AC_SUBST("GNULIB_STPCPY", 1), + checks.AC_SUBST("GNULIB_STPNCPY", 1), + checks.AC_SUBST("GNULIB_STRCHRNUL", 1), + checks.AC_SUBST("GNULIB_STRDUP", 1), + checks.AC_SUBST("GNULIB_STRERROR", 1), + checks.AC_SUBST("GNULIB_STRERROR_R", 1), + checks.AC_SUBST("GNULIB_STRNDUP", 1), + checks.AC_SUBST("GNULIB_STRNLEN", 1), + checks.AC_SUBST("GNULIB_STRVERSCMP", 1), + + # --- gl_MATH_MODULE_INDICATOR (AC_SUBST for math.in.h) --- + checks.AC_SUBST("GNULIB_FREXP", 1), + checks.AC_SUBST("GNULIB_FREXPL", 1), + checks.AC_SUBST("GNULIB_ISNAN", 1), + checks.AC_SUBST("GNULIB_ISNAND", 1), + checks.AC_SUBST("GNULIB_ISNANF", 1), + checks.AC_SUBST("GNULIB_ISNANL", 1), + checks.AC_SUBST("GNULIB_LDEXPL", 1), + checks.AC_SUBST("GNULIB_SIGNBIT", 1), + + # --- gl_WCHAR_MODULE_INDICATOR (AC_SUBST for wchar.in.h) --- + checks.AC_SUBST("GNULIB_MBRTOWC", 1), + checks.AC_SUBST("GNULIB_MBSINIT", 1), + checks.AC_SUBST("GNULIB_WCWIDTH", 1), + + # --- gl_WCTYPE_MODULE_INDICATOR (AC_SUBST for wctype.in.h) --- + checks.AC_SUBST("GNULIB_ISWBLANK", 1), + checks.AC_SUBST("GNULIB_ISWDIGIT", 1), + checks.AC_SUBST("GNULIB_ISWXDIGIT", 1), + + # --- gl_SPAWN_MODULE_INDICATOR (AC_SUBST for spawn.in.h) --- + checks.AC_SUBST("GNULIB_POSIX_SPAWN", 1), + checks.AC_SUBST("GNULIB_POSIX_SPAWN_FILE_ACTIONS_ADDCHDIR", 1), + checks.AC_SUBST("GNULIB_POSIX_SPAWN_FILE_ACTIONS_ADDCLOSE", 1), + checks.AC_SUBST("GNULIB_POSIX_SPAWN_FILE_ACTIONS_ADDDUP2", 1), + checks.AC_SUBST("GNULIB_POSIX_SPAWN_FILE_ACTIONS_ADDOPEN", 1), + checks.AC_SUBST("GNULIB_POSIX_SPAWN_FILE_ACTIONS_DESTROY", 1), + checks.AC_SUBST("GNULIB_POSIX_SPAWN_FILE_ACTIONS_INIT", 1), + checks.AC_SUBST("GNULIB_POSIX_SPAWNATTR_DESTROY", 1), + checks.AC_SUBST("GNULIB_POSIX_SPAWNATTR_INIT", 1), + checks.AC_SUBST("GNULIB_POSIX_SPAWNATTR_SETFLAGS", 1), + checks.AC_SUBST("GNULIB_POSIX_SPAWNATTR_SETPGROUP", 1), + checks.AC_SUBST("GNULIB_POSIX_SPAWNATTR_SETSIGMASK", 1), + checks.AC_SUBST("GNULIB_POSIX_SPAWNP", 1), + + # --- gl_SIGNAL_MODULE_INDICATOR (AC_SUBST for signal.in.h) --- + checks.AC_SUBST("GNULIB_RAISE", 1), + checks.AC_SUBST("GNULIB_SIGACTION", 1), + checks.AC_SUBST("GNULIB_SIGPROCMASK", 1), + + # --- gl_SYS_STAT_MODULE_INDICATOR (AC_SUBST for sys_stat.in.h) --- + checks.AC_SUBST("GNULIB_FSTAT", 1), + checks.AC_SUBST("GNULIB_FSTATAT", 1), + checks.AC_SUBST("GNULIB_LSTAT", 1), + checks.AC_SUBST("GNULIB_STAT", 1), + + # --- gl_SYS_TIME_MODULE_INDICATOR (AC_SUBST for sys_time.in.h) --- + checks.AC_SUBST("GNULIB_GETTIMEOFDAY", 1), + + # --- gl_SYS_RESOURCE_MODULE_INDICATOR --- + checks.AC_SUBST("GNULIB_GETRUSAGE", 1), + + # --- gl_SYS_WAIT_MODULE_INDICATOR (AC_SUBST for sys_wait.in.h) --- + checks.AC_SUBST("GNULIB_WAITPID", 1), + + # --- gl_FCNTL_MODULE_INDICATOR (AC_SUBST for fcntl.in.h) --- + checks.AC_SUBST("GNULIB_FCNTL", 1), + checks.AC_SUBST("GNULIB_OPEN", 1), + checks.AC_SUBST("GNULIB_OPENAT", 1), + + # --- gl_ICONV_MODULE_INDICATOR --- + checks.AC_SUBST("GNULIB_ICONV", 1), + + # --- gl_DIRENT_MODULE_INDICATOR --- + checks.AC_SUBST("GNULIB_CLOSEDIR", 1), + checks.AC_SUBST("GNULIB_DIRFD", 1), + checks.AC_SUBST("GNULIB_FDOPENDIR", 1), + checks.AC_SUBST("GNULIB_OPENDIR", 1), + checks.AC_SUBST("GNULIB_READDIR", 1), + checks.AC_SUBST("GNULIB_REWINDDIR", 1), + + # --- gl_LOCALE_MODULE_INDICATOR --- + checks.AC_SUBST("GNULIB_SETLOCALE_NULL", 1), + + # --- gl_STRINGS_MODULE_INDICATOR --- + checks.AC_SUBST("GNULIB_FFS", 1), + + # ====================================================================== + # Compatibility substitutions for older gnulib variable names used by + # bison 3.8.2 templates (newer gnulib uses _FOR_*_POSIX suffixed names) + # ====================================================================== + checks.AC_SUBST("REPLACE_CALLOC", 0), + checks.AC_SUBST("REPLACE_MALLOC", 0), + checks.AC_SUBST("REPLACE_REALLOC", 0), + ], +) + +# Checks from m4/m4.m4 +# AC_PROG_GNU_M4 - line 268 +autoconf( + name = "m4_m4", + checks = [ + # Look for GNU M4 1.4.6 or later + # AC_SUBST M4 - path to m4 program (used in Makefiles) + checks.AC_SUBST("M4", "m4"), + # AC_SUBST M4_GNU - --gnu or empty (used in Makefiles) + checks.AC_SUBST("M4_GNU", "--gnu"), + # AC_SUBST M4_DEBUGFILE - --debugfile or --error-output (used in Makefiles) + checks.AC_SUBST("M4_DEBUGFILE", "--debugfile"), + # AC_DEFINE_UNQUOTED M4_GNU_OPTION (configure.ac line 270-271) + # Note: M4 itself is AC_DEFINE_UNQUOTED in configure.ac, but we use AC_SUBST for Makefile compatibility + checks.AC_DEFINE("M4_GNU_OPTION", '"--gnu"'), + ], +) + +# Checks from m4/printf-posix-rpl.m4 +# gl_FUNC_PRINTF_POSIX - may be called via gnulib modules +autoconf( + name = "m4_printf-posix-rpl", + checks = [ + # Check if printf needs POSIX replacement + # AC_SUBST REPLACE_PRINTF - 0 or 1 + checks.AC_SUBST("REPLACE_PRINTF", "0"), + # AC_DEFINE REPLACE_PRINTF_POSIX - 0 or 1 + checks.AC_DEFINE("REPLACE_PRINTF_POSIX", "0"), + ], +) + +# Checks from m4/wchar_t.m4 +# gt_TYPE_WCHAR_T - may be called via gnulib +autoconf( + name = "m4_wchar_t", + checks = [ + # Check if has the wchar_t type + # AC_DEFINE HAVE_WCHAR_T - 1 if found (for C preprocessor) + checks.AC_DEFINE("HAVE_WCHAR_T", "1"), + # AC_SUBST for stddef.in.h template (@HAVE_WCHAR_T@ substitution) + checks.AC_SUBST("HAVE_WCHAR_T", 1), + ], +) + +# Checks from m4/year2038.m4 +# gl_YEAR2038_EARLY and gl_YEAR2038_BODY - may be called via gnulib +autoconf( + name = "m4_year2038", + checks = [ + # Check for time_t past year 2038 support + # On mingw, AC_DEFINE __MINGW_USE_VC2005_COMPAT + # For 32-bit systems, may need _TIME_BITS=64 and _FILE_OFFSET_BITS=64 + # Most 64-bit systems already have 64-bit time_t, so these are typically not needed + # AC_DEFINE _TIME_BITS and _FILE_OFFSET_BITS if needed (left empty for most systems) + ] + select({ + "@platforms//os:windows": [ + checks.AC_DEFINE("__MINGW_USE_VC2005_COMPAT", "1"), + ], + "//conditions:default": [], + }), +) + +BISON_UNIQUE_AUTOCONF_TARGETS = [ + # Strip `m4/` prefix and `.m4` suffix. + "m4_{}".format(file[3:-3]) + for file in BISON_UNIQUE_M4_FILES +] + +# Standard autoconf checks from configure.ac +# AC_CHECK_HEADERS_ONCE([locale.h]) - line 278 +# AC_C_INLINE - line 281 +# AC_CHECK_FUNCS_ONCE([setlocale]) - line 288 +autoconf( + name = "configure_ac", + checks = [ + # checks.AC_C_INLINE(), + checks.AC_CHECK_FUNC("setlocale"), + checks.AC_SUBST("GUARD_PREFIX", "GL"), + checks.AC_SUBST("GNULIB_LOCALENAME", 0), + checks.AC_DEFINE("M4", '"/usr/bin/m4"'), + checks.AC_DEFINE("PACKAGE_COPYRIGHT_YEAR", 2026), + + # Checks from m4/bison-i18n.m4 (BISON_I18N - configure.ac line 295) + # Internationalization support (simplified - assumes no NLS for cross-platform build) + checks.AC_DEFINE("YYENABLE_NLS", "0"), + checks.AC_SUBST("BISON_USE_NLS", "no"), + checks.AC_SUBST("BISON_LOCALEDIR", ""), + + # ================================================================= + # Header availability probes (HAVE_*_H) + # + # The generated lib/.h wrappers expand to `#include_next ` + # when HAVE__H=1, otherwise they fall back to a gnulib-provided + # replacement. rules_cc_autoconf's gnulib *_DEFAULTS targets + # hard-code HAVE__H=1, which breaks on toolchains lacking the + # POSIX header set (most prominently MSVC and clang-cl on Windows, + # where `os:windows` selects can't discriminate from MinGW). + # Probe the real toolchain so subsequent substitutions and config.h + # entries reflect what's actually available. + # ================================================================= + ] + [ + # Bind each HAVE_*_H subst to the cache variable already populated + # by the corresponding gnulib m4 module (transitively in `deps` + # via GNULIB_M4_DEPS). These modules probe the header but don't + # emit the AC_SUBST themselves, so without these overrides the + # subst falls back to the bogus HAVE_*_H=1 baked into the matching + # *_DEFAULTS target — which breaks generated wrappers on + # toolchains lacking the header (notably MSVC and clang-cl on + # Windows, where an `os:windows` select can't discriminate from + # MinGW). + # + # Headers NOT listed here: + # - alloca.h, getopt.h, sched.h, spawn.h, strings.h, sys/ioctl.h, + # sys/resource.h, sys/times.h, unistd.h: the matching gnulib + # m4 module already emits an AC_SUBST tied to the probe — + # re-substing here would collide. + checks.AC_SUBST( + name, + condition = cache, + ) + for name, cache in [ + ("HAVE_FCNTL_H", "ac_cv_header_fcntl_h"), + ("HAVE_ICONV_H", "ac_cv_header_iconv_h"), + ("HAVE_SYS_TIME_H", "ac_cv_header_sys_time_h"), + ("HAVE_SYS_WAIT_H", "ac_cv_header_sys_wait_h"), + ("HAVE_TERMIOS_H", "ac_cv_header_termios_h"), + ] + ] + [ + # ================================================================= + # Gnulib conditional source compilation gates (COMPILE_* variables) + # These determine which replacement sources to compile based on + # function availability. COMPILE_*=1 means the function is MISSING + # and the gnulib replacement should be compiled. + # ================================================================= + + # rawmemchr — GNU extension, missing on macOS + checks.AC_TRY_LINK( + name = "bison_cv_func_rawmemchr", + code = """\ +#define _GNU_SOURCE 1 +#include +int main(void) { (void)rawmemchr; return 0; } +""", + ), + checks.AC_SUBST( + "COMPILE_RAWMEMCHR", + condition = "!bison_cv_func_rawmemchr", + ), + checks.AC_SUBST( + "COMPILE_MEMPCPY", + condition = "!ac_cv_func_mempcpy", + ), + checks.AC_SUBST("COMPILE_REALLOCARRAY", "1"), + checks.AC_TRY_LINK( + name = "bison_cv_func_strverscmp", + code = """\ +#include +int main(void) { return strverscmp("1.0", "2.0"); } +""", + ), + checks.AC_SUBST( + "COMPILE_STRVERSCMP", + condition = "!bison_cv_func_strverscmp", + ), + # Drive HAVE_DECL_STRVERSCMP from the same probe so the gnulib + # string.h wrapper emits a declaration on toolchains that lack it + # (e.g. the Windows CRT under MSVC / clang-cl, where the implicit + # declaration is a C99 error). + checks.AC_SUBST( + "HAVE_DECL_STRVERSCMP", + condition = "bison_cv_func_strverscmp", + ), + checks.AC_TRY_LINK( + name = "bison_cv_func_canonicalize_file_name", + code = """\ +#ifdef __cplusplus +extern "C" +#endif +char *canonicalize_file_name(const char *); +int main(void) { return canonicalize_file_name(".") != 0; } +""", + ), + checks.AC_SUBST( + "COMPILE_CANONICALIZE_LGPL", + condition = "!bison_cv_func_canonicalize_file_name", + ), + + # error.c — compiled when error_at_line() is missing (macOS) + checks.AC_CHECK_FUNC("error_at_line"), + checks.AC_SUBST( + "COMPILE_ERROR", + condition = "!ac_cv_func_error_at_line", + ), + + # fpending.c — compiled when __fpending() is missing (macOS) + checks.AC_TRY_LINK( + name = "bison_cv_func___fpending", + code = """\ +#include +#if HAVE_STDIO_EXT_H +# include +#endif +int main(void) { return ! __fpending(stdin); } +""", + ), + checks.AC_SUBST( + "COMPILE_FPENDING", + condition = "!bison_cv_func___fpending", + ), + + # fseterr.c — compiled when __fseterr() is missing (macOS) + checks.AC_TRY_LINK( + name = "bison_cv_func___fseterr", + code = """\ +#include +#ifdef __cplusplus +extern "C" +#endif +void __fseterr(FILE *); +int main(void) { __fseterr(stdin); return 0; } +""", + ), + checks.AC_SUBST( + "COMPILE_FSETERR", + condition = "!bison_cv_func___fseterr", + ), + checks.AC_SUBST("COMPILE_OBSTACK_PRINTF", "1"), + ] + select({ + "@platforms//os:linux": [ + # getopt: __GETOPT_PREFIX=rpl_ always set → replacement always needed + checks.AC_SUBST("COMPILE_GETOPT", "1"), + checks.AC_SUBST("COMPILE_OPEN", "0"), + checks.AC_SUBST("COMPILE_UNLINK", "0"), + checks.AC_SUBST("COMPILE_STRERROR_OVERRIDE", "0"), + checks.AC_SUBST("COMPILE_MBRTOWC", "1"), + checks.AC_SUBST("COMPILE_SPAWN_FACTION_ADDCHDIR", "1"), + ], + "@platforms//os:macos": [ + checks.AC_SUBST("COMPILE_GETOPT", "1"), + checks.AC_SUBST("COMPILE_OPEN", "1"), + checks.AC_SUBST("COMPILE_UNLINK", "1"), + checks.AC_SUBST("COMPILE_STRERROR_OVERRIDE", "1"), + checks.AC_SUBST("COMPILE_MBRTOWC", "0"), + checks.AC_SUBST("COMPILE_SPAWN_FACTION_ADDCHDIR", "1"), + ], + "@platforms//os:windows": [ + checks.AC_SUBST("COMPILE_GETOPT", "1"), + checks.AC_SUBST("COMPILE_OPEN", "0"), + checks.AC_SUBST("COMPILE_UNLINK", "0"), + checks.AC_SUBST("COMPILE_STRERROR_OVERRIDE", "0"), + checks.AC_SUBST("COMPILE_MBRTOWC", "0"), + checks.AC_SUBST("COMPILE_SPAWN_FACTION_ADDCHDIR", "1"), + # Override string_h toolchain defaults for POSIX functions missing + # on Windows. Without these the generated string.h skips their + # declarations, causing implicit-int errors on MSVC. + checks.AC_SUBST("HAVE_STPCPY", 0), + checks.AC_SUBST("HAVE_STPNCPY", 0), + # MSVC's _access() doesn't support X_OK (mode=1) and returns + # EINVAL. Enable gnulib access replacement (lib/access.c) which + # converts X_OK to R_OK before calling _access(). + checks.AC_SUBST("GNULIB_ACCESS", 1), + ], + "//conditions:default": [ + checks.AC_SUBST("COMPILE_GETOPT", "1"), + checks.AC_SUBST("COMPILE_OPEN", "0"), + checks.AC_SUBST("COMPILE_UNLINK", "0"), + checks.AC_SUBST("COMPILE_STRERROR_OVERRIDE", "0"), + checks.AC_SUBST("COMPILE_MBRTOWC", "0"), + checks.AC_SUBST("COMPILE_SPAWN_FACTION_ADDCHDIR", "1"), + ], + }), + deps = [ + ":bison_package_info", + ] + BISON_UNIQUE_AUTOCONF_TARGETS + GNULIB_M4_DEPS, +) + +# Generate header files from templates using autoconf_hdr +# These templates contain @PLACEHOLDER@ markers that need to be processed +[ + autoconf_hdr( + name = hdr[:-len(".h")] + "_h", + out = hdr, + defaults = True, + inlines = { + "/* The definition of _GL_ARG_NONNULL is copied here. */": "lib/arg-nonnull.h", + "/* The definition of _GL_WARN_ON_USE is copied here. */": "lib/warn-on-use.h", + "/* The definitions of _GL_FUNCDECL_RPL etc. are copied here. */": "lib/c++defs.h", + }, + mode = "subst", + substitutions = { + "libc_hidden_proto": "// libc_hidden_proto", + "__always_inline": "inline _GL_ATTRIBUTE_ALWAYS_INLINE", + "__glibc_likely": "_GL_LIKELY", + "__glibc_unlikely": "_GL_UNLIKELY", + }, + template = template, + deps = [":configure_ac"], + ) + for hdr, template in GENERATED_SRCS.items() +] + +autoconf_hdr( + name = "lib/config_h", + out = "lib/config.h", + template = "lib/config.in.h", + deps = [":configure_ac"], +) + +write_file( + name = "configmake_h_src", + out = "lib/configmake.h", + content = [ + "#define LOCALEDIR \"\"", + "#define PKGDATADIR \"bison/data\"", + "", + ], + newline = "unix", + tags = ["manual"], +) + +# Gnulib's wrapper headers (generated lib/stdio.h, lib/fcntl.h, ... plus +# the checked-in lib/*-safer.h helpers) must shadow the libc headers: they +# forward via #include_next and add gnulib decorations +# (_GL_ATTRIBUTE_DEALLOC etc.) that lib/ and src/ sources rely on. +# `includes = ["lib"]` emits -isystem, which loses against toolchains that +# inject libc headers as earlier -isystem entries (e.g. the zero-sysroot +# hermetic-llvm BCR toolchain). Plain -I outranks every -isystem (and a dir +# listed as both -I and -isystem stays -isystem, so the -isystem form must +# go entirely). This restores autotools' AM_CPPFLAGS = -I./lib ordering. +BISON_COPTS = [ + "-Iexternal/" + repo_name() + "/lib", + "-I$(BINDIR)/external/" + repo_name() + "/lib", +] + select({ + "@rules_cc//cc/compiler:clang": [ + "-w", + "-std=c11", + "-Wno-unused-but-set-variable", + ], + "@rules_cc//cc/compiler:gcc": [ + "-w", + "-std=c11", + ], + "@rules_cc//cc/compiler:msvc-cl": [ + # C4116: unnamed type definition in parentheses + "/wd4116", + ], + "//conditions:default": [], +}) + +# Gnulib conditional sources — each file is compiled only when its condition +# variable evaluates to true. Conditions come from three sources: +# - REPLACE_*: upstream gnulib modules (function exists but is buggy/missing) +# - COMPILE_*: configure_ac checks (function absent on platform) +# - ac_cv_define_REPLACE_POSIX_SPAWN: spawn subsystem needs full replacement +autoconf_srcs( + name = "gnulib_conditional_srcs", + srcs = { + # --- REPLACE_* gated (upstream gnulib decides) --- + "lib/asprintf.c": "REPLACE_VASPRINTF", + # --- COMPILE_* gated (function absent → replacement compiled) --- + "lib/canonicalize-lgpl.c": "COMPILE_CANONICALIZE_LGPL", + "lib/error.c": "COMPILE_ERROR", + "lib/fcntl.c": "REPLACE_FCNTL", + "lib/fopen.c": "REPLACE_FOPEN", + "lib/fpending.c": "COMPILE_FPENDING", + "lib/fprintf.c": "REPLACE_FPRINTF", + "lib/free.c": "REPLACE_FREE", + "lib/fseterr.c": "COMPILE_FSETERR", + "lib/fstat.c": "REPLACE_FSTAT", + "lib/getopt.c": "COMPILE_GETOPT", + "lib/getopt1.c": "COMPILE_GETOPT", + "lib/iconv_open.c": "REPLACE_ICONV_OPEN", + "lib/lstat.c": "REPLACE_LSTAT", + "lib/mbrtowc.c": "COMPILE_MBRTOWC", + "lib/mempcpy.c": "COMPILE_MEMPCPY", + "lib/obstack_printf.c": "COMPILE_OBSTACK_PRINTF", + "lib/open.c": "COMPILE_OPEN", + "lib/perror.c": "REPLACE_PERROR", + "lib/printf.c": "REPLACE_PRINTF", + "lib/rawmemchr.c": "COMPILE_RAWMEMCHR", + "lib/readlink.c": "REPLACE_READLINK", + "lib/reallocarray.c": "COMPILE_REALLOCARRAY", + "lib/rename.c": "REPLACE_RENAME", + "lib/snprintf.c": "REPLACE_SNPRINTF", + # --- Spawn replacement (all-or-nothing when REPLACE_POSIX_SPAWN=1) --- + "lib/spawn.c": "ac_cv_define_REPLACE_POSIX_SPAWN", + "lib/spawn_faction_addchdir.c": "COMPILE_SPAWN_FACTION_ADDCHDIR", + "lib/spawn_faction_addclose.c": "ac_cv_define_REPLACE_POSIX_SPAWN", + "lib/spawn_faction_adddup2.c": "ac_cv_define_REPLACE_POSIX_SPAWN", + "lib/spawn_faction_addopen.c": "ac_cv_define_REPLACE_POSIX_SPAWN", + "lib/spawn_faction_destroy.c": "ac_cv_define_REPLACE_POSIX_SPAWN", + "lib/spawn_faction_init.c": "ac_cv_define_REPLACE_POSIX_SPAWN", + "lib/spawnattr_destroy.c": "ac_cv_define_REPLACE_POSIX_SPAWN", + "lib/spawnattr_init.c": "ac_cv_define_REPLACE_POSIX_SPAWN", + "lib/spawnattr_setflags.c": "ac_cv_define_REPLACE_POSIX_SPAWN", + "lib/spawnattr_setpgroup.c": "ac_cv_define_REPLACE_POSIX_SPAWN", + "lib/spawnattr_setsigmask.c": "ac_cv_define_REPLACE_POSIX_SPAWN", + "lib/spawni.c": "ac_cv_define_REPLACE_POSIX_SPAWN", + "lib/spawnp.c": "ac_cv_define_REPLACE_POSIX_SPAWN", + "lib/sprintf.c": "REPLACE_SPRINTF", + "lib/stat.c": "REPLACE_STAT", + "lib/strchrnul.c": "REPLACE_STRCHRNUL", + "lib/strerror-override.c": "COMPILE_STRERROR_OVERRIDE", + "lib/strerror.c": "REPLACE_STRERROR", + "lib/strerror_r.c": "REPLACE_STRERROR_R", + "lib/strverscmp.c": "COMPILE_STRVERSCMP", + "lib/unlink.c": "COMPILE_UNLINK", + "lib/vasprintf.c": "REPLACE_VASPRINTF", + "lib/vfprintf.c": "REPLACE_VFPRINTF", + "lib/vsnprintf.c": "REPLACE_VSNPRINTF", + "lib/vsprintf.c": "REPLACE_VSPRINTF", + }, + defaults = True, + deps = [":configure_ac"], +) + +# Shared headers for lib/ targets (mirrors autotools AM_CPPFLAGS = -I./lib) +cc_library( + name = "headers", + hdrs = ["lib/config.h"] + [ + ":{}".format(hdr) + for hdr in GENERATED_SRCS.keys() + ] + glob( + include = ["lib/**/*.h"], + exclude = GENERATED_SRCS.keys() + [ + "lib/config.h", + "lib/configmake.h", + ], + ) + [ + "src/scan-code.c", + "src/scan-gram.c", + "src/scan-skel.c", + ":configmake_h_src", + ], + textual_hdrs = [ + "lib/timevar.def", + "lib/printf-frexp.c", + ], +) + +alias( + name = "libbison", + actual = ":lib/bison", +) + +# Unconditional sources are always compiled on all platforms. +# Conditional sources are gated by autoconf_srcs targets based on actual +# check results (REPLACE_*, HAVE_*), matching native autoconf behavior. +cc_library( + name = "lib/bison", + srcs = [ + # === Unconditional sources (from lib_libbison_a_SOURCES in gnulib.mk) === + "lib/allocator.c", + "lib/areadlink.c", + "lib/argmatch.c", + "lib/asnprintf.c", + "lib/basename.c", + "lib/basename-lgpl.c", + "lib/binary-io.c", + "lib/bitrotate.c", + "lib/bitset.c", + "lib/bitset/array.c", + "lib/bitset/list.c", + "lib/bitset/stats.c", + "lib/bitset/table.c", + "lib/bitset/vector.c", + "lib/bitsetv.c", + "lib/c-ctype.c", + "lib/c-strcasecmp.c", + "lib/c-strncasecmp.c", + "lib/canonicalize.c", + "lib/careadlinkat.c", + "lib/cloexec.c", + "lib/close-stream.c", + "lib/closeout.c", + "lib/concat-filename.c", + "lib/dirname.c", + "lib/dirname-lgpl.c", + "lib/dup-safer.c", + "lib/dup-safer-flag.c", + "lib/execute.c", + "lib/exitfail.c", + "lib/fatal-signal.c", + "lib/fd-safer.c", + "lib/fd-safer-flag.c", + "lib/file-set.c", + "lib/findprog-in.c", + "lib/fopen-safer.c", + "lib/fstrcmp.c", + "lib/get-errno.c", + "lib/gethrxtime.c", + "lib/getprogname.c", + "lib/gettime.c", + "lib/gl_array_list.c", + "lib/gl_hash_map.c", + "lib/gl_linked_list.c", + "lib/gl_list.c", + "lib/gl_map.c", + "lib/gl_oset.c", + "lib/gl_rbtree_oset.c", + "lib/gl_rbtreehash_list.c", + "lib/gl_xlist.c", + "lib/gl_xmap.c", + "lib/glthread/lock.c", + "lib/glthread/threadlib.c", + "lib/glthread/tls.c", + "lib/hash.c", + "lib/hash-pjw.c", + "lib/hash-triple-simple.c", + "lib/ialloc.c", + "lib/integer_length.c", + "lib/integer_length_l.c", + "lib/localcharset.c", + "lib/malloc/scratch_buffer_dupfree.c", + "lib/malloc/scratch_buffer_grow.c", + "lib/malloc/scratch_buffer_grow_preserve.c", + "lib/malloc/scratch_buffer_set_array_size.c", + "lib/math.c", + "lib/mbchar.c", + "lib/mbfile.c", + "lib/mbswidth.c", + "lib/obstack.c", + "lib/path-join.c", + "lib/pipe-safer.c", + "lib/pipe2.c", + "lib/pipe2-safer.c", + "lib/printf-args.c", + "lib/printf-frexp.c", + "lib/printf-frexpl.c", + "lib/printf-parse.c", + "lib/progname.c", + "lib/quotearg.c", + "lib/readline.c", + "lib/sig-handler.c", + "lib/spawn-pipe.c", + "lib/stripslash.c", + "lib/timespec.c", + "lib/timevar.c", + "lib/unicodeio.c", + "lib/unistd.c", + "lib/unistr/u8-mbtoucr.c", + "lib/unistr/u8-uctomb.c", + "lib/unistr/u8-uctomb-aux.c", + "lib/uniwidth/width.c", + "lib/vasnprintf.c", + "lib/wait-process.c", + "lib/wctype-h.c", + "lib/xalloc-die.c", + "lib/xconcat-filename.c", + "lib/xhash.c", + "lib/xmalloc.c", + "lib/xmemdup0.c", + "lib/xreadlink.c", + "lib/xsize.c", + "lib/xstrndup.c", + "lib/xtime.c", + # Always-enabled gnulib modules (gl_GNULIB_ENABLED_* always true for bison) + "lib/hard-locale.c", + "lib/malloca.c", + "lib/setlocale_null.c", + "lib/stat-time.c", + ] + [ + ":gnulib_conditional_srcs", + ] + select({ + "@platforms//os:windows": [ + # gnulib access() replacement: converts X_OK to R_OK for MSVC + "lib/access.c", + # POSIX function replacements (missing on Windows) + "lib/ffsl.c", + "lib/fsync.c", + "lib/getdtablesize.c", + "lib/getrusage.c", + "lib/gettimeofday.c", + "lib/pipe.c", + "lib/sigaction.c", + "lib/sigprocmask.c", + "lib/stpcpy.c", + "lib/stpncpy.c", + "lib/strndup.c", + "lib/waitpid.c", + "lib/wcwidth.c", + # Windows-specific gnulib support + "lib/msvc-inval.c", + "lib/msvc-nothrow.c", + "lib/stat-w32.c", + "lib/windows-mutex.c", + "lib/windows-once.c", + "lib/windows-recmutex.c", + "lib/windows-rwlock.c", + "lib/windows-spawn.c", + "lib/windows-tls.c", + ], + "//conditions:default": [], + }), + copts = BISON_COPTS, + local_defines = LOCAL_DEFINES + [ + "DEFAULT_TEXT_DOMAIN=\\\"bison-gnulib\\\"", + ] + select({ + "@platforms//os:windows": [ + "SPAWN_PIPE_IMPL_AVOID_POSIX_SPAWN=1", + ], + "//conditions:default": [], + }), + deps = [":headers"], +) + +alias( + name = "liby", + actual = ":lib/y", +) + +cc_library( + name = "lib/y", + srcs = [ + "lib/main.c", + "lib/yyerror.c", + ], + copts = BISON_COPTS, + implementation_deps = [":headers"], + local_defines = LOCAL_DEFINES, +) + +BISON_SRC_SRCS = glob( + include = [ + "src/*.c", + ], + exclude = [ + "src/bazel_runfiles.cc", + "src/i18n-strings.c", + "src/scan-code.c", + "src/scan-gram.c", + "src/scan-skel.c", + "src/main.c", + ], +) + +BISON_HDRS_SRCS = glob( + include = ["src/*.h"], +) + +cc_library( + name = "bison_bazel_runfiles", + srcs = ["src/bazel_runfiles.cc"], + deps = ["@rules_cc//cc/runfiles"], +) + +# Runfiles for bison binary +filegroup( + name = "bison_data", + srcs = glob(["data/**/*"]) + [ + "@m4", + ], +) + +filegroup( + name = "bison_pkgdata", + srcs = glob(["data/**/*"]), + visibility = ["//visibility:public"], +) + +label_flag( + name = "m4", + build_setting_default = "@m4//:m4", + visibility = ["//visibility:public"], +) + +label_flag( + name = "bison_pkgdatadir", + build_setting_default = ":bison_pkgdata", + visibility = ["//visibility:public"], +) + +# Link options for different compilers +BISON_LINKOPTS = select({ + "@rules_cc//cc/compiler:msvc-cl": [ + # LNK4001: no object files specified; libraries used + "/IGNORE:4001", + ], + "//conditions:default": [], +}) + +# Bison binary +cc_binary( + name = "bin/bison", + srcs = BISON_SRC_SRCS + ["src/main.c"] + BISON_HDRS_SRCS, + copts = BISON_COPTS, + data = [":bison_data"], + includes = ["src"], + linkopts = BISON_LINKOPTS + select({ + "@platforms//os:linux": ["-lpthread"], + "@platforms//os:macos": ["-liconv"], + "//conditions:default": [], + }), + local_defines = LOCAL_DEFINES, + visibility = ["//visibility:public"], + deps = [ + ":bison_bazel_runfiles", + ":headers", + ":libbison", + ":liby", + ], +) + +alias( + name = "bison", + actual = ":bin/bison", + visibility = ["//visibility:public"], +) + +# Yacc binary (alias for bison) +alias( + name = "yacc", + actual = ":bin/bison", + visibility = ["//visibility:public"], +) diff --git a/bazel/registry/modules/bison/3.8.2.bcr.10/overlay/MODULE.bazel b/bazel/registry/modules/bison/3.8.2.bcr.10/overlay/MODULE.bazel new file mode 120000 index 00000000..9b599e3a --- /dev/null +++ b/bazel/registry/modules/bison/3.8.2.bcr.10/overlay/MODULE.bazel @@ -0,0 +1 @@ +../MODULE.bazel \ No newline at end of file diff --git a/bazel/registry/modules/bison/3.8.2.bcr.10/overlay/bison.bzl b/bazel/registry/modules/bison/3.8.2.bcr.10/overlay/bison.bzl new file mode 100644 index 00000000..56fc1d6a --- /dev/null +++ b/bazel/registry/modules/bison/3.8.2.bcr.10/overlay/bison.bzl @@ -0,0 +1,131 @@ +"""Rule for running GNU Bison with M4 and PKGDATADIR configured automatically.""" + +def _collect_tool_files(target): + """Collect files and default runfiles from a target into a depset for tools.""" + info = target[DefaultInfo] + transitive = [info.files] + if info.default_runfiles: + transitive.append(info.default_runfiles.files) + return depset(transitive = transitive) + +def _resolve_pkgdatadir(files): + """Derive the bison PKGDATADIR path from the provided files. + + If the label resolves to a single directory (TreeArtifact), its path is + used directly. Otherwise, a file within the data tree is located and its + path is truncated at the ``data`` component. + """ + if len(files) == 1 and files[0].is_directory: + return files[0].path + for f in files: + idx = f.path.find("/data/") + if idx >= 0: + return f.path[:idx + 5] + if f.path.startswith("data/"): + return "data" + fail("Could not determine BISON_PKGDATADIR: no 'data' directory found in provided files") + +def _arg_map_expand_outputs(value): + arg, out_map = value + for part, output in out_map.items(): + arg = arg.replace(part, output.path) + return arg + +def _bison_impl(ctx): + tool = ctx.executable.bison + m4 = ctx.file.m4 + pkgdatadir = _resolve_pkgdatadir(ctx.files.bison_pkgdatadir) + + env = { + "BISON_PKGDATADIR": pkgdatadir, + "M4": m4.path, + } + + out_map = {} + for file, label in zip(ctx.outputs.outs, ctx.attr.outs): + _, _, relative = str(label).partition("//") + out_map["$(execpath {})".format(label)] = file + out_map["$(execpath {})".format(relative)] = file + + args = ctx.actions.args() + for arg in ctx.attr.args: + args.add_all([(ctx.expand_location(arg, ctx.attr.srcs), out_map)], map_each = _arg_map_expand_outputs) + + tools = depset(transitive = [ + _collect_tool_files(ctx.attr.m4), + _collect_tool_files(ctx.attr.bison_pkgdatadir), + ]) + + ctx.actions.run( + executable = tool, + arguments = [args], + inputs = ctx.files.srcs, + tools = tools, + outputs = ctx.outputs.outs, + mnemonic = "Bison", + env = env, + ) + + return [DefaultInfo(files = depset(ctx.outputs.outs))] + +bison = rule( + doc = """\ +Runs GNU Bison on a grammar file to produce parser source and optionally a header. + +This rule configures `BISON_PKGDATADIR` and `M4` environment variables +automatically. The interface follows the same pattern as `bazel_skylib`'s +`run_binary`: provide `srcs`, `outs`, and `args` with `$(execpath ...)` +expansions for input and output paths. + +The m4 binary and bison data directory can be overridden globally via the +`//:m4` and `//:bison_pkgdatadir` label_flags, or per-target via the `m4` +and `bison_pkgdatadir` attrs. + +Example: + load("@bison//:bison.bzl", "bison") + + bison( + name = "parser", + srcs = ["parser.y"], + outs = ["parser.c", "parser.h"], + args = ["-o", "$(execpath parser.c)", "-d", "$(execpath parser.y)"], + ) +""", + implementation = _bison_impl, + attrs = { + "args": attr.string_list( + doc = "Arguments to pass to bison. Supports $(execpath ...) for input and output paths.", + mandatory = True, + ), + "bison": attr.label( + doc = "The bison binary to use.", + default = Label("//:bison"), + cfg = "exec", + executable = True, + ), + "bison_pkgdatadir": attr.label( + doc = """\ +Bison's data directory (containing m4sugar, skeletons, etc.). If this +resolves to a single directory, it is used directly. If it resolves to +files, the path is truncated at the `data` component. Override globally +with --@bison//:bison_pkgdatadir=