kepler-formal: bump with one line, no submodule, no per-platform build flags

.dockerignore

@@ -1,6 +1,8 @@
 # Build working directories
 tools/OpenROAD/build/
-tools/kepler-formal/build/
+# Local Bazel outputs; the image builds its own.
+etc/kepler-formal/bazel-*
+etc/kepler-formal/MODULE.bazel.lock
 
 # Build files
 build_openroad.log

.gitignore

@@ -104,6 +104,8 @@ bazel-out
 bazel-OpenROAD-flow-scripts
 bazel-testlogs
 MODULE.bazel.lock
+# etc/kepler-formal
+bazel-kepler-formal
 
 # python venv
 venv/

.gitmodules

@@ -4,6 +4,3 @@
 [submodule "tools/OpenROAD"]
 	path = tools/OpenROAD
 	url = ../OpenROAD.git
-[submodule "tools/kepler-formal"]
-	path = tools/kepler-formal
-	url = https://github.com/keplertech/kepler-formal

build_openroad.sh

@@ -385,12 +385,6 @@ __local_build()
                 source /opt/rh/devtoolset-8/enable
                 set -u
         fi
-        # EL8: the default GCC 8 is too old for kepler-formal.
-        if [[ -f "/opt/rh/gcc-toolset-13/enable" ]]; then
-                set +u
-                source /opt/rh/gcc-toolset-13/enable
-                set -u
-        fi
 
         if [ -z "${SKIP_OPENROAD+x}" ]; then
                 echo "[INFO FLW-0018] Compiling OpenROAD."
@@ -423,27 +417,19 @@ __local_build()
                 ${YOSYS_ARGS}
         ${NICE} cmake --build tools/yosys/build --target install -j "${PROC}"
 
