file for the build and install tree.
These files allow users of CMake to use Z3 via a CMake config package.
Clients can do `find_package(Z3 CONFIG)` to get use the package from
their projects.
When generating the files for the install tree we try to generate
the files so that they are relocatable so that it shouldn't matter
if the installed files aren't in the CMAKE_INSTALL_PREFIX when
a user consumes them. As long as the relative locations of the files
aren't changed things should still work.
A new CMake cache variable `CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR` has been
added so that the install location of the Z3 CMake package files can be
controlled.
This addresses #915 .
CMake will automatically pick up changes in git's HEAD so that
the necessary code is rebuilt when the build system is invoked.
Two new options `INCLUDE_GIT_HASH` and `INCLUDE_GIT_DESCRIBE` have been
added that enable/disable including the git hash and the output of `git
describe` respectively. By default if the source tree is a git
repository both options are on, otherwise they are false by default.
To support the `Z3GITHASH` macro a different implementation is used from
the old build system. In that build system the define is passed on the
command line. This would not work well for CMake because CMake
conservatively (and correctly) rebuilds *everything* if the flags given
to the compiler change. This would result in the entire project being
rebuilt everytime git's `HEAD` changed. Instead in this implementation
a CMake specific version of `version.h.in` (named `version.h.cmake.in`)
is added that uses the `#cmakedefine` feature of CMake's
`configure_file()` command to define `Z3GITHASH` if it is available and
not define it otherwise. This way only object files that depend on
`version.h` get re-built rather than the whole project.
It is unfortunate that the build systems now have different `version.h`
file templates. However they are very simple and I don't want to
modify how templates are handled in the python/Makefile build system.
`INTERFACE` was the not appropriate usage requirement to use. However
it only caused a problem when USE_LIB_GMP was enabled. With `INTERFACE`
`-lgmp` was not specified on the link line so `libz3.so` did not have a
reference to the library and linking against `libz3.so` by clients
would fail with missing references to symbols in `libgmp`.
We don't install Z3_DOTNET_ASSEMBLY_DLL into the gac. Instead we just copy into
installation directory.
There are several reasons for this:
* We can't install the Z3_DOTNET_ASSEMBLY_DLL into the gac in a portable
way like we can with mono (i.e. the ``-root`` flag).
* It isn't best practice to use ``gacutil.exe``
on Windows to install into the GAC, see
https://msdn.microsoft.com/en-us/library/yf1d93sz(v=vs.110).aspx .
Taking this approach should be sufficient because we can now do
something like this
```
mkdir build
cmake -G Ninja -DCMAKE_INSTALL_PREFIX=<some_path> ../
ninja
mkdir <some_path>
ninja install
```
and then put the contents of <some_path> into a zip file which creates a redistributable zip file for Windows.
and ``Microsoft.Z3.xml`` to the root build directory rather than
``<root_build_directory>/src/api/dotnet``.
This fixes#573 which makes the behaviour consistent with the Python
build system.
using CMake 2.8.12.2. It seems ``install_jar()`` in the version of
``UseJava.cmake`` shipped with that version of CMake doesn't handle
the ``DESTINATION`` argument correctly and treats that as the
installation location so CMake would install to
``/usr/local/DESTINATION`` rather than ``/usr/locale/share``.
the ``.jar`` file is created as ``com.microsoft.z3-4.4.2.0.jar``
and a symlink named ``com.microsoft.z3.jar`` is created which points
to it in the build and install directory.
I'm not entirely happy with some parts of the implementation
* The default locations for installing ``com.microsoft.z3.jar`` and ``libz3java.so``
aren't correct. CMake cache variables have been provided that allow the user to change
where these get installed.
* The name of ``libz3java.so``. It doesn't conform to the Debian
packaging guidelines (https://www.debian.org/doc/packaging-manuals/java-policy/x126.html)
and I have not provided an option to change this.
* The fact that ``SONAME`` and ``VERSION`` are not set on ``libz3java.so``.
These issues should be addressed once we know the correct way to handle
installation.
When using Mono support for installing/uninstalling the bindings
is also implemented. For Windows install/uninstall is not implemented
because the python build system does not implement it and Microsoft's
documentation (https://msdn.microsoft.com/en-us/library/dkkx7f79.aspx)
says that the gacutil should only be used for development and not for
production.
For now a warning is just emitted if ``INSTALL_DOTNET_BINDINGS``
is enabled and the .NET toolchain is native Windows. Someone with
better knowledge of how to correctly install assemblies under Windows
should implement this or remove this message.
A notable difference from the Python build system is the
``/linkresource:`` flag is not passed to the C# compiler. This means
a user of the .NET bindings will have to copy the Z3 library (i.e.
``libz3.dll``) to their application directory manually. The reason
for this difference is that using this flag requires the working
directory to be the directory containing the Z3 library (i.e.
``libz3.dll``) but setting this up with multi-configuration generators
doesn't currently seem possible.
executables, include files and libraries. We use
``GNUInstallDirs.cmake`` which ships with CMake to do the difficult work
of setting a sensible default and setting up CMake cache variables.
These can be overriden when running CMake by setting the
``CMAKE_INSTALL_BINDIR``, ``CMAKE_INSTALL_INCLUDEDIR`` and
``CMAKE_INSTALL_LIBDIR`` cache variables.
by 03a8ef2795 . This relates to #463
Also leave a note regarding ``compiler_flags_override.cmake`` its
value is a bit dubious now that the compiler flags are almost the CMake
defaults.
Most file generation scripts don't depend on it anymore.
The exceptions are uses of ``update_api.py``. An explicit dependency
has been added here and a ``FIXME`` has been left to indicate that this
should be removed once ``update_api.py`` is completly independent of
``mk_util.py``.
a list ``Z3_GENERATED_FILE_EXTRA_DEPENDENCIES`` that is used by
the ``add_custom_command()`` declarations. This will let
us easily change the common dependencies for generating build files in
the future.
is applied to targets. The ``LINK_FLAGS`` property of a target is
a string and not a list and so if ``Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS``
contained more than one flag the linker line would end up being
``-flag1;flag2;flag3;...`` which would not work. Now we use a new
function ``z3_append_linker_flag_list_to_target()`` to iterate through
the list and update the ``LINK_FLAGS`` property of the specified target
correctly.
and the cmake directory into a new directory ``contrib/cmake`` that
mirrors the directory structure of the root. This is a comprimise
between me and Christoph Wintersteiger that was suggested by Arie
Gurfinkel that allows the CMake build system to live in the Z3
repository but not impact the Z3 developers that want to avoid the CMake
build system. The build system will not work in its new location
and a bootstrap script will soon be provided that allows a developer
to copy the files back to their correct location.
