Static library

[wintersteiger]

We have a flag to build a static library, but that has had issues for a long time. There was a request on stackoverflow recently: Build z3 as static library instead of DLL

[wintersteiger]

See also issue #454.

[chadbrewbaker]

Use case is getting Z3 to run on AWS Lambda. You have to statically link in everything for portability. On your executable if you run

ldd a.out

you get a grocery list of dynamic libs that need to be removed. Might try running this on some of the test executables as a meta-test to make sure everything is static.

[delcypher]

@chadbrewbaker If you're building using clang or gcc the CMake build system which is currently awaiting review in #461 is capable of building a static version of the Z3 executable and a static library.

To do this run

git clone -b cmake_build_system4 git@github.com:delcypher/z3-1.git z3
cd z3
python contrib/cmake/bootstrap.py create
mkdir build
cd build
LDFLAGS="-static" cmake -DBUILD_LIBZ3_SHARED=OFF ../
make
ldd z3
        not a dynamic executable

[wintersteiger]

@chadbrewbaker: Is that just on AWS, or does this apply to other systems as well? And, did you build Z3 there or did you build it elsewhere and then upload it?

[wintersteiger]

@chadbrewbaker: I suppose you are running on the default z3 binary? That is indeed a dynamically linked to the system library, but you can easily fix that by adding -static to LINK_FLAGS in config.mk.

Note to self: we might want to consider adding an option to mk_make.py for this, may be useful for more requests considering the various cloud systems.

[chadbrewbaker]

As part of your binary releases, a statically compiled binary on AWS Linux for AWS Lambda would be awesome. If you need help getting a build box I can get you a Packer script.

Yes other systems I have used in the past like Blue Gene/L have needed static compiles. Also, static ARM builds for Android/IOS might be nice. IMHO z3 should become a standard UNIX shell utility and library.

[wintersteiger]

We don't have the bandwith to provide and maintain packages for all different package systems, but we do very much encourage community-supported packages, so if you can find a maintainer who would like to provide these packages, we would be happy to support them.

[wintersteiger]

Closing issue as fixed. Feel free to start a new issue for discussion of community-supported static packages!