-        echo "[INFO FLW-0031] Compiling kepler-formal"
-        # -march=x86-64-v3 is valid only for x86 compilers. On Arm, use the
-        # Armv8-A baseline, so that the binary runs on any aarch64 machine.
-        # EL9 ships TBB 2020, where concurrent_map needs
-        # TBB_PREVIEW_CONCURRENT_ORDERED_CONTAINERS; oneTBB ignores it.
-        # EL installs libraries in lib64 by default; the RPATH points to lib.
-        case "$(uname -m)" in
-                aarch64|arm64) KEPLER_MARCH="-march=armv8-a" ;;
-                *) KEPLER_MARCH="-march=x86-64-v3" ;;
-        esac
-        ${NICE} cmake -B tools/kepler-formal/build tools/kepler-formal \
-                -DCMAKE_BUILD_TYPE=Release \
-                -DCMAKE_CXX_FLAGS_RELEASE="-Ofast ${KEPLER_MARCH} -ffast-math -flto -DTBB_PREVIEW_CONCURRENT_ORDERED_CONTAINERS=1" \
-                -DCMAKE_EXE_LINKER_FLAGS="-flto" \
-                -DCMAKE_BUILD_RPATH="${DIR}/tools/kepler-formal/build/thirdparty/naja/src/dnl:${DIR}/tools/kepler-formal/build/thirdparty/naja/src/nl/nl:${DIR}/tools/kepler-formal/build/thirdparty/naja/src/optimization" \
-                -DCMAKE_INSTALL_RPATH="${INSTALL_PATH}/kepler-formal/lib" \
-                -DCMAKE_INSTALL_LIBDIR=lib \
-                -DCMAKE_BUILD_WITH_INSTALL_RPATH=OFF \
-                -DCMAKE_INSTALL_RPATH_USE_LINK_PATH=OFF \
-                -DCMAKE_INSTALL_PREFIX="${INSTALL_PATH}/kepler-formal"
-        ${NICE} cmake --build tools/kepler-formal/build --target install -j "${PROC}"
+        echo "[INFO FLW-0031] Installing kepler-formal"
+        # etc/kepler-formal pins kepler-formal; Bazel downloads it, its
+        # dependencies and the compiler. See etc/kepler-formal/README.md.
+        if ! command -v bazelisk &> /dev/null; then
+                echo "[ERROR FLW-0034] kepler-formal needs bazelisk; run etc/DependencyInstaller.sh -common." >&2
+                exit 1
+        fi
+        KEPLER_PREFIX="${INSTALL_PATH}/kepler-formal"
+        if [[ "${KEPLER_PREFIX}" != /* ]]; then
+                KEPLER_PREFIX="$(pwd)/${KEPLER_PREFIX}"
+        fi
+        (cd "${DIR}/etc/kepler-formal" && \
+                ${NICE} bazelisk run --jobs="${PROC}" //:install -- "${KEPLER_PREFIX}")
 
         if [ ${WITH_VERIFIC} -eq 1 ]; then
                 echo "[INFO FLW-0032] Cleaning up Verific components."

docker/Dockerfile.builder

@@ -30,6 +30,7 @@ FROM orfs-builder-base AS orfs-tools-builder
 # Exclude install so a local build's output (e.g. tools/install/OpenROAD)
 # cannot leak into the image; the build below starts from an empty install.
 COPY --link --exclude=OpenROAD --exclude=AutoTuner --exclude=install tools tools
+COPY --link etc/kepler-formal etc/kepler-formal
 ARG numThreads=$(nproc)
 ARG verificPath=""
 

etc/DependencyInstaller.sh

@@ -26,7 +26,7 @@ _versionCompare() {
     test $a "$2" $b
 }
 
-# Yosys and kepler-formal are built with CMake. Yosys needs CMake >= 3.28,
+# Yosys is built with CMake and needs CMake >= 3.28,
 # newer than Ubuntu 22.04 ships, so fetch a release from Kitware when the
 # one on PATH is too old.
 cmakeMinVersion=3.28
@@ -108,36 +108,6 @@ _installBison() {
     rm -rf "${workDir}"
 }
 
-# kepler-formal needs oneTBB and its CMake package. EL8 ships TBB 2018, which
-# has neither, so build oneTBB there. Build it static, because the
-# kepler-formal RPATH does not include the prefix.
-tbbVersion=2021.13.0
-tbbChecksum=3ad5dd08954b39d113dc5b3f8a8dc6dc1fd5250032b7c491eb07aed5c94133e1
-
-_installTbb() {
-    local prefix=${PREFIX:-"/usr/local"}
-    if compgen -G "${prefix}/lib*/cmake/TBB/TBBConfig.cmake" > /dev/null; then
-        echo "oneTBB found in ${prefix}, skipping install"
-        return
-    fi
-    local tarball="oneTBB-${tbbVersion}.tar.gz"
-    local workDir
-    workDir=$(mktemp -d)
-    (
-        # _installCmake may have put CMake in a prefix that is not on PATH.
-        export PATH="${prefix}/bin:${PATH}"
-        cd "${workDir}"
-        wget -q -O "${tarball}" "https://github.com/uxlfoundation/oneTBB/archive/refs/tags/v${tbbVersion}.tar.gz"
-        sha256sum -c <(echo "${tbbChecksum}  ${tarball}")
-        tar xzf "${tarball}"
-        cmake -S "oneTBB-${tbbVersion}" -B build -DCMAKE_BUILD_TYPE=Release \
-            -DTBB_TEST=OFF -DBUILD_SHARED_LIBS=OFF -DCMAKE_INSTALL_PREFIX="${prefix}"
-        cmake --build build -j "${numThreads}"
-        cmake --install build
-    )
-    rm -rf "${workDir}"
-}
-
 _installORDependencies() {
     if [[ ${YOSYS_VER} == "" ]]; then
         YOSYS_VER=v$(grep 'yosys_ver =' tools/yosys/docs/source/conf.py | awk -F'"' '{print $2}')
@@ -232,14 +202,12 @@ _install_EL8_EL9_Packages() {
 
     # EL8 and EL9 use `dnf`, instead of `yum`
     dnf -y update
-    # EPEL has tcl-tclreadline and capnproto.
+    # EPEL has tcl-tclreadline.
     dnf -y install "https://dl.fedoraproject.org/pub/epel/epel-release-latest-${elVersion}.noarch.rpm"
-    # The rest builds Yosys and kepler-formal.
+    # The rest builds Yosys.
     dnf -y install \
         bison \
         boost-devel \
-        capnproto \
-        capnproto-devel \
         findutils \
         flex \
         gcc \
@@ -260,7 +228,7 @@ _install_EL8_EL9_Packages() {
         wget \
         zlib-devel
 
-    # kepler-formal and the pip lock files need Python 3.10 or newer, which
+    # The pip lock files need Python 3.10 or newer, which
     # is newer than the EL8 and EL9 defaults.
     dnf -y install python3.12 python3.12-devel python3.12-pip
     update-alternatives --install /usr/bin/python3 python3 "$(command -v python3.12)" 50
@@ -272,13 +240,9 @@ _install_EL8_EL9_Packages() {
             readline-devel \
             tcl-tclreadline \
             tcl-tclreadline-devel
-        # The default GCC 8 is too old for kepler-formal.
-        dnf -y install gcc-toolset-13
     fi
 
     if [[ "${elVersion}" == "9" ]]; then
-        # EL8 builds oneTBB instead, in -common.
-        dnf -y install tbb-devel
         dnf -y install \
             https://mirror.stream.centos.org/9-stream/AppStream/x86_64/os/Packages/readline-devel-8.1-4.el9.x86_64.rpm
     fi
@@ -345,13 +309,11 @@ _installUbuntuPackages() {
         bison \
         build-essential \
         ca-certificates \
-        capnproto \
         curl \
         flex \
         git \
         help2man \
         libboost-iostreams-dev \
-        libcapnp-dev \
         libffi-dev \
         libfl-dev \
         libfl2 \
@@ -364,7 +326,6 @@ _installUbuntuPackages() {
         libqt5svg5-dev \
         libqt5xmlpatterns5-dev \
         libreadline-dev \
-        libtbb-dev \
         libz-dev \
         perl \
         pkg-config \
@@ -467,7 +428,7 @@ _installUbuntuPackages() {
 
 _installDarwinPackages() {
     brew install libffi tcl-tk ruby
-    brew install python libomp doxygen capnp tbb bison flex boost spdlog zlib cmake
+    brew install python libomp doxygen bison flex boost spdlog zlib cmake
     brew link --force libomp
     brew install --cask klayout
     brew install docker docker-buildx
@@ -697,9 +658,6 @@ case "${os}" in
         if [[ "${option}" == "common" || "${option}" == "all" ]]; then
             _installCmake
             _installBison
-            if [[ "${elVersion}" == "8" ]]; then
-                _installTbb
-            fi
             _installPipCommon
         fi
         ;;

etc/DockerTag.sh

@@ -16,7 +16,8 @@ if [[ "$@" == "-dev" ]]; then
 elif [[ "$@" == "-tools" ]]; then
     # Everything the orfs-tools target of Dockerfile.builder depends on:
     # the dev image, the build scripts, the ignore file that filters the
-    # build context, and the checked-out tools except OpenROAD.
+    # build context, the checked-out tools except OpenROAD, and the
+    # pinned kepler-formal.
     ignore_file=./docker/Dockerfile.builder.dockerignore
     if [[ ! -f "${ignore_file}" ]]; then
         ignore_file=./.dockerignore
@@ -26,9 +27,11 @@ elif [[ "$@" == "-tools" ]]; then
         cat ./build_openroad.sh ./dev_env.sh ./etc/setup_compiler_wrappers.sh
         cat "${ignore_file}"
         # Drop the trailing describe output, which depends on fetched tags.
-        git submodule status tools/yosys tools/kepler-formal | awk '{print $1, $2}'
+        git submodule status tools/yosys | awk '{print $1, $2}'
         git ls-tree HEAD tools/ | grep -v -e 'tools/OpenROAD$' -e 'tools/AutoTuner$' \
-            -e 'tools/yosys$' -e 'tools/kepler-formal$'
+            -e 'tools/yosys$'
+        # The kepler-formal version and the Bazel settings that install it.
+        git ls-tree -r HEAD etc/kepler-formal
     } | sha256sum | awk '{print substr($1, 1, 6)}'
 elif [[ "$@" == "-master" ]]; then
     git fetch --tags >&2

etc/kepler-formal/.bazelrc

@@ -0,0 +1,9 @@
+common --registry=https://bcr.bazel.build/
+
+build --cxxopt=-std=c++20
+build --host_cxxopt=-std=c++20
+build -c opt
+
+# As kepler-formal's own .bazelrc.
+common --enable_platform_specific_config
+build:linux --dynamic_mode=off

etc/kepler-formal/.bazelversion

@@ -0,0 +1 @@
+8.6.0

etc/kepler-formal/BUILD.bazel

@@ -0,0 +1,5 @@
+# bazelisk run //:install -- <prefix>
+alias(
+    name = "install",
+    actual = "@kepler-formal//:install",
+)

etc/kepler-formal/MODULE.bazel

@@ -0,0 +1,29 @@
+"""Pins the kepler-formal that build_openroad.sh installs.
+
+ORFS is not a Bazel project: this module exists only to install
+kepler-formal into tools/install/kepler-formal. See README.md.
+"""
+
+module(name = "orfs-kepler-formal")
+
+# To bump kepler-formal, change this version.
+bazel_dep(name = "kepler-formal", version = "0.5.0-20261020-0be91596")
+
+# TODO(keplertech/kepler-formal#292): delete this override once a
+# kepler-formal version with the //:install target is on the registry,
+# and move the version above to it.
+git_override(
+    module_name = "kepler-formal",
+    commit = "99d66cac88978312853a10b82657781f8e99d843",
+    remote = "https://github.com/oharboe/kepler-formal.git",
+)
+
+# kepler-formal builds with a downloaded clang. It registers that
+# toolchain for its own builds only, so a module that depends on it
+# registers it too. Elsewhere the host compiler is used.
+bazel_dep(name = "llvm", version = "0.8.24")
+
+llvm_toolchains = use_extension("@llvm//extensions:toolchain.bzl", "toolchain")
+use_repo(llvm_toolchains, "llvm_toolchains")
+
+register_toolchains("@llvm_toolchains//:all")

etc/kepler-formal/README.md

@@ -0,0 +1,39 @@
+# kepler-formal
+
+To bump kepler-formal, change the version in `MODULE.bazel`.
+
+`build_openroad.sh --local` installs kepler-formal into
+`tools/install/kepler-formal/bin/kepler-formal` from this folder:
+
+```shell
+cd etc/kepler-formal
+bazelisk run //:install -- "$(pwd)/../../tools/install/kepler-formal"
+```
+
+ORFS is not a Bazel project. This folder only pins kepler-formal; the
+install is kepler-formal's own `//:install` target.
+
+## How this maps to `DependencyInstaller.sh`
+
+`DependencyInstaller.sh` downloads a pinned CMake from Kitware when the
+one the OS ships is too old, and checks it against a checksum. Bazel
+does the same for kepler-formal and every library it needs, from the
+[Bazel Central Registry](https://registry.bazel.build/), which keeps the
+URL, the checksum and the build file of each version:
+
+| `DependencyInstaller.sh`, `build_openroad.sh` | Here |
+| --- | --- |
+| oneTBB and capnproto from the OS, or built from a pinned tarball | `bazel_dep` versions in kepler-formal's `MODULE.bazel` |
+| A pinned CMake when the OS's is too old | bazelisk runs the Bazel named in `.bazelversion` |
+| `gcc-toolset-13` on EL8, because GCC 8 is too old | A pinned clang is downloaded on x86-64 Linux; elsewhere the host compiler is used |
+| `tools/kepler-formal` and the submodules inside it | The version in `MODULE.bazel`; sources are checked against their checksums and cached in `~/.cache/bazel` |
+| An RPATH that points at the install's `lib/` | The binary finds its libraries next to itself, in `bin/kepler-formal.runfiles/` |
+
+## What goes away as upstream merges
+
+1. When a registry version of kepler-formal has the install target
+   (keplertech/kepler-formal#292, after
+   bazelbuild/bazel-central-registry#11201): delete the `git_override` in
+   `MODULE.bazel` and move the version to it.
+2. When kepler-formal registers its compiler for modules that depend on
+   it: delete the toolchain lines in `MODULE.bazel`.