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=a218fc2b3c6a....
Change:
-%ifnarch %{ix86} %{arm}
Thanks.
Full change:
============
commit a218fc2b3c6a8a9ae3098d4e5a6ed0ddf5a2fc6f
Author: Jerry James <loganjerry(a)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_HTMLorMML'
- #
--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-%{version}.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/52d025a6b0ae2af55bf8f537ddeb9cd8...
-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(a)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(a)fedoraproject.org> - 2.6.2-8
- Rebuilt for
https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild