Missing runtime dependency on boost breaks release build

[Baltoli]

The release build for macOS and Arch Linux is broken because the packages for those platforms do not include Boost as a runtime dependency, but only as a build dependency.

Symptoms

The Arch Linux and macOS release jobs failed consistently with errors from llvm-kompile when running the pl-tutorial integration tests. Because the output was interleaved, it wasn't immediately clear what the problem was, but the symptoms appeared identical across both jobs.

Investigation

I copied the Arch Linux packaging job directly into the test-pr workflow¹ without the package upload step, and verified that doing so reproduced the failure. With a further modification to enable --output-sync and to print verbose output from kompile, I narrowed the problem down to definitions using --enable-search.

At this point, kompile was swallowing useful diagnostics from llvm-kompile², so I copied the exact invocation being run as a standalone shell command in the package test script. This produced output that included the error from clang that a boost header was missing, which was enough evidence for me to figure out the root cause.

Root Cause

In runtimeverification/llvm-backend#844, a seemingly innocuous change was made to change the return type of a function from void * to std::shared_ptr<KOREPattern>. This required that the backend's runtime header imported the AST library header to see the declaration of KOREPattern.

Transitively, AST.h pulls in a boost header. This happens in two places:

• when compiling C++ files in the backend using CMake
• when compiling C++ code at kompile time with llvm-kompile - notably, search.cpp (the entrypoint for backend interpreters using search) is such a case

If Boost is not installed at run-time, then the second case will fail. This produces the failure observed in CI. The Debian-based systems we test (Ubuntu, Debian) do not fail similarly, because in #3136 we added Boost as a runtime dependency to their packaging³. This change should have been propagated to Arch and macOS.

Fix

• Boost is a runtime dependency kframework/homebrew-k#28
• Boost is a runtime dependency #3709

The Homebrew PR should be merged first, to make sure that the release will go through correctly when the K PR is merged.

Evidence that this fix is correct can be seen on the testing draft PR that I opened; this job is a successful run of the Arch packaging in isolation as part of the test-pr job.

Longer-term, we may want to reevaluate how we do package testing, but for now to get unblocked I suggest merging the immediate hotfix PRs.

Footnotes

1. It's substantially simpler than the macOS / Homebrew workflow, and doesn't need any additional steps / context to be run on its own. ↩

2. Because the --verbose output from llvm-kompile is implemented using the shell feature set -x, it won't appear when being invoked by a non-shell program - in this case, Java. ↩

3. As a corollary here, the Python bindings for the LLVM backend would not have worked on Arch, nor on macOS if Boost happened not to be installed on a host machine at runtime. It does tend to be installed, though, which caused me a bit of confusion trying to reproduce the issue locally. ↩

[Baltoli]

Confirmed that this has been fixed: https://github.com/runtimeverification/k/actions/runs/6509030415