kepler-formal: delete the submodule and the per-platform build code; a bump is one line

.dockerignore

@@ -1,6 +1,11 @@
 # Build working directories
 tools/OpenROAD/build/
-tools/kepler-formal/build/
+# A checkout from before kepler-formal moved to etc/kepler-formal keeps
+# the old submodule tree; keep it out of the image and its licenses.
+tools/kepler-formal/
+# 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,7 +385,9 @@ __local_build()
                 source /opt/rh/devtoolset-8/enable
                 set -u
         fi
-        # EL8: the default GCC 8 is too old for kepler-formal.
+        # EL8: the default GCC 8 is too old for Yosys, which needs C++20.
+        # It stays active for kepler-formal, which uses the host compiler
+        # where no downloaded clang is registered (aarch64).
         if [[ -f "/opt/rh/gcc-toolset-13/enable" ]]; then
                 set +u
                 source /opt/rh/gcc-toolset-13/enable
@@ -423,27 +425,20 @@ __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}" && \
+                ./install_licenses.sh "${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}')
@@ -236,14 +206,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 \
@@ -264,7 +232,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
@@ -276,13 +244,11 @@ _install_EL8_EL9_Packages() {
             readline-devel \
             tcl-tclreadline \
             tcl-tclreadline-devel
-        # The default GCC 8 is too old for kepler-formal.
+        # The default GCC 8 is too old for Yosys, which needs C++20.
         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
@@ -349,13 +315,11 @@ _installUbuntuPackages() {
         bison \
         build-essential \
         ca-certificates \
-        capnproto \
         curl \
         flex \
         git \
         help2man \
         libboost-iostreams-dev \
-        libcapnp-dev \
         libffi-dev \
         libfl-dev \
         libfl2 \
@@ -368,7 +332,6 @@ _installUbuntuPackages() {
         libqt5svg5-dev \
         libqt5xmlpatterns5-dev \
         libreadline-dev \
-        libtbb-dev \
         libz-dev \
         perl \
         pkg-config \
@@ -471,7 +434,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
@@ -701,9 +664,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,14 @@
+common --registry=https://bcr.bazel.build/
+
+# kepler-formal and naja do not set the C++ standard on their targets,
+# so the build sets it, as their registry presubmits do. OpenROAD
+# requires C++20 too.
+build --cxxopt=-std=c++20
+build --host_cxxopt=-std=c++20
+build -c opt
+
+# As kepler-formal's own .bazelrc: link statically on Linux. The clang
+# toolchain is chosen by register_toolchains in MODULE.bazel, on x86-64
+# Linux only.
+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,30 @@
+"""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 = "1.0.0-20261105-6870bd1a")
+
+# kepler-formal builds with a downloaded clang on x86-64 Linux. It
+# registers that toolchain for its own builds only, a dev_dependency by
+# design, so a module that depends on it registers it too, at the same
+# version, as kepler-formal's .github/consumer-test does. Elsewhere the
+# host compiler is used.
+bazel_dep(name = "llvm", version = "0.8.26")
+
+llvm_toolchains = use_extension("@llvm//extensions:toolchain.bzl", "toolchain")
+llvm_toolchains.exec(
+    arch = "x86_64",
+    os = "linux",
+)
+llvm_toolchains.target(
+    arch = "x86_64",
+    os = "linux",
+)
+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.
+
+That target installs only kepler-formal's own license. `build_openroad.sh`
+then runs `install_licenses.sh` with the same prefix, which copies the
+license notices of every module linked into the binary or shipped in its
+runfiles to `share/kepler-formal/licenses/<module>/`:
+
+```shell
+./install_licenses.sh "$(pwd)/../../tools/install/kepler-formal"
+```
+
+## 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, `gcc-toolset-13` on EL8, which Yosys still needs |
+| `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/` |

etc/kepler-formal/install_licenses.sh

@@ -0,0 +1,54 @@
+#!/usr/bin/env bash
+# Usage: install_licenses.sh <prefix>
+#
+# Copies the license notices of every module that goes into the
+# kepler-formal binary and its runfiles (naja, yaml-cpp, spdlog, kissat,
+# the embedded Python, the statically linked libc++, ...) into
+# <prefix>/share/kepler-formal/licenses/<repository>/. kepler-formal's
+# //:install ships only its own LICENSE.rst and LICENSES/.
+#
+# The modules are the repositories cquery finds in the binary's target
+# configuration; build tools such as bison run in the exec configuration
+# and are left out. Run it after `bazelisk run //:install`, from this
+# folder, so that the repositories are fetched.
+set -euo pipefail
+
+if [[ $# -ne 1 ]]; then
+    echo "Usage: $0 <prefix>" >&2
+    exit 1
+fi
+dest="$(cd "$1" && pwd)/share/kepler-formal/licenses"
+binary=@kepler-formal//src/bin:kepler-formal
+
+cd "$(dirname "$0")"
+external="$(bazelisk info output_base)/external"
+config="$(bazelisk cquery "${binary}" | awk '{print $NF}')"
+repos="$(bazelisk cquery --consistent_labels "deps(${binary})" \
+    | awk -v c="${config}" '$NF == c' \
+    | sed -n 's|^@@\([^/]*\)//.*|\1|p' | sort -u)"
+
+rm -rf "${dest}"
+count=0
+for repo in ${repos}; do
+    [[ -n "${repo}" ]] || continue
+    # Some modules unpack into a subdirectory (zlib-1.3.2/, slang-12.0/),
+    # and the llvm-project one keeps libc++'s notice in libcxx/. The
+    # embedded Python keeps its own in lib/python3.X/.
+    files="$(cd "${external}/${repo}" && find . -maxdepth 3 \
+        \( \( -iname 'LICENSE*' -o -iname 'LICENCE*' -o -iname 'COPYING*' \
+              -o -iname 'NOTICE*' -o -iname 'COPYRIGHT*' \) \
+           \( -path './*' -a ! -path './*/*/*' \
+              -o -path './lib/python*/LICENSE.txt' \) \) \
+        -print -prune)"
+    [[ -n "${files}" ]] || continue
+    mkdir -p "${dest}/${repo}"
+    while IFS= read -r f; do
+        (cd "${external}/${repo}" && cp -rL --parents "${f}" "${dest}/${repo}/")
+    done <<< "${files}"
+    count=$((count + 1))
+done
+if [[ ${count} -eq 0 ]]; then
+    echo "[ERROR] no license notices found for ${binary} in ${external}" >&2
+    exit 1
+fi
+echo "Installed the license notices of ${count} modules in ${dest}"