Version 4.13.3

[skip changelog]

changelog

@@ -1,18 +1,3 @@
-* Sat Jul 20 2024 Fedora Release Engineering <releng@fedoraproject.org> - 4.13.0-6
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild
-
-* Tue Jul 16 2024 Jerry James <loganjerry@gmail.com> - 4.13.0-5
-- Rebuild for ocaml-zarith 1.14
-
-* Wed Jun 19 2024 Richard W.M. Jones <rjones@redhat.com> - 4.13.0-4
-- OCaml 5.2.0 ppc64le fix
-
-* Fri Jun 07 2024 Python Maint <python-maint@redhat.com> - 4.13.0-3
-- Rebuilt for Python 3.13
-
-* Wed May 29 2024 Richard W.M. Jones <rjones@redhat.com> - 4.13.0-2
-- OCaml 5.2.0 for Fedora 41
-
 * Thu Mar 14 2024 Jerry James <loganjerry@gmail.com> - 4.13.0-1
 - Version 4.13.0
 

sources

@@ -1 +1 @@
-SHA512 (z3-5.1.0.tar.gz) = 03a854f720a56484ab99b8a5517150f1c9106400f54ad758cfa58e3ee2f95e349396a64d4f527a5bb9ee37f10ad9ecfa1916d1f5c921f04089deda409374491b
+SHA512 (z3-4.13.3.tar.gz) = c899f57d8cb5450801463b07cd651869d766a920e41a4beedc96c4978e940bfadff9af2fbbb5ba10f94f6742bb33f7abaca0a351f3e1803d778e84d735d6829e

z3.spec

@@ -7,43 +7,23 @@
 # unless somebody is really, really persuasive and available to help fix it
 # if it breaks.
 
-# A Go interface is now available, but Fedora no longer builds Go library
-# packages (https://docs.fedoraproject.org/en-US/packaging-guidelines/Golang/).
-
 # Tests are off by default because some of the tests require more memory than
 # the koji builders have available.
 %bcond test 0
 
 Name:           z3
-Version:        5.1.0
+Version:        4.13.3
 Release:        %autorelease
 Summary:        Satisfiability Modulo Theories (SMT) solver
 
-%global giturl  https://github.com/Z3Prover/z3
-%global majver  %{gsub %version ^(%d*%.%d*)%..*$ %1}
-
 License:        MIT
 URL:            https://github.com/Z3Prover/z3/wiki
-VCS :           git:%{giturl}.git
-Source:         %{giturl}/archive/%{name}-%{version}.tar.gz
+VCS:            https://github.com/Z3Prover/z3
+Source0:        %{vcs}/archive/%{name}-%{version}.tar.gz
 # Do not try to build or install native OCaml artifacts on bytecode-only arches
-Patch:          %{name}-ocaml.patch
-
-# See https://fedoraproject.org/wiki/Changes/EncourageI686LeafRemoval
-ExcludeArch:    %{ix86}
-BuildSystem:    cmake
-BuildOption(conf): -G Ninja
-BuildOption(conf): -DCMAKE_INSTALL_INCLUDEDIR=%{_includedir}/z3
-BuildOption(conf): -DZ3_BUILD_DOCUMENTATION:BOOL=ON
-%ifarch %{java_arches}
-BuildOption(conf): -DZ3_BUILD_JAVA_BINDINGS:BOOL=ON
-%endif
-BuildOption(conf): -DZ3_BUILD_PYTHON_BINDINGS:BOOL=ON
-BuildOption(conf): -DCMAKE_INSTALL_PYTHON_PKG_DIR=%{python3_sitelib}
-BuildOption(conf): -DZ3_INCLUDE_GIT_HASH:BOOL=OFF
-BuildOption(conf): -DZ3_INCLUDE_GIT_DESCRIBE:BOOL=OFF
-BuildOption(conf): -DZ3_USE_LIB_GMP:BOOL=ON
+Patch0:         %{name}-ocaml.patch
 
+BuildRequires:  cmake
 BuildRequires:  doxygen
 BuildRequires:  gcc-c++
 BuildRequires:  gmp-devel
@@ -55,32 +35,40 @@ BuildRequires:  javapackages-tools
 %endif
 BuildRequires:  make
 BuildRequires:  ninja-build
+%ifnarch %{ix86}
 BuildRequires:  ocaml
 BuildRequires:  ocaml-findlib
+BuildRequires:  ocaml-ocamldoc
 BuildRequires:  ocaml-zarith-devel
+%endif
 BuildRequires:  python3-devel
 BuildRequires:  %{py3_dist setuptools}
 
 %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.
+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
 
+# This can be removed when F40 reaches EOL
+%ifnarch %{java_arches}
+Obsoletes:      java-z3 < 4.8.17-5
+%endif
+
 %description libs
 Library for applications that use z3 functionality.
 
 %package devel
