z3/z3.spec

# 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 medtag   95c9ccb2959a

Name:           z3
Version:        4.4.1
Release:        7%{?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++
BuildRequires:  gmp-devel
BuildRequires:  graphviz
BuildRequires:  java-devel
BuildRequires:  jpackage-utils
BuildRequires:  ocaml
BuildRequires:  ocaml-findlib
BuildRequires:  ocaml-ocamldoc
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 %{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.
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 "s/'tstomp\.cpp',/& '-fPIC',/" \
  -e 's/ -fvisibility=hidden//' \
  -e '/dllfile/s/\$(SLINK_FLAGS)/& -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 '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"),' \
    -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
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

%build
export CXXFLAGS="$RPM_OPT_FLAGS -fPIC"
export LDFLAGS="$RPM_LD_FLAGS -Wl,--as-needed -lgmp"
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 --ml
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++ $RPM_OPT_FLAGS -fopenmp -o z3 shell/*.o $LDFLAGS -L. -lz3
popd

# Build the documentation
pushd doc
%{__python2} mk_api_doc.py --ml
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

# 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
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 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

# 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}
mkdir -p %{buildroot}%{_jnidir}
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
# with upstream to fix the leaks, then try again to see if the tests can be
# 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"
#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}
%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/Z3/*.cmx
%{_libdir}/ocaml/Z3/*.cmxa
%{_libdir}/ocaml/Z3/*.ml
%{_libdir}/ocaml/Z3/*.mli

%files -n python-%{name}
%{python2_sitearch}/%{name}/

%changelog
* Tue Jul 19 2016 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 4.4.1-7
- https://fedoraproject.org/wiki/Changes/Automatic_Provides_for_Python_RPM_Packages

* Wed Jul 13 2016 Jerry James <loganjerry@gmail.com> - 4.4.1-6
- Fix Java interface (bz 1353773)

* Thu Jun 30 2016 Jerry James <loganjerry@gmail.com> - 4.4.1-5
- Fix __init__.py (bz 1351580)

* Fri Feb 05 2016 Fedora Release Engineering <releng@fedoraproject.org> - 4.4.1-4
- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild

* Tue Feb 02 2016 Jonathan Wakely <jwakely@redhat.com> - 4.4.1-3
- Patched for C++11 compatibility.

* Wed Jan 20 2016 Jerry James <loganjerry@gmail.com> - 4.4.1-2
- Add __init__.py to the python interface (bz 1298429)

* Thu Oct  8 2015 Jerry James <loganjerry@gmail.com> - 4.4.1-1
- New upstream version

* Tue Jul 28 2015 Richard W.M. Jones <rjones@redhat.com> - 4.4.0-4
- OCaml 4.02.3 rebuild.

* Thu Jun 25 2015 Richard W.M. Jones <rjones@redhat.com> - 4.4.0-3
- ocaml-4.02.2 final rebuild.

* Thu Jun 18 2015 Richard W.M. Jones <rjones@redhat.com> - 4.4.0-2
- ocaml-4.02.2 rebuild.

* 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)

* Mon Mar 30 2015 Jerry James <loganjerry@gmail.com> - 4.3.2-2.20150329git.29606b5
- Update to latest git HEAD
- Include examples in -doc

* Sat Mar 28 2015 Jerry James <loganjerry@gmail.com> - 4.3.2-1.20150327git.ac21ffe
- Initial RPM