jjames pushed to z3 (f22). "Initial import."
notifications at fedoraproject.org
notifications at fedoraproject.org
Sat Apr 25 18:05:36 UTC 2015
>From 4dc7a51663939b4ad07d122ad1ea11f5cf499557 Mon Sep 17 00:00:00 2001
From: Jerry James <jamesjer at betterlinux.com>
Date: Thu, 23 Apr 2015 09:09:07 -0600
Subject: Initial import.
diff --git a/.gitignore b/.gitignore
index e69de29..cdde729 100644
--- a/.gitignore
+++ b/.gitignore
@@ -0,0 +1 @@
+/Z3Prover-z3-29606b5.tar.gz
diff --git a/sources b/sources
index e69de29..6984e99 100644
--- a/sources
+++ b/sources
@@ -0,0 +1 @@
+634e88648020946f2895b77174f8f557 Z3Prover-z3-29606b5.tar.gz
diff --git a/z3-sse2.patch b/z3-sse2.patch
new file mode 100644
index 0000000..23bfb01
--- /dev/null
+++ b/z3-sse2.patch
@@ -0,0 +1,22 @@
+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
+@@ -31,7 +31,7 @@ Revision History:
+ #include <fenv.h>
+ #endif
+
+-#ifndef _M_IA64
++#ifdef __x86_64
+ #define USE_INTRINSICS
+ #endif
+
+@@ -51,7 +51,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
+
diff --git a/z3.spec b/z3.spec
new file mode 100644
index 0000000..53cab32
--- /dev/null
+++ b/z3.spec
@@ -0,0 +1,268 @@
+# Python 3 NOTE: Although there are references to python 3 support in the
+# source tree, building with python 3 currently fails. I fixed several
+# problems before giving up. If someone would like to fix all of the problems
+# 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
+
+Name: z3
+Version: 4.3.2
+Release: 3.%{gitdate}git.%{shorttag}%{?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
+# Do not try to build with SSE2 on non-x86_64 arches
+Patch0: %{name}-sse2.patch
+
+BuildRequires: doxygen
+BuildRequires: gmp-devel
+BuildRequires: graphviz
+BuildRequires: java-devel
+BuildRequires: jpackage-utils
+BuildRequires: ocaml
+BuildRequires: ocaml-camlidl-devel
+BuildRequires: python2-devel
+
+Requires: %{name}-libs%{?_isa} = %{version}-%{release}
+
+%description
+Z3 is a satisfiability modulo theories (SMT) solver; given a set of
+constraints with variables, it reports a set of values for those
+variables that would meet the constraints. The Z3 input format is an
+extension of the one defined by the SMT-LIB 2.0 standard. Z3 supports
+arithmetic, fixed-size bit-vectors, extensional arrays, datatypes,
+uninterpreted functions, and quantifiers.
+
+%package libs
+Summary: Library for applications that use z3 functionality
+
+%description libs
+Library for applications that use z3 functionality.
+
+%package devel
+Summary: Header files for build applications that use z3
+Requires: %{name}-libs%{?_isa} = %{version}-%{release}
+
+%description devel
+Header files for build applications that use z3.
+
+%package doc
+Summary: API documentation for Z3
+BuildArch: noarch
+
+%description doc
+API documentation for Z3.
+
+%package -n java-%{name}
+Summary: Java interface to z3
+Requires: %{name}-libs%{?_isa} = %{version}-%{release}
+Requires: java
+Requires: jpackage-utils
+
+%description -n java-%{name}
+Java interface to z3.
+
+%package -n ocaml-%{name}
+Summary: Ocaml interface to z3
+Requires: %{name}-libs%{?_isa} = %{version}-%{release}
+
+%description -n ocaml-%{name}
+Ocaml interface to z3.
+
+%package -n ocaml-%{name}-devel
+Summary: Files for building ocaml applications that use z3
+Requires: ocaml-%{name}%{?_isa} = %{version}-%{release}
+
+%description -n ocaml-%{name}-devel
+Files for building ocaml applications that use z3.
+
+%package -n python-%{name}
+Summary: Python 2 interface to z3
+Requires: %{name}-libs%{?_isa} = %{version}-%{release}
+
+%description -n python-%{name}
+Python 2 interface to z3.
+
+%prep
+%setup -q -n %{user}-%{name}-%{shorttag}
+%patch0 -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, build the library with -fPIC on all arches, and use an soname.
+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/\(SLIBEXTRAFLAGS = '\)'/\1-Wl,--no-whole-archive -Wl,--as-needed'/" \
+ -e "s|-shared|& $RPM_LD_FLAGS -Wl,--whole-archive|" \
+ -e 's/\(libz3$(SO_EXT)\)\(\\n\)/\1 -Wl,--no-whole-archive\2/' \
+ -e '/fPIC/d;' \
+ -e "s/'tstomp\.cpp',/& '-fPIC',/" \
+ -e 's/-shared/& -Wl,-h,lib%{name}.so.0/' \
+ -i scripts/mk_util.py
+
+# Do not try to build with SSE2 support on non-x86_64 arches.
+%ifnarch x86_64
+sed -i '/msse2/d;s/ -mfpmath=sse//' scripts/mk_util.py
+%endif
+
+# Comply with the Java packaging guidelines
+sed -e "s/\(System\.load\)Library/\1/" \
+ -e "s,get_component('java')\.dll_name.*,'%{_libdir}/z3/libz3java.so')," \
+ -i scripts/update_api.py
+
+# Fix character encoding
+iconv -f iso8859-1 -t utf-8 RELEASE_NOTES > RELEASE_NOTES.utf8
+touch -r RELEASE_NOTES RELEASE_NOTES.utf8
+mv -f RELEASE_NOTES.utf8 RELEASE_NOTES
+
+# Fix permissions
+chmod a-x examples/interp/iz3.cpp
+
+%build
+export CXXFLAGS="$RPM_OPT_FLAGS -fPIC"
+export LDFLAGS="$RPM_LD_FLAGS -Wl,--as-needed"
+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
+make %{?_smp_mflags} -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.
+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
+popd
+
+# Build the documentation
+pushd doc
+%{__python2} mk_api_doc.py
+popd
+
+%install
+export LANG="en_US.UTF-8"
+
+mkdir -p %{buildroot}%{python2_sitearch}/%{name}
+make -C build install
+
+# On 64-bit systems, move the library to the right directory
+if [ "%{_libdir}" != "%{_prefix}/lib" ]; then
+ mkdir -p %{buildroot}%{_libdir}
+ mv %{buildroot}%{_prefix}/lib/libz3.so* %{buildroot}%{_libdir}
+fi
+
+# Make library links
+mv %{buildroot}%{_libdir}/libz3.so %{buildroot}%{_libdir}/libz3.so.0.0.0
+ln -s libz3.so.0.0.0 %{buildroot}%{_libdir}/libz3.so.0
+ln -s libz3.so.0 %{buildroot}%{_libdir}/libz3.so
+
+# Move the header files into their own directory
+mkdir -p %{buildroot}%{_includedir}/%{name}
+mv %{buildroot}%{_includedir}/*.h %{buildroot}%{_includedir}/%{name}
+
+# Link, rather than copy, the library into the python dir
+rm -f %{buildroot}%{python2_sitearch}/%{name}/lib%{name}.so
+ln -s %{_libdir}/lib%{name}.so.0 \
+ %{buildroot}%{python2_sitearch}/%{name}/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
+mkdir -p %{buildroot}%{_libdir}/%{name}
+mkdir -p %{buildroot}%{_jnidir}
+cp -p build/com.microsoft.z3.jar %{buildroot}%{_jnidir}
+ln -s %{_jnidir}/com.microsoft.z3.jar %{buildroot}%{_libdir}/%{name}
+cp -p build/lib%{name}java.so %{buildroot}%{_libdir}/%{name}
+
+# Fix permissions
+chmod 0755 %{buildroot}%{_bindir}/* %{buildroot}%{_libdir}/*.so.0.0.0 \
+ %{buildroot}%{_libdir}/%{name}/*.so
+
+%check
+export LANG="en_US.UTF-8"
+pushd build
+make test
+./test-z3 /a
+popd
+
+%post libs -p /sbin/ldconfig
+
+%postun libs -p /sbin/ldconfig
+
+%files
+%doc README RELEASE_NOTES
+%{_bindir}/%{name}
+
+%files libs
+%license LICENSE.txt
+%{_libdir}/lib%{name}.so.*
+
+%files devel
+%{_includedir}/%{name}/
+%{_libdir}/lib%{name}.so
+
+%files doc
+%doc doc/api/html examples
+%license LICENSE.txt
+
+%files -n java-%{name}
+%{_libdir}/%{name}/
+%{_jnidir}/com.microsoft.z3.jar
+
+%files -n ocaml-%{name}
+%{_bindir}/ocaml%{name}
+
+%files -n ocaml-%{name}-devel
+%{_libdir}/ocaml/%{name}/
+
+%files -n python-%{name}
+%{python2_sitearch}/%{name}/
+
+%changelog
+* Wed Apr 22 2015 Jerry James <loganjerry at gmail.com> - 4.3.2-3.20150329git.29606b5
+- Fix issues found on review (bz 1206826)
+
+* Mon Mar 30 2015 Jerry James <loganjerry at gmail.com> - 4.3.2-2.20150329git.29606b5
+- Update to latest git HEAD
+- Include examples in -doc
+
+* Sat Mar 28 2015 Jerry James <loganjerry at gmail.com> - 4.3.2-1.20150327git.ac21ffe
+- Initial RPM
--
cgit v0.10.2
http://pkgs.fedoraproject.org/cgit/z3.git/commit/?h=f22&id=4dc7a51663939b4ad07d122ad1ea11f5cf499557
More information about the scm-commits
mailing list