Z3Prover / z3

The Z3 Theorem Prover
Other
10.35k stars 1.48k forks source link

CMake fails to configure on Mac because of `PythonInterp` #6147

Closed victorpaleologue closed 2 years ago

victorpaleologue commented 2 years ago

On MacOS Monterey, arm64:

$ cmake -B build-vscode .      
-- Z3 version 4.9.2.0
-- Found simple git working directory
-- Found git directory "/Users/victor.paleologue/Code/Palaio/HTN/z3/.git"
-- Adding git dependency "/Users/victor.paleologue/Code/Palaio/HTN/z3/.git/HEAD"
-- Adding git dependency "/Users/victor.paleologue/Code/Palaio/HTN/z3/.git/refs/heads/master"
-- Using Git hash in version output: 9d9414c1110bc65108202cdcc473c703d12b54f1
-- Using Git description in version output: z3-4.8.4-6429-g9d9414c11
-- CMake generator: Unix Makefiles
-- Build type: Debug
-- Found PythonInterp: /usr/bin/python3 (found version "3.8.9") 
-- PYTHON_EXECUTABLE: /usr/bin/python3
-- Detected target architecture: arm64
-- Platform: Darwin
-- Not using libgmp
-- Not using Z3_API_LOG_SYNC
-- Thread-safe build
-- C++ compiler supports -Wall
-- Treating only serious compiler warnings as errors
-- C++ compiler supports -Werror=odr
-- C++ compiler supports -Werror=delete-non-virtual-dtor
-- C++ compiler supports -Werror=overloaded-virtual
-- C++ compiler supports -Werror=non-virtual-dtor
-- C++ compiler supports -Werror=null-dereference
-- C++ compiler does not support -Werror=no-unreachable-code-return
-- C++ compiler supports -fvisibility=hidden
-- C++ compiler supports -fvisibility-inlines-hidden
-- C++ compiler supports -fPIC
-- LTO disabled
-- CMAKE_CXX_FLAGS: " -Werror=odr  -Werror=delete-non-virtual-dtor  -Werror=overloaded-virtual  -Werror=non-virtual-dtor  -Werror=null-dereference "
-- CMAKE_EXE_LINKER_FLAGS: ""
-- CMAKE_STATIC_LINKER_FLAGS: ""
-- CMAKE_SHARED_LINKER_FLAGS: ""
-- CMAKE_CXX_FLAGS_DEBUG: "-g -O0"
-- CMAKE_EXE_LINKER_FLAGS_DEBUG: ""
-- CMAKE_SHARED_LINKER_FLAGS_DEBUG: ""
-- CMAKE_STATIC_LINKER_FLAGS_DEBUG: ""
-- Z3_COMPONENT_CXX_DEFINES: $<$<CONFIG:Debug>:Z3DEBUG>;$<$<CONFIG:Release>:_EXTERNAL_RELEASE>;$<$<CONFIG:RelWithDebInfo>:_EXTERNAL_RELEASE>;-D_MP_INTERNAL;$<$<CONFIG:Debug>:_TRACE>
-- Z3_COMPONENT_CXX_FLAGS: -Wall;-fvisibility=hidden;-fvisibility-inlines-hidden;-fPIC
-- Z3_DEPENDENT_LIBS: Threads::Threads
-- Z3_COMPONENT_EXTRA_INCLUDE_DIRS: /Users/victor.paleologue/Code/Palaio/HTN/z3/build-vscode/src;/Users/victor.paleologue/Code/Palaio/HTN/z3/src
-- Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS: 
-- CMAKE_INSTALL_LIBDIR: "lib"
-- CMAKE_INSTALL_BINDIR: "bin"
-- CMAKE_INSTALL_INCLUDEDIR: "include"
-- CMAKE_INSTALL_PKGCONFIGDIR: "lib/pkgconfig"
-- CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR: "lib/cmake/z3"
-- Adding component util
-- Adding component polynomial
-- Adding rule to generate "algebraic_params.hpp"
-- Adding component dd
-- Adding component hilbert
-- Adding component simplex
-- Adding component automata
-- Adding component interval
-- Adding component realclosure
-- Adding rule to generate "rcf_params.hpp"
-- Adding component subpaving
-- Adding component ast
-- Adding rule to generate "pp_params.hpp"
-- Adding component params
-- Adding rule to generate "arith_rewriter_params.hpp"
-- Adding rule to generate "array_rewriter_params.hpp"
-- Adding rule to generate "bool_rewriter_params.hpp"
-- Adding rule to generate "bv_rewriter_params.hpp"
-- Adding rule to generate "fpa_rewriter_params.hpp"
-- Adding rule to generate "fpa2bv_rewriter_params.hpp"
-- Adding rule to generate "pattern_inference_params_helper.hpp"
-- Adding rule to generate "poly_rewriter_params.hpp"
-- Adding rule to generate "rewriter_params.hpp"
-- Adding rule to generate "seq_rewriter_params.hpp"
-- Adding component rewriter
-- Adding component normal_forms
-- Adding rule to generate "nnf_params.hpp"
-- Adding component macros
-- Adding component model
-- Adding rule to generate "model_evaluator_params.hpp"
-- Adding rule to generate "model_params.hpp"
-- Adding component tactic
-- Adding rule to generate "tactic_params.hpp"
-- Adding component substitution
-- Adding component euf
-- Adding component smt_params
-- Adding rule to generate "smt_params_helper.hpp"
-- Adding component parser_util
-- Adding rule to generate "parser_params.hpp"
-- Adding component grobner
-- Adding component sat
-- Adding rule to generate "sat_asymm_branch_params.hpp"
-- Adding rule to generate "sat_params.hpp"
-- Adding rule to generate "sat_scc_params.hpp"
-- Adding rule to generate "sat_simplifier_params.hpp"
-- Adding component nlsat
-- Adding rule to generate "nlsat_params.hpp"
-- Adding component core_tactics
-- Adding component subpaving_tactic
-- Adding component aig_tactic
-- Adding component arith_tactics
-- Adding component solver
-- Adding rule to generate "combined_solver_params.hpp"
-- Adding rule to generate "parallel_params.hpp"
-- Adding rule to generate "solver_params.hpp"
-- Adding component cmd_context
-- Adding component extra_cmds
-- Adding component smt2parser
-- Adding component mbp
-- Adding component qe_lite
-- Adding component solver_assertions
-- Adding component pattern
-- Adding component bit_blaster
-- Adding component lp
-- Adding component sat_smt
-- Adding component sat_tactic
-- Adding component nlsat_tactic
-- Adding component ackermannization
-- Adding rule to generate "ackermannization_params.hpp"
-- Adding rule to generate "ackermannize_bv_tactic_params.hpp"
-- Adding component proofs
-- Adding component fpa
-- Adding component proto_model
-- Adding component smt
-- Adding component bv_tactics
-- Adding component smt_tactic
-- Adding component sls_tactic
-- Adding rule to generate "sls_params.hpp"
-- Adding component qe
-- Adding component muz
-- Adding rule to generate "fp_params.hpp"
-- Adding component dataflow
-- Adding component transforms
-- Adding component rel
-- Adding component clp
-- Adding component tab
-- Adding component bmc
-- Adding component ddnf
-- Adding component spacer
-- Adding component fp
-- Adding component ufbv_tactic
-- Adding component sat_solver
-- Adding component smtlogic_tactics
-- Adding rule to generate "qfufbv_tactic_params.hpp"
-- Adding component fpa_tactics
-- Adding component fd_solver
-- Adding component portfolio
-- Adding component opt
-- Adding rule to generate "opt_params.hpp"
-- Adding component api
-- Adding component api_dll
-- Adding component fuzzing
-- Building documentation disabled
-- Configuring done
-- Generating done
-- Build files have been written to: /Users/victor.paleologue/Code/Palaio/HTN/z3/build-vscode

