From 4b517b96df66c87b46a1f9c9b2e8a2d26ed0195b Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 12 Jun 2017 10:21:50 +0100 Subject: [PATCH 1/6] [CMake] Move CMake files into their intended location so the `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. --- .gitignore | 11 ----------- {contrib/cmake/cmake => cmake}/Z3Config.cmake.in | 0 .../cmake/cmake => cmake}/cmake_uninstall.cmake.in | 0 {contrib/cmake/cmake => cmake}/compiler_lto.cmake | 0 .../cmake/cmake => cmake}/compiler_warnings.cmake | 0 .../cxx_compiler_flags_overrides.cmake | 0 {contrib/cmake/cmake => cmake}/git_utils.cmake | 0 .../cmake => cmake}/modules/FindDotNetToolchain.cmake | 0 {contrib/cmake/cmake => cmake}/modules/FindGMP.cmake | 0 .../cmake/cmake => cmake}/msvc_legacy_quirks.cmake | 0 .../cmake/cmake => cmake}/target_arch_detect.cmake | 0 {contrib/cmake/cmake => cmake}/target_arch_detect.cpp | 0 {contrib/cmake/cmake => cmake}/z3_add_component.cmake | 0 {contrib/cmake/cmake => cmake}/z3_add_cxx_flag.cmake | 0 .../z3_append_linker_flag_list_to_target.cmake | 0 {contrib/cmake/doc => doc}/CMakeLists.txt | 0 {contrib/cmake/examples => examples}/CMakeLists.txt | 0 .../cmake/examples => examples}/c++/CMakeLists.txt | 0 {contrib/cmake/examples => examples}/c/CMakeLists.txt | 0 .../cmake/examples => examples}/python/CMakeLists.txt | 0 .../cmake/examples => examples}/tptp/CMakeLists.txt | 0 {contrib/cmake/src => src}/CMakeLists.txt | 0 .../cmake/src => src}/ackermannization/CMakeLists.txt | 0 {contrib/cmake/src => src}/api/CMakeLists.txt | 0 {contrib/cmake/src => src}/api/dll/CMakeLists.txt | 0 {contrib/cmake/src => src}/api/dotnet/CMakeLists.txt | 0 .../src => src}/api/dotnet/cmake_install_gac.cmake.in | 0 .../api/dotnet/cmake_uninstall_gac.cmake.in | 0 {contrib/cmake/src => src}/api/java/CMakeLists.txt | 0 {contrib/cmake/src => src}/api/python/CMakeLists.txt | 0 {contrib/cmake/src => src}/ast/CMakeLists.txt | 0 {contrib/cmake/src => src}/ast/fpa/CMakeLists.txt | 0 {contrib/cmake/src => src}/ast/macros/CMakeLists.txt | 0 .../cmake/src => src}/ast/normal_forms/CMakeLists.txt | 0 {contrib/cmake/src => src}/ast/pattern/CMakeLists.txt | 0 .../src => src}/ast/proof_checker/CMakeLists.txt | 0 .../cmake/src => src}/ast/rewriter/CMakeLists.txt | 0 .../ast/rewriter/bit_blaster/CMakeLists.txt | 0 .../cmake/src => src}/ast/simplifier/CMakeLists.txt | 0 .../cmake/src => src}/ast/substitution/CMakeLists.txt | 0 {contrib/cmake/src => src}/cmd_context/CMakeLists.txt | 0 .../src => src}/cmd_context/extra_cmds/CMakeLists.txt | 0 {contrib/cmake/src => src}/duality/CMakeLists.txt | 0 {contrib/cmake/src => src}/interp/CMakeLists.txt | 0 .../cmake/src => src}/math/automata/CMakeLists.txt | 0 {contrib/cmake/src => src}/math/euclid/CMakeLists.txt | 0 .../cmake/src => src}/math/grobner/CMakeLists.txt | 0 .../cmake/src => src}/math/hilbert/CMakeLists.txt | 0 .../cmake/src => src}/math/interval/CMakeLists.txt | 0 .../cmake/src => src}/math/polynomial/CMakeLists.txt | 0 .../cmake/src => src}/math/realclosure/CMakeLists.txt | 0 .../cmake/src => src}/math/simplex/CMakeLists.txt | 0 .../cmake/src => src}/math/subpaving/CMakeLists.txt | 0 .../src => src}/math/subpaving/tactic/CMakeLists.txt | 0 {contrib/cmake/src => src}/model/CMakeLists.txt | 0 {contrib/cmake/src => src}/muz/base/CMakeLists.txt | 0 {contrib/cmake/src => src}/muz/bmc/CMakeLists.txt | 0 {contrib/cmake/src => src}/muz/clp/CMakeLists.txt | 0 .../cmake/src => src}/muz/dataflow/CMakeLists.txt | 0 {contrib/cmake/src => src}/muz/ddnf/CMakeLists.txt | 0 {contrib/cmake/src => src}/muz/duality/CMakeLists.txt | 0 {contrib/cmake/src => src}/muz/fp/CMakeLists.txt | 0 {contrib/cmake/src => src}/muz/pdr/CMakeLists.txt | 0 {contrib/cmake/src => src}/muz/rel/CMakeLists.txt | 0 {contrib/cmake/src => src}/muz/tab/CMakeLists.txt | 0 .../cmake/src => src}/muz/transforms/CMakeLists.txt | 0 {contrib/cmake/src => src}/nlsat/CMakeLists.txt | 0 .../cmake/src => src}/nlsat/tactic/CMakeLists.txt | 0 {contrib/cmake/src => src}/opt/CMakeLists.txt | 0 {contrib/cmake/src => src}/parsers/smt/CMakeLists.txt | 0 .../cmake/src => src}/parsers/smt2/CMakeLists.txt | 0 .../cmake/src => src}/parsers/util/CMakeLists.txt | 0 {contrib/cmake/src => src}/qe/CMakeLists.txt | 0 {contrib/cmake/src => src}/sat/CMakeLists.txt | 0 .../cmake/src => src}/sat/sat_solver/CMakeLists.txt | 0 {contrib/cmake/src => src}/sat/tactic/CMakeLists.txt | 0 {contrib/cmake/src => src}/shell/CMakeLists.txt | 0 {contrib/cmake/src => src}/smt/CMakeLists.txt | 0 {contrib/cmake/src => src}/smt/params/CMakeLists.txt | 0 .../cmake/src => src}/smt/proto_model/CMakeLists.txt | 0 {contrib/cmake/src => src}/smt/tactic/CMakeLists.txt | 0 {contrib/cmake/src => src}/solver/CMakeLists.txt | 0 {contrib/cmake/src => src}/tactic/CMakeLists.txt | 0 {contrib/cmake/src => src}/tactic/aig/CMakeLists.txt | 0 .../cmake/src => src}/tactic/arith/CMakeLists.txt | 0 {contrib/cmake/src => src}/tactic/bv/CMakeLists.txt | 0 {contrib/cmake/src => src}/tactic/core/CMakeLists.txt | 0 {contrib/cmake/src => src}/tactic/fpa/CMakeLists.txt | 0 .../cmake/src => src}/tactic/nlsat_smt/CMakeLists.txt | 0 .../cmake/src => src}/tactic/portfolio/CMakeLists.txt | 0 {contrib/cmake/src => src}/tactic/sls/CMakeLists.txt | 0 .../cmake/src => src}/tactic/smtlogics/CMakeLists.txt | 0 {contrib/cmake/src => src}/tactic/ufbv/CMakeLists.txt | 0 {contrib/cmake/src => src}/test/CMakeLists.txt | 0 .../cmake/src => src}/test/fuzzing/CMakeLists.txt | 0 {contrib/cmake/src => src}/util/CMakeLists.txt | 0 {contrib/cmake/src => src}/util/lp/CMakeLists.txt | 0 97 files changed, 11 deletions(-) rename {contrib/cmake/cmake => cmake}/Z3Config.cmake.in (100%) rename {contrib/cmake/cmake => cmake}/cmake_uninstall.cmake.in (100%) rename {contrib/cmake/cmake => cmake}/compiler_lto.cmake (100%) rename {contrib/cmake/cmake => cmake}/compiler_warnings.cmake (100%) rename {contrib/cmake/cmake => cmake}/cxx_compiler_flags_overrides.cmake (100%) rename {contrib/cmake/cmake => cmake}/git_utils.cmake (100%) rename {contrib/cmake/cmake => cmake}/modules/FindDotNetToolchain.cmake (100%) rename {contrib/cmake/cmake => cmake}/modules/FindGMP.cmake (100%) rename {contrib/cmake/cmake => cmake}/msvc_legacy_quirks.cmake (100%) rename {contrib/cmake/cmake => cmake}/target_arch_detect.cmake (100%) rename {contrib/cmake/cmake => cmake}/target_arch_detect.cpp (100%) rename {contrib/cmake/cmake => cmake}/z3_add_component.cmake (100%) rename {contrib/cmake/cmake => cmake}/z3_add_cxx_flag.cmake (100%) rename {contrib/cmake/cmake => cmake}/z3_append_linker_flag_list_to_target.cmake (100%) rename {contrib/cmake/doc => doc}/CMakeLists.txt (100%) rename {contrib/cmake/examples => examples}/CMakeLists.txt (100%) rename {contrib/cmake/examples => examples}/c++/CMakeLists.txt (100%) rename {contrib/cmake/examples => examples}/c/CMakeLists.txt (100%) rename {contrib/cmake/examples => examples}/python/CMakeLists.txt (100%) rename {contrib/cmake/examples => examples}/tptp/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/ackermannization/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/api/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/api/dll/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/api/dotnet/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/api/dotnet/cmake_install_gac.cmake.in (100%) rename {contrib/cmake/src => src}/api/dotnet/cmake_uninstall_gac.cmake.in (100%) rename {contrib/cmake/src => src}/api/java/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/api/python/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/ast/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/ast/fpa/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/ast/macros/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/ast/normal_forms/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/ast/pattern/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/ast/proof_checker/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/ast/rewriter/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/ast/rewriter/bit_blaster/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/ast/simplifier/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/ast/substitution/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/cmd_context/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/cmd_context/extra_cmds/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/duality/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/interp/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/math/automata/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/math/euclid/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/math/grobner/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/math/hilbert/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/math/interval/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/math/polynomial/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/math/realclosure/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/math/simplex/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/math/subpaving/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/math/subpaving/tactic/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/model/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/muz/base/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/muz/bmc/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/muz/clp/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/muz/dataflow/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/muz/ddnf/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/muz/duality/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/muz/fp/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/muz/pdr/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/muz/rel/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/muz/tab/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/muz/transforms/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/nlsat/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/nlsat/tactic/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/opt/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/parsers/smt/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/parsers/smt2/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/parsers/util/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/qe/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/sat/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/sat/sat_solver/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/sat/tactic/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/shell/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/smt/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/smt/params/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/smt/proto_model/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/smt/tactic/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/solver/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/tactic/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/tactic/aig/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/tactic/arith/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/tactic/bv/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/tactic/core/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/tactic/fpa/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/tactic/nlsat_smt/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/tactic/portfolio/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/tactic/sls/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/tactic/smtlogics/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/tactic/ufbv/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/test/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/test/fuzzing/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/util/CMakeLists.txt (100%) rename {contrib/cmake/src => src}/util/lp/CMakeLists.txt (100%) diff --git a/.gitignore b/.gitignore index cc1c2a754..b7e4a0186 100644 --- a/.gitignore +++ b/.gitignore @@ -75,14 +75,3 @@ src/api/ml/z3.mllib *.bak doc/api doc/code - -# CMake files copied over by the ``contrib/cmake/boostrap.py`` script -# See #461 -examples/CMakeLists.txt -examples/*/CMakeLists.txt -src/CMakeLists.txt -src/*/CMakeLists.txt -src/*/*/CMakeLists.txt -src/*/*/*/CMakeLists.txt -src/api/dotnet/cmake_install_gac.cmake.in -src/api/dotnet/cmake_uninstall_gac.cmake.in diff --git a/contrib/cmake/cmake/Z3Config.cmake.in b/cmake/Z3Config.cmake.in similarity index 100% rename from contrib/cmake/cmake/Z3Config.cmake.in rename to cmake/Z3Config.cmake.in diff --git a/contrib/cmake/cmake/cmake_uninstall.cmake.in b/cmake/cmake_uninstall.cmake.in similarity index 100% rename from contrib/cmake/cmake/cmake_uninstall.cmake.in rename to cmake/cmake_uninstall.cmake.in diff --git a/contrib/cmake/cmake/compiler_lto.cmake b/cmake/compiler_lto.cmake similarity index 100% rename from contrib/cmake/cmake/compiler_lto.cmake rename to cmake/compiler_lto.cmake diff --git a/contrib/cmake/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake similarity index 100% rename from contrib/cmake/cmake/compiler_warnings.cmake rename to cmake/compiler_warnings.cmake diff --git a/contrib/cmake/cmake/cxx_compiler_flags_overrides.cmake b/cmake/cxx_compiler_flags_overrides.cmake similarity index 100% rename from contrib/cmake/cmake/cxx_compiler_flags_overrides.cmake rename to cmake/cxx_compiler_flags_overrides.cmake diff --git a/contrib/cmake/cmake/git_utils.cmake b/cmake/git_utils.cmake similarity index 100% rename from contrib/cmake/cmake/git_utils.cmake rename to cmake/git_utils.cmake diff --git a/contrib/cmake/cmake/modules/FindDotNetToolchain.cmake b/cmake/modules/FindDotNetToolchain.cmake similarity index 100% rename from contrib/cmake/cmake/modules/FindDotNetToolchain.cmake rename to cmake/modules/FindDotNetToolchain.cmake diff --git a/contrib/cmake/cmake/modules/FindGMP.cmake b/cmake/modules/FindGMP.cmake similarity index 100% rename from contrib/cmake/cmake/modules/FindGMP.cmake rename to cmake/modules/FindGMP.cmake diff --git a/contrib/cmake/cmake/msvc_legacy_quirks.cmake b/cmake/msvc_legacy_quirks.cmake similarity index 100% rename from contrib/cmake/cmake/msvc_legacy_quirks.cmake rename to cmake/msvc_legacy_quirks.cmake diff --git a/contrib/cmake/cmake/target_arch_detect.cmake b/cmake/target_arch_detect.cmake similarity index 100% rename from contrib/cmake/cmake/target_arch_detect.cmake rename to cmake/target_arch_detect.cmake diff --git a/contrib/cmake/cmake/target_arch_detect.cpp b/cmake/target_arch_detect.cpp similarity index 100% rename from contrib/cmake/cmake/target_arch_detect.cpp rename to cmake/target_arch_detect.cpp diff --git a/contrib/cmake/cmake/z3_add_component.cmake b/cmake/z3_add_component.cmake similarity index 100% rename from contrib/cmake/cmake/z3_add_component.cmake rename to cmake/z3_add_component.cmake diff --git a/contrib/cmake/cmake/z3_add_cxx_flag.cmake b/cmake/z3_add_cxx_flag.cmake similarity index 100% rename from contrib/cmake/cmake/z3_add_cxx_flag.cmake rename to cmake/z3_add_cxx_flag.cmake diff --git a/contrib/cmake/cmake/z3_append_linker_flag_list_to_target.cmake b/cmake/z3_append_linker_flag_list_to_target.cmake similarity index 100% rename from contrib/cmake/cmake/z3_append_linker_flag_list_to_target.cmake rename to cmake/z3_append_linker_flag_list_to_target.cmake diff --git a/contrib/cmake/doc/CMakeLists.txt b/doc/CMakeLists.txt similarity index 100% rename from contrib/cmake/doc/CMakeLists.txt rename to doc/CMakeLists.txt diff --git a/contrib/cmake/examples/CMakeLists.txt b/examples/CMakeLists.txt similarity index 100% rename from contrib/cmake/examples/CMakeLists.txt rename to examples/CMakeLists.txt diff --git a/contrib/cmake/examples/c++/CMakeLists.txt b/examples/c++/CMakeLists.txt similarity index 100% rename from contrib/cmake/examples/c++/CMakeLists.txt rename to examples/c++/CMakeLists.txt diff --git a/contrib/cmake/examples/c/CMakeLists.txt b/examples/c/CMakeLists.txt similarity index 100% rename from contrib/cmake/examples/c/CMakeLists.txt rename to examples/c/CMakeLists.txt diff --git a/contrib/cmake/examples/python/CMakeLists.txt b/examples/python/CMakeLists.txt similarity index 100% rename from contrib/cmake/examples/python/CMakeLists.txt rename to examples/python/CMakeLists.txt diff --git a/contrib/cmake/examples/tptp/CMakeLists.txt b/examples/tptp/CMakeLists.txt similarity index 100% rename from contrib/cmake/examples/tptp/CMakeLists.txt rename to examples/tptp/CMakeLists.txt diff --git a/contrib/cmake/src/CMakeLists.txt b/src/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/CMakeLists.txt rename to src/CMakeLists.txt diff --git a/contrib/cmake/src/ackermannization/CMakeLists.txt b/src/ackermannization/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ackermannization/CMakeLists.txt rename to src/ackermannization/CMakeLists.txt diff --git a/contrib/cmake/src/api/CMakeLists.txt b/src/api/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/api/CMakeLists.txt rename to src/api/CMakeLists.txt diff --git a/contrib/cmake/src/api/dll/CMakeLists.txt b/src/api/dll/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/api/dll/CMakeLists.txt rename to src/api/dll/CMakeLists.txt diff --git a/contrib/cmake/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/api/dotnet/CMakeLists.txt rename to src/api/dotnet/CMakeLists.txt diff --git a/contrib/cmake/src/api/dotnet/cmake_install_gac.cmake.in b/src/api/dotnet/cmake_install_gac.cmake.in similarity index 100% rename from contrib/cmake/src/api/dotnet/cmake_install_gac.cmake.in rename to src/api/dotnet/cmake_install_gac.cmake.in diff --git a/contrib/cmake/src/api/dotnet/cmake_uninstall_gac.cmake.in b/src/api/dotnet/cmake_uninstall_gac.cmake.in similarity index 100% rename from contrib/cmake/src/api/dotnet/cmake_uninstall_gac.cmake.in rename to src/api/dotnet/cmake_uninstall_gac.cmake.in diff --git a/contrib/cmake/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/api/java/CMakeLists.txt rename to src/api/java/CMakeLists.txt diff --git a/contrib/cmake/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/api/python/CMakeLists.txt rename to src/api/python/CMakeLists.txt diff --git a/contrib/cmake/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/CMakeLists.txt rename to src/ast/CMakeLists.txt diff --git a/contrib/cmake/src/ast/fpa/CMakeLists.txt b/src/ast/fpa/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/fpa/CMakeLists.txt rename to src/ast/fpa/CMakeLists.txt diff --git a/contrib/cmake/src/ast/macros/CMakeLists.txt b/src/ast/macros/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/macros/CMakeLists.txt rename to src/ast/macros/CMakeLists.txt diff --git a/contrib/cmake/src/ast/normal_forms/CMakeLists.txt b/src/ast/normal_forms/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/normal_forms/CMakeLists.txt rename to src/ast/normal_forms/CMakeLists.txt diff --git a/contrib/cmake/src/ast/pattern/CMakeLists.txt b/src/ast/pattern/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/pattern/CMakeLists.txt rename to src/ast/pattern/CMakeLists.txt diff --git a/contrib/cmake/src/ast/proof_checker/CMakeLists.txt b/src/ast/proof_checker/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/proof_checker/CMakeLists.txt rename to src/ast/proof_checker/CMakeLists.txt diff --git a/contrib/cmake/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/rewriter/CMakeLists.txt rename to src/ast/rewriter/CMakeLists.txt diff --git a/contrib/cmake/src/ast/rewriter/bit_blaster/CMakeLists.txt b/src/ast/rewriter/bit_blaster/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/rewriter/bit_blaster/CMakeLists.txt rename to src/ast/rewriter/bit_blaster/CMakeLists.txt diff --git a/contrib/cmake/src/ast/simplifier/CMakeLists.txt b/src/ast/simplifier/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/simplifier/CMakeLists.txt rename to src/ast/simplifier/CMakeLists.txt diff --git a/contrib/cmake/src/ast/substitution/CMakeLists.txt b/src/ast/substitution/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/substitution/CMakeLists.txt rename to src/ast/substitution/CMakeLists.txt diff --git a/contrib/cmake/src/cmd_context/CMakeLists.txt b/src/cmd_context/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/cmd_context/CMakeLists.txt rename to src/cmd_context/CMakeLists.txt diff --git a/contrib/cmake/src/cmd_context/extra_cmds/CMakeLists.txt b/src/cmd_context/extra_cmds/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/cmd_context/extra_cmds/CMakeLists.txt rename to src/cmd_context/extra_cmds/CMakeLists.txt diff --git a/contrib/cmake/src/duality/CMakeLists.txt b/src/duality/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/duality/CMakeLists.txt rename to src/duality/CMakeLists.txt diff --git a/contrib/cmake/src/interp/CMakeLists.txt b/src/interp/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/interp/CMakeLists.txt rename to src/interp/CMakeLists.txt diff --git a/contrib/cmake/src/math/automata/CMakeLists.txt b/src/math/automata/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/automata/CMakeLists.txt rename to src/math/automata/CMakeLists.txt diff --git a/contrib/cmake/src/math/euclid/CMakeLists.txt b/src/math/euclid/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/euclid/CMakeLists.txt rename to src/math/euclid/CMakeLists.txt diff --git a/contrib/cmake/src/math/grobner/CMakeLists.txt b/src/math/grobner/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/grobner/CMakeLists.txt rename to src/math/grobner/CMakeLists.txt diff --git a/contrib/cmake/src/math/hilbert/CMakeLists.txt b/src/math/hilbert/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/hilbert/CMakeLists.txt rename to src/math/hilbert/CMakeLists.txt diff --git a/contrib/cmake/src/math/interval/CMakeLists.txt b/src/math/interval/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/interval/CMakeLists.txt rename to src/math/interval/CMakeLists.txt diff --git a/contrib/cmake/src/math/polynomial/CMakeLists.txt b/src/math/polynomial/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/polynomial/CMakeLists.txt rename to src/math/polynomial/CMakeLists.txt diff --git a/contrib/cmake/src/math/realclosure/CMakeLists.txt b/src/math/realclosure/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/realclosure/CMakeLists.txt rename to src/math/realclosure/CMakeLists.txt diff --git a/contrib/cmake/src/math/simplex/CMakeLists.txt b/src/math/simplex/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/simplex/CMakeLists.txt rename to src/math/simplex/CMakeLists.txt diff --git a/contrib/cmake/src/math/subpaving/CMakeLists.txt b/src/math/subpaving/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/subpaving/CMakeLists.txt rename to src/math/subpaving/CMakeLists.txt diff --git a/contrib/cmake/src/math/subpaving/tactic/CMakeLists.txt b/src/math/subpaving/tactic/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/subpaving/tactic/CMakeLists.txt rename to src/math/subpaving/tactic/CMakeLists.txt diff --git a/contrib/cmake/src/model/CMakeLists.txt b/src/model/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/model/CMakeLists.txt rename to src/model/CMakeLists.txt diff --git a/contrib/cmake/src/muz/base/CMakeLists.txt b/src/muz/base/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/base/CMakeLists.txt rename to src/muz/base/CMakeLists.txt diff --git a/contrib/cmake/src/muz/bmc/CMakeLists.txt b/src/muz/bmc/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/bmc/CMakeLists.txt rename to src/muz/bmc/CMakeLists.txt diff --git a/contrib/cmake/src/muz/clp/CMakeLists.txt b/src/muz/clp/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/clp/CMakeLists.txt rename to src/muz/clp/CMakeLists.txt diff --git a/contrib/cmake/src/muz/dataflow/CMakeLists.txt b/src/muz/dataflow/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/dataflow/CMakeLists.txt rename to src/muz/dataflow/CMakeLists.txt diff --git a/contrib/cmake/src/muz/ddnf/CMakeLists.txt b/src/muz/ddnf/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/ddnf/CMakeLists.txt rename to src/muz/ddnf/CMakeLists.txt diff --git a/contrib/cmake/src/muz/duality/CMakeLists.txt b/src/muz/duality/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/duality/CMakeLists.txt rename to src/muz/duality/CMakeLists.txt diff --git a/contrib/cmake/src/muz/fp/CMakeLists.txt b/src/muz/fp/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/fp/CMakeLists.txt rename to src/muz/fp/CMakeLists.txt diff --git a/contrib/cmake/src/muz/pdr/CMakeLists.txt b/src/muz/pdr/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/pdr/CMakeLists.txt rename to src/muz/pdr/CMakeLists.txt diff --git a/contrib/cmake/src/muz/rel/CMakeLists.txt b/src/muz/rel/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/rel/CMakeLists.txt rename to src/muz/rel/CMakeLists.txt diff --git a/contrib/cmake/src/muz/tab/CMakeLists.txt b/src/muz/tab/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/tab/CMakeLists.txt rename to src/muz/tab/CMakeLists.txt diff --git a/contrib/cmake/src/muz/transforms/CMakeLists.txt b/src/muz/transforms/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/transforms/CMakeLists.txt rename to src/muz/transforms/CMakeLists.txt diff --git a/contrib/cmake/src/nlsat/CMakeLists.txt b/src/nlsat/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/nlsat/CMakeLists.txt rename to src/nlsat/CMakeLists.txt diff --git a/contrib/cmake/src/nlsat/tactic/CMakeLists.txt b/src/nlsat/tactic/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/nlsat/tactic/CMakeLists.txt rename to src/nlsat/tactic/CMakeLists.txt diff --git a/contrib/cmake/src/opt/CMakeLists.txt b/src/opt/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/opt/CMakeLists.txt rename to src/opt/CMakeLists.txt diff --git a/contrib/cmake/src/parsers/smt/CMakeLists.txt b/src/parsers/smt/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/parsers/smt/CMakeLists.txt rename to src/parsers/smt/CMakeLists.txt diff --git a/contrib/cmake/src/parsers/smt2/CMakeLists.txt b/src/parsers/smt2/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/parsers/smt2/CMakeLists.txt rename to src/parsers/smt2/CMakeLists.txt diff --git a/contrib/cmake/src/parsers/util/CMakeLists.txt b/src/parsers/util/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/parsers/util/CMakeLists.txt rename to src/parsers/util/CMakeLists.txt diff --git a/contrib/cmake/src/qe/CMakeLists.txt b/src/qe/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/qe/CMakeLists.txt rename to src/qe/CMakeLists.txt diff --git a/contrib/cmake/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/sat/CMakeLists.txt rename to src/sat/CMakeLists.txt diff --git a/contrib/cmake/src/sat/sat_solver/CMakeLists.txt b/src/sat/sat_solver/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/sat/sat_solver/CMakeLists.txt rename to src/sat/sat_solver/CMakeLists.txt diff --git a/contrib/cmake/src/sat/tactic/CMakeLists.txt b/src/sat/tactic/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/sat/tactic/CMakeLists.txt rename to src/sat/tactic/CMakeLists.txt diff --git a/contrib/cmake/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/shell/CMakeLists.txt rename to src/shell/CMakeLists.txt diff --git a/contrib/cmake/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/smt/CMakeLists.txt rename to src/smt/CMakeLists.txt diff --git a/contrib/cmake/src/smt/params/CMakeLists.txt b/src/smt/params/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/smt/params/CMakeLists.txt rename to src/smt/params/CMakeLists.txt diff --git a/contrib/cmake/src/smt/proto_model/CMakeLists.txt b/src/smt/proto_model/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/smt/proto_model/CMakeLists.txt rename to src/smt/proto_model/CMakeLists.txt diff --git a/contrib/cmake/src/smt/tactic/CMakeLists.txt b/src/smt/tactic/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/smt/tactic/CMakeLists.txt rename to src/smt/tactic/CMakeLists.txt diff --git a/contrib/cmake/src/solver/CMakeLists.txt b/src/solver/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/solver/CMakeLists.txt rename to src/solver/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/CMakeLists.txt b/src/tactic/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/CMakeLists.txt rename to src/tactic/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/aig/CMakeLists.txt b/src/tactic/aig/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/aig/CMakeLists.txt rename to src/tactic/aig/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/arith/CMakeLists.txt b/src/tactic/arith/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/arith/CMakeLists.txt rename to src/tactic/arith/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/bv/CMakeLists.txt b/src/tactic/bv/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/bv/CMakeLists.txt rename to src/tactic/bv/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/core/CMakeLists.txt rename to src/tactic/core/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/fpa/CMakeLists.txt b/src/tactic/fpa/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/fpa/CMakeLists.txt rename to src/tactic/fpa/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/nlsat_smt/CMakeLists.txt b/src/tactic/nlsat_smt/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/nlsat_smt/CMakeLists.txt rename to src/tactic/nlsat_smt/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/portfolio/CMakeLists.txt b/src/tactic/portfolio/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/portfolio/CMakeLists.txt rename to src/tactic/portfolio/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/sls/CMakeLists.txt b/src/tactic/sls/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/sls/CMakeLists.txt rename to src/tactic/sls/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/smtlogics/CMakeLists.txt b/src/tactic/smtlogics/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/smtlogics/CMakeLists.txt rename to src/tactic/smtlogics/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/ufbv/CMakeLists.txt b/src/tactic/ufbv/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/ufbv/CMakeLists.txt rename to src/tactic/ufbv/CMakeLists.txt diff --git a/contrib/cmake/src/test/CMakeLists.txt b/src/test/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/test/CMakeLists.txt rename to src/test/CMakeLists.txt diff --git a/contrib/cmake/src/test/fuzzing/CMakeLists.txt b/src/test/fuzzing/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/test/fuzzing/CMakeLists.txt rename to src/test/fuzzing/CMakeLists.txt diff --git a/contrib/cmake/src/util/CMakeLists.txt b/src/util/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/util/CMakeLists.txt rename to src/util/CMakeLists.txt diff --git a/contrib/cmake/src/util/lp/CMakeLists.txt b/src/util/lp/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/util/lp/CMakeLists.txt rename to src/util/lp/CMakeLists.txt From 5be503798ff97f8f9249a46145be23955a2e41ae Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 12 Jun 2017 10:29:01 +0100 Subject: [PATCH 2/6] [CMake] Remove bootstrap check. Now that the CMake files are in their correct location we don't need it anymore. --- CMakeLists.txt | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 7400f67e2..5ed7ee06a 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -14,16 +14,6 @@ if (POLICY CMP0054) cmake_policy(SET CMP0054 OLD) endif() -# Provide a friendly message if the user hasn't run the bootstrap script -# to copy all the CMake files into their correct location. -# It is unfortunate that we have to do this, see #461 for the discussion -# on this. -if (NOT (EXISTS "${CMAKE_SOURCE_DIR}/src/CMakeLists.txt")) - message(FATAL_ERROR "Cannot find \"${CMAKE_SOURCE_DIR}/src/CMakeLists.txt\"" - ". This probably means you need to run" - "``python contrib/cmake/bootstrap.py create``") -endif() - set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") project(Z3 CXX) From 5c3b11f034ff0550aaced0b61266382edb28ba9c Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 12 Jun 2017 10:39:49 +0100 Subject: [PATCH 3/6] [CMake] Modify `contrib/cmake/bootstrap.py` to do nothing except print a warning. Now that the CMake files have been moved into their intended location it is no longer necessary for this script to exist. However we do not want to break out-of-tree scripts that build Z3 using CMake to suddenly break. So the script has been modified to do nothing except print a warning. Eventually we should remove this script. --- contrib/cmake/bootstrap.py | 233 ++----------------------------------- 1 file changed, 10 insertions(+), 223 deletions(-) diff --git a/contrib/cmake/bootstrap.py b/contrib/cmake/bootstrap.py index a3c81fb25..dac08b383 100755 --- a/contrib/cmake/bootstrap.py +++ b/contrib/cmake/bootstrap.py @@ -1,25 +1,13 @@ #!/usr/bin/env python """ -This script is used to copy or delete the -CMake build system files from the contrib/cmake -folder into the their correct location in the Z3 -repository. +This script is an artifact of compromise that was +made when the CMake build system was first introduced +(see #461). -It offers two modes - -* create - This will symlink the ``cmake`` directory and copy (or hard link) -the appropriate files into their correct locations in the repository. - -* remove - This will remove the symlinked ``cmake`` -directory and remove the files added by the above -methods. - -This has the advantage -that editing the hard link edits the underlying file -(making development easier because copying files is -not neccessary) and CMake will regenerate correctly -because the modification time stamps will be correct. +This script now does nothing. It remains only to not +break out-of-tree scripts that build Z3 using CMake. +Eventually this script will be removed. """ import argparse import logging @@ -28,189 +16,6 @@ import pprint import shutil import sys -def get_full_path_to_script(): - return os.path.abspath(__file__) - -def get_cmake_contrib_dir(): - return os.path.dirname(get_full_path_to_script()) - -def get_repo_root_dir(): - r = os.path.dirname(os.path.dirname(get_cmake_contrib_dir())) - assert os.path.isdir(r) - return r - -# These are paths that should be ignored when checking if a folder -# in the ``contrib/cmake`` exists in the root of the repository -verificationExceptions = { - os.path.join(get_repo_root_dir(), 'cmake'), - os.path.join(get_repo_root_dir(), 'cmake', 'modules') -} - -def contribPathToRepoPath(path): - assert path.startswith(get_cmake_contrib_dir()) - stripped = path[len(get_cmake_contrib_dir()) + 1:] # Plus one is to remove leading slash - assert not os.path.isabs(stripped) - logging.debug('stripped:{}'.format(stripped)) - r = os.path.join(get_repo_root_dir(), stripped) - assert os.path.isabs(r) - logging.debug('Converted contrib path "{}" to repo path "{}"'.format(path, r)) - return r - -def verify_mirrored_directory_struture(): - """ - Check that the directories contained in ``contrib/cmake`` exist - in the root of the repo. - """ - for (dirpath, _, _) in os.walk(get_cmake_contrib_dir()): - expectedDir = contribPathToRepoPath(dirpath) - logging.debug('expectedDir:{}'.format(expectedDir)) - if (not (os.path.exists(expectedDir) and os.path.isdir(expectedDir)) and - expectedDir not in verificationExceptions): - logging.error(('Expected to find directory "{}" but it does not exist' - ' or is not a directory').format(expectedDir)) - return 1 - - return 0 - -def mk_sym_link(target, linkName): - logging.info('Making symbolic link target="{}", linkName="{}"'.format(target, linkName)) - if os.path.exists(linkName): - logging.info('Removing existing link "{}"'.format(linkName)) - if not os.path.islink(linkName): - logging.warning('"{}" overwriting file that is not a symlink'.format(linkName)) - delete_path(linkName) - if os.name == 'posix': - os.symlink(target, linkName) - else: - # TODO: Windows does support symlinks but the implementation to do that - # from python is a little complicated so for now lets just copy everyting - logging.warning('Creating symbolic links is not supported. Just making a copy instead') - if os.path.isdir(target): - # Recursively copy directory - shutil.copytree(src=target, dst=linkName, symlinks=False) - else: - # Copy file - assert os.path.isfile(target) - shutil.copy2(src=target, dst=linkName) - -def delete_path(path): - logging.info('Removing "{}"'.format(path)) - if not os.path.exists(path): - logging.warning('"{}" does not exist'.format(path)) - return - if os.path.isdir(path) and not os.path.islink(path): - # FIXME: If we can get symbolic link support on Windows we - # can disallow this completely. - assert os.name == 'nt' - shutil.rmtree(path) - else: - os.remove(path) - -def shouldSkipFile(path): - # Skip this script - if path == get_full_path_to_script(): - return True - # Skip the maintainers file - if path == os.path.join(get_cmake_contrib_dir(), 'maintainers.txt'): - return True - # Skip Vim temporary files - if os.path.basename(path).startswith('.') and path.endswith('.swp'): - return True - return False - - -def create(useHardLinks): - """ - Copy or hard link files in the CMake contrib directory - into the repository where they are intended to live. - - Note that symbolic links for the CMakeLists.txt files - are not appropriate because they won't have the right - file modification time when the files they point to - are modified. This would prevent CMake from correctly - reconfiguring when it detects this is required. - """ - - # Make the ``cmake`` directory a symbolic link. - # We treat this one specially as it is the only directory - # that doesn't already exist in the repository root so - # we can just use a symlink here - linkName = os.path.join(get_repo_root_dir(), 'cmake') - target = os.path.join(get_cmake_contrib_dir(), 'cmake') - specialDir = target - mk_sym_link(target, linkName) - - for (dirPath,_ , fileNames) in os.walk(get_cmake_contrib_dir()): - # Skip the special directory and its children - if dirPath.startswith(specialDir): - logging.info('Skipping directory "{}"'.format(dirPath)) - continue - - for fileName in fileNames: - fileInContrib = os.path.join(dirPath, fileName) - # Skip files - if shouldSkipFile(fileInContrib): - logging.info('Skipping "{}"'.format(fileInContrib)) - continue - fileInRepo = contribPathToRepoPath(fileInContrib) - logging.info('"{}" => "{}"'.format(fileInContrib, fileInRepo)) - if useHardLinks: - if not os.name == 'posix': - logging.error('Hard links are not supported on your platform') - return False - if os.path.exists(fileInRepo): - delete_path(fileInRepo) - os.link(fileInContrib, fileInRepo) - else: - try: - shutil.copy2(src=fileInContrib, dst=fileInRepo) - except shutil.Error as e: - # Can hit this if used created hard links first and then run again without - # wanting hard links - if sys.version_info.major <= 2: - logging.error(e.message) - else: - # Python >= 3 - if isinstance(e, shutil.SameFileError): - logging.error('Trying to copy "{}" to "{}" but they are the same file'.format( - fileInContrib, fileInRepo)) - else: - logging.error(e) - logging.error('You should remove the files using the "remove" mode ' - 'and try to create again. You probably are mixing the ' - 'hard-link and non-hard-link create modes') - return False - return True - -def remove(): - """ - Remove the CMake files from their intended location in - the repository. This is used to remove - the files created by the ``create()`` function. - """ - # This directory is treated specially as it is normally - # a symlink. - linkName = os.path.join(get_repo_root_dir(), 'cmake') - delete_path(linkName) - specialDir = os.path.join(get_cmake_contrib_dir(), 'cmake') - - for (dirPath,_ , fileNames) in os.walk(get_cmake_contrib_dir()): - # Skip the special directory and its children - if dirPath.startswith(specialDir): - logging.info('Skipping directory "{}"'.format(dirPath)) - continue - for fileName in fileNames: - fileInContrib = os.path.join(dirPath, fileName) - # Skip files - if shouldSkipFile(fileInContrib): - logging.info('Skipping "{}"'.format(fileInContrib)) - continue - fileInRepo = contribPathToRepoPath(fileInContrib) - if os.path.exists(fileInRepo): - logging.info('Removing "{}"'.format(fileInRepo)) - delete_path(fileInRepo) - return True - def main(args): logging.basicConfig(level=logging.INFO) parser = argparse.ArgumentParser(description=__doc__) @@ -233,28 +38,10 @@ def main(args): logLevel = getattr(logging, pargs.log_level.upper(),None) logging.basicConfig(level=logLevel) - - # Before we start make sure we can transplant the CMake files on to - # repository - if verify_mirrored_directory_struture() != 0: - logging.error('"{}" does not mirror "{}"'.format(get_cmake_contrib_dir(), get_repo_root_dir())) - return 1 - - if pargs.mode == "create": - if not create(useHardLinks=pargs.hard_link): - logging.error("Failed to create") - return 1 - elif pargs.mode == "create_hard_link": - if not create(useHardLinks=True): - logging.error("Failed to create_hard_link") - return 1 - elif pargs.mode == "remove": - if not remove(): - logging.error("Failed to remove") - return 1 - else: - logging.error('Unknown mode "{}"'.format(pargs.mode)) - + logging.warning('Use of this script is deprecated. The script will be removed in the future') + logging.warning('Action "{}" ignored'.format(pargs.mode)) + if pargs.hard_link: + logging.warning('Hard link option ignored') return 0 if __name__ == '__main__': From 814fcd6a17e2602ddeb446347d89441c56162402 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 12 Jun 2017 10:44:19 +0100 Subject: [PATCH 4/6] [CMake] Remove documentation on "Bootstrapping". It is no longer relevant. --- README-CMake.md | 66 ------------------------------------------------- 1 file changed, 66 deletions(-) diff --git a/README-CMake.md b/README-CMake.md index 1b7d89542..7550808fc 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -33,34 +33,6 @@ git clean -fx src which will remove the generated source files. -### Bootstrapping - -Most of Z3's CMake files do not live in their correct location. Instead those -files live in the ``contrib/cmake`` folder and a script is provided that will -copy (or hard link) the files into their correct location. - -To copy the files run - -``` -python contrib/cmake/bootstrap.py create -``` - -in the root of the repository. Once you have done this you can now build Z3 using CMake. -Make sure you remember to rerun this command if you pull down new code/rebase/change branch so -that the copied CMake files are up to date. - -To remove the copied files run - -``` -python contrib/cmake/bootstrap.py remove -``` - -Note if you plan to do development on Z3 you should read the developer -notes on bootstrapping in this document. - -What follows is a brief walk through of how to build Z3 using some -of the more commonly used CMake generators. - ### Unix Makefiles Run the following in the top level directory of the Z3 repository. @@ -328,44 +300,6 @@ link is not created when building under Windows. These notes are help developers and packagers of Z3. -### Boostrapping the CMake build - -Z3's CMake system is experimental and not officially supported. Consequently -Z3's developers have decided that they do not want the CMake files in the -``src/`` and ``examples/`` folders. Instead the ``contrib/cmake/bootstrap.py`` -script copies or hard links them into the correct locations. For context -on this decision see https://github.com/Z3Prover/z3/pull/461 . - -The ``contrib/cmake/bootstrap.py create`` command just copies over files which makes -development harder because you have to copy your modifications over to the -files in ``contrib/cmake`` for your changes to committed to git. If you are on a UNIX like -platform you can create hard links instead by running - -``` -contrib/cmake/boostrap.py create --hard-link -``` - -Using hard links means that modifying any of the "copied" files also modifies the -file under version control. Using hard links also means that the file modification time -will appear correct (i.e. the hard-linked "copies" have the same file modification time -as the corresponding file under version control) which means CMake will correctly reconfigure -when invoked. This is why using symbolic links is not an option because the file modification -time of a symbolic link is not the same as the file modification of the file being pointed to. - -Unfortunately a downside to using hard links (or just plain copies) is that if -you pull down new code (i.e. ``git pull``) then some of the CMake files under -version control may change but the corresponding hard-linked "copies" will not. - -This mean that (regardless of whether or not you use hard links) every time you -pull down new code or change branch or do an interactive rebase you must run -(with or without ``--hard-link``): - -``` -contrb/cmake/boostrap.py create -``` - -in order to be sure that the copied CMake files are not out of date. - ### Install/Uninstall Install and uninstall targets are supported. Use ``CMAKE_INSTALL_PREFIX`` to From 3a692fe33c2992576ad381d050836a3b0913c996 Mon Sep 17 00:00:00 2001 From: "KangJing Huang (Chaserhkj)" Date: Tue, 13 Jun 2017 00:25:36 -0400 Subject: [PATCH 5/6] Add translate method for FuncDecl in java api --- src/api/java/FuncDecl.java | 32 +++++++++++++++++++++++++------- 1 file changed, 25 insertions(+), 7 deletions(-) diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java index 273e853c0..5909540b4 100644 --- a/src/api/java/FuncDecl.java +++ b/src/api/java/FuncDecl.java @@ -1,6 +1,6 @@ /** Copyright (c) 2012-2014 Microsoft Corporation - + Module Name: FuncDecl.java @@ -12,8 +12,8 @@ Author: @author Christoph Wintersteiger (cwinter) 2012-03-15 Notes: - -**/ + +**/ package com.microsoft.z3; @@ -59,6 +59,24 @@ public class FuncDecl extends AST return Native.getFuncDeclId(getContext().nCtx(), getNativeObject()); } + /** + * Translates (copies) the AST to the Context {@code ctx}. + * @param ctx A context + * + * @return A copy of the AST which is associated with {@code ctx} + * @throws Z3Exception on error + **/ + public FuncDecl translate(Context ctx) + { + + if (getContext() == ctx) { + return this; + } else { + return new FuncDecl(ctx, Native.translate(getContext().nCtx(), + getNativeObject(), ctx.nCtx())); + } + } + /** * The arity of the function declaration **/ @@ -68,7 +86,7 @@ public class FuncDecl extends AST } /** - * The size of the domain of the function declaration + * The size of the domain of the function declaration * @see #getArity **/ public int getDomainSize() @@ -324,7 +342,7 @@ public class FuncDecl extends AST } FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range) - + { super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.getNativeObject(), AST.arrayLength(domain), AST.arrayToNative(domain), @@ -333,7 +351,7 @@ public class FuncDecl extends AST } FuncDecl(Context ctx, String prefix, Sort[] domain, Sort range) - + { super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix, AST.arrayLength(domain), AST.arrayToNative(domain), @@ -351,7 +369,7 @@ public class FuncDecl extends AST } /** - * Create expression that applies function to arguments. + * Create expression that applies function to arguments. **/ public Expr apply(Expr ... args) { From 5799947183980eb440cfff243ca794e14872ce0b Mon Sep 17 00:00:00 2001 From: "KangJing Huang (Chaserhkj)" Date: Tue, 13 Jun 2017 02:37:41 -0400 Subject: [PATCH 6/6] Fix docstrings for FuncDecl.translate --- src/api/java/FuncDecl.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java index 5909540b4..8b1ad4b44 100644 --- a/src/api/java/FuncDecl.java +++ b/src/api/java/FuncDecl.java @@ -60,10 +60,10 @@ public class FuncDecl extends AST } /** - * Translates (copies) the AST to the Context {@code ctx}. + * Translates (copies) the function declaration to the Context {@code ctx}. * @param ctx A context * - * @return A copy of the AST which is associated with {@code ctx} + * @return A copy of the function declaration which is associated with {@code ctx} * @throws Z3Exception on error **/ public FuncDecl translate(Context ctx)