rpms
/
z3
2
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

New upstream version.

This commit is contained in:
Jerry James 2015-05-28 10:05:25 -06:00
parent f43a07744b
commit ec1011a621
5 changed files with 1812 additions and 53 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.gitignore vendored
View File

@ -1 +1,2 @@
/Z3Prover-z3-29606b5.tar.gz
/z3-4.4.0.tar.gz

2
sources
View File

@ -1 +1 @@
634e88648020946f2895b77174f8f557 Z3Prover-z3-29606b5.tar.gz
2bcbb0381cc1572cace99aac8af08990 z3-4.4.0.tar.gz

1761
z3-export.patch Normal file
View File

File diff suppressed because it is too large Load Diff

6
z3-sse2.patch
View File

@ -1,7 +1,5 @@
diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp
index 40d20b6..afcde2d 100644
--- a/src/util/hwf.cpp
+++ b/src/util/hwf.cpp
--- ./src/util/hwf.cpp.orig 2015-04-29 08:40:46.000000000 -0600
+++ ./src/util/hwf.cpp 2015-05-27 21:40:59.984496739 -0600
@@ -31,7 +31,7 @@ Revision History:
#include <fenv.h>
#endif

95
z3.spec
View File

@ -4,22 +4,20 @@
# and submit the results upstream, I'm sure many people would be grateful.
%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
%global gitdate 20150329
%global gittag 29606b5179f76783ffb0c2ca0ed9d614847064b3
%global shorttag %(cut -b -7 <<< %{gittag})
%global medtag %(cut -b -12 <<< %{gittag})
%global user Z3Prover
%global medtag 7f6ef0b6c081
Name: z3
Version: 4.3.2
Release: 3.%{gitdate}git.%{shorttag}%{?dist}
Version: 4.4.0
Release: 1%{?dist}
Summary: Satisfiability Modulo Theories (SMT) solver
License: MIT
URL: https://github.com/Z3Prover/z3
Source0: https://github.com/%{user}/%{name}/tarball/%{gittag}/%{user}-%{name}-%{shorttag}.tar.gz
Source0: https://github.com/Z3Prover/z3/archive/%{name}-%{version}.tar.gz
# Do not try to build with SSE2 on non-x86_64 arches
Patch0: %{name}-sse2.patch
# Export symbols needed by the z3 binary; problem started with 4.4.0 release
Patch1: %{name}-export.patch
BuildRequires: doxygen
BuildRequires: gmp-devel
@ -27,7 +25,8 @@ BuildRequires: graphviz
BuildRequires: java-devel
BuildRequires: jpackage-utils
BuildRequires: ocaml
BuildRequires: ocaml-camlidl-devel
BuildRequires: ocaml-findlib
BuildRequires: ocaml-ocamldoc
BuildRequires: python2-devel
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
@ -91,8 +90,9 @@ Requires: %{name}-libs%{?_isa} = %{version}-%{release}
Python 2 interface to z3.
%prep
%setup -q -n %{user}-%{name}-%{shorttag}
%patch0 -p1
%setup -q -n %{name}-%{name}-%{version}
%patch0
%patch1
# Install python objects into the right place, enable verbose builds, use
# Fedora CFLAGS, preserve timestamps when installing, include the entire
@ -128,6 +128,11 @@ 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 \) | \
xargs 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
%build
export CXXFLAGS="$RPM_OPT_FLAGS -fPIC"
@ -136,7 +141,7 @@ export LANG="en_US.UTF-8"
export PYTHON="%{__python2}"
# This is NOT an autoconf-generated configure script.
./configure -p %{buildroot}%{_prefix} --githash=%{medtag} --gmp --java
./configure -p %{buildroot}%{_prefix} --githash=%{medtag} --gmp --java --ml
make %{?_smp_mflags} -C build
# The z3 binary is NOT linked with libz3, but instead has duplicate copies of a
@ -145,36 +150,23 @@ pushd build
mv libz3.so libz3.so.0.0.0
ln -s libz3.so.0.0.0 libz3.so.0
ln -s libz3.so.0 libz3.so
g++ $CXXFLAGS -fopenmp -o z3 shell/*.o $LDFLAGS -L. -lz3
popd
# Build the ocaml interface
pushd src/api/ml
./generate_mlapi.sh
%if %{opt}
ocamlopt -c -g -ccopt -g -ccopt -fomit-frame-pointer -ccopt -Wno-cast-qual \
-I .. z3_stubs.c z3_theory_stubs.c z3.mli z3.ml
ar rcs libz3stubs.a z3.o z3_stubs.o z3_theory_stubs.o
ocamlopt -a -g -ccopt -g -cclib -L$PWD/../../../build -cclib -lz3 \
-cclib -lcamlidl -cclib -lz3stubs z3.cmx -o z3.cmxa
%endif
ocamlc -c -g -ccopt -g -ccopt -fomit-frame-pointer -ccopt -Wno-cast-qual \
-I .. z3_stubs.c z3_theory_stubs.c z3.mli z3.ml
ar rcs libz3stubs.a z3.o z3_stubs.o z3_theory_stubs.o
ocamlc -custom -a -g -ccopt -g -cclib -L$PWD/../../../build -cclib -lz3 \
-cclib -lcamlidl -cclib -lz3stubs z3.cmo -o z3.cma
ocamlmktop -o ocamlz3 z3.cma -ccopt -L. -cclib -lz3 -cclib -lcamlidl
g++ $RPM_OPT_FLAGS -fopenmp -o z3 shell/*.o $LDFLAGS -L. -lz3
popd
# Build the documentation
pushd doc
%{__python2} mk_api_doc.py
%{__python2} mk_api_doc.py --ml
popd
%install
export LANG="en_US.UTF-8"
mkdir -p %{buildroot}%{python2_sitearch}/%{name}
# Install the ocaml interface in the right place
sed 's,ocamlfind [[:alpha:]]* ,&-destdir %{buildroot}%{_libdir}/ocaml -ldconf ignore ,' \
-i build/Makefile
# Install
mkdir -p %{buildroot}%{python2_sitearch}/%{name} %{buildroot}%{_libdir}/ocaml
make -C build install
# On 64-bit systems, move the library to the right directory
@ -192,31 +184,25 @@ 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 dir
# Link, rather than copy, the library into the python and ocaml dirs
rm -f %{buildroot}%{python2_sitearch}/%{name}/lib%{name}.so
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
# Install the Ocaml interface
mkdir -p %{buildroot}%{_libdir}/ocaml/%{name}
cp -p src/api/ml/ocamlz3 %{buildroot}%{_bindir}
%if %{opt}
cp -p src/api/ml/%{name}.cmxa %{buildroot}%{_libdir}/ocaml/%{name}
%endif
cp -p src/api/ml/%{name}.{cma,mli} %{buildroot}%{_libdir}/ocaml/%{name}
# Install the Java interface
# Move the Java interface to its correct location
mkdir -p %{buildroot}%{_libdir}/%{name}
mkdir -p %{buildroot}%{_jnidir}
cp -p build/com.microsoft.z3.jar %{buildroot}%{_jnidir}
mv %{buildroot}%{_prefix}/lib/*.jar %{buildroot}%{_jnidir}
ln -s %{_jnidir}/com.microsoft.z3.jar %{buildroot}%{_libdir}/%{name}
cp -p build/lib%{name}java.so %{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
#%%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
# with upstream to fix the leaks, then try again to see if the tests can be
@ -254,15 +240,28 @@ chmod 0755 %{buildroot}%{_bindir}/* %{buildroot}%{_libdir}/*.so.0.0.0 \
%{_jnidir}/com.microsoft.z3.jar
%files -n ocaml-%{name}
%{_bindir}/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/*.so
%files -n ocaml-%{name}-devel
%{_libdir}/ocaml/%{name}/
%{_libdir}/ocaml/Z3/*.cmx
%{_libdir}/ocaml/Z3/*.cmxa
%{_libdir}/ocaml/Z3/*.ml
%{_libdir}/ocaml/Z3/*.mli
%files -n python-%{name}
%{python2_sitearch}/%{name}/
%changelog
* Wed May 27 2015 Jerry James <loganjerry@gmail.com> - 4.4.0-1
- New upstream version
* Wed Apr 22 2015 Jerry James <loganjerry@gmail.com> - 4.3.2-3.20150329git.29606b5
- Fix issues found on review (bz 1206826)