search

mht208 / homebrew-formal

Homebrew formulae for formal methods
36 stars 10 forks source link

Building z3 fails on OS X 10.9 #3

Open ehamberg opened 10 years ago

ehamberg commented 10 years ago

Building z3 fails on OS X 10.9. Output from brew install -v3 z3:

$ brew install -v3 z3
==> Cloning https://git01.codeplex.com/z3
git --git-dir /Library/Caches/Homebrew/z3--git/.git status -s
Updating /Library/Caches/Homebrew/z3--git
git config remote.origin.url https://git01.codeplex.com/z3
git config remote.origin.fetch +refs/tags/v4.3.1:refs/tags/v4.3.1
git --git-dir /Library/Caches/Homebrew/z3--git/.git rev-parse -q --verify v4.3.1
git checkout -f v4.3.1
HEAD is now at 89c1785... fixed clang++ for linux
git reset --hard v4.3.1
HEAD is now at 89c1785 fixed clang++ for linux
==> Checking out tag v4.3.1
git checkout-index -a -f --prefix=/private/tmp/z3-UO51/
==> autoconf
==> ./configure --prefix=/usr/local/Cellar/z3/4.3.1
checking whether we are using the GNU C++ compiler... no
checking whether clang++ accepts -g... no
checking for gcc... clang
checking whether we are using the GNU C compiler... no
checking whether clang accepts -g... no
checking for clang option to accept ISO C89... unsupported
checking whether make sets $(MAKE)... yes
checking for grep that handles long lines and -e... /usr/bin/grep
checking for a sed that does not truncate output... /usr/local/bin/gsed
checking size of int *... 8
configure: creating ./config.status
config.status: creating scripts/config-debug.mk
config.status: creating scripts/config-release.mk
Z3 was configured with success.
Host platform:  osx
Compiler:       clang++
Arithmetic:     internal
Python:         python
Prefix:         /usr/local/Cellar/z3/4.3.1
64-bit:         yes

To build and install Z3, execute:
   python scripts/mk_make.py
   cd build
   make
   sudo make install
==> /usr/local/opt/python/bin/python2 scripts/mk_make.py
New component: 'util'
New component: 'polynomial'
New component: 'sat'
New component: 'nlsat'
New component: 'interval'
New component: 'subpaving'
New component: 'ast'
New component: 'rewriter'
New component: 'model'
New component: 'tactic'
New component: 'substitution'
New component: 'parser_util'
New component: 'grobner'
New component: 'euclid'
New component: 'front_end_params'
New component: 'simplifier'
New component: 'normal_forms'
New component: 'core_tactics'
New component: 'sat_tactic'
New component: 'arith_tactics'
New component: 'nlsat_tactic'
New component: 'subpaving_tactic'
New component: 'aig_tactic'
New component: 'solver'
New component: 'cmd_context'
New component: 'extra_cmds'
New component: 'smt2parser'
New component: 'pattern'
New component: 'macros'
New component: 'proof_checker'
New component: 'bit_blaster'
New component: 'proto_model'
New component: 'smt'
New component: 'user_plugin'
New component: 'bv_tactics'
New component: 'fuzzing'
New component: 'fpa'
New component: 'smt_tactic'
New component: 'sls_tactic'
New component: 'muz_qe'
New component: 'smtlogic_tactics'
New component: 'ufbv_tactic'
New component: 'portfolio'
New component: 'smtparser'
New component: 'api'
New component: 'shell'
New component: 'test'
New component: 'api_dll'
New component: 'dotnet'
New component: 'cpp'
Python bindinds directory was detected.
New component: 'cpp_example'
New component: 'c_example'
New component: 'maxsat'
New component: 'dotnet_example'
New component: 'py_example'
Generated 'src/util/version.h'
Updated 'src/api/dotnet/Properties/AssemblyInfo.cs'
Generated 'src/ast/pattern/database.h'
Generated 'src/shell/install_tactic.cpp'
Generated 'src/test/install_tactic.cpp'
Generated 'src/api/dll/install_tactic.cpp'
Generated 'src/api/python/z3consts.py'
Generated 'src/api/dotnet/Enumerations.cs'
Generated 'src/api/api_log_macros.h'
Generated 'src/api/api_log_macros.cpp'
Generated 'src/api/api_commands.cpp'
Generated 'src/api/python/z3core.py'
Generated 'src/api/dotnet/Native.cs'
Listing src/api/python ...
Compiling src/api/python/z3.py ...
Compiling src/api/python/z3consts.py ...
Compiling src/api/python/z3core.py ...
Compiling src/api/python/z3printer.py ...
Compiling src/api/python/z3test.py ...
Compiling src/api/python/z3types.py ...
Generated 'z3.pyc'
Generated 'z3consts.pyc'
Generated 'z3core.pyc'
Generated 'z3printer.pyc'
Generated 'z3test.pyc'
Generated 'z3types.pyc'
Writing build/Makefile
Copied Z3Py example 'example.py' to 'build'
Makefile was successfully generated.
  python packages dir: /usr/local/Cellar/z3/4.3.1/lib/python2.7/site-packages
  compilation mode: Release
