bazel: plain bazel_deps via an in-tree registry

.bazelignore

@@ -1,2 +1,4 @@
 thirdparty
-deps
+bazel/registry
+# A separate workspace, built from its own directory.
+.github/consumer-test

.bazelrc

@@ -1,3 +1,24 @@
+# naja's development pin comes from bazel/registry/ (until naja is on
+# BCR); versions not on BCR yet come from their open BCR pull requests,
+# each pinned to a commit (drop a line once its PR merges); everything
+# else from BCR.
+common --registry=file://%workspace%/bazel/registry
+#   bison 3.8.2.bcr.10                     bazelbuild/bazel-central-registry#10879
+#   sv-lang 11.0.0-20260701-b60d729d.bcr.1 bazelbuild/bazel-central-registry#10882
+#   naja-if 0.0.0-20260723-099677d9        bazelbuild/bazel-central-registry#10881
+#   naja-verilog 0.0.0-20260909-be6544b1   bazelbuild/bazel-central-registry#10885
+#   kissat 4.0.4                           bazelbuild/bazel-central-registry#10880
+#   cadical 3.0.0                          bazelbuild/bazel-central-registry#10883
+#   glucose 4.2.1-20251230-674dbba         bazelbuild/bazel-central-registry#10884
+common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/bb42d7dc14939aaf578926cf1c93bd987ca9fac7/
+common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/5888fdb942da7cf4a6eecd8d5bc07c777e82c4ee/
+common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/377d10e631e9461794687b9ff1d4bbbde0c9ad1d/
+common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/649d563703219943c013c9e5af8884ea81b2ab19/
+common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/985ff91136fd9c24be49d268c8f8acb416137a01/
+common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/cf30c24de5255b58a523064f8a624848b4bd1bab/
+common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/0dc1d20b35db8595fbaaf762dbf5046fb19ae188/
+common --registry=https://bcr.bazel.build/
+
 common --enable_platform_specific_config
 
 build --cxxopt=-std=c++20
@@ -10,10 +31,5 @@ build --workspace_status_command=tools/workspace_status.sh
 common:linux --repo_env=BAZEL_DO_NOT_DETECT_CPP_TOOLCHAIN=1
 build:linux --dynamic_mode=off
 
-# Force C11 for host tools to work around rules_foreign_cc pkg-config
-# bootstrap failure: bundled glib uses 'bool' as a struct field name,
-# which is a keyword in GCC 15's default C23 mode.
-build --host_conlyopt=-std=c11
-
 # Recommended: show test output on failure
 test --test_output=errors

.bcr/metadata.template.json

@@ -0,0 +1,20 @@
+{
+    "homepage": "https://github.com/keplertech/kepler-formal",
+    "maintainers": [
+        {
+            "github": "xtofalex",
+            "github_user_id": 3635601,
+            "name": "Christophe Alexandre"
+        },
+        {
+            "github": "nanocoh",
+            "github_user_id": 115838389,
+            "name": "Noam Cohen"
+        }
+    ],
+    "repository": [
+        "github:keplertech/kepler-formal"
+    ],
+    "versions": [],
+    "yanked_versions": {}
+}

.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"

.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"
+}

.github/consumer-test/.bazelrc

@@ -1,10 +1,29 @@
+# Same registries as kepler-formal's .bazelrc. A consumer outside this
+# repository lists kepler-formal's bazel/registry/ by URL instead, see
+# bazel/registry/README.md.
+common --registry=file://%workspace%/../../bazel/registry
+#   bison 3.8.2.bcr.10                     bazelbuild/bazel-central-registry#10879
+#   sv-lang 11.0.0-20260701-b60d729d.bcr.1 bazelbuild/bazel-central-registry#10882
+#   naja-if 0.0.0-20260723-099677d9        bazelbuild/bazel-central-registry#10881
+#   naja-verilog 0.0.0-20260909-be6544b1   bazelbuild/bazel-central-registry#10885
+#   kissat 4.0.4                           bazelbuild/bazel-central-registry#10880
+#   cadical 3.0.0                          bazelbuild/bazel-central-registry#10883
+#   glucose 4.2.1-20251230-674dbba         bazelbuild/bazel-central-registry#10884
+common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/bb42d7dc14939aaf578926cf1c93bd987ca9fac7/
+common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/5888fdb942da7cf4a6eecd8d5bc07c777e82c4ee/
+common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/377d10e631e9461794687b9ff1d4bbbde0c9ad1d/
+common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/649d563703219943c013c9e5af8884ea81b2ab19/
+common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/985ff91136fd9c24be49d268c8f8acb416137a01/
+common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/cf30c24de5255b58a523064f8a624848b4bd1bab/
+common --registry=https://raw.githubusercontent.com/oharboe/bazel-central-registry/0dc1d20b35db8595fbaaf762dbf5046fb19ae188/
+common --registry=https://bcr.bazel.build/
+
 common --enable_platform_specific_config
 
 build --cxxopt=-std=c++20
 build --host_cxxopt=-std=c++20
 
-# Same guards as the root .bazelrc: the hermetic toolchain must win
-# resolution, and host tools stay on C11 for the rules_foreign_cc
-# pkg-config bootstrap.
+# Same guard as the root .bazelrc: the hermetic toolchain must win
+# resolution.
 common:linux --repo_env=BAZEL_DO_NOT_DETECT_CPP_TOOLCHAIN=1
-build --host_conlyopt=-std=c11
+build:linux --dynamic_mode=off

.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",
-)

.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/...

.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

.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"

.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]

.reuse/dep5

@@ -7,15 +7,15 @@ 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
 
 Files: test/*
 Copyright: 2025 keplertech.io
 License: Apache-2.0
 
-Files: BUILD.bazel MODULE.bazel .bazelrc .bazelversion .bazelignore .gitignore
+Files: BUILD.bazel MODULE.bazel .bazelrc .bazelversion .bazelignore .gitignore CLAUDE.md AGENTS.md
 Copyright: 2025 keplertech.io
 License: Apache-2.0
 

AGENTS.md

@@ -0,0 +1 @@
+CLAUDE.md

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 <workspace>/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",