This PR substantially modernizes Z3's CMake build, replacing a
significant amount of hand-rolled dependency bookkeeping with CMake's
native target-graph features.
The main benefits are:
* **Less custom build logic.** The existing component system in
`cmake/z3_add_component.cmake` manually walks and records the
component-dependency graph. This PR moves that information onto CMake
targets themselves, eliminating much of the `Z3_COMPONENT_*` /
`Z3_DEPENDENT_*` variable machinery.
* **A more accurate target graph.** Component dependencies, generated
registration headers, and static-component linking are now modeled
directly in CMake rather than reconstructed separately.
* **More natural source-tree organization.** `add_subdirectory()` calls
no longer need to be kept in a global topological order or reach deeply
into the source tree. Forward component dependencies are allowed, so
each directory can add its own children in a natural, alphabetical
order.
* **Better dependency propagation.** External dependencies such as GMP,
Threads, and `atomic` are available to the components that actually need
them. In particular, non-system GMP installations now work correctly
because component targets can see GMP's include path.
* **Cleaner package consumption.** Build-only compiler/linker policy is
separated from the dependencies exported to static-package consumers,
and Z3 behaves more cleanly when included via `add_subdirectory()` or
`FetchContent`.
* **Less code with the same observable package behavior.** The PR
changes 34 files with +566/-902 lines, for a net reduction of roughly
336 lines, while preserving the existing targets, public headers,
install layout, and registration behavior.
The main enabler is raising the minimum CMake version from 3.16 to
**3.30**.
CMake 3.30 introduced **custom transitive properties**, which let
targets propagate the registered module headers, tactic headers, and
memory headers needed for generated registration code. This replaces the
custom graph-walking logic previously used to accumulate those headers.
As a result, the three functions `z3_add_install_tactic_rule`,
`z3_add_memory_initializer_rule`, and
`z3_add_gparams_register_modules_rule` are replaced by a single,
substantially simpler function, `z3_generate_registration`, which
generates the required headers from properties propagated through the
target graph.
Newer CMake also lets us model chains of `OBJECT` libraries correctly.
Historically, only `OBJECT` libraries named directly in
`target_link_libraries()` contributed their object files to the final
link, which made transitive static-component dependencies awkward to
represent. Using `INTERFACE_LINK_LIBRARIES_DIRECT`, those chains can now
be expressed directly in the target graph.
Every Z3 component also links to a new `INTERFACE` target, `z3_common`.
This target owns the external library dependencies that consumers of a
component may need, including GMP, Threads, `atomic`, and similar
dependencies. Previously, these dependencies were attached only to the
final `libz3` target; among other things, that meant individual
components could not see the include path for a non-system GMP
installation.
`z3_common` is exported for static-package consumers, but Z3's own build
policy is not. Internal compiler and linker flags now live on a separate
`z3_internal_options` target used throughout the build. A possible
follow-up is to replace `z3_internal_options` with toolchain files
and/or CMake presets, but that would be a more disruptive change and is
intentionally left out of this PR.
Once CMake itself has an accurate model of the component graph, several
pieces of surrounding machinery become unnecessary. We no longer need a
topologically sorted list of `add_subdirectory()` calls or the previous
requirement that child components be declared before their dependents.
Each directory now adds its own subdirectories, in alphabetical order.
Public headers are likewise installed through CMake file sets instead of
hand-written `install(FILES ...)` rules.
The CMake version bump also enables a few smaller cleanups:
* use `GENERATOR_IS_MULTI_CONFIG` instead of inferring that from whether
`CMAKE_CONFIGURATION_TYPES` is defined;
* use `PROJECT_IS_TOP_LEVEL` guards so Z3 behaves correctly when
consumed as a subdirectory or through `FetchContent`;
* use `block()` instead of manually saving and restoring state around
the Python `find_package()` call.
One unrelated fix is included alongside these changes: the .NET example
now stages its `csproj` and `Program.cs` into the build tree with
`add_custom_command()` rather than `configure_file(..., COPYONLY)`, so
the `dotnet` build target correctly notices source changes.
Overall, the PR moves responsibility for dependency propagation and
graph structure out of Z3's custom CMake code and back into CMake
itself. The result is a smaller build system with fewer ordering
constraints and less duplicated state, while keeping the package's
externally visible behavior unchanged.
to allow a new mode `SERIOUS_ONLY`.
Modes:
`ON` - All warnings are treated as errors (same as before)
`OFF` - Warnings are not treated as errors (same as before)
`SERIOUS_ONLY` - A subset of "serious" warnings are treated as errors.
Upgrade code is included to upgrade old CMake cache's to use the new
type of `WARNINGS_AS_ERRORS`. We should remove it eventually. The
user's previous setting is preserved when doing this.
Very few warnings are treated as errors for now. Developers can
add more later as they see fit.
`contrib/cmake/bootstrap.py` script no longer needs to be executed.
The previous location of the CMake files was a compromise proposed
by @agurfinkel in #461. While this has served us well (allowing progress
to be made) over time limitations of this approach have appeared.
The main problem is that doing many git operations (e.g. pull, rebase)
means the CMake files don't get updated unless the user remembers to
run the script. This can lead to broken and confusing build system
behaviour.
This commit only does the file moving and necessary changes to
`.gitignore`. Other changes will be done in subsequent commits.
2017-06-12 11:59:00 +01:00
Renamed from contrib/cmake/cmake/z3_add_cxx_flag.cmake (Browse further)