~/Code/Palaio/HTN/z3 on  master! ⌚ 14:33:24
$ cmake -B build-host .  
-- The CXX compiler identification is AppleClang 13.1.6.13160021
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Check for working CXX compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/c++ - skipped
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Z3 version 4.9.2.0
-- Found simple git working directory
-- Found git directory "/Users/victor.paleologue/Code/Palaio/HTN/z3/.git"
-- Adding git dependency "/Users/victor.paleologue/Code/Palaio/HTN/z3/.git/HEAD"
-- Adding git dependency "/Users/victor.paleologue/Code/Palaio/HTN/z3/.git/refs/heads/master"
-- Found Git: /usr/bin/git (found version "2.32.1 (Apple Git-133)") 
-- Using Git hash in version output: 9d9414c1110bc65108202cdcc473c703d12b54f1
-- Using Git description in version output: z3-4.8.4-6429-g9d9414c11
-- CMake generator: Unix Makefiles
-- CMAKE_BUILD_TYPE is not set. Setting default
-- The available build types are: Debug;Release;RelWithDebInfo;MinSizeRel
-- Build type: RelWithDebInfo
CMake Error at /Applications/CMake.app/Contents/share/cmake-3.22/Modules/FindPackageHandleStandardArgs.cmake:230 (message):
  Could NOT find PythonInterp (missing: PYTHON_EXECUTABLE)
Call Stack (most recent call first):
  /Applications/CMake.app/Contents/share/cmake-3.22/Modules/FindPackageHandleStandardArgs.cmake:594 (_FPHSA_FAILURE_MESSAGE)
  /Applications/CMake.app/Contents/share/cmake-3.22/Modules/FindPythonInterp.cmake:169 (FIND_PACKAGE_HANDLE_STANDARD_ARGS)
  CMakeLists.txt:163 (find_package)

-- Configuring incomplete, errors occurred!
See also "/Users/victor.paleologue/Code/Palaio/HTN/z3/build-host/CMakeFiles/CMakeOutput.log".
See also "/Users/victor.paleologue/Code/Palaio/HTN/z3/build-host/CMakeFiles/CMakeError.log".
victorpaleologue commented 2 years ago

@NikolajBjorner thank you for the swift merge! I guess I can close the issue now; please let me know if I got it wrong.