java-smt
java-smt copied to clipboard
Ensure that we do not publish native solver binaries with unwanted library dependencies
The current build targets for publishing solver binaries are suboptimal because they make it easy to (accidentally) build and publish solver binaries that are broken or depend on libraries on which we do not want them to depend.
-
compile-mathsat-bindings
executescompile.sh
, but does not fail if the latter reports an undefined symbol in the binary. The output of the task instead tells the user to proceed and publish a broken binary. I assume the same is true for building the Z3 bindings. -
compile.sh
for MathSAT asks the user to check for unwanted dependencies, but this is hidden when the ant target is used as the documentation says. For Z3, there is not even such a check in the script.
An automatic check for unwanted dependencies would be really good, because building the binaries is getting more and more complex. For example, currently we need to build MathSAT on something like Ubuntu 16.04, which has gcc >= 4.9, but we need to build Z3 on Ubuntu 14.04, because it does not have libgomp >= 4.
This script could be used as inspiration for such a check.
Other scripts that could be an inspiration are in these LWN comments.
Of course, if we use a container solution to implement #125 this check is not so important anymore.
AppImages have the same problems and they have some documentation with hints.
bingcc is a GCC wrapper that might allow us to compile binaries on newer systems without introducing a dependency on newer libraries.