`kepler-formal` links naja's Python bindings, so the binary is not relocatable and cannot be built as a dependency without PIC everywhere

[ovebryne]

Summary

Observed on main at f70c2e38592d704c8cccf68433b091e82c8118f0.

The kepler-formal C++ binary has a hard dependency on naja's Python wrapping.
Two things follow: the built binary is not self-contained, and building
kepler-formal as a Bazel dependency fails to link unless the entire transitive
C/C++ tree is compiled PIC.

Where it comes from

bazel/naja.BUILD.bazel — the :naja compatibility library pulls in the
Python loader alongside the C++ engine libraries:

cc_library(
    name = "naja",
    deps = [
        "//src/dnl:naja_dnl",
        ...
        "//src/nl/python/pyloader:naja_snl_pyloader",
        "//src/optimization:naja_opt",
    ],
)

src/bin/BUILD.bazel — the binary links the Python wrapping's shared library
and ships the Python module as data:

cc_binary(
    name = "kepler-formal",
    data = [":naja_python_module"],
    dynamic_deps = ["@naja//src/nl/python/naja_wrapping:naja_runtime"],
    ...
)

Consequence 1 — the C++ binary needs the system Python runtime

readelf -d on the built binary lists as direct NEEDED entries:

libtbb.so.12   libtbbmalloc.so.2   libnaja_runtime.so   libpython3.14.so.1.0

libnaja_runtime.so resolves to a path inside the Bazel output tree, so copying
just the binary to another machine gives:

error while loading shared libraries: libnaja_runtime.so:
cannot open shared object file: No such file or directory

The libpython3.14.so.1.0 entry is the part we would flag hardest. It is a
direct dependency of the binary, not something inherited through
libnaja_runtime.so (that library does not link Python at all), and it resolves
to the system Python at /usr/lib/x86_64-linux-gnu/, which the build does not
ship. It pulls libz and libexpat behind it. So a formal-verification CLI
cannot start unless the host has a matching CPython runtime installed — and the
version is baked into the binary, so a host with a different Python minor
version will not do.

Running it elsewhere therefore means shipping libnaja_runtime.so and TBB,
having the right libpython3.14, and setting LD_LIBRARY_PATH.

To be fair to the current design: TBB is deliberately shared — your own comment
in src/bin/BUILD.bazel says it is "bundled in the release tarball" — and
libstdc++/libm/libc are dynamic as usual. The two that look unintended are
libnaja_runtime.so and libpython3.14, and both trace to the same cause.

Consequence 2 — cannot link when built as a Bazel dependency

Linking a shared library requires position-independent objects. A consumer that
declares bazel_dep(name = "kepler-formal") and invokes the binary as a build
tool hits this in the exec configuration, where toolchains commonly compile
non-PIC. Setting --force_pic in the consumer does not help: it applies to the
target configuration only, and there is no --host_force_pic. The target
configuration builds fine; only the exec configuration fails.

What does not work (so you don't spend time on it)

Scoping -fPIC into the exec configuration for kepler-formal's own sources is
not enough — the requirement propagates outward:

scope added (exec config)	result
kepler-formal sources	naja symbols resolve, capnp symbols fail
+ capnp	capnp resolves, zlib symbols fail
blanket external/.*	recompiles the whole external tree; abandoned

So this is not something a consumer can paper over with a flag.

Ask

Can the C++ binary be built without the Python bindings — for example the
pyloader dropped from the :naja C++ dep list, and naja_runtime linked
statically or behind an opt-out? That would drop the libpython dependency with
it, since nothing else in the binary needs it. If the pyloader is genuinely required by the
C++ driver, saying so is a useful answer too; then the request is just a
statically linked variant for embedding.

Happy to test a branch.

[nanocoh]

Hi @ovebryne :) we will look at it and come back with our analysis.