-Summary:        Header files for building applications that use z3
+Summary:        Header files for build applications that use z3
 Requires:       z3-libs%{?_isa} = %{version}-%{release}
 
 %description devel
-Header files for building applications that use z3.
+Header files for build applications that use z3.
 
 %package doc
 # The content is MIT.
@@ -88,19 +76,37 @@ Header files for building applications that use z3.
 # examples/tptp/tptp5.tab.c
 # examples/tptp/tptp5.tab.c
 # Other licenses are due to files installed by doxygen.
-# html/clipboard.js: MIT
-# html/cookie.js: MIT
+# html/bc_s.png: GPL-1.0-or-later
+# html/bdwn.png: GPL-1.0-or-later
+# html/closed.png: GPL-1.0-or-later
+# html/doc.png: GPL-1.0-or-later
 # html/doxygen.css: GPL-1.0-or-later
 # html/doxygen.svg: GPL-1.0-or-later
 # html/dynsections.js: MIT
+# html/folderclosed.png: GPL-1.0-or-later
+# html/folderopen.png: GPL-1.0-or-later
 # html/jquery.js: MIT
-# html/navtree.css: GPL-1.0-or-later
+# html/nav_f.png: GPL-1.0-or-later
+# html/nav_g.png: GPL-1.0-or-later
+# html/nav_h.png: GPL-1.0-or-later
+# html/open.png: GPL-1.0-or-later
 # html/search/search.css: GPL-1.0-or-later
 # html/search/search.js: MIT
+# html/search/search_l.png: GPL-1.0-or-later
+# html/search/search_m.png: GPL-1.0-or-later
+# html/search/search_r.png: GPL-1.0-or-later
+# html/splitbar.png: GPL-1.0-or-later
+# html/sync_off.png: GPL-1.0-or-later
+# html/sync_on.png: GPL-1.0-or-later
+# html/tab_a.png: GPL-1.0-or-later
+# html/tab_b.png: GPL-1.0-or-later
+# html/tab_h.png: GPL-1.0-or-later
+# html/tab_s.png: GPL-1.0-or-later
 # html/tabs.css: GPL-1.0-or-later
 License:        MIT AND GPL-3.0-or-later WITH Bison-exception-2.2 AND GPL-1.0-or-later
 Summary:        API documentation for Z3
-BuildArch:      noarch
+# FIXME: this should be noarch, but we end up with different numbers of inheritance
+# graphs on different architectures.  Why?
 
 %description doc
 API documentation for Z3.
@@ -116,6 +122,8 @@ Requires:       javapackages-tools
 Java interface to z3.
 %endif
 
+# OCaml packages not built on i686 since OCaml 5 / Fedora 39.
+%ifnarch %{ix86}
 %package -n ocaml-z3
 Summary:        Ocaml interface to z3
 Requires:       z3-libs%{?_isa} = %{version}-%{release}
@@ -130,22 +138,20 @@ Requires:       ocaml-zarith-devel%{?_isa}
 
 %description -n ocaml-z3-devel
 Files for building ocaml applications that use z3.
+%endif
 
 %package -n python3-z3
 Summary:        Python 3 interface to z3
 BuildArch:      noarch
 Requires:       z3-libs = %{version}-%{release}
 
-# Provide the PyPI name
-%py_provides python3-z3-solver
-
 %description -n python3-z3
 Python 3 interface to z3.
 
 %prep
 %autosetup -N -n %{name}-%{name}-%{version}
 %ifnarch %{ocaml_native_compiler}
-%patch 0 -p1
+%patch -P0 -p1
 %endif
 
 # Enable verbose builds, use Fedora CFLAGS, preserve timestamps when installing,
@@ -157,29 +163,37 @@ sed \
   -e "s/\(['\"]\)cp\([^[:alnum:]]\)/\1cp -p\2/" \
   -e "s/\(SLIBEXTRAFLAGS = '\)'/\1-Wl,--no-whole-archive'/" \
   -e '/SLIBFLAGS/s|-shared|& %{build_ldflags} -Wl,--whole-archive|' \
-  -e 's/\(libz3$(SO_EXT)\)\( \$(SLINK\)/\1 -Wl,--no-whole-archive\2/' \
+  -e 's/\(libz3$(SO_EXT)\)\(\\n\)/\1 -Wl,--no-whole-archive\2/' \
   -e "s/OCAML_FLAGS = ''/OCAML_FLAGS = '-g'/" \
   -i scripts/mk_util.py
 
 # Comply with the Java packaging guidelines and fill in the version for python
+majver=$(cut -d. -f-2 <<< %{version})
 sed -e '/libz3java/s,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so"),' \
-    -e "s/'so'/'so.%{majver}'/" \
+    -e "s/'so'/'so.$majver'/" \
     -i scripts/update_api.py
 
 # Turn off HTML timestamps for reproducible builds
 sed -i '/HTML_TIMESTAMP/s/YES/NO/' doc/z3api.cfg.in doc/z3code.dox
 
-%build -p
+%build
 export PYTHON=%{python3}
 
-%build -a
-# Remove meaningless memory addresses from the pydoc documentation
-# See https://github.com/python/cpython/issues/83572
-sed -ri 's/, handle [0-9a-fA-F]+//' \
-    %{_vpath_builddir}/doc/api/html/z3{,.z3{,num,poly,printer,rcf,util}}.html
-sed -ri 's/ at 0x[0-9a-fA-F]+//g' \
-    %{_vpath_builddir}/doc/api/html/z3.z3core.html
+%cmake -G Ninja \
+  -DCMAKE_INSTALL_INCLUDEDIR=%{_includedir}/z3 \
+  -DCMAKE_JAVA_COMPILE_FLAGS="-source;1.8;-target;1.8" \
+  -DZ3_BUILD_DOCUMENTATION:BOOL=ON \
+%ifarch %{java_arches}
+  -DZ3_BUILD_JAVA_BINDINGS:BOOL=ON \
+%endif
+  -DZ3_BUILD_PYTHON_BINDINGS:BOOL=ON \
+  -DZ3_INCLUDE_GIT_HASH:BOOL=OFF \
+  -DZ3_INCLUDE_GIT_DESCRIBE:BOOL=OFF \
+  -DZ3_USE_LIB_GMP:BOOL=ON
 
+%cmake_build
+
+%ifnarch %{ix86}
 # The cmake build system does not build the OCaml interface.  Do that manually.
 #
 # First, run the configure script to generate several files.
@@ -196,8 +210,12 @@ sed -i '/^api/s/ libz3\$(SO_EXT)//g' build/Makefile
 
 # Fourth, build the OCaml interface
 %make_build -C build ml
+%endif
+
+%install
+# Install the C++, python3, and Java interfaces
+%cmake_install
 
-%install -a
 %ifarch %{java_arches}
 # Move the Java interface to its correct location
 mkdir -p %{buildroot}%{_libdir}/z3
@@ -207,6 +225,7 @@ ln -s %{_jnidir}/com.microsoft.z3.jar %{buildroot}%{_libdir}/z3
 mv %{buildroot}%{_libdir}/libz3java.so %{buildroot}%{_libdir}/z3
 %endif
 
+%ifnarch %{ix86}
 # Install the OCaml interface
 cd build/api/ml
 mkdir -p %{buildroot}%{ocamldir}/Z3
@@ -217,6 +236,7 @@ cp -p META *.{a,cma,cmi,mli} %{buildroot}%{ocamldir}/Z3
 mkdir -p %{buildroot}%{ocamldir}/stublibs
 cp -p *.so %{buildroot}%{ocamldir}/stublibs
 cd -
+%endif
 
 # We handle the documentation files below
 rm -rf %{buildroot}%{_docdir}/Z3
@@ -229,8 +249,8 @@ help2man -N -o %{buildroot}%{_mandir}/man1/z3.1 \
 # Fix the pkgconfig file
 sed -i 's,//usr,,' %{buildroot}%{_libdir}/pkgconfig/z3.pc
 
-%check
 %if %{with test}
+%check
 cd build
 make test-z3
 ./test-z3 /a
@@ -244,7 +264,7 @@ cd -
 
 %files libs
 %license LICENSE.txt
-%{_libdir}/libz3.so.5.1{,.*}
+%{_libdir}/libz3.so.4.13*
 
 %files devel
 %{_includedir}/z3/
@@ -259,9 +279,10 @@ cd -
 %ifarch %{java_arches}
 %files -n java-z3
 %{_libdir}/z3/
-%{_jnidir}/com.microsoft.z3.jar
+%{_jnidir}/com.microsoft.z3*jar
 %endif
 
+%ifnarch %{ix86}
 %files -n ocaml-z3
 %dir %{ocamldir}/Z3/
 %{ocamldir}/Z3/META
@@ -270,7 +291,7 @@ cd -
 %ifarch %{ocaml_native_compiler}
 %{ocamldir}/Z3/*.cmxs
 %endif
-%{ocamldir}/stublibs/dllz3ml.so
+%{ocamldir}/stublibs/*.so
 
 %files -n ocaml-z3-devel
 %{ocamldir}/Z3/*.a
@@ -279,6 +300,7 @@ cd -
 %{ocamldir}/Z3/*.cmxa
 %endif
 %{ocamldir}/Z3/*.mli
+%endif
 
 %files -n python3-z3
 %{python3_sitelib}/z3/