mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-09-16 01:24:24 +00:00
Code Activity
z3/cmake
History
Exact
Alex Reinking 595e2a16fc
[CMake] Silence redundant status messages (#10751) 
The CMake build is pretty noisy by default. This PR adjusts log-levels
and removes unnecessary `USES_TERMINAL` directives to allow a
CMake-generated Ninja build to produce no additional output when the
build succeeds.

After this PR, I see:

```console
$ cmake --build build
[906/906] Linking CXX executable z3
```

Ninja overwrites the previous status line when a command produces no
output. But on `master`, I see this:

<details>
<summary>Overly verbose build output</summary>

```console
$ cmake --build build
[52/906] Generating "/Users/areinking/dev/z3/build/src/math/polynomial/algebraic_params.hpp" from "algebraic_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/math/polynomial/algebraic_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/math/polynomial/algebraic_params.hpp"
[58/906] Generating "/Users/areinking/dev/z3/build/src/math/realclosure/rcf_params.hpp" from "rcf_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/math/realclosure/rcf_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/math/realclosure/rcf_params.hpp"
[78/906] Generating "/Users/areinking/dev/z3/build/src/ast/pp_params.hpp" from "pp_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/ast/pp_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/ast/pp_params.hpp"
[136/906] Generating "/Users/areinking/dev/z3/build/src/params/arith_rewriter_params.hpp" from "arith_rewriter_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/params/arith_rewriter_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/params/arith_rewriter_params.hpp"
[137/906] Generating "/Users/areinking/dev/z3/build/src/params/array_rewriter_params.hpp" from "array_rewriter_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/params/array_rewriter_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/params/array_rewriter_params.hpp"
[138/906] Generating "/Users/areinking/dev/z3/build/src/params/bool_rewriter_params.hpp" from "bool_rewriter_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/params/bool_rewriter_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/params/bool_rewriter_params.hpp"
[139/906] Generating "/Users/areinking/dev/z3/build/src/params/bv_rewriter_params.hpp" from "bv_rewriter_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/params/bv_rewriter_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/params/bv_rewriter_params.hpp"
[140/906] Generating "/Users/areinking/dev/z3/build/src/params/fpa_rewriter_params.hpp" from "fpa_rewriter_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/params/fpa_rewriter_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/params/fpa_rewriter_params.hpp"
[141/906] Generating "/Users/areinking/dev/z3/build/src/params/fpa2bv_rewriter_params.hpp" from "fpa2bv_rewriter_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/params/fpa2bv_rewriter_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/params/fpa2bv_rewriter_params.hpp"
[142/906] Generating "/Users/areinking/dev/z3/build/src/params/pattern_inference_params_helper.hpp" from "pattern_inference_params_helper.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/params/pattern_inference_params_helper.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/params/pattern_inference_params_helper.hpp"
[143/906] Generating "/Users/areinking/dev/z3/build/src/params/poly_rewriter_params.hpp" from "poly_rewriter_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/params/poly_rewriter_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/params/poly_rewriter_params.hpp"
[144/906] Generating "/Users/areinking/dev/z3/build/src/params/rewriter_params.hpp" from "rewriter_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/params/rewriter_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/params/rewriter_params.hpp"
[145/906] Generating "/Users/areinking/dev/z3/build/src/params/sat_params.hpp" from "sat_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/params/sat_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/params/sat_params.hpp"
[146/906] Generating "/Users/areinking/dev/z3/build/src/params/seq_rewriter_params.hpp" from "seq_rewriter_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/params/seq_rewriter_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/params/seq_rewriter_params.hpp"
[147/906] Generating "/Users/areinking/dev/z3/build/src/params/sls_params.hpp" from "sls_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/params/sls_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/params/sls_params.hpp"
[148/906] Generating "/Users/areinking/dev/z3/build/src/params/smt_params_helper.hpp" from "smt_params_helper.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/params/smt_params_helper.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/params/smt_params_helper.hpp"
[149/906] Generating "/Users/areinking/dev/z3/build/src/params/solver_params.hpp" from "solver_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/params/solver_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/params/solver_params.hpp"
[150/906] Generating "/Users/areinking/dev/z3/build/src/params/tactic_params.hpp" from "tactic_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/params/tactic_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/params/tactic_params.hpp"
[151/906] Generating "/Users/areinking/dev/z3/build/src/params/tptp.hpp" from "tptp.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/params/tptp.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/params/tptp.hpp"
[219/906] Generating "/Users/areinking/dev/z3/build/src/parsers/util/parser_params.hpp" from "parser_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/parsers/util/parser_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/parsers/util/parser_params.hpp"
[225/906] Generating "/Users/areinking/dev/z3/build/src/sat/sat_asymm_branch_params.hpp" from "sat_asymm_branch_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/sat/sat_asymm_branch_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/sat/sat_asymm_branch_params.hpp"
[229/906] Generating "/Users/areinking/dev/z3/build/src/ast/normal_forms/nnf_params.hpp" from "nnf_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/ast/normal_forms/nnf_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/ast/normal_forms/nnf_params.hpp"
[230/906] Generating "/Users/areinking/dev/z3/build/src/model/model_evaluator_params.hpp" from "model_evaluator_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/model/model_evaluator_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/model/model_evaluator_params.hpp"
[236/906] Generating "/Users/areinking/dev/z3/build/src/model/model_params.hpp" from "model_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/model/model_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/model/model_params.hpp"
[243/906] Generating "/Users/areinking/dev/z3/build/src/sat/sat_scc_params.hpp" from "sat_scc_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/sat/sat_scc_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/sat/sat_scc_params.hpp"
[244/906] Generating "/Users/areinking/dev/z3/build/src/sat/sat_simplifier_params.hpp" from "sat_simplifier_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/sat/sat_simplifier_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/sat/sat_simplifier_params.hpp"
[362/906] Generating "/Users/areinking/dev/z3/build/src/solver/combined_solver_params.hpp" from "combined_solver_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/solver/combined_solver_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/solver/combined_solver_params.hpp"
[366/906] Generating "/Users/areinking/dev/z3/build/src/solver/parallel_params.hpp" from "parallel_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/solver/parallel_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/solver/parallel_params.hpp"
[369/906] Generating "/Users/areinking/dev/z3/build/src/nlsat/nlsat_params.hpp" from "nlsat_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/nlsat/nlsat_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/nlsat/nlsat_params.hpp"
[380/906] Building CXX object src/sat/smt/CMakeFiles/sat_smt.dir/arith_diagnostics.cpp.o
/Users/areinking/dev/z3/src/sat/smt/arith_diagnostics.cpp:212:9: warning: default label in switch which covers all enumeration values [-Wcovered-switch-default]
  212 |         default:
      |         ^
1 warning generated.
[421/906] Generating "/Users/areinking/dev/z3/build/src/math/lp/lp_params_helper.hpp" from "lp_params_helper.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/math/lp/lp_params_helper.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/math/lp/lp_params_helper.hpp"
[532/906] Generating "/Users/areinking/dev/z3/build/src/ackermannization/ackermannization_params.hpp" from "ackermannization_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/ackermannization/ackermannization_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/ackermannization/ackermannization_params.hpp"
[536/906] Generating "database.h"
INFO:root:Generated "/Users/areinking/dev/z3/build/src/ast/pattern/database.h"
[630/906] Generating "/Users/areinking/dev/z3/build/src/ackermannization/ackermannize_bv_tactic_params.hpp" from "ackermannize_bv_tactic_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/ackermannization/ackermannize_bv_tactic_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/ackermannization/ackermannize_bv_tactic_params.hpp"
[701/906] Generating "/Users/areinking/dev/z3/build/src/muz/base/fp_params.hpp" from "fp_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/muz/base/fp_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/muz/base/fp_params.hpp"
[807/906] Generating "/Users/areinking/dev/z3/build/src/tactic/smtlogics/qfufbv_tactic_params.hpp" from "qfufbv_tactic_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/tactic/smtlogics/qfufbv_tactic_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/tactic/smtlogics/qfufbv_tactic_params.hpp"
[826/906] Generating "/Users/areinking/dev/z3/build/src/opt/opt_params.hpp" from "opt_params.pyg"
INFO:root:Using /Users/areinking/dev/z3/src/opt/opt_params.pyg
INFO:root:Generated "/Users/areinking/dev/z3/build/src/opt/opt_params.hpp"
[849/906] Generating api_commands.cpp;api_log_macros.cpp;api_log_macros.h
Faking emission of 'z3/z3core.py'
Generated '/Users/areinking/dev/z3/build/src/api/api_log_macros.h'
Generated '/Users/areinking/dev/z3/build/src/api/api_log_macros.cpp'
Generated '/Users/areinking/dev/z3/build/src/api/api_commands.cpp'
Generated '6'
[883/906] Generating "/Users/areinking/dev/z3/build/src/api/dll/gparams_register_modules.cpp"
INFO:root:Generated "/Users/areinking/dev/z3/build/src/api/dll/gparams_register_modules.cpp"
[884/906] Generating "/Users/areinking/dev/z3/build/src/api/dll/install_tactic.cpp"
INFO:root:Generated "/Users/areinking/dev/z3/build/src/api/dll/install_tactic.cpp"
[885/906] Generating "/Users/areinking/dev/z3/build/src/api/dll/mem_initializer.cpp"
INFO:root:Generated "/Users/areinking/dev/z3/build/src/api/dll/mem_initializer.cpp"
[886/906] Generating "/Users/areinking/dev/z3/build/src/shell/gparams_register_modules.cpp"
INFO:root:Generated "/Users/areinking/dev/z3/build/src/shell/gparams_register_modules.cpp"
[888/906] Generating "/Users/areinking/dev/z3/build/src/shell/install_tactic.cpp"
INFO:root:Generated "/Users/areinking/dev/z3/build/src/shell/install_tactic.cpp"
[889/906] Generating "/Users/areinking/dev/z3/build/src/shell/mem_initializer.cpp"
INFO:root:Generated "/Users/areinking/dev/z3/build/src/shell/mem_initializer.cpp"
[906/906] Linking CXX executable z3
```
</details>

The countless `INFO:root:...` lines just name the same files as the
`COMMENT` lines Ninja outputs regardless. The "Faking emission of
'z3/z3core.py'" line reads like a problem, but is benign. The only code
change is to silence this warning:

```
[380/906] Building CXX object src/sat/smt/CMakeFiles/sat_smt.dir/arith_diagnostics.cpp.o
/Users/areinking/dev/z3/src/sat/smt/arith_diagnostics.cpp:212:9: warning: default label in switch which covers all enumeration values [-Wcovered-switch-default]
  212 |         default:
      |         ^
1 warning generated.
```
2026-09-09 05:21:01 -07:00
..
modules [CMake] Require only the GMP C interface (#10716) 2026-09-01 19:04:20 -07:00
tests/package [CMake] Use z3::libz3 as the preferred way to consume Z3 (#10733) 2026-09-04 13:33:23 -07:00
check_link_atomic.cmake [CMake] Rework the CMake component graph (#10741) TY 2026-09-06 02:37:34 -07:00
cmake_uninstall.cmake.in [CMake] Move CMake files into their intended location so the 2017-06-12 11:59:00 +01:00
compiler_lto.cmake [CMake] Rework the CMake component graph (#10741) TY 2026-09-06 02:37:34 -07:00
compiler_warnings.cmake [CMake] Rework the CMake component graph (#10741) TY 2026-09-06 02:37:34 -07:00
git_utils.cmake [CMake] Simplify version computation (#10710) 2026-09-01 13:09:18 -07:00
msvc_legacy_quirks.cmake [CMake] Rework the CMake component graph (#10741) TY 2026-09-06 02:37:34 -07:00
target_arch_detect.cmake Change from BINARY_DIR to PROJECT_BINARY_DIR 2019-05-15 11:25:40 -07:00
target_arch_detect.cpp set ARM64 if detected under OSX 2022-04-07 08:35:56 +02:00
z3_add_component.cmake [CMake] Silence redundant status messages (#10751) 2026-09-09 05:21:01 -07:00
z3_add_cxx_flag.cmake [CMake] Rework the CMake component graph (#10741) TY 2026-09-06 02:37:34 -07:00
Z3Config.cmake.in [CMake] Refresh build documentation and invocation style (#10753) 2026-09-07 18:18:43 -07:00
Z3StaticDependencies.cmake.in [CMake] Support co-installed static and shared packages (#10717) 2026-09-01 17:21:20 -07:00