Type 'cd build; make' to build Z3
==> make
src/smt/smt_statistics.cpp
src/util/approx_nat.cpp
src/util/common_msgs.cpp
src/util/instruction_count.cpp
src/util/luby.cpp
src/util/mem_stat.cpp
src/util/scoped_ctrl_c.cpp
src/test/ex.cpp
src/test/timeout.cpp
src/api/dll/dll.cpp
src/util/approx_set.cpp
src/util/cooperate.cpp
src/util/hash.cpp
src/util/page.cpp
src/util/timeit.cpp
src/util/z3_exception.cpp
src/test/api_bug.cpp
src/test/for_each_file.cpp
src/test/get_implied_equalities.cpp
src/test/optional.cpp
src/test/smt2print_parse.cpp
src/util/bit_util.cpp
src/util/bit_vector.cpp
src/util/debug.cpp
src/util/lbool.cpp
src/util/permutation.cpp
src/util/prime_generator.cpp
src/util/region.cpp
src/util/scoped_timer.cpp
src/util/small_object_allocator.cpp
src/util/stack.cpp
src/util/timeout.cpp
src/util/timer.cpp
src/util/trace.cpp
src/test/bit_vector.cpp
src/test/chashtable.cpp
src/test/escaped.cpp
src/test/hashtable.cpp
src/test/heap.cpp
src/test/list.cpp
src/test/main.cpp
src/test/map.cpp
src/test/mpfx.cpp
src/test/permutation.cpp
src/test/random.cpp
src/test/region.cpp
src/test/small_object_allocator.cpp
src/test/stack.cpp
src/test/uint_set.cpp
src/test/vector.cpp
src/shell/z3_log_frontend.cpp
src/api/api_commands.cpp
src/api/api_log.cpp
src/sat/sat_clause.cpp
src/sat/sat_clause_set.cpp
src/sat/sat_clause_use_list.cpp
src/sat/sat_model_converter.cpp
src/sat/sat_watched.cpp
src/util/mpn.cpp
src/util/mpz.cpp
src/test/bits.cpp
src/test/buffer.cpp
src/test/interval_skip_list.cpp
src/test/prime_generator.cpp
src/test/string_buffer.cpp
src/api/z3_replayer.cpp
src/math/euclid/euclidean_solver.cpp
src/util/cmd_context_types.cpp
src/util/hwf.cpp
src/util/mpf.cpp
src/util/mpff.cpp
src/util/mpfx.cpp
src/util/mpq.cpp
In file included from ../src/util/hwf.cpp:52:
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../lib/clang/5.0/include/emmintrin.h:1388:22: error: expected expression
  return (__m128)__in;
                     ^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../lib/clang/5.0/include/emmintrin.h:1394:23: error: expected expression
  return (__m128i)__in;
                      ^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../lib/clang/5.0/include/emmintrin.h:1400:23: error: expected expression
  return (__m128d)__in;
                      ^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../lib/clang/5.0/include/emmintrin.h:1406:23: error: expected expression
  return (__m128i)__in;
                      ^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../lib/clang/5.0/include/emmintrin.h:1412:22: error: expected expression
  return (__m128)__in;
                     ^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../lib/clang/5.0/include/emmintrin.h:1418:23: error: expected expression
  return (__m128d)__in;
                      ^
src/util/smt2_util.cpp
6 errors generated.
make: *** [util/hwf.o] Error 1
make: *** Waiting for unfinished jobs....
==> Formula
Tap: mht208/formal
Path: /usr/local/Library/Taps/mht208-formal/z3.rb
==> Configuration
HOMEBREW_VERSION: 0.9.5
HEAD: 32726535393df26e6f2a0b8d972b3b1a2d7afa12
CPU: 8-core 64-bit ivybridge
OS X: 10.9-x86_64
Xcode: 5.0.2
CLT: 5.0.1.0.1.1382131676
X11: 2.7.5 => /opt/X11
==> ENV
HOMEBREW_CC: clang
HOMEBREW_CXX: clang++
MAKEFLAGS: -j8
CMAKE_PREFIX_PATH: /usr/local
CMAKE_INCLUDE_PATH: /usr/include/libxml2:/System/Library/Frameworks/OpenGL.framework/Versions/Current/Headers:/usr/local/opt/python/Frameworks/Python.framework/Versions/2.7/Headers
CMAKE_LIBRARY_PATH: /System/Library/Frameworks/OpenGL.framework/Versions/Current/Libraries
PKG_CONFIG_PATH: /usr/local/opt/python/Frameworks/Python.framework/Versions/2.7/lib/pkgconfig
PKG_CONFIG_LIBDIR: /usr/lib/pkgconfig:/usr/local/Library/ENV/pkgconfig/10.9
HOMEBREW_VERBOSE: 1
ACLOCAL_PATH: /usr/local/share/aclocal
PATH: /usr/local/opt/python/bin:/usr/local/Library/ENV/4.3:/usr/local/opt/autoconf/bin:/usr/local/opt/git/bin:/usr/bin:/bin:/usr/sbin:/sbin:/usr/local/bin

Error: z3 did not build
Logs:
     /Users/ehamberg/Library/Logs/Homebrew/z3/01.autoconf
     /Users/ehamberg/Library/Logs/Homebrew/z3/02.4.3.1
     /Users/ehamberg/Library/Logs/Homebrew/z3/02.4.3.1.cc
     /Users/ehamberg/Library/Logs/Homebrew/z3/03.python2
     /Users/ehamberg/Library/Logs/Homebrew/z3/04.make
     /Users/ehamberg/Library/Logs/Homebrew/z3/04.make.cc
     /Users/ehamberg/Library/Logs/Homebrew/z3/config.log
mht208 commented 10 years ago

I found a thread discussing this problem: http://z3.codeplex.com/workitem/74