350 lines
11 KiB
RPMSpec
350 lines
11 KiB
RPMSpec
%global medtag b0aaa4c6d7a7
|
|
|
|
Name: z3
|
|
Version: 4.6.0
|
|
Release: 2%{?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
|
|
# Do not try to build with SSE2 on non-x86_64 arches
|
|
Patch0: %{name}-sse2.patch
|
|
# Fix a vector access
|
|
Patch1: %{name}-vector.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: ocaml-num-devel
|
|
BuildRequires: python2-devel
|
|
BuildRequires: python2-setuptools
|
|
BuildRequires: python3-devel
|
|
BuildRequires: python3-setuptools
|
|
|
|
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 python2-%{name}
|
|
%{?python_provide:%python_provide python2-%{name}}
|
|
Summary: Python 2 interface to z3
|
|
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
|
|
|
|
%description -n python2-%{name}
|
|
Python 2 interface to z3.
|
|
|
|
%package -n python3-%{name}
|
|
%{?python_provide:%python_provide python3-%{name}}
|
|
Summary: Python 3 interface to z3
|
|
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
|
|
|
|
%description -n python3-%{name}
|
|
Python 3 interface to z3.
|
|
|
|
%prep
|
|
%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
|
|
# contents of the archives in the library, link the library with the correct
|
|
# 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}'|" \
|
|
-e 's/@$(CXX)/$(CXX)/' \
|
|
-e '/O3/d' \
|
|
-e "s/\(['\"]\)cp\([^[:alnum:]]\)/\1cp -p\2/" \
|
|
-e "s/\(SLIBEXTRAFLAGS = '\)'/\1-Wl,--no-whole-archive -Wl,--as-needed'/" \
|
|
-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 '/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.
|
|
%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
|
|
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,z3enums\.mli,z3enums.ml,' doc/mk_api_doc.py
|
|
|
|
%build
|
|
export CXXFLAGS="$RPM_OPT_FLAGS -fPIC"
|
|
export LDFLAGS="$RPM_LD_FLAGS -Wl,--as-needed -lgmp"
|
|
export LANG="C.UTF-8"
|
|
export PYTHON="%{__python2}"
|
|
|
|
# This is NOT an autoconf-generated configure script.
|
|
./configure -p %{_prefix} --githash=%{medtag} --gmp --java --ml --python
|
|
# 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.
|
|
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 --no-dotnet
|
|
popd
|
|
|
|
# Build for python3
|
|
mv build build2
|
|
sed -i "s|%{python2_sitearch}|%{python3_sitearch}|" scripts/mk_util.py
|
|
export PYTHON="%{__python3}"
|
|
./configure -p %{_prefix} --githash=%{medtag} --gmp --python
|
|
# FIXME: intermittent build failures with %%{?_smp_mflags}
|
|
make -C build
|
|
|
|
%install
|
|
export LANG="C.UTF-8"
|
|
|
|
# Install the python3 interface
|
|
make -C build install DESTDIR=%{buildroot}
|
|
rm -f %{buildroot}%{python3_sitearch}/%{name}/lib/libz3.so
|
|
ln -s %{_libdir}/libz3.so.0 %{buildroot}%{python3_sitearch}/%{name}/lib/libz3.so
|
|
|
|
# Install the python2 interface
|
|
make -C build2 install DESTDIR=%{buildroot}
|
|
rm -f %{buildroot}%{python2_sitearch}/%{name}/lib/libz3.so
|
|
ln -s %{_libdir}/libz3.so.0 %{buildroot}%{python2_sitearch}/%{name}/lib/libz3.so
|
|
|
|
# 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}
|
|
|
|
# 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}
|
|
|
|
#%%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="C.UTF-8"
|
|
#pushd build
|
|
#make test
|
|
#./test-z3 /a
|
|
#popd
|
|
|
|
%ldconfig_scriptlets
|
|
|
|
%files
|
|
%doc README.md 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/*.cma
|
|
%{_libdir}/ocaml/Z3/*.cmi
|
|
%{_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/*.mli
|
|
|
|
%files -n python2-%{name}
|
|
%{python2_sitearch}/%{name}/
|
|
|
|
%files -n python3-%{name}
|
|
%{python3_sitearch}/%{name}/
|
|
|
|
%changelog
|
|
* Fri Feb 09 2018 Fedora Release Engineering <releng@fedoraproject.org> - 4.6.0-2
|
|
- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
|
|
|
|
* Sun Dec 24 2017 Jerry James <loganjerry@gmail.com> - 4.6.0-1
|
|
- New upstream version (bz 1527531)
|
|
- Add a python3 subpackage
|
|
|
|
* Sun Dec 17 2017 Zbigniew Jędrzejewski-Szmek <zbyszek@in.waw.pl> - 4.5.0-8
|
|
- Python 2 binary package renamed to python2-z3
|
|
See https://fedoraproject.org/wiki/FinalizingFedoraSwitchtoPython3
|
|
|
|
* Fri Nov 17 2017 Richard W.M. Jones <rjones@redhat.com> - 4.5.0-7
|
|
- OCaml 4.06.0 rebuild.
|
|
- Add dependency on ocaml-num.
|
|
|
|
* Tue Aug 08 2017 Richard W.M. Jones <rjones@redhat.com> - 4.5.0-6
|
|
- OCaml 4.05.0 rebuild.
|
|
|
|
* Thu Jul 27 2017 Fedora Release Engineering <releng@fedoraproject.org> - 4.5.0-5
|
|
- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild
|
|
|
|
* Tue Jun 27 2017 Richard W.M. Jones <rjones@redhat.com> - 4.5.0-4
|
|
- OCaml 4.04.2 rebuild.
|
|
|
|
* Fri May 12 2017 Richard W.M. Jones <rjones@redhat.com> - 4.5.0-3
|
|
- OCaml 4.04.1 rebuild.
|
|
|
|
* Sat Feb 11 2017 Fedora Release Engineering <releng@fedoraproject.org> - 4.5.0-2
|
|
- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild
|
|
|
|
* 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.
|
|
|
|
* 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
|