The package rpms/yices.git has added or updated architecture specific content in its spec file (ExclusiveArch/ExcludeArch or %ifarch/%ifnarch) in commit(s): https://src.fedoraproject.org/cgit/rpms/yices.git/commit/?id=a218fc2b3c6a8a9....
Change: -%ifnarch %{ix86} %{arm}
Thanks.
Full change: ============
commit a218fc2b3c6a8a9ae3098d4e5a6ed0ddf5a2fc6f Author: Jerry James loganjerry@gmail.com Date: Mon Oct 25 08:01:38 2021 -0600
Version 2.6.4.
- Drop upstreamed -big-endian and -sphinx3 patches. - Enable tests on 32-bit platforms.
diff --git a/README.md b/README.md new file mode 100644 index 0000000..df2e238 --- /dev/null +++ b/README.md @@ -0,0 +1,11 @@ +# yices + +[Yices 2](https://yices.csl.sri.com/) is a solver for +[Satisfiability Modulo Theories](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories) +(SMT) problems. Yices 2 can process input written in the SMT-LIB language, or +in Yices' own specification language. The package provides a +[C API](https://github.com/SRI-CSL/yices2/blob/master/src/include/yices.h). +Separately, bindings for [Java](https://github.com/SRI-CSL/yices2_java_bindings), +[Python](https://github.com/SRI-CSL/yices2_python_bindings), +[Go](https://github.com/SRI-CSL/yices2_go_bindings), and +[OCaml](https://github.com/SRI-CSL/yices2_ocaml_bindings) are available. diff --git a/sources b/sources index 5efcc73..43c97dc 100644 --- a/sources +++ b/sources @@ -1,2 +1,2 @@ -SHA512 (Yices-2.6.2.tar.gz) = 58990cff2a70d4fae797efdf3c52a15772eb824bc6865682fa64e63b571054eb042a252e52b67b2f89fb191444543f0ad55f9b34086bdd8bcd083ef10422d388 +SHA512 (Yices-2.6.4.tar.gz) = d8102c41fda0e200fd1336ae317b516d2797d10c187b8f7aecf0c9b08b4b487b90bef8c358099b2da51c0367326939f9610fd4e6d5a41a392cf1114bd04b8763 SHA512 (cudd-3.0.0.tar.gz) = a26728fedc3033ae2a842000f43f215b4abc914cd00fe0097fd483e59dc630568bfa6a115baa93af94b2f70f3d538761a12143fdb757167e90395c9fd244318c diff --git a/yices-big-endian.patch b/yices-big-endian.patch deleted file mode 100644 index 32c6441..0000000 --- a/yices-big-endian.patch +++ /dev/null @@ -1,78 +0,0 @@ ---- a/configure.ac -+++ b/configure.ac -@@ -152,15 +152,9 @@ dnl - dnl Check for endianness - dnl -------------------- - dnl --dnl The neorationals code is little-endian only for now. --dnl TODO: support big-endian architectures at some point --dnl For now, we check here and fail. --dnl --bigendian="" --AC_C_BIGENDIAN([bigendian=yes],[bigendian=no],[bigendian=yes]) --if test "x$bigendian" = xyes ; then -- AC_MSG_ERROR([Can't build for your architecture. Yices builds only on little-endian hardware. Please file an issue at $repo_url]) --fi -+WORDS_BIGENDIAN="" -+AC_C_BIGENDIAN([WORDS_BIGENDIAN=yes],[WORDS_BIGENDIAN=no],[WORDS_BIGENDIAN=yes]) -+AC_SUBST(WORDS_BIGENDIAN) - - dnl - dnl CHECK_THREAD_LOCAL ---- a/make.include.in -+++ b/make.include.in -@@ -66,6 +66,7 @@ RANLIB=@RANLIB@ - GPERF=@GPERF@ - STRIP=@STRIP@ - NO_STACK_PROTECTOR=@NO_STACK_PROTECTOR@ -+WORDS_BIGENDIAN=@WORDS_BIGENDIAN@ - - # thread-safe build - HAVE_TLS=@HAVE_TLS@ ---- a/src/Makefile -+++ b/src/Makefile -@@ -595,6 +595,13 @@ libyices_def=libyices.def - ########################### - - # -+# Whether we are building for a big endian architecture -+# -+ifeq ($(WORDS_BIGENDIAN),yes) -+ CPPFLAGS += -DWORDS_BIGENDIAN -+endif -+ -+# - # Whether we have support for mcsat - # - ifeq ($(ENABLE_MCSAT),yes) ---- a/src/terms/rationals.h -+++ b/src/terms/rationals.h -@@ -47,8 +47,13 @@ - * signed numerator, and a 31 bit unsigned denominator. - */ - typedef struct { -+#ifdef WORDS_BIGENDIAN -+ int32_t num; -+ uint32_t den; -+#else - uint32_t den; - int32_t num; -+#endif - } rat32_t; - - typedef struct { ---- a/tests/unit/Makefile -+++ b/tests/unit/Makefile -@@ -84,6 +84,12 @@ static_tests := $(src_c:%.c=$(static_bin - libyices := $(libdir)/libyices.a - static_libyices := $(static_libdir)/libyices.a - -+# -+# Whether we are building for a big endian architecture -+# -+ifeq ($(WORDS_BIGENDIAN),yes) -+ CPPFLAGS += -DWORDS_BIGENDIAN -+endif - - # - # Whether we have support for mcsat diff --git a/yices-cryptominisat.patch b/yices-cryptominisat.patch index 0e3917a..c8ca3ac 100644 --- a/yices-cryptominisat.patch +++ b/yices-cryptominisat.patch @@ -13,8 +13,8 @@ +#include <cryptominisat5/cryptominisat_c.h> #endif
- #include "solvers/cdcl/delegate.h" -@@ -293,44 +293,44 @@ static void cadical_as_delegate(delegate + #ifdef HAVE_KISSAT +@@ -308,44 +308,44 @@ static void cadical_as_delegate(delegate
#if HAVE_CRYPTOMINISAT static void cryptominisat_add_empty_clause(void *solver) { @@ -76,7 +76,7 @@ default: return STATUS_UNKNOWN; } } -@@ -341,28 +341,23 @@ static smt_status_t cryptominisat_check( +@@ -356,28 +356,23 @@ static smt_status_t cryptominisat_check( * that cryptominisat always produces a full truth assignment. */ static bval_t cryptominisat_get_value(void *solver, bvar_t x) { diff --git a/yices-sphinx3.patch b/yices-sphinx3.patch deleted file mode 100644 index 0783c16..0000000 --- a/yices-sphinx3.patch +++ /dev/null @@ -1,57 +0,0 @@ ---- a/doc/sphinx/source/basic-usage.rst -+++ b/doc/sphinx/source/basic-usage.rst -@@ -263,7 +263,7 @@ Running this example should produce some - - To avoid these issues, we recommend compiling with mingw. - It is still possible to use Visual Studio or other compilers on Windows, -- as long as you avoid functions in the Yices API that take a :c:type:`FILE *` -+ as long as you avoid functions in the Yices API that take a `FILE *` - argument. File :file:`examples/example1b.c` in the distribution shows - how to use alternative functions for pretty printing. You can also - download this file :download:`here <_static/example1b.c>`. ---- a/doc/sphinx/source/conf.py -+++ b/doc/sphinx/source/conf.py -@@ -14,6 +14,7 @@ - - import sys - import os -+from sphinx import version_info - - # If extensions (or modules to document with autodoc) are in another directory, - # add these directories to sys.path here. If the directory is relative to the -@@ -33,7 +34,7 @@ needs_sphinx = '1.0' - # - # mathjax_path = 'https://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorM...' - # --extensions = ['cenum'] -+extensions = [] if version_info[0] >= 3 else ['cenum'] - - # Add any paths that contain templates here, relative to this directory. - templates_path = ['_templates'] ---- a/doc/sphinx/source/error-reports.rst -+++ b/doc/sphinx/source/error-reports.rst -@@ -41,7 +41,7 @@ The following functions give access to t - be used for diagnostic. - - --.. c:function:: int32_t yices_print_error(int fd) -+.. c:function:: int32_t yices_print_error_fd(int fd) - - This is a variant of the previous function that writes to file - descriptor *fd* instead of an output stream. The file must be open ---- a/doc/sphinx/source/_static/classic.css -+++ b/doc/sphinx/source/_static/classic.css -@@ -199,11 +199,13 @@ span.raw-html { - } - - table { -+ border: 1px solid black; - border-collapse: collapse; - margin: 0 -0.5em 0 -0.5em; - } - - table td, table th { -+ border: 1px solid black; - padding: 0.2em 0.5em 0.2em 0.5em; - } - diff --git a/yices.spec b/yices.spec index b0cb7b2..2611bec 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices -Version: 2.6.2 -Release: 8%{?dist} +Version: 2.6.4 +Release: 1%{?dist} Summary: SMT solver
# The yices code is GPLv3+. The cudd code is BSD. @@ -11,14 +11,8 @@ Source0: https://github.com/SRI-CSL/yices2/archive/Yices-%%7Bversion%7D.tar.g # when there were no more Fedora users. Instead of resurrecting the package for # the sole use of yices, we bundle a snapshot of the last released version. Source1: https://github.com/ivmai/cudd/archive/cudd-3.0.0.tar.gz -# Fix the build on big endian machines -# https://github.com/SRI-CSL/yices2/pull/185 -Patch0: %{name}-big-endian.patch # Adapt to newer versions of cryptominisat -Patch1: %{name}-cryptominisat.patch -# Adapt to sphinx 3.x -# https://github.com/SRI-CSL/yices2/commit/52d025a6b0ae2af55bf8f537ddeb9cd8f25... -Patch2: %{name}-sphinx3.patch +Patch0: %{name}-cryptominisat.patch
BuildRequires: cadical-devel BuildRequires: cryptominisat-devel @@ -73,8 +67,7 @@ BuildArch: noarch This package contains yices documentation.
%prep -%autosetup -n yices2-Yices-%{version} -p1 -%setup -q -n yices2-Yices-%{version} -T -D -a 1 +%autosetup -n yices2-Yices-%{version} -a 1 -p1
# Do not try to avoid -fstack-protector sed -i 's/@NO_STACK_PROTECTOR@//' make.include.in @@ -94,7 +87,7 @@ sed -i 's/cp/install -m 0644/' utils/make_source_version %build # Build cudd cd cudd-cudd-3.0.0 -%configure CFLAGS="%{optflags} -fPIC" CXXFLAGS="%{optflags} -fPIC" +%configure CFLAGS="%{build_cflags} -fPIC" CXXFLAGS="%{build_cxxflags} -fPIC" %make_build cd -
@@ -127,10 +120,8 @@ rm -f %{buildroot}%{_libdir}/libyices.a mkdir -p %{buildroot}%{_mandir}/man1 cp -p doc/*.1 %{buildroot}%{_mandir}/man1
-%ifnarch %{ix86} %{arm} %check make check MODE=debug -%endif
%files %doc doc/SMT-LIB-LANGUAGE doc/YICES-LANGUAGE @@ -153,6 +144,11 @@ make check MODE=debug %license copyright.txt LICENSE.txt
%changelog +* Mon Oct 25 2021 Jerry James loganjerry@gmail.com - 2.6.4-1 +- Version 2.6.4 +- Drop upstreamed -big-endian and -sphinx3 patches +- Enable tests on 32-bit platforms + * Fri Jul 23 2021 Fedora Release Engineering releng@fedoraproject.org - 2.6.2-8 - Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild
arch-excludes@lists.fedoraproject.org
-
githook-noreply＠fedoraproject.org