New upstream version.
Also: - All patches except -sse2 have been upstreamed; drop them. - Upstream now ships __init__.py; drop our version. - Drop all the buildroot tricks; Makefile supports DESTDIR now. - Use C.UTF-8 instead of en_US.UTF-8.
This commit is contained in:
Jerry James
parent
bf833fdae8
commit
1afb4a3f9f
|
|
@ -1,2 +1,3 @@
|
|||
/z3-4.4.0.tar.gz
|
||||
/z3-4.4.1.tar.gz
|
||||
/z3-4.5.0.tar.gz
|
||||
|
|
|
|||
2
sources
2
sources
|
|
@ -1 +1 @@
|
|||
4336a9df24f090e711c6d42fd4e2b1fc z3-4.4.1.tar.gz
|
||||
f332befa0d66d81818a06279a0973e25 z3-4.5.0.tar.gz
|
||||
|
|
|
|||
|
|
@ -1,23 +0,0 @@
|
|||
From 27399309009314f56cdfbd8333f287b1a9b7a3a6 Mon Sep 17 00:00:00 2001
|
||||
From: Nuno Lopes <nlopes@microsoft.com>
|
||||
Date: Fri, 27 Nov 2015 12:13:44 +0000
|
||||
Subject: [PATCH] fix build with clang
|
||||
|
||||
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
|
||||
---
|
||||
src/util/mpz.cpp | 2 +-
|
||||
1 file changed, 1 insertion(+), 1 deletion(-)
|
||||
|
||||
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
|
||||
index 8559279..7dca14b 100644
|
||||
--- a/src/util/mpz.cpp
|
||||
+++ b/src/util/mpz.cpp
|
||||
@@ -134,7 +134,7 @@ mpz_manager<SYNCH>::mpz_manager():
|
||||
#endif
|
||||
|
||||
mpz one(1);
|
||||
- set(m_two64, UINT64_MAX);
|
||||
+ set(m_two64, (uint64)UINT64_MAX);
|
||||
add(m_two64, one, m_two64);
|
||||
}
|
||||
|
||||
|
|
@ -1,20 +1,12 @@
|
|||
--- ./src/util/hwf.cpp.orig 2015-10-05 06:07:19.000000000 -0600
|
||||
+++ ./src/util/hwf.cpp 2015-10-08 19:57:59.046584973 -0600
|
||||
@@ -29,7 +29,7 @@ Revision History:
|
||||
--- src/util/hwf.cpp.orig 2016-11-07 15:02:30.000000000 -0700
|
||||
+++ src/util/hwf.cpp 2016-11-08 21:01:53.533487316 -0700
|
||||
@@ -29,8 +29,7 @@ Revision History:
|
||||
#include<fenv.h>
|
||||
#endif
|
||||
|
||||
-#ifndef _M_IA64
|
||||
+#ifdef __x86_64
|
||||
-#if defined(__x86_64__) || defined(_M_X64) || \
|
||||
- defined(__i386) || defined(_M_IX86)
|
||||
+#if defined(__x86_64__) || defined(_M_X64)
|
||||
#define USE_INTRINSICS
|
||||
#endif
|
||||
|
||||
@@ -47,7 +47,7 @@ Revision History:
|
||||
// Luckily, these are kind of standardized, at least for Windows/Linux/OSX.
|
||||
#ifdef __clang__
|
||||
#undef USE_INTRINSICS
|
||||
-#else
|
||||
+#elif defined(USE_INTRINSICS)
|
||||
#include <emmintrin.h>
|
||||
#endif
|
||||
|
||||
|
|
|
|||
|
|
@ -1,23 +0,0 @@
|
|||
From f02d273ee39ae047222e362c37213d29135dc661 Mon Sep 17 00:00:00 2001
|
||||
From: Jonathan Wakely <github@kayari.org>
|
||||
Date: Tue, 2 Feb 2016 23:39:11 +0000
|
||||
Subject: [PATCH] Convert stream to bool explicitly
|
||||
|
||||
In C++11 there is no implicit conversion from iostream classes to `void*`, just an explicit conversion to bool.
|
||||
---
|
||||
src/util/debug.cpp | 2 +-
|
||||
1 file changed, 1 insertion(+), 1 deletion(-)
|
||||
|
||||
diff --git a/src/util/debug.cpp b/src/util/debug.cpp
|
||||
index 54c67fe..66676c6 100644
|
||||
--- a/src/util/debug.cpp
|
||||
+++ b/src/util/debug.cpp
|
||||
@@ -76,7 +76,7 @@ void invoke_gdb() {
|
||||
for (;;) {
|
||||
std::cerr << "(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB\n";
|
||||
char result;
|
||||
- bool ok = (std::cin >> result);
|
||||
+ bool ok = bool(std::cin >> result);
|
||||
if (!ok) exit(ERR_INTERNAL_FATAL); // happens if std::cin is eof or unattached.
|
||||
switch(result) {
|
||||
case 'C':
|
||||
83
z3.spec
83
z3.spec
|
|
@ -4,23 +4,18 @@
|
|||
# and submit the results upstream, I'm sure many people would be grateful.
|
||||
|
||||
%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
|
||||
%global medtag 95c9ccb2959a
|
||||
%global medtag d57a2a6dce92
|
||||
|
||||
Name: z3
|
||||
Version: 4.4.1
|
||||
Release: 8%{?dist}
|
||||
Version: 4.5.0
|
||||
Release: 1%{?dist}
|
||||
Summary: Satisfiability Modulo Theories (SMT) solver
|
||||
|
||||
License: MIT
|
||||
URL: https://github.com/Z3Prover/z3
|
||||
Source0: https://github.com/Z3Prover/z3/archive/%{name}-%{version}.tar.gz
|
||||
Source1: %{name}_init.py
|
||||
# Do not try to build with SSE2 on non-x86_64 arches
|
||||
Patch0: %{name}-sse2.patch
|
||||
# https://github.com/Z3Prover/z3/pull/427
|
||||
Patch1: %{name}-stream-bool.patch
|
||||
# https://github.com/Z3Prover/z3/commit/27399309009314f56cdfbd8333f287b1a9b7a3a6
|
||||
Patch2: %{name}-ambiguous-overload.patch
|
||||
|
||||
BuildRequires: doxygen
|
||||
BuildRequires: gcc-c++
|
||||
|
|
@ -32,6 +27,7 @@ BuildRequires: ocaml
|
|||
BuildRequires: ocaml-findlib
|
||||
BuildRequires: ocaml-ocamldoc
|
||||
BuildRequires: python2-devel
|
||||
BuildRequires: python2-setuptools
|
||||
|
||||
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
|
||||
|
||||
|
|
@ -96,25 +92,23 @@ Python 2 interface to z3.
|
|||
%prep
|
||||
%setup -q -n %{name}-%{name}-%{version}
|
||||
%patch0
|
||||
%patch1 -p1
|
||||
%patch2 -p1
|
||||
|
||||
# Install python objects into the right place, enable verbose builds, use
|
||||
# Fedora CFLAGS, preserve timestamps when installing, include the entire
|
||||
# contents of the archives in the library, link the library with the correct
|
||||
# flags, don't hide library symbols needed by the executable, and use an
|
||||
# soname.
|
||||
# flags, don't hide library symbols needed by the executable, use an soname,
|
||||
# and build the ocaml files with debug info.
|
||||
sed -e "s|^\(PYTHON_PACKAGE_DIR=\).*|\1'%{python2_sitearch}/z3'|" \
|
||||
-e "s|\(PYTHON_PACKAGE_DIR = \).*|\1'%{buildroot}%{python2_sitearch}/z3'|" \
|
||||
-e 's/@$(CXX)/$(CXX)/' \
|
||||
-e 's/ -O3//;s/ -fomit-frame-pointer//' \
|
||||
-e "s/@cp /&-p /" \
|
||||
-e "s/\(['\"]\)cp\([^[:alnum:]]\)/\1cp -p\2/" \
|
||||
-e "s/\(SLIBEXTRAFLAGS = '\)'/\1-Wl,--no-whole-archive -Wl,--as-needed'/" \
|
||||
-e "s|-shared|& $RPM_LD_FLAGS -Wl,--whole-archive|" \
|
||||
-e "/SLIBFLAGS/s|-shared|& $RPM_LD_FLAGS -Wl,--whole-archive|" \
|
||||
-e 's/\(libz3$(SO_EXT)\)\(\\n\)/\1 -Wl,--no-whole-archive\2/' \
|
||||
-e "s/'tstomp\.cpp',/& '-fPIC',/" \
|
||||
-e 's/ -fvisibility=hidden//' \
|
||||
-e '/dllfile/s/\$(SLINK_FLAGS)/& -Wl,-h,lib%{name}.so.0/' \
|
||||
-e '/dll_file/s/\$(SLINK_FLAGS)/& -Wl,-h,lib%{name}.so.0/' \
|
||||
-e "s/OCAML_FLAGS = ''/OCAML_FLAGS = '-g'/" \
|
||||
-i scripts/mk_util.py
|
||||
|
||||
# Do not try to build with SSE2 support on non-x86_64 arches.
|
||||
|
|
@ -123,7 +117,7 @@ sed -i 's/exec_compiler_cmd.*-msse.*:/None:/' scripts/mk_util.py
|
|||
%endif
|
||||
|
||||
# Comply with the Java packaging guidelines
|
||||
sed -e 's,\(System\.load\)Library("\([^"]*\)"),\1("%{_libdir}/z3/\2.so"),' \
|
||||
sed -e 's,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so"),' \
|
||||
-i scripts/update_api.py
|
||||
|
||||
# Fix character encoding
|
||||
|
|
@ -132,22 +126,25 @@ touch -r RELEASE_NOTES RELEASE_NOTES.utf8
|
|||
mv -f RELEASE_NOTES.utf8 RELEASE_NOTES
|
||||
|
||||
# Fix permissions
|
||||
chmod a-x examples/interp/iz3.cpp
|
||||
find -O3 src -type f -perm /0111 \( -name \*.cpp -o -name \*.h \) \
|
||||
-exec chmod 0644 {} +
|
||||
|
||||
# Fix ocaml documentation generation (broken in 4.4.0)
|
||||
sed -i 's,api\\html\\ml,api/html/ml,' doc/mk_api_doc.py
|
||||
# Fix ocaml documentation generation (broken in 4.4.0, broken more in 4.5.0)
|
||||
sed -e 's,api\\html\\ml,api/html/ml,' \
|
||||
-e 's,python/z3.py,python/z3/z3.py,' \
|
||||
-e 's,z3enums\.mli,z3enums.ml,' \
|
||||
-i doc/mk_api_doc.py
|
||||
|
||||
%build
|
||||
export CXXFLAGS="$RPM_OPT_FLAGS -fPIC"
|
||||
export LDFLAGS="$RPM_LD_FLAGS -Wl,--as-needed -lgmp"
|
||||
export LANG="en_US.UTF-8"
|
||||
export LANG="C.UTF-8"
|
||||
export PYTHON="%{__python2}"
|
||||
|
||||
# This is NOT an autoconf-generated configure script.
|
||||
./configure -p %{buildroot}%{_prefix} --githash=%{medtag} --gmp --java --ml
|
||||
make %{?_smp_mflags} -C build
|
||||
./configure -p %{_prefix} --githash=%{medtag} --gmp --java --ml
|
||||
# FIXME: intermittent build failures with %%{?_smp_mflags}
|
||||
make -C build
|
||||
|
||||
# The z3 binary is NOT linked with libz3, but instead has duplicate copies of a
|
||||
# lot of object files, so rebuild it. But first, add library links.
|
||||
|
|
@ -164,15 +161,10 @@ pushd doc
|
|||
popd
|
||||
|
||||
%install
|
||||
export LANG="en_US.UTF-8"
|
||||
|
||||
# Install the ocaml interface in the right place
|
||||
sed 's,ocamlfind [[:alpha:]]* ,&-destdir %{buildroot}%{_libdir}/ocaml -ldconf ignore ,' \
|
||||
-i build/Makefile
|
||||
export LANG="C.UTF-8"
|
||||
|
||||
# Install
|
||||
mkdir -p %{buildroot}%{python2_sitearch}/%{name} %{buildroot}%{_libdir}/ocaml
|
||||
make -C build install
|
||||
make -C build install DESTDIR=%{buildroot}
|
||||
|
||||
# On 64-bit systems, move the library to the right directory
|
||||
if [ "%{_libdir}" != "%{_prefix}/lib" ]; then
|
||||
|
|
@ -189,15 +181,11 @@ ln -s libz3.so.0 %{buildroot}%{_libdir}/libz3.so
|
|||
mkdir -p %{buildroot}%{_includedir}/%{name}
|
||||
mv %{buildroot}%{_includedir}/*.h %{buildroot}%{_includedir}/%{name}
|
||||
|
||||
# Link, rather than copy, the library into the python and ocaml dirs
|
||||
rm -f %{buildroot}%{python2_sitearch}/%{name}/lib%{name}.so
|
||||
# Install the python interface
|
||||
mkdir -p %{buildroot}%{python2_sitearch}
|
||||
cp -a build/python/%{name} %{buildroot}%{python2_sitearch}
|
||||
ln -s %{_libdir}/lib%{name}.so.0 \
|
||||
%{buildroot}%{python2_sitearch}/%{name}/lib%{name}.so
|
||||
rm -f %{buildroot}%{_libdir}/ocaml/Z3/lib%{name}.so
|
||||
ln -s %{_libdir}/lib%{name}.so.0 %{buildroot}%{_libdir}/ocaml/Z3/lib%{name}.so
|
||||
|
||||
# Add __init__.py for the python module
|
||||
cp -p %{SOURCE1} %{buildroot}%{python2_sitearch}/%{name}/__init__.py
|
||||
|
||||
# Move the Java interface to its correct location
|
||||
mkdir -p %{buildroot}%{_libdir}/%{name}
|
||||
|
|
@ -206,10 +194,6 @@ mv %{buildroot}%{_prefix}/lib/*.jar %{buildroot}%{_jnidir}
|
|||
ln -s %{_jnidir}/com.microsoft.z3.jar %{buildroot}%{_libdir}/%{name}
|
||||
mv %{buildroot}%{_prefix}/lib/lib%{name}java.so %{buildroot}%{_libdir}/%{name}
|
||||
|
||||
# Fix permissions
|
||||
chmod 0755 %{buildroot}%{_bindir}/* %{buildroot}%{_libdir}/*.so.0.0.0 \
|
||||
%{buildroot}%{_libdir}/%{name}/*.so
|
||||
|
||||
#%%check
|
||||
# Some of the tests require more memory than the koji builders have available.
|
||||
# However, valgrind also shows a large number of memory leaks. I will work
|
||||
|
|
@ -217,7 +201,7 @@ chmod 0755 %{buildroot}%{_bindir}/* %{buildroot}%{_libdir}/*.so.0.0.0 \
|
|||
# run on the koji builders successfully. If not, the tests will have to be run
|
||||
# manually on machines with more available memory.
|
||||
#
|
||||
#export LANG="en_US.UTF-8"
|
||||
#export LANG="C.UTF-8"
|
||||
#pushd build
|
||||
#make test
|
||||
#./test-z3 /a
|
||||
|
|
@ -228,7 +212,7 @@ chmod 0755 %{buildroot}%{_bindir}/* %{buildroot}%{_libdir}/*.so.0.0.0 \
|
|||
%postun libs -p /sbin/ldconfig
|
||||
|
||||
%files
|
||||
%doc README RELEASE_NOTES
|
||||
%doc README.md RELEASE_NOTES
|
||||
%{_bindir}/%{name}
|
||||
|
||||
%files libs
|
||||
|
|
@ -250,23 +234,28 @@ chmod 0755 %{buildroot}%{_bindir}/* %{buildroot}%{_libdir}/*.so.0.0.0 \
|
|||
%files -n ocaml-%{name}
|
||||
%dir %{_libdir}/ocaml/Z3/
|
||||
%{_libdir}/ocaml/Z3/META
|
||||
%{_libdir}/ocaml/Z3/*.a
|
||||
%{_libdir}/ocaml/Z3/*.cma
|
||||
%{_libdir}/ocaml/Z3/*.cmi
|
||||
%{_libdir}/ocaml/Z3/*.cmo
|
||||
%{_libdir}/ocaml/Z3/*.o
|
||||
%{_libdir}/ocaml/Z3/*.cmxs
|
||||
%{_libdir}/ocaml/Z3/*.so
|
||||
|
||||
%files -n ocaml-%{name}-devel
|
||||
%{_libdir}/ocaml/Z3/*.a
|
||||
%{_libdir}/ocaml/Z3/*.cmx
|
||||
%{_libdir}/ocaml/Z3/*.cmxa
|
||||
%{_libdir}/ocaml/Z3/*.ml
|
||||
%{_libdir}/ocaml/Z3/*.mli
|
||||
|
||||
%files -n python-%{name}
|
||||
%{python2_sitearch}/%{name}/
|
||||
|
||||
%changelog
|
||||
* Tue Nov 8 2016 Jerry James <loganjerry@gmail.com> - 4.5.0-1
|
||||
- New upstream version
|
||||
- All patches except -sse2 have been upstreamed; drop them
|
||||
- Upstream now ships __init__.py; drop our version
|
||||
- Drop all the buildroot tricks; Makefile supports DESTDIR now
|
||||
- Use C.UTF-8 instead of en_US.UTF-8
|
||||
|
||||
* Sat Nov 05 2016 Richard W.M. Jones <rjones@redhat.com> - 4.4.1-8
|
||||
- Rebuild for OCaml 4.04.0.
|
||||
|
||||
|
|
|
|||
|
|
@ -1 +0,0 @@
|
|||
from z3 import *
|
||||
Loading…
Reference in New Issue