From 57bf5789d2ee5160723c28e3362fc5dd67bf3952 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 3 Mar 2021 12:11:52 -0700 Subject: [PATCH 1/5] Rebuild for ocaml-zarith 1.12. --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index ec018e5..d5daf57 100644 --- a/z3.spec +++ b/z3.spec @@ -1,6 +1,6 @@ Name: z3 Version: 4.8.10 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -231,6 +231,9 @@ help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} %{python3_sitelib}/%{name}/ %changelog +* Wed Mar 3 2021 Jerry James - 4.8.10-2 +- Rebuild for ocaml-zarith 1.12 + * Sat Feb 13 2021 Jerry James - 4.8.10-1 - Version 4.8.10 From f68e634694abddd3f1c36f014162f0c49e757762 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 8 Jun 2021 08:27:35 -0600 Subject: [PATCH 2/5] Version 4.8.11. --- sources | 2 +- z3.spec | 7 +++++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/sources b/sources index 6e928b0..4762877 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.8.10.tar.gz) = d2741d7ad3e1d5ee3fec92095b061a96a700c3327b2eb2090d4162bdcaeaebca8c072ef79c5daac1f6de3456165c2cc38e13f1045bc707779d1027b943837c5b +SHA512 (z3-4.8.11.tar.gz) = ceab703d0413d0135e0f4e6c3ba2bb58d6a4823385edb0bf7ecc96949a3073b687d415a2674c86c9f876adb52823f98f9fbbc107d799ed756dc16292f9864894 diff --git a/z3.spec b/z3.spec index d5daf57..ca162cb 100644 --- a/z3.spec +++ b/z3.spec @@ -1,6 +1,6 @@ Name: z3 -Version: 4.8.10 -Release: 2%{?dist} +Version: 4.8.11 +Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -231,6 +231,9 @@ help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} %{python3_sitelib}/%{name}/ %changelog +* Tue Jun 8 2021 Jerry James - 4.8.11-1 +- Version 4.8.11 + * Wed Mar 3 2021 Jerry James - 4.8.10-2 - Rebuild for ocaml-zarith 1.12 From c5deed3cea715cb14eb90f04d2ea33b0cd3a6cd9 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 13 Jul 2021 13:11:43 -0600 Subject: [PATCH 3/5] Version 4.8.12. --- sources | 2 +- z3.spec | 5 ++++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/sources b/sources index 4762877..6d9a0b2 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.8.11.tar.gz) = ceab703d0413d0135e0f4e6c3ba2bb58d6a4823385edb0bf7ecc96949a3073b687d415a2674c86c9f876adb52823f98f9fbbc107d799ed756dc16292f9864894 +SHA512 (z3-4.8.12.tar.gz) = 0b377923bdaffaca1846aa2abd61003bbecadfcdfc908ed3097d0aac8f32028ac39d93fb4a9c2e2c2bfffbdbee80aa415875f17de6c2ee2ae8e2b7921f788c6e diff --git a/z3.spec b/z3.spec index ca162cb..a277c7d 100644 --- a/z3.spec +++ b/z3.spec @@ -1,5 +1,5 @@ Name: z3 -Version: 4.8.11 +Version: 4.8.12 Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver @@ -231,6 +231,9 @@ help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} %{python3_sitelib}/%{name}/ %changelog +* Tue Jul 13 2021 Jerry James - 4.8.12-1 +- Version 4.8.12 + * Tue Jun 8 2021 Jerry James - 4.8.11-1 - Version 4.8.11 From cd0cb0d441f0f4ba866004ef796d09ffe75fdf89 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 19 Nov 2021 12:28:26 -0700 Subject: [PATCH 4/5] Version 4.8.13. --- README.md | 5 +++++ sources | 2 +- z3.spec | 12 ++++++------ 3 files changed, 12 insertions(+), 7 deletions(-) create mode 100644 README.md diff --git a/README.md b/README.md new file mode 100644 index 0000000..fcd0204 --- /dev/null +++ b/README.md @@ -0,0 +1,5 @@ +# z3 + +[Z3](https://github.com/Z3Prover/z3) is a theorem prover from Microsoft +Research. If you are not familiar with Z3, you can start +[here](https://github.com/Z3Prover/z3/wiki#background). diff --git a/sources b/sources index 6d9a0b2..9e39523 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.8.12.tar.gz) = 0b377923bdaffaca1846aa2abd61003bbecadfcdfc908ed3097d0aac8f32028ac39d93fb4a9c2e2c2bfffbdbee80aa415875f17de6c2ee2ae8e2b7921f788c6e +SHA512 (z3-4.8.13.tar.gz) = c5e8f34525ed3b6b2935d7f01ce2f90f5dd99b4cdd035664b36c967fb1c7f3b05abed45c7288e2261723e73d68728ee91a0f67d92012d86b04598d7b54369c30 diff --git a/z3.spec b/z3.spec index a277c7d..d5b5caf 100644 --- a/z3.spec +++ b/z3.spec @@ -1,5 +1,5 @@ Name: z3 -Version: 4.8.12 +Version: 4.8.13 Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver @@ -97,7 +97,7 @@ sed \ -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 "/SLIBFLAGS/s|-shared|& %{build_ldflags} -Wl,--whole-archive|" \ -e 's/\(libz3$(SO_EXT)\)\(\\n\)/\1 -Wl,--no-whole-archive\2/' \ -e "s/OCAML_FLAGS = ''/OCAML_FLAGS = '-g'/" \ -i scripts/mk_util.py @@ -111,16 +111,13 @@ sed -e '/libz3java/s,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so") # Update an OCaml interface sed -i 's/Pervasives/Stdlib/' src/api/ml/z3.ml -# FIXME: For unknown reasons, cmake replaces the version with nothing at all -sed -i 's/@VERSION@/%{version}/' z3.pc.cmake.in - # 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 %build -export CXXFLAGS="$RPM_OPT_FLAGS" +export CXXFLAGS="%{build_cxxflags}" export LANG="C.UTF-8" export PYTHON="%{python3}" @@ -231,6 +228,9 @@ help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} %{python3_sitelib}/%{name}/ %changelog +* Fri Nov 19 2021 Jerry James - 4.8.13-1 +- Version 4.8.13 + * Tue Jul 13 2021 Jerry James - 4.8.12-1 - Version 4.8.12 From a41041377d554a995159adf7ea620ed37bc708d3 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 24 Dec 2021 11:30:57 -0700 Subject: [PATCH 5/5] Version 4.8.14. Conditionalize the %check script. --- sources | 2 +- z3.spec | 29 +++++++++++++++++------------ 2 files changed, 18 insertions(+), 13 deletions(-) diff --git a/sources b/sources index 9e39523..d3aac3a 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.8.13.tar.gz) = c5e8f34525ed3b6b2935d7f01ce2f90f5dd99b4cdd035664b36c967fb1c7f3b05abed45c7288e2261723e73d68728ee91a0f67d92012d86b04598d7b54369c30 +SHA512 (z3-4.8.14.tar.gz) = 10170516ca472258d2f9df28cd036e43023a76a25f1e1670290c62f3890d935bf82770970054a5fd3a0f02559409e7ed4b18fb08347c040ff2f9e0918e152aab diff --git a/z3.spec b/z3.spec index d5b5caf..110df81 100644 --- a/z3.spec +++ b/z3.spec @@ -1,5 +1,9 @@ +# Tests are off by default because some of the tests require more memory than +# the koji builders have available. +%bcond_with test + Name: z3 -Version: 4.8.13 +Version: 4.8.14 Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver @@ -108,9 +112,6 @@ sed -e '/libz3java/s,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so") -e "s/@MAJVER@/$majver/" \ -i scripts/update_api.py -# Update an OCaml interface -sed -i 's/Pervasives/Stdlib/' src/api/ml/z3.ml - # Fix character encoding iconv -f iso8859-1 -t utf-8 RELEASE_NOTES > RELEASE_NOTES.utf8 touch -r RELEASE_NOTES RELEASE_NOTES.utf8 @@ -178,14 +179,14 @@ rm -rf %{buildroot}%{_docdir}/Z3 mkdir -p %{buildroot}%{_mandir}/man1 help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} -#%%check -# Some of the tests require more memory than the koji builders have available. -# -#export LANG="C.UTF-8" -#pushd build -#make test-z3 -#./test-z3 /a -#popd +%if %{with test} +%check +export LANG="C.UTF-8" +cd build +make test-z3 +./test-z3 /a +cd - +%endif %files %doc README.md RELEASE_NOTES @@ -228,6 +229,10 @@ help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} %{python3_sitelib}/%{name}/ %changelog +* Fri Dec 24 2021 Jerry James - 4.8.14-1 +- Version 4.8.14 +- Conditionalize the %%check script + * Fri Nov 19 2021 Jerry James - 4.8.13-1 - Version 4.8.13