From 209e3a0a7c69881eb3babfa494986e32b47018ae Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 30 May 2018 21:49:23 -0600 Subject: [PATCH 01/54] Use %ldconfig_scriptlets. --- yices.spec | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/yices.spec b/yices.spec index b4bf813..20ad246 100644 --- a/yices.spec +++ b/yices.spec @@ -88,9 +88,7 @@ cp -p doc/*.1 %{buildroot}%{_mandir}/man1 %check make check MODE=debug -%post -p /sbin/ldconfig - -%postun -p /sbin/ldconfig +%ldconfig_scriptlets %files %doc doc/YICES-LANGUAGE From ef8ac9e1c94a0d4e4aa310e9ee62abedae0fa9da Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 4 Jul 2018 21:23:57 -0600 Subject: [PATCH 02/54] New upstream version. --- .gitignore | 2 +- sources | 2 +- yices.spec | 7 +++++-- 3 files changed, 7 insertions(+), 4 deletions(-) diff --git a/.gitignore b/.gitignore index 1f8b9ec..9ffab0f 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1 @@ -/Yices-2.5.4.tar.gz +/Yices-*.tar.gz diff --git a/sources b/sources index 3d5e038..c7cf0f9 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (Yices-2.5.4.tar.gz) = 68f86dcf44a36decac6be22a371bb645a5fa7c04629e9ff7ae8354c39ed95560c1b0b50fcba3b41c083929af8b205ef288f7586a636f263923d677dd15cc7703 +SHA512 (Yices-2.6.0.tar.gz) = e85aa059201bdc636817d91bc7f9b14c80f26abbd48eae0d828fca5a656eb18193ac545482aa43f7a12e8a05f5eb0edf7eab490e63b7f2ec3d5fc5d057abd45a diff --git a/yices.spec b/yices.spec index 20ad246..fc23f1c 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices -Version: 2.5.4 -Release: 3%{?dist} +Version: 2.6.0 +Release: 1%{?dist} Summary: SMT solver License: GPLv3+ @@ -111,6 +111,9 @@ make check MODE=debug %license LICENSE.txt %changelog +* Wed Jul 4 2018 Jerry James - 2.6.0-1 +- New upstream version + * Fri Feb 09 2018 Fedora Release Engineering - 2.5.4-3 - Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild From 0e0f7c62d51b4d9eda930fa3134048ee8cc0eea2 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 14 Jul 2018 09:42:46 +0000 Subject: [PATCH 03/54] - Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- yices.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/yices.spec b/yices.spec index fc23f1c..82da7a6 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices Version: 2.6.0 -Release: 1%{?dist} +Release: 2%{?dist} Summary: SMT solver License: GPLv3+ @@ -111,6 +111,9 @@ make check MODE=debug %license LICENSE.txt %changelog +* Sat Jul 14 2018 Fedora Release Engineering - 2.6.0-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild + * Wed Jul 4 2018 Jerry James - 2.6.0-1 - New upstream version From a3d8539242235087ba8ac0183b4ec58f7e6b9ba1 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 30 Oct 2018 20:14:02 -0600 Subject: [PATCH 04/54] New upstream version. --- sources | 2 +- yices.spec | 9 +++++---- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/sources b/sources index c7cf0f9..cc68492 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (Yices-2.6.0.tar.gz) = e85aa059201bdc636817d91bc7f9b14c80f26abbd48eae0d828fca5a656eb18193ac545482aa43f7a12e8a05f5eb0edf7eab490e63b7f2ec3d5fc5d057abd45a +SHA512 (Yices-2.6.1.tar.gz) = 586f24a8e3da45726ee69f4b3a744f2c04c3b400304319c00667c81c6799a846906ed580a9c4dd0df87a23ddb8e4fefb0b8ab60c13c19dc29243ba116717d1f2 diff --git a/yices.spec b/yices.spec index 82da7a6..a139512 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices -Version: 2.6.0 -Release: 2%{?dist} +Version: 2.6.1 +Release: 1%{?dist} Summary: SMT solver License: GPLv3+ @@ -88,8 +88,6 @@ cp -p doc/*.1 %{buildroot}%{_mandir}/man1 %check make check MODE=debug -%ldconfig_scriptlets - %files %doc doc/YICES-LANGUAGE %license LICENSE.txt @@ -111,6 +109,9 @@ make check MODE=debug %license LICENSE.txt %changelog +* Tue Oct 30 2018 Jerry James - 2.6.1-1 +- New upstream version + * Sat Jul 14 2018 Fedora Release Engineering - 2.6.0-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild From 706f3de7c19486984939cae210f79f5194948342 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sun, 3 Feb 2019 12:59:18 +0000 Subject: [PATCH 05/54] - Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- yices.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/yices.spec b/yices.spec index a139512..86e3f12 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices Version: 2.6.1 -Release: 1%{?dist} +Release: 2%{?dist} Summary: SMT solver License: GPLv3+ @@ -109,6 +109,9 @@ make check MODE=debug %license LICENSE.txt %changelog +* Sun Feb 03 2019 Fedora Release Engineering - 2.6.1-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild + * Tue Oct 30 2018 Jerry James - 2.6.1-1 - New upstream version From 215bda4ece5c7c8f96d6f38f83914c83e1bb7b4a Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 27 Jul 2019 04:49:35 +0000 Subject: [PATCH 06/54] - Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- yices.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/yices.spec b/yices.spec index 86e3f12..5646671 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices Version: 2.6.1 -Release: 2%{?dist} +Release: 3%{?dist} Summary: SMT solver License: GPLv3+ @@ -109,6 +109,9 @@ make check MODE=debug %license LICENSE.txt %changelog +* Sat Jul 27 2019 Fedora Release Engineering - 2.6.1-3 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild + * Sun Feb 03 2019 Fedora Release Engineering - 2.6.1-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild From dc5aeb964d25f9787cd4844f8a8bd8b6a2f92388 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 22 Nov 2019 11:52:13 -0700 Subject: [PATCH 07/54] Add -fwrapv to build flags; thanks to Jeff Law for the diagnosis. --- yices.spec | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/yices.spec b/yices.spec index 5646671..32262ab 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices Version: 2.6.1 -Release: 3%{?dist} +Release: 4%{?dist} Summary: SMT solver License: GPLv3+ @@ -65,6 +65,9 @@ sed -i 's/\r//' examples/{jinpeng,problem_with_input}.ys sed -i 's/cp/install -m 0644/' utils/make_source_version %build +#bv64_interval_abstraction depends on wrapping for signed overflow +%global optflags %{optflags} -fwrapv + %configure --enable-mcsat mv configs/make.include.%{_host} configs/make.include.$(./config.guess) make %{?_smp_mflags} MODE=debug @@ -109,6 +112,9 @@ make check MODE=debug %license LICENSE.txt %changelog +* Fri Nov 22 2019 Jerry James - 2.6.1-4 +- Add -fwrapv to build flags; thanks to Jeff Law for the diagnosis + * Sat Jul 27 2019 Fedora Release Engineering - 2.6.1-3 - Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild From 999fdcbd0d176ae822e6d354496f2cbe9a0264a1 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 23 Jan 2020 10:01:59 -0700 Subject: [PATCH 08/54] Add -missing-typedef patch to fix FTBFS with gcc 10. Set -doc subpackage to noarch. --- yices-missing-typedef.patch | 13 +++++++++++++ yices.rpmlintrc | 8 ++++++++ yices.spec | 14 +++++++++++--- 3 files changed, 32 insertions(+), 3 deletions(-) create mode 100644 yices-missing-typedef.patch create mode 100644 yices.rpmlintrc diff --git a/yices-missing-typedef.patch b/yices-missing-typedef.patch new file mode 100644 index 0000000..9528060 --- /dev/null +++ b/yices-missing-typedef.patch @@ -0,0 +1,13 @@ +https://github.com/SRI-CSL/yices2/commit/fadc2d5b303cef258cde295a0af2799b62d2513a + +--- a/src/frontend/smt2/smt2_commands.h ++++ b/src/frontend/smt2/smt2_commands.h +@@ -129,7 +129,7 @@ enum smt2_errors { + * - array theory sort and functions + * - processing of term annotations + */ +-enum smt2_opcodes { ++typedef enum smt2_opcodes { + SMT2_EXIT = NUM_BASE_OPCODES, // [exit] + SMT2_SILENT_EXIT, // [silent-exit] + SMT2_GET_ASSERTIONS, // [get-assertions] diff --git a/yices.rpmlintrc b/yices.rpmlintrc new file mode 100644 index 0000000..5aa0040 --- /dev/null +++ b/yices.rpmlintrc @@ -0,0 +1,8 @@ +# THIS FILE IS FOR WHITELISTING RPMLINT ERRORS AND WARNINGS IN TASKOTRON +# https://fedoraproject.org/wiki/Taskotron/Tasks/dist.rpmlint#Whitelisting_errors + +# The dictionary is missing some technical terms +addFilter(r'W: spelling-error .* (bitvectors|satisfiability|tuples)') + +# Documentation is in the -doc subpackage +addFilter(r'yices-devel\.[^:]+: W: no-documentation') diff --git a/yices.spec b/yices.spec index 32262ab..e72d458 100644 --- a/yices.spec +++ b/yices.spec @@ -1,11 +1,13 @@ Name: yices Version: 2.6.1 -Release: 4%{?dist} +Release: 5%{?dist} Summary: SMT solver License: GPLv3+ URL: http://yices.csl.sri.com/ Source0: https://github.com/SRI-CSL/yices2/archive/Yices-%{version}.tar.gz +# https://github.com/SRI-CSL/yices2/commit/fadc2d5b303cef258cde295a0af2799b62d2513a +Patch0: %{name}-missing-typedef.patch BuildRequires: gcc BuildRequires: gmp-devel @@ -45,12 +47,13 @@ Command line tools that use the yices library. %package doc Summary: Documentation for yices +BuildArch: noarch %description doc This package contains yices documentation. %prep -%setup -q -n yices2-Yices-%{version} +%autosetup -n yices2-Yices-%{version} -p1 # Do not try to avoid -fstack-protector sed -i '/NO_STACK_PROTECTOR=""/,/AC_SUBST(NO_STACK_PROTECTOR)/d' configure.ac @@ -94,7 +97,8 @@ make check MODE=debug %files %doc doc/YICES-LANGUAGE %license LICENSE.txt -%{_libdir}/*.so.* +%{_libdir}/*.so.2 +%{_libdir}/*.so.2.* %files devel %{_includedir}/%{name}/ @@ -112,6 +116,10 @@ make check MODE=debug %license LICENSE.txt %changelog +* Thu Jan 23 2020 Jerry James - 2.6.1-5 +- Add -missing-typedef patch to fix FTBFS with gcc 10 +- Set -doc subpackage to noarch + * Fri Nov 22 2019 Jerry James - 2.6.1-4 - Add -fwrapv to build flags; thanks to Jeff Law for the diagnosis From 003f0f4a84ff8c10830ba90abb382678a4467f34 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 23 Jan 2020 10:09:01 -0700 Subject: [PATCH 09/54] Fix shared library entry in %files. --- yices.spec | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/yices.spec b/yices.spec index e72d458..8df576a 100644 --- a/yices.spec +++ b/yices.spec @@ -97,8 +97,7 @@ make check MODE=debug %files %doc doc/YICES-LANGUAGE %license LICENSE.txt -%{_libdir}/*.so.2 -%{_libdir}/*.so.2.* +%{_libdir}/*.so.2* %files devel %{_includedir}/%{name}/ From e5af1f967c53d333899d2725aef0dc8a5128f485 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Fri, 31 Jan 2020 05:07:48 +0000 Subject: [PATCH 10/54] - Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- yices.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/yices.spec b/yices.spec index 8df576a..b16384b 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices Version: 2.6.1 -Release: 5%{?dist} +Release: 6%{?dist} Summary: SMT solver License: GPLv3+ @@ -115,6 +115,9 @@ make check MODE=debug %license LICENSE.txt %changelog +* Fri Jan 31 2020 Fedora Release Engineering - 2.6.1-6 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild + * Thu Jan 23 2020 Jerry James - 2.6.1-5 - Add -missing-typedef patch to fix FTBFS with gcc 10 - Set -doc subpackage to noarch From c31ab501bc80bdc94e078ebae78904c3e087d387 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 26 Mar 2020 11:48:16 -0600 Subject: [PATCH 11/54] Version 2.6.2. Also: - Drop upstreamed -missing-typedef patch. - Add -big-endian patch to fix s390x build. - Add -cryptominisat5 patch to fix build with recent cryptominisat releases. --- .gitignore | 1 + sources | 3 +- yices-big-endian.patch | 63 ++++++++++++++++++++ yices-cryptominisat.patch | 114 ++++++++++++++++++++++++++++++++++++ yices-missing-typedef.patch | 13 ---- yices.spec | 74 +++++++++++++++++------ 6 files changed, 236 insertions(+), 32 deletions(-) create mode 100644 yices-big-endian.patch create mode 100644 yices-cryptominisat.patch delete mode 100644 yices-missing-typedef.patch diff --git a/.gitignore b/.gitignore index 9ffab0f..6d06f33 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,2 @@ /Yices-*.tar.gz +/cudd-*.tar.gz diff --git a/sources b/sources index cc68492..5efcc73 100644 --- a/sources +++ b/sources @@ -1 +1,2 @@ -SHA512 (Yices-2.6.1.tar.gz) = 586f24a8e3da45726ee69f4b3a744f2c04c3b400304319c00667c81c6799a846906ed580a9c4dd0df87a23ddb8e4fefb0b8ab60c13c19dc29243ba116717d1f2 +SHA512 (Yices-2.6.2.tar.gz) = 58990cff2a70d4fae797efdf3c52a15772eb824bc6865682fa64e63b571054eb042a252e52b67b2f89fb191444543f0ad55f9b34086bdd8bcd083ef10422d388 +SHA512 (cudd-3.0.0.tar.gz) = a26728fedc3033ae2a842000f43f215b4abc914cd00fe0097fd483e59dc630568bfa6a115baa93af94b2f70f3d538761a12143fdb757167e90395c9fd244318c diff --git a/yices-big-endian.patch b/yices-big-endian.patch new file mode 100644 index 0000000..005e664 --- /dev/null +++ b/yices-big-endian.patch @@ -0,0 +1,63 @@ +--- 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 { diff --git a/yices-cryptominisat.patch b/yices-cryptominisat.patch new file mode 100644 index 0000000..0e3917a --- /dev/null +++ b/yices-cryptominisat.patch @@ -0,0 +1,114 @@ +--- a/src/solvers/cdcl/delegate.c ++++ b/src/solvers/cdcl/delegate.c +@@ -21,11 +21,11 @@ + #include + + #ifdef HAVE_CADICAL +-#include "ccadical.h" ++#include + #endif + + #ifdef HAVE_CRYPTOMINISAT +-#include "cryptominisat5/cmsat_c.h" ++#include + #endif + + #include "solvers/cdcl/delegate.h" +@@ -293,44 +293,44 @@ static void cadical_as_delegate(delegate + + #if HAVE_CRYPTOMINISAT + static void cryptominisat_add_empty_clause(void *solver) { +- cmsat_add_clause(solver, NULL, 0); ++ cmsat_add_clause((SATSolver *)solver, NULL, 0); + } + + static void cryptominisat_add_unit_clause(void *solver, literal_t l) { +- uint32_t c[1]; ++ c_Lit c[1]; + + assert(l >= 0); +- c[0] = l; +- cmsat_add_clause(solver, c, 1); ++ c[0].x = l; ++ cmsat_add_clause((SATSolver *)solver, c, 1); + } + + static void cryptominisat_add_binary_clause(void *solver, literal_t l1, literal_t l2) { +- uint32_t c[2]; ++ c_Lit c[2]; + + assert(l1 >= 0 && l2 >= 0); +- c[0] = l1; +- c[1] = l2; +- cmsat_add_clause(solver, c, 2); ++ c[0].x = l1; ++ c[1].x = l2; ++ cmsat_add_clause((SATSolver *)solver, c, 2); + } + + static void cryptominisat_add_ternary_clause(void *solver, literal_t l1, literal_t l2, literal_t l3) { +- uint32_t c[3]; ++ c_Lit c[3]; + + assert(l1 >= 0 && l2 >= 0 && l3 >= 0); +- c[0] = l1; +- c[1] = l2; +- c[2] = l3; +- cmsat_add_clause(solver, c, 3); ++ c[0].x = l1; ++ c[1].x = l2; ++ c[2].x = l3; ++ cmsat_add_clause((SATSolver *)solver, c, 3); + } + + static void cryptominisat_add_clause(void *solver, uint32_t n, literal_t *a) { +- cmsat_add_clause(solver, (uint32_t*) a, n); ++ cmsat_add_clause((SATSolver *)solver, (c_Lit *)a, n); + } + + static smt_status_t cryptominisat_check(void *solver) { +- switch (cmsat_solve(solver)) { +- case CMSAT_SAT: return STATUS_SAT; +- case CMSAT_UNSAT: return STATUS_UNSAT; ++ switch (cmsat_solve((SATSolver *)solver).x) { ++ case L_TRUE: return STATUS_SAT; ++ case L_FALSE: return STATUS_UNSAT; + default: return STATUS_UNKNOWN; + } + } +@@ -341,28 +341,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) { +- switch (cmsat_var_value(solver, x)) { +- case CMSAT_VAL_TRUE: ++ slice_lbool model = cmsat_get_model((SATSolver *)solver); ++ if ((size_t)x < model.num_vals && model.vals[x].x == L_TRUE) + return VAL_TRUE; +- +- case CMSAT_VAL_FALSE: +- default: +- return VAL_FALSE; +- } ++ return VAL_FALSE; + } + +-static void cryptominisat_set_verbosity(void *solver, uint32_t level) { ++static void cryptominisat_set_verbosity(void *solver __attribute__((unused)), uint32_t level __attribute__((unused))) { + // verbosity 0 --> quiet (this is the default) +- cmsat_set_verbosity(solver, level); + } + + static void cryptominisat_delete(void *solver) { +- cmsat_free_solver(solver); ++ cmsat_free((SATSolver *)solver); + } + + static void cryptominisat_as_delegate(delegate_t *d, uint32_t nvars) { +- d->solver = cmsat_new_solver(); +- cmsat_new_vars(d->solver, nvars); ++ d->solver = cmsat_new(); ++ cmsat_new_vars((SATSolver *)d->solver, nvars); + init_ivector(&d->buffer, 0); // not used + d->add_empty_clause = cryptominisat_add_empty_clause; + d->add_unit_clause = cryptominisat_add_unit_clause; diff --git a/yices-missing-typedef.patch b/yices-missing-typedef.patch deleted file mode 100644 index 9528060..0000000 --- a/yices-missing-typedef.patch +++ /dev/null @@ -1,13 +0,0 @@ -https://github.com/SRI-CSL/yices2/commit/fadc2d5b303cef258cde295a0af2799b62d2513a - ---- a/src/frontend/smt2/smt2_commands.h -+++ b/src/frontend/smt2/smt2_commands.h -@@ -129,7 +129,7 @@ enum smt2_errors { - * - array theory sort and functions - * - processing of term annotations - */ --enum smt2_opcodes { -+typedef enum smt2_opcodes { - SMT2_EXIT = NUM_BASE_OPCODES, // [exit] - SMT2_SILENT_EXIT, // [silent-exit] - SMT2_GET_ASSERTIONS, // [get-assertions] diff --git a/yices.spec b/yices.spec index b16384b..cec23a4 100644 --- a/yices.spec +++ b/yices.spec @@ -1,21 +1,37 @@ Name: yices -Version: 2.6.1 -Release: 6%{?dist} +Version: 2.6.2 +Release: 1%{?dist} Summary: SMT solver -License: GPLv3+ +# The yices code is GPLv3+. The cudd code is BSD. +License: GPLv3+ and BSD URL: http://yices.csl.sri.com/ Source0: https://github.com/SRI-CSL/yices2/archive/Yices-%{version}.tar.gz -# https://github.com/SRI-CSL/yices2/commit/fadc2d5b303cef258cde295a0af2799b62d2513a -Patch0: %{name}-missing-typedef.patch +# The CUDD web site disappeared in 2018. The Fedora package was retired in 2019 +# 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 +BuildRequires: cadical-devel +BuildRequires: cryptominisat-devel BuildRequires: gcc +BuildRequires: gcc-c++ BuildRequires: gmp-devel BuildRequires: gperf +BuildRequires: latexmk BuildRequires: libpoly-devel BuildRequires: libtool +BuildRequires: python3dist(sphinx) BuildRequires: tex(latex) +# See Source1 comment +Provides: bundled(cudd) = 3.0.0 + %description Yices 2 is an efficient SMT solver that decides the satisfiability of formulas containing uninterpreted function symbols with equality, linear @@ -54,9 +70,13 @@ This package contains yices documentation. %prep %autosetup -n yices2-Yices-%{version} -p1 +%setup -q -n yices2-Yices-%{version} -T -D -a 1 # Do not try to avoid -fstack-protector -sed -i '/NO_STACK_PROTECTOR=""/,/AC_SUBST(NO_STACK_PROTECTOR)/d' configure.ac +sed -i 's/@NO_STACK_PROTECTOR@//' make.include.in + +# Do not override our build flags +sed -i 's/ -O3//;s/ -fomit-frame-pointer//' src/Makefile tests/unit/Makefile # Generate the configure script autoreconf -fi @@ -68,20 +88,32 @@ sed -i 's/\r//' examples/{jinpeng,problem_with_input}.ys 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" +%make_build +cd - + #bv64_interval_abstraction depends on wrapping for signed overflow %global optflags %{optflags} -fwrapv +export CPPFLAGS="-I$PWD/cudd-cudd-3.0.0/cudd -DHAVE_CADICAL -DHAVE_CRYPTOMINISAT" +export LDFLAGS="$RPM_LD_FLAGS -L$PWD/cudd-cudd-3.0.0/cudd/.libs" +export LIBS="-lcadical -lcryptominisat5" %configure --enable-mcsat -mv configs/make.include.%{_host} configs/make.include.$(./config.guess) -make %{?_smp_mflags} MODE=debug + +guess=$(./config.guess) +if [ "%{_host}" != "$guess" ]; then + mv configs/make.include.%{_host} configs/make.include.${guess} +fi +%make_build MODE=debug # Build the manual -pushd doc/manual -pdflatex manual -bibtex manual -pdflatex manual -pdflatex manual -popd +make doc + +# Build the interface documentation +make -C doc/sphinx html +rm doc/sphinx/build/html/.buildinfo %install make install prefix=%{buildroot}%{_prefix} exec_prefix=%{buildroot}%{_prefix} \ @@ -95,8 +127,8 @@ cp -p doc/*.1 %{buildroot}%{_mandir}/man1 make check MODE=debug %files -%doc doc/YICES-LANGUAGE -%license LICENSE.txt +%doc doc/SMT-LIB-LANGUAGE doc/YICES-LANGUAGE +%license copyright.txt LICENSE.txt %{_libdir}/*.so.2* %files devel @@ -111,10 +143,16 @@ make check MODE=debug %{_mandir}/man1/* %files doc -%doc doc/manual/manual.pdf examples -%license LICENSE.txt +%doc doc/manual/manual.pdf doc/sphinx/build/html examples +%license copyright.txt LICENSE.txt %changelog +* Thu Mar 26 2020 Jerry James - 2.6.2-1 +- Version 2.6.2 +- Drop upstreamed -missing-typedef patch +- Add -big-endian patch to fix s390x build +- Add -cryptominisat5 patch to fix build with recent cryptominisat releases + * Fri Jan 31 2020 Fedora Release Engineering - 2.6.1-6 - Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild From 26ecb5e37f7ca9b6f55f7769242761890fb434bd Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 26 Mar 2020 15:26:59 -0600 Subject: [PATCH 12/54] Disable tests on 32-bit platforms due to failures from overflowing integers. --- yices-big-endian.patch | 15 +++++++++++++++ yices.spec | 4 ++++ 2 files changed, 19 insertions(+) diff --git a/yices-big-endian.patch b/yices-big-endian.patch index 005e664..32c6441 100644 --- a/yices-big-endian.patch +++ b/yices-big-endian.patch @@ -61,3 +61,18 @@ } 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.spec b/yices.spec index cec23a4..f9274c4 100644 --- a/yices.spec +++ b/yices.spec @@ -123,8 +123,10 @@ 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 @@ -152,6 +154,8 @@ make check MODE=debug - Drop upstreamed -missing-typedef patch - Add -big-endian patch to fix s390x build - Add -cryptominisat5 patch to fix build with recent cryptominisat releases +- Skip tests on 32-bit platforms; some tests fail due to the limited size of a + C integer * Fri Jan 31 2020 Fedora Release Engineering - 2.6.1-6 - Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild From 71932b74a41e3d875dd48b2c82261a54af210140 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 16 Apr 2020 11:40:11 -0600 Subject: [PATCH 13/54] Use native sphinx 3 support for enum instead of cenum extension (bz 1823515). --- yices.spec | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/yices.spec b/yices.spec index f9274c4..edf7d9e 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices Version: 2.6.2 -Release: 1%{?dist} +Release: 2%{?dist} Summary: SMT solver # The yices code is GPLv3+. The cudd code is BSD. @@ -87,6 +87,13 @@ sed -i 's/\r//' examples/{jinpeng,problem_with_input}.ys # Fix permissions sed -i 's/cp/install -m 0644/' utils/make_source_version +# Sphinx 3 has native support for enum; the cenum sphinx extenion is not needed +# https://github.com/SRI-CSL/yices2/issues/198 +sphinx_ver=$(sphinx-build --version | cut -d' ' -f2 | cut -d. -f1) +if [ "$sphinx_ver" -gt 2 ]; then + sed -i '/cenum/d' doc/sphinx/source/conf.py +fi + %build # Build cudd cd cudd-cudd-3.0.0 @@ -149,6 +156,9 @@ make check MODE=debug %license copyright.txt LICENSE.txt %changelog +* Thu Apr 16 2020 Jerry James - 2.6.2-2 +- Use native sphinx 3 support for enum instead of cenum extension (bz 1823515) + * Thu Mar 26 2020 Jerry James - 2.6.2-1 - Version 2.6.2 - Drop upstreamed -missing-typedef patch From 2323fdc98b4f0998b23753ee501187b739f51a1c Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sat, 25 Apr 2020 17:34:16 -0600 Subject: [PATCH 14/54] Rebuild for cryptominisat 5.7.0. Switch to upstream's solution for sphinx 3 support. --- yices-sphinx3.patch | 57 +++++++++++++++++++++++++++++++++++++++++++++ yices.spec | 16 ++++++------- 2 files changed, 65 insertions(+), 8 deletions(-) create mode 100644 yices-sphinx3.patch diff --git a/yices-sphinx3.patch b/yices-sphinx3.patch new file mode 100644 index 0000000..0783c16 --- /dev/null +++ b/yices-sphinx3.patch @@ -0,0 +1,57 @@ +--- 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 edf7d9e..f17f7a9 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices Version: 2.6.2 -Release: 2%{?dist} +Release: 3%{?dist} Summary: SMT solver # The yices code is GPLv3+. The cudd code is BSD. @@ -16,6 +16,9 @@ Source1: https://github.com/ivmai/cudd/archive/cudd-3.0.0.tar.gz 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/52d025a6b0ae2af55bf8f537ddeb9cd8f2519237 +Patch2: %{name}-sphinx3.patch BuildRequires: cadical-devel BuildRequires: cryptominisat-devel @@ -87,13 +90,6 @@ sed -i 's/\r//' examples/{jinpeng,problem_with_input}.ys # Fix permissions sed -i 's/cp/install -m 0644/' utils/make_source_version -# Sphinx 3 has native support for enum; the cenum sphinx extenion is not needed -# https://github.com/SRI-CSL/yices2/issues/198 -sphinx_ver=$(sphinx-build --version | cut -d' ' -f2 | cut -d. -f1) -if [ "$sphinx_ver" -gt 2 ]; then - sed -i '/cenum/d' doc/sphinx/source/conf.py -fi - %build # Build cudd cd cudd-cudd-3.0.0 @@ -156,6 +152,10 @@ make check MODE=debug %license copyright.txt LICENSE.txt %changelog +* Sat Apr 25 2020 Jerry James - 2.6.2-3 +- Rebuild for cryptominisat 5.7.0 +- Switch to upstream's solution for sphinx 3 support + * Thu Apr 16 2020 Jerry James - 2.6.2-2 - Use native sphinx 3 support for enum instead of cenum extension (bz 1823515) From b2c63e99b0d39e165752d10190e10202d599c0ae Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Wed, 29 Jul 2020 15:14:34 +0000 Subject: [PATCH 15/54] - Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- yices.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/yices.spec b/yices.spec index f17f7a9..0348889 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices Version: 2.6.2 -Release: 3%{?dist} +Release: 4%{?dist} Summary: SMT solver # The yices code is GPLv3+. The cudd code is BSD. @@ -152,6 +152,9 @@ make check MODE=debug %license copyright.txt LICENSE.txt %changelog +* Wed Jul 29 2020 Fedora Release Engineering - 2.6.2-4 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild + * Sat Apr 25 2020 Jerry James - 2.6.2-3 - Rebuild for cryptominisat 5.7.0 - Switch to upstream's solution for sphinx 3 support From ab926fb05c01fa4e26d8de2f51a63f9c1d871126 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 3 Aug 2020 18:36:19 -0600 Subject: [PATCH 16/54] Rebuild for cadical 1.3.0. --- yices.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/yices.spec b/yices.spec index 0348889..c271e79 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices Version: 2.6.2 -Release: 4%{?dist} +Release: 5%{?dist} Summary: SMT solver # The yices code is GPLv3+. The cudd code is BSD. @@ -152,6 +152,9 @@ make check MODE=debug %license copyright.txt LICENSE.txt %changelog +* Mon Aug 3 2020 Jerry James - 2.6.2-5 +- Rebuild for cadical 1.3.0 + * Wed Jul 29 2020 Fedora Release Engineering - 2.6.2-4 - Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild From fbeb3f6a56ed218ea6d6ed582ab82a7c022a3cdf Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 9 Nov 2020 21:37:05 -0700 Subject: [PATCH 17/54] Explicitly BR make. --- yices.spec | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/yices.spec b/yices.spec index c271e79..0294e2c 100644 --- a/yices.spec +++ b/yices.spec @@ -29,7 +29,8 @@ BuildRequires: gperf BuildRequires: latexmk BuildRequires: libpoly-devel BuildRequires: libtool -BuildRequires: python3dist(sphinx) +BuildRequires: make +BuildRequires: %{py3_dist sphinx} BuildRequires: tex(latex) # See Source1 comment From acd9bd9b4e9c59cff202e298878166dc587dd196 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 27 Nov 2020 09:04:04 -0700 Subject: [PATCH 18/54] Rebuild for cryptominisat 5.8.0. --- yices.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/yices.spec b/yices.spec index 0294e2c..9169f02 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices Version: 2.6.2 -Release: 5%{?dist} +Release: 6%{?dist} Summary: SMT solver # The yices code is GPLv3+. The cudd code is BSD. @@ -153,6 +153,9 @@ make check MODE=debug %license copyright.txt LICENSE.txt %changelog +* Fri Nov 27 2020 Jerry James - 2.6.2-6 +- Rebuild for cryptominisat 5.8.0 + * Mon Aug 3 2020 Jerry James - 2.6.2-5 - Rebuild for cadical 1.3.0 From 92391e3a22bbda04efaeb6d87e2d407c0159ef24 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Thu, 28 Jan 2021 00:33:29 +0000 Subject: [PATCH 19/54] - Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- yices.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/yices.spec b/yices.spec index 9169f02..562add2 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices Version: 2.6.2 -Release: 6%{?dist} +Release: 7%{?dist} Summary: SMT solver # The yices code is GPLv3+. The cudd code is BSD. @@ -153,6 +153,9 @@ make check MODE=debug %license copyright.txt LICENSE.txt %changelog +* Thu Jan 28 2021 Fedora Release Engineering - 2.6.2-7 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild + * Fri Nov 27 2020 Jerry James - 2.6.2-6 - Rebuild for cryptominisat 5.8.0 From 122b53cda3bd80067c4a3c8a1af238019702ae6d Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Fri, 23 Jul 2021 22:08:36 +0000 Subject: [PATCH 20/54] - Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- yices.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/yices.spec b/yices.spec index 562add2..b0cb7b2 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices Version: 2.6.2 -Release: 7%{?dist} +Release: 8%{?dist} Summary: SMT solver # The yices code is GPLv3+. The cudd code is BSD. @@ -153,6 +153,9 @@ make check MODE=debug %license copyright.txt LICENSE.txt %changelog +* Fri Jul 23 2021 Fedora Release Engineering - 2.6.2-8 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild + * Thu Jan 28 2021 Fedora Release Engineering - 2.6.2-7 - Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild From a218fc2b3c6a8a9ae3098d4e5a6ed0ddf5a2fc6f Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 25 Oct 2021 08:01:38 -0600 Subject: [PATCH 21/54] Version 2.6.4. - Drop upstreamed -big-endian and -sphinx3 patches. - Enable tests on 32-bit platforms. --- README.md | 11 ++++++ sources | 2 +- yices-big-endian.patch | 78 --------------------------------------- yices-cryptominisat.patch | 6 +-- yices-sphinx3.patch | 57 ---------------------------- yices.spec | 24 +++++------- 6 files changed, 25 insertions(+), 153 deletions(-) create mode 100644 README.md delete mode 100644 yices-big-endian.patch delete mode 100644 yices-sphinx3.patch 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 #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/52d025a6b0ae2af55bf8f537ddeb9cd8f2519237 -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 - 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 - 2.6.2-8 - Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild From 4669f5bbe6f179739cef3ff092c03a3b3f614f9a Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 11 Jan 2022 15:09:20 -0700 Subject: [PATCH 22/54] Build with kissat support. --- yices.rpmlintrc | 8 -------- yices.spec | 10 +++++++--- 2 files changed, 7 insertions(+), 11 deletions(-) delete mode 100644 yices.rpmlintrc diff --git a/yices.rpmlintrc b/yices.rpmlintrc deleted file mode 100644 index 5aa0040..0000000 --- a/yices.rpmlintrc +++ /dev/null @@ -1,8 +0,0 @@ -# THIS FILE IS FOR WHITELISTING RPMLINT ERRORS AND WARNINGS IN TASKOTRON -# https://fedoraproject.org/wiki/Taskotron/Tasks/dist.rpmlint#Whitelisting_errors - -# The dictionary is missing some technical terms -addFilter(r'W: spelling-error .* (bitvectors|satisfiability|tuples)') - -# Documentation is in the -doc subpackage -addFilter(r'yices-devel\.[^:]+: W: no-documentation') diff --git a/yices.spec b/yices.spec index 2611bec..121d9e5 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices Version: 2.6.4 -Release: 1%{?dist} +Release: 2%{?dist} Summary: SMT solver # The yices code is GPLv3+. The cudd code is BSD. @@ -20,6 +20,7 @@ BuildRequires: gcc BuildRequires: gcc-c++ BuildRequires: gmp-devel BuildRequires: gperf +BuildRequires: kissat-devel BuildRequires: latexmk BuildRequires: libpoly-devel BuildRequires: libtool @@ -94,9 +95,9 @@ cd - #bv64_interval_abstraction depends on wrapping for signed overflow %global optflags %{optflags} -fwrapv -export CPPFLAGS="-I$PWD/cudd-cudd-3.0.0/cudd -DHAVE_CADICAL -DHAVE_CRYPTOMINISAT" +export CPPFLAGS="-I$PWD/cudd-cudd-3.0.0/cudd -DHAVE_CADICAL -DHAVE_CRYPTOMINISAT -DHAVE_KISSAT" export LDFLAGS="$RPM_LD_FLAGS -L$PWD/cudd-cudd-3.0.0/cudd/.libs" -export LIBS="-lcadical -lcryptominisat5" +export LIBS="-lcadical -lcryptominisat5 -lkissat" %configure --enable-mcsat guess=$(./config.guess) @@ -144,6 +145,9 @@ make check MODE=debug %license copyright.txt LICENSE.txt %changelog +* Tue Jan 11 2022 Jerry James - 2.6.4-2 +- Build with kissat support + * Mon Oct 25 2021 Jerry James - 2.6.4-1 - Version 2.6.4 - Drop upstreamed -big-endian and -sphinx3 patches From 685d81a79a0e3c91fdcb5ae5a31bbe5d0d8c44ee Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 22 Jan 2022 05:42:06 +0000 Subject: [PATCH 23/54] - Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- yices.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/yices.spec b/yices.spec index 121d9e5..269a193 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices Version: 2.6.4 -Release: 2%{?dist} +Release: 3%{?dist} Summary: SMT solver # The yices code is GPLv3+. The cudd code is BSD. @@ -145,6 +145,9 @@ make check MODE=debug %license copyright.txt LICENSE.txt %changelog +* Sat Jan 22 2022 Fedora Release Engineering - 2.6.4-3 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild + * Tue Jan 11 2022 Jerry James - 2.6.4-2 - Build with kissat support From 953e1f38049d57e88d3a6aae051e52468ad873df Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 23 Jul 2022 13:45:07 +0000 Subject: [PATCH 24/54] Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- yices.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/yices.spec b/yices.spec index 269a193..96289ea 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices Version: 2.6.4 -Release: 3%{?dist} +Release: 4%{?dist} Summary: SMT solver # The yices code is GPLv3+. The cudd code is BSD. @@ -145,6 +145,9 @@ make check MODE=debug %license copyright.txt LICENSE.txt %changelog +* Sat Jul 23 2022 Fedora Release Engineering - 2.6.4-4 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild + * Sat Jan 22 2022 Fedora Release Engineering - 2.6.4-3 - Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild From 346da4370cf7f78415d19e7729131e101127f796 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Timm=20B=C3=A4der?= Date: Mon, 28 Nov 2022 12:38:10 +0100 Subject: [PATCH 25/54] Get rid of an imlicit int function declaration in a configure check --- implicit-int.patch | 12 ++++++++++++ yices.spec | 7 ++++++- 2 files changed, 18 insertions(+), 1 deletion(-) create mode 100644 implicit-int.patch diff --git a/implicit-int.patch b/implicit-int.patch new file mode 100644 index 0000000..579b87e --- /dev/null +++ b/implicit-int.patch @@ -0,0 +1,12 @@ +diff -ruN yices2-Yices-2.6.4/cudd-cudd-3.0.0/configure.ac yices2-Yices-2.6.4.orig/cudd-cudd-3.0.0/configure.ac +--- a/cudd-cudd-3.0.0/configure.ac 2016-01-20 23:59:33.000000000 +0100 ++++ b/cudd-cudd-3.0.0/configure.ac 2022-11-28 12:32:24.297791070 +0100 +@@ -131,7 +131,7 @@ + AC_CACHE_VAL(ac_cv_have_ieee_754, + [ AC_TRY_RUN([ + #include +-main(void) ++int main(void) + { + if (HUGE_VAL != HUGE_VAL * 3 || HUGE_VAL != HUGE_VAL / 3) return 1; + return 0; diff --git a/yices.spec b/yices.spec index 96289ea..a6c3e4f 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices Version: 2.6.4 -Release: 4%{?dist} +Release: 5%{?dist} Summary: SMT solver # The yices code is GPLv3+. The cudd code is BSD. @@ -13,6 +13,8 @@ Source0: https://github.com/SRI-CSL/yices2/archive/Yices-%{version}.tar.g Source1: https://github.com/ivmai/cudd/archive/cudd-3.0.0.tar.gz # Adapt to newer versions of cryptominisat Patch0: %{name}-cryptominisat.patch +# Get rid of an implicit-int function declaration in a configure check. +Patch1: implicit-int.patch BuildRequires: cadical-devel BuildRequires: cryptominisat-devel @@ -145,6 +147,9 @@ make check MODE=debug %license copyright.txt LICENSE.txt %changelog +* Mon Nov 28 2022 Timm Bäder - 2.6.4-5 +- Get rid of an implicit int function declaration in a configure check + * Sat Jul 23 2022 Fedora Release Engineering - 2.6.4-4 - Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild From 89f048de687540c009b5db98ba600bba73d1cd5c Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 28 Nov 2022 09:19:48 -0700 Subject: [PATCH 26/54] Regenerate the cudd configure script to fix FTBFS. Convert License tag to SPDX. --- yices.spec | 30 ++++++++++++++++++++---------- 1 file changed, 20 insertions(+), 10 deletions(-) diff --git a/yices.spec b/yices.spec index a6c3e4f..408ff83 100644 --- a/yices.spec +++ b/yices.spec @@ -3,8 +3,8 @@ Version: 2.6.4 Release: 5%{?dist} Summary: SMT solver -# The yices code is GPLv3+. The cudd code is BSD. -License: GPLv3+ and BSD +# The yices code is GPL-3.0-or-later. The cudd code is BSD-3-Clause. +License: GPL-3.0-or-later and BSD-3-Clause URL: http://yices.csl.sri.com/ Source0: https://github.com/SRI-CSL/yices2/archive/Yices-%{version}.tar.gz # The CUDD web site disappeared in 2018. The Fedora package was retired in 2019 @@ -78,8 +78,11 @@ sed -i 's/@NO_STACK_PROTECTOR@//' make.include.in # Do not override our build flags sed -i 's/ -O3//;s/ -fomit-frame-pointer//' src/Makefile tests/unit/Makefile -# Generate the configure script +# Generate the configure scripts autoreconf -fi +cd cudd-cudd-3.0.0 +autoreconf -fi +cd - # Fix end of line encodings sed -i 's/\r//' examples/{jinpeng,problem_with_input}.ys @@ -95,11 +98,11 @@ cd cudd-cudd-3.0.0 cd - #bv64_interval_abstraction depends on wrapping for signed overflow -%global optflags %{optflags} -fwrapv - +export CFLAGS='%{build_cflags} -fwrapv' +export CXXFLAGS='%{build_cxxflags} -fwrapv' export CPPFLAGS="-I$PWD/cudd-cudd-3.0.0/cudd -DHAVE_CADICAL -DHAVE_CRYPTOMINISAT -DHAVE_KISSAT" -export LDFLAGS="$RPM_LD_FLAGS -L$PWD/cudd-cudd-3.0.0/cudd/.libs" -export LIBS="-lcadical -lcryptominisat5 -lkissat" +export LDFLAGS="%{build_ldflags} -L$PWD/cudd-cudd-3.0.0/cudd/.libs" +export LIBS='-lcadical -lcryptominisat5 -lkissat' %configure --enable-mcsat guess=$(./config.guess) @@ -129,24 +132,31 @@ make check MODE=debug %files %doc doc/SMT-LIB-LANGUAGE doc/YICES-LANGUAGE %license copyright.txt LICENSE.txt -%{_libdir}/*.so.2* +%{_libdir}/libyices.so.2* %files devel %{_includedir}/%{name}/ -%{_libdir}/*.so +%{_libdir}/libyices.so %files tools %{_bindir}/yices %{_bindir}/yices-sat %{_bindir}/yices-smt %{_bindir}/yices-smt2 -%{_mandir}/man1/* +%{_mandir}/man1/yices.1* +%{_mandir}/man1/yices-sat.1* +%{_mandir}/man1/yices-smt.1* +%{_mandir}/man1/yices-smt2.1* %files doc %doc doc/manual/manual.pdf doc/sphinx/build/html examples %license copyright.txt LICENSE.txt %changelog +* Mon Nov 28 2022 Jerry James - 2.6.4-5 +- Regenerate the cudd configure script to fix FTBFS +- Convert License tag to SPDX + * Mon Nov 28 2022 Timm Bäder - 2.6.4-5 - Get rid of an implicit int function declaration in a configure check From 0dc286da4b9e5e7d4cb4f6c964284f3ee16deb4a Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 14 Dec 2022 16:09:04 -0700 Subject: [PATCH 27/54] Clarify license of the doc subpackage. --- yices.spec | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/yices.spec b/yices.spec index 408ff83..dad961c 100644 --- a/yices.spec +++ b/yices.spec @@ -63,6 +63,35 @@ Requires: %{name}%{?_isa} = %{version}-%{release} Command line tools that use the yices library. %package doc +# The content is GPL-3.0-or-later. Other licenses are due to files copied in +# by Sphinx and due to fonts embedded in PDFs. +# Sphinx file licenses: +# _static/_sphinx_javascript_frameworks_compat.js: BSD-2-Clause +# _static/basic.css: BSD-2-Clause +# _static/classic.css: BSD-2-Clause +# _static/default.css: BSD-2-Clause +# _static/doctools.js: BSD-2-Clause +# _static/documentation_options.js: BSD-2-Clause +# _static/epub.css: BSD-2-Clause +# _static/file.png: BSD-2-Clause +# _static/jquery*.js: MIT +# _static/language_data.js: BSD-2-Clause +# _static/minus.png: BSD-2-Clause +# _static/plus.png: BSD-2-Clause +# _static/searchtools.js: BSD-2-Clause +# _static/sidebar.js: BSD-2-Clause +# _static/underscore*.js: MIT +# genindex.html: BSD-2-Clause +# search.html: BSD-2-Clause +# searchindex.js: BSD-2-Clause +# +# Font licenses: +# AMS: OFL-1.1-RFN +# CM: Knuth-CTAN +# DejaVu: LPPL-1.0 +# LaTeX: LPPL-1.0 +# Nimbus: AGPL-3.0-only +License: GPL-3.0-or-later AND BSD-2-Clause AND MIT AND OFL-1.1-RFN AND Knuth-CTAN AND LPPL-1.0 AND AGPL-3.0-only Summary: Documentation for yices BuildArch: noarch From a4fab3edb052ee2145eb93dcd75ffc2760c08107 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 21 Jan 2023 08:05:33 +0000 Subject: [PATCH 28/54] Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- yices.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/yices.spec b/yices.spec index dad961c..5c2658c 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices Version: 2.6.4 -Release: 5%{?dist} +Release: 6%{?dist} Summary: SMT solver # The yices code is GPL-3.0-or-later. The cudd code is BSD-3-Clause. @@ -182,6 +182,9 @@ make check MODE=debug %license copyright.txt LICENSE.txt %changelog +* Sat Jan 21 2023 Fedora Release Engineering - 2.6.4-6 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild + * Mon Nov 28 2022 Jerry James - 2.6.4-5 - Regenerate the cudd configure script to fix FTBFS - Convert License tag to SPDX From 54c1b94569aae1480f999dd8f5528397361aed18 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 22 Jul 2023 19:30:57 +0000 Subject: [PATCH 29/54] Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- yices.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/yices.spec b/yices.spec index 5c2658c..8d11365 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices Version: 2.6.4 -Release: 6%{?dist} +Release: 7%{?dist} Summary: SMT solver # The yices code is GPL-3.0-or-later. The cudd code is BSD-3-Clause. @@ -182,6 +182,9 @@ make check MODE=debug %license copyright.txt LICENSE.txt %changelog +* Sat Jul 22 2023 Fedora Release Engineering - 2.6.4-7 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild + * Sat Jan 21 2023 Fedora Release Engineering - 2.6.4-6 - Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild From 9f7217058663c190dc5f5ea814cae20ab4456b5c Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 10 Jan 2024 08:39:58 -0700 Subject: [PATCH 30/54] Rebuild for cadical 1.9.4 Update font licenses from LPPL-1.0 to LPPL-1.3a --- yices.spec | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/yices.spec b/yices.spec index 8d11365..8273bdd 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices Version: 2.6.4 -Release: 7%{?dist} +Release: 8%{?dist} Summary: SMT solver # The yices code is GPL-3.0-or-later. The cudd code is BSD-3-Clause. @@ -88,10 +88,10 @@ Command line tools that use the yices library. # Font licenses: # AMS: OFL-1.1-RFN # CM: Knuth-CTAN -# DejaVu: LPPL-1.0 -# LaTeX: LPPL-1.0 +# DejaVu: LPPL-1.3a +# LaTeX: LPPL-1.3a # Nimbus: AGPL-3.0-only -License: GPL-3.0-or-later AND BSD-2-Clause AND MIT AND OFL-1.1-RFN AND Knuth-CTAN AND LPPL-1.0 AND AGPL-3.0-only +License: GPL-3.0-or-later AND BSD-2-Clause AND MIT AND OFL-1.1-RFN AND Knuth-CTAN AND LPPL-1.3a AND AGPL-3.0-only Summary: Documentation for yices BuildArch: noarch @@ -182,6 +182,10 @@ make check MODE=debug %license copyright.txt LICENSE.txt %changelog +* Wed Jan 10 2024 Jerry James - 2.6.4-8 +- Rebuild for cadical 1.9.4 +- Update font licenses from LPPL-1.0 to LPPL-1.3a + * Sat Jul 22 2023 Fedora Release Engineering - 2.6.4-7 - Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild From efe215c436ed75a2679d806fabd7c299105a7b21 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 10 Jan 2024 08:40:22 -0700 Subject: [PATCH 31/54] Stop building for 32-bit x86 --- yices.spec | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/yices.spec b/yices.spec index 8273bdd..fd081e1 100644 --- a/yices.spec +++ b/yices.spec @@ -16,6 +16,9 @@ Patch0: %{name}-cryptominisat.patch # Get rid of an implicit-int function declaration in a configure check. Patch1: implicit-int.patch +# See https://fedoraproject.org/wiki/Changes/EncourageI686LeafRemoval +ExcludeArch: %{ix86} + BuildRequires: cadical-devel BuildRequires: cryptominisat-devel BuildRequires: gcc @@ -185,6 +188,7 @@ make check MODE=debug * Wed Jan 10 2024 Jerry James - 2.6.4-8 - Rebuild for cadical 1.9.4 - Update font licenses from LPPL-1.0 to LPPL-1.3a +- Stop building for 32-bit x86 * Sat Jul 22 2023 Fedora Release Engineering - 2.6.4-7 - Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild From 92f8e5c3859a929f7dd7a7a76a4c63bdd91001dd Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 27 Jan 2024 10:47:14 +0000 Subject: [PATCH 32/54] Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild --- yices.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/yices.spec b/yices.spec index fd081e1..dce05df 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices Version: 2.6.4 -Release: 8%{?dist} +Release: 9%{?dist} Summary: SMT solver # The yices code is GPL-3.0-or-later. The cudd code is BSD-3-Clause. @@ -185,6 +185,9 @@ make check MODE=debug %license copyright.txt LICENSE.txt %changelog +* Sat Jan 27 2024 Fedora Release Engineering - 2.6.4-9 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild + * Wed Jan 10 2024 Jerry James - 2.6.4-8 - Rebuild for cadical 1.9.4 - Update font licenses from LPPL-1.0 to LPPL-1.3a From bfa527cd5ef79c36cc2ccbf6fbb7e2a825452a99 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 31 Jan 2024 16:46:55 -0700 Subject: [PATCH 33/54] Rebuild for cryptominisat 5.11.15 --- yices.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/yices.spec b/yices.spec index dce05df..fad4bce 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices Version: 2.6.4 -Release: 9%{?dist} +Release: 10%{?dist} Summary: SMT solver # The yices code is GPL-3.0-or-later. The cudd code is BSD-3-Clause. @@ -185,6 +185,9 @@ make check MODE=debug %license copyright.txt LICENSE.txt %changelog +* Wed Jan 31 2024 Jerry James - 2.6.4-10 +- Rebuild for cryptominisat 5.11.15 + * Sat Jan 27 2024 Fedora Release Engineering - 2.6.4-9 - Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild From f62cc67a58f2b86dd7619a62a2f0e26b39b02091 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 9 Feb 2024 09:55:46 -0700 Subject: [PATCH 34/54] Rebuild for cryptominisat 5.11.21 --- yices.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/yices.spec b/yices.spec index fad4bce..43741c3 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices Version: 2.6.4 -Release: 10%{?dist} +Release: 11%{?dist} Summary: SMT solver # The yices code is GPL-3.0-or-later. The cudd code is BSD-3-Clause. @@ -185,6 +185,9 @@ make check MODE=debug %license copyright.txt LICENSE.txt %changelog +* Fri Feb 9 2024 Jerry James - 2.6.4-11 +- Rebuild for cryptominisat 5.11.21 + * Wed Jan 31 2024 Jerry James - 2.6.4-10 - Rebuild for cryptominisat 5.11.15 From be95aaac3339958dd25342961ef793f53e302976 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 20 Feb 2024 14:03:45 -0700 Subject: [PATCH 35/54] Fix the SPDX expression --- yices.spec | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/yices.spec b/yices.spec index 43741c3..b93f11d 100644 --- a/yices.spec +++ b/yices.spec @@ -1,10 +1,10 @@ Name: yices Version: 2.6.4 -Release: 11%{?dist} +Release: 12%{?dist} Summary: SMT solver # The yices code is GPL-3.0-or-later. The cudd code is BSD-3-Clause. -License: GPL-3.0-or-later and BSD-3-Clause +License: GPL-3.0-or-later AND BSD-3-Clause URL: http://yices.csl.sri.com/ Source0: https://github.com/SRI-CSL/yices2/archive/Yices-%{version}.tar.gz # The CUDD web site disappeared in 2018. The Fedora package was retired in 2019 @@ -185,6 +185,9 @@ make check MODE=debug %license copyright.txt LICENSE.txt %changelog +* Tue Feb 20 2024 Jerry James - 2.6.4-12 +- Fix the SPDX expression + * Fri Feb 9 2024 Jerry James - 2.6.4-11 - Rebuild for cryptominisat 5.11.21 From ef0cd4c3cb04af1fdd1d26810646f295b403d01d Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 25 Jun 2024 08:24:48 -0600 Subject: [PATCH 36/54] Convert to %autorelease and %autochangelog [skip changelog] --- changelog | 109 +++++++++++++++++++++++++++++++++++++++++++++++++++ yices.spec | 112 +---------------------------------------------------- 2 files changed, 111 insertions(+), 110 deletions(-) create mode 100644 changelog diff --git a/changelog b/changelog new file mode 100644 index 0000000..826b5cd --- /dev/null +++ b/changelog @@ -0,0 +1,109 @@ +* Tue Feb 20 2024 Jerry James - 2.6.4-12 +- Fix the SPDX expression + +* Fri Feb 9 2024 Jerry James - 2.6.4-11 +- Rebuild for cryptominisat 5.11.21 + +* Wed Jan 31 2024 Jerry James - 2.6.4-10 +- Rebuild for cryptominisat 5.11.15 + +* Sat Jan 27 2024 Fedora Release Engineering - 2.6.4-9 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild + +* Wed Jan 10 2024 Jerry James - 2.6.4-8 +- Rebuild for cadical 1.9.4 +- Update font licenses from LPPL-1.0 to LPPL-1.3a +- Stop building for 32-bit x86 + +* Sat Jul 22 2023 Fedora Release Engineering - 2.6.4-7 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild + +* Sat Jan 21 2023 Fedora Release Engineering - 2.6.4-6 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild + +* Mon Nov 28 2022 Jerry James - 2.6.4-5 +- Regenerate the cudd configure script to fix FTBFS +- Convert License tag to SPDX + +* Mon Nov 28 2022 Timm Bäder - 2.6.4-5 +- Get rid of an implicit int function declaration in a configure check + +* Sat Jul 23 2022 Fedora Release Engineering - 2.6.4-4 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild + +* Sat Jan 22 2022 Fedora Release Engineering - 2.6.4-3 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild + +* Tue Jan 11 2022 Jerry James - 2.6.4-2 +- Build with kissat support + +* Mon Oct 25 2021 Jerry James - 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 - 2.6.2-8 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild + +* Thu Jan 28 2021 Fedora Release Engineering - 2.6.2-7 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild + +* Fri Nov 27 2020 Jerry James - 2.6.2-6 +- Rebuild for cryptominisat 5.8.0 + +* Mon Aug 3 2020 Jerry James - 2.6.2-5 +- Rebuild for cadical 1.3.0 + +* Wed Jul 29 2020 Fedora Release Engineering - 2.6.2-4 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild + +* Sat Apr 25 2020 Jerry James - 2.6.2-3 +- Rebuild for cryptominisat 5.7.0 +- Switch to upstream's solution for sphinx 3 support + +* Thu Apr 16 2020 Jerry James - 2.6.2-2 +- Use native sphinx 3 support for enum instead of cenum extension (bz 1823515) + +* Thu Mar 26 2020 Jerry James - 2.6.2-1 +- Version 2.6.2 +- Drop upstreamed -missing-typedef patch +- Add -big-endian patch to fix s390x build +- Add -cryptominisat5 patch to fix build with recent cryptominisat releases +- Skip tests on 32-bit platforms; some tests fail due to the limited size of a + C integer + +* Fri Jan 31 2020 Fedora Release Engineering - 2.6.1-6 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild + +* Thu Jan 23 2020 Jerry James - 2.6.1-5 +- Add -missing-typedef patch to fix FTBFS with gcc 10 +- Set -doc subpackage to noarch + +* Fri Nov 22 2019 Jerry James - 2.6.1-4 +- Add -fwrapv to build flags; thanks to Jeff Law for the diagnosis + +* Sat Jul 27 2019 Fedora Release Engineering - 2.6.1-3 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild + +* Sun Feb 03 2019 Fedora Release Engineering - 2.6.1-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild + +* Tue Oct 30 2018 Jerry James - 2.6.1-1 +- New upstream version + +* Sat Jul 14 2018 Fedora Release Engineering - 2.6.0-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild + +* Wed Jul 4 2018 Jerry James - 2.6.0-1 +- New upstream version + +* Fri Feb 09 2018 Fedora Release Engineering - 2.5.4-3 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild + +* Tue Jan 2 2018 Jerry James - 2.5.4-2 +- Add a -doc subpackage +- Fix end of line encodings +- Fix permissions on yices_debug_version.c + +* Mon Jan 1 2018 Jerry James - 2.5.4-1 +- Initial RPM diff --git a/yices.spec b/yices.spec index b93f11d..069480b 100644 --- a/yices.spec +++ b/yices.spec @@ -1,6 +1,6 @@ Name: yices Version: 2.6.4 -Release: 12%{?dist} +Release: %autorelease Summary: SMT solver # The yices code is GPL-3.0-or-later. The cudd code is BSD-3-Clause. @@ -185,112 +185,4 @@ make check MODE=debug %license copyright.txt LICENSE.txt %changelog -* Tue Feb 20 2024 Jerry James - 2.6.4-12 -- Fix the SPDX expression - -* Fri Feb 9 2024 Jerry James - 2.6.4-11 -- Rebuild for cryptominisat 5.11.21 - -* Wed Jan 31 2024 Jerry James - 2.6.4-10 -- Rebuild for cryptominisat 5.11.15 - -* Sat Jan 27 2024 Fedora Release Engineering - 2.6.4-9 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild - -* Wed Jan 10 2024 Jerry James - 2.6.4-8 -- Rebuild for cadical 1.9.4 -- Update font licenses from LPPL-1.0 to LPPL-1.3a -- Stop building for 32-bit x86 - -* Sat Jul 22 2023 Fedora Release Engineering - 2.6.4-7 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild - -* Sat Jan 21 2023 Fedora Release Engineering - 2.6.4-6 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild - -* Mon Nov 28 2022 Jerry James - 2.6.4-5 -- Regenerate the cudd configure script to fix FTBFS -- Convert License tag to SPDX - -* Mon Nov 28 2022 Timm Bäder - 2.6.4-5 -- Get rid of an implicit int function declaration in a configure check - -* Sat Jul 23 2022 Fedora Release Engineering - 2.6.4-4 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild - -* Sat Jan 22 2022 Fedora Release Engineering - 2.6.4-3 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild - -* Tue Jan 11 2022 Jerry James - 2.6.4-2 -- Build with kissat support - -* Mon Oct 25 2021 Jerry James - 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 - 2.6.2-8 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild - -* Thu Jan 28 2021 Fedora Release Engineering - 2.6.2-7 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild - -* Fri Nov 27 2020 Jerry James - 2.6.2-6 -- Rebuild for cryptominisat 5.8.0 - -* Mon Aug 3 2020 Jerry James - 2.6.2-5 -- Rebuild for cadical 1.3.0 - -* Wed Jul 29 2020 Fedora Release Engineering - 2.6.2-4 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild - -* Sat Apr 25 2020 Jerry James - 2.6.2-3 -- Rebuild for cryptominisat 5.7.0 -- Switch to upstream's solution for sphinx 3 support - -* Thu Apr 16 2020 Jerry James - 2.6.2-2 -- Use native sphinx 3 support for enum instead of cenum extension (bz 1823515) - -* Thu Mar 26 2020 Jerry James - 2.6.2-1 -- Version 2.6.2 -- Drop upstreamed -missing-typedef patch -- Add -big-endian patch to fix s390x build -- Add -cryptominisat5 patch to fix build with recent cryptominisat releases -- Skip tests on 32-bit platforms; some tests fail due to the limited size of a - C integer - -* Fri Jan 31 2020 Fedora Release Engineering - 2.6.1-6 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild - -* Thu Jan 23 2020 Jerry James - 2.6.1-5 -- Add -missing-typedef patch to fix FTBFS with gcc 10 -- Set -doc subpackage to noarch - -* Fri Nov 22 2019 Jerry James - 2.6.1-4 -- Add -fwrapv to build flags; thanks to Jeff Law for the diagnosis - -* Sat Jul 27 2019 Fedora Release Engineering - 2.6.1-3 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild - -* Sun Feb 03 2019 Fedora Release Engineering - 2.6.1-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild - -* Tue Oct 30 2018 Jerry James - 2.6.1-1 -- New upstream version - -* Sat Jul 14 2018 Fedora Release Engineering - 2.6.0-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild - -* Wed Jul 4 2018 Jerry James - 2.6.0-1 -- New upstream version - -* Fri Feb 09 2018 Fedora Release Engineering - 2.5.4-3 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild - -* Tue Jan 2 2018 Jerry James - 2.5.4-2 -- Add a -doc subpackage -- Fix end of line encodings -- Fix permissions on yices_debug_version.c - -* Mon Jan 1 2018 Jerry James - 2.5.4-1 -- Initial RPM +%autochangelog From e18eae7dccc1519897306cf7632c6e38357fa5da Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 25 Jun 2024 10:12:36 -0600 Subject: [PATCH 37/54] Version 2.6.5 --- sources | 2 +- yices.spec | 7 ++++--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/sources b/sources index 43c97dc..6ce754a 100644 --- a/sources +++ b/sources @@ -1,2 +1,2 @@ -SHA512 (Yices-2.6.4.tar.gz) = d8102c41fda0e200fd1336ae317b516d2797d10c187b8f7aecf0c9b08b4b487b90bef8c358099b2da51c0367326939f9610fd4e6d5a41a392cf1114bd04b8763 +SHA512 (Yices-2.6.5.tar.gz) = 8f01c6d516f2aa901b30e9248c3df78930e670c8e1a795b1bb112561f4e338e6e11eadfc2e6cbfc089f6593561b5874fbe816be677dd09c0834a01829c5cf490 SHA512 (cudd-3.0.0.tar.gz) = a26728fedc3033ae2a842000f43f215b4abc914cd00fe0097fd483e59dc630568bfa6a115baa93af94b2f70f3d538761a12143fdb757167e90395c9fd244318c diff --git a/yices.spec b/yices.spec index 069480b..1adff25 100644 --- a/yices.spec +++ b/yices.spec @@ -1,12 +1,13 @@ Name: yices -Version: 2.6.4 +Version: 2.6.5 Release: %autorelease Summary: SMT solver # The yices code is GPL-3.0-or-later. The cudd code is BSD-3-Clause. License: GPL-3.0-or-later AND BSD-3-Clause URL: http://yices.csl.sri.com/ -Source0: https://github.com/SRI-CSL/yices2/archive/Yices-%{version}.tar.gz +VCS: https://github.com/SRI-CSL/yices2 +Source0: %{vcs}/archive/Yices-%{version}.tar.gz # The CUDD web site disappeared in 2018. The Fedora package was retired in 2019 # 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. @@ -125,7 +126,7 @@ sed -i 's/cp/install -m 0644/' utils/make_source_version %build # Build cudd cd cudd-cudd-3.0.0 -%configure CFLAGS="%{build_cflags} -fPIC" CXXFLAGS="%{build_cxxflags} -fPIC" +%configure CFLAGS='%{build_cflags} -fPIC' CXXFLAGS='%{build_cxxflags} -fPIC' %make_build cd - From 35a66d79e8f764686297c891509f201d9b88cb29 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Zbigniew=20J=C4=99drzejewski-Szmek?= Date: Tue, 2 Jul 2024 13:00:50 +0200 Subject: [PATCH 38/54] Use $SOURCE_DATE_EPOCH instead of the current date Using the current date breaks build reproducibility. --- yices.spec | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/yices.spec b/yices.spec index 1adff25..0354bc3 100644 --- a/yices.spec +++ b/yices.spec @@ -111,6 +111,10 @@ sed -i 's/@NO_STACK_PROTECTOR@//' make.include.in # Do not override our build flags sed -i 's/ -O3//;s/ -fomit-frame-pointer//' src/Makefile tests/unit/Makefile +# Use $SOURCE_DATE_EPOCH (or current date) +sed -i "s/^now=.*/now=$(date +%Y-%m-%d ${SOURCE_DATE_EPOCH:+--date=@$SOURCE_DATE_EPOCH})/" \ + utils/make_source_version + # Generate the configure scripts autoreconf -fi cd cudd-cudd-3.0.0 From ad5910f6a89866762622ad6890dc9df26a8be866 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 16 Jul 2024 15:48:35 -0600 Subject: [PATCH 39/54] Rebuild for cryptominisat 5.11.22 --- yices.spec | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/yices.spec b/yices.spec index 0354bc3..2357e68 100644 --- a/yices.spec +++ b/yices.spec @@ -1,3 +1,5 @@ +%global giturl https://github.com/SRI-CSL/yices2 + Name: yices Version: 2.6.5 Release: %autorelease @@ -6,16 +8,16 @@ Summary: SMT solver # The yices code is GPL-3.0-or-later. The cudd code is BSD-3-Clause. License: GPL-3.0-or-later AND BSD-3-Clause URL: http://yices.csl.sri.com/ -VCS: https://github.com/SRI-CSL/yices2 -Source0: %{vcs}/archive/Yices-%{version}.tar.gz +VCS : git:%{giturl}.git +Source0: %{giturl}/archive/Yices-%{version}.tar.gz # The CUDD web site disappeared in 2018. The Fedora package was retired in 2019 # 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 # Adapt to newer versions of cryptominisat -Patch0: %{name}-cryptominisat.patch +Patch: %{name}-cryptominisat.patch # Get rid of an implicit-int function declaration in a configure check. -Patch1: implicit-int.patch +Patch: implicit-int.patch # See https://fedoraproject.org/wiki/Changes/EncourageI686LeafRemoval ExcludeArch: %{ix86} From d056a9c7a9c2503bc6e0162eebf1922f0cd68e72 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 20 Jul 2024 10:42:09 +0000 Subject: [PATCH 40/54] Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild From 7fe83ff4acde36d405166d17d615d180139f1034 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 15 Jan 2025 15:11:42 -0700 Subject: [PATCH 41/54] Move configuration steps to %conf --- yices.spec | 1 + 1 file changed, 1 insertion(+) diff --git a/yices.spec b/yices.spec index 2357e68..79aa2b4 100644 --- a/yices.spec +++ b/yices.spec @@ -107,6 +107,7 @@ This package contains yices documentation. %prep %autosetup -n yices2-Yices-%{version} -a 1 -p1 +%conf # Do not try to avoid -fstack-protector sed -i 's/@NO_STACK_PROTECTOR@//' make.include.in From 0f9eefa2ce199931f475177bfb6b4e8f85d897d3 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sun, 19 Jan 2025 16:34:09 +0000 Subject: [PATCH 42/54] Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild From 605ad4cf449a0345b411f839eef27b98f15613a8 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 11 Feb 2025 10:51:35 -0700 Subject: [PATCH 43/54] Rebuild for cryptominisat 5.12.1 From ce84bc512018b6dd40d9bb56213a37a6b827be9c Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 1 May 2025 09:46:30 -0600 Subject: [PATCH 44/54] Rebuild for cryptominisat 5.13.0 From 570a70c5086a1b07bf01bfac47e2cceeca439540 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 18 Jul 2025 14:04:04 -0600 Subject: [PATCH 45/54] Version 2.7.0 --- .gitignore | 1 + sources | 2 +- yices-cryptominisat.patch | 10 +++++----- yices.spec | 11 ++++------- 4 files changed, 11 insertions(+), 13 deletions(-) diff --git a/.gitignore b/.gitignore index 6d06f33..1c8e76a 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ /Yices-*.tar.gz +/yices-*.tar.gz /cudd-*.tar.gz diff --git a/sources b/sources index 6ce754a..5aa08fc 100644 --- a/sources +++ b/sources @@ -1,2 +1,2 @@ -SHA512 (Yices-2.6.5.tar.gz) = 8f01c6d516f2aa901b30e9248c3df78930e670c8e1a795b1bb112561f4e338e6e11eadfc2e6cbfc089f6593561b5874fbe816be677dd09c0834a01829c5cf490 +SHA512 (yices-2.7.0.tar.gz) = 0ed9811bfc505793078aa87afd86177a79bb5b9a4ec579fa0c43076cc997ff432d66588e996c1303d91bfb2163110312f30f1fc75a4d2f60d5786499bdd26b92 SHA512 (cudd-3.0.0.tar.gz) = a26728fedc3033ae2a842000f43f215b4abc914cd00fe0097fd483e59dc630568bfa6a115baa93af94b2f70f3d538761a12143fdb757167e90395c9fd244318c diff --git a/yices-cryptominisat.patch b/yices-cryptominisat.patch index c8ca3ac..be1cc37 100644 --- a/yices-cryptominisat.patch +++ b/yices-cryptominisat.patch @@ -68,12 +68,12 @@ static smt_status_t cryptominisat_check(void *solver) { - switch (cmsat_solve(solver)) { -- case CMSAT_SAT: return STATUS_SAT; -- case CMSAT_UNSAT: return STATUS_UNSAT; +- case CMSAT_SAT: return YICES_STATUS_SAT; +- case CMSAT_UNSAT: return YICES_STATUS_UNSAT; + switch (cmsat_solve((SATSolver *)solver).x) { -+ case L_TRUE: return STATUS_SAT; -+ case L_FALSE: return STATUS_UNSAT; - default: return STATUS_UNKNOWN; ++ case L_TRUE: return YICES_STATUS_SAT; ++ case L_FALSE: return YICES_STATUS_UNSAT; + default: return YICES_STATUS_UNKNOWN; } } @@ -356,28 +356,23 @@ static smt_status_t cryptominisat_check( diff --git a/yices.spec b/yices.spec index 79aa2b4..8f5caac 100644 --- a/yices.spec +++ b/yices.spec @@ -1,7 +1,7 @@ %global giturl https://github.com/SRI-CSL/yices2 Name: yices -Version: 2.6.5 +Version: 2.7.0 Release: %autorelease Summary: SMT solver @@ -9,7 +9,7 @@ Summary: SMT solver License: GPL-3.0-or-later AND BSD-3-Clause URL: http://yices.csl.sri.com/ VCS : git:%{giturl}.git -Source0: %{giturl}/archive/Yices-%{version}.tar.gz +Source0: %{giturl}/archive/yices-%{version}.tar.gz # The CUDD web site disappeared in 2018. The Fedora package was retired in 2019 # 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. @@ -105,7 +105,7 @@ BuildArch: noarch This package contains yices documentation. %prep -%autosetup -n yices2-Yices-%{version} -a 1 -p1 +%autosetup -n yices2-yices-%{version} -a 1 -p1 %conf # Do not try to avoid -fstack-protector @@ -137,9 +137,6 @@ cd cudd-cudd-3.0.0 %make_build cd - -#bv64_interval_abstraction depends on wrapping for signed overflow -export CFLAGS='%{build_cflags} -fwrapv' -export CXXFLAGS='%{build_cxxflags} -fwrapv' export CPPFLAGS="-I$PWD/cudd-cudd-3.0.0/cudd -DHAVE_CADICAL -DHAVE_CRYPTOMINISAT -DHAVE_KISSAT" export LDFLAGS="%{build_ldflags} -L$PWD/cudd-cudd-3.0.0/cudd/.libs" export LIBS='-lcadical -lcryptominisat5 -lkissat' @@ -172,7 +169,7 @@ make check MODE=debug %files %doc doc/SMT-LIB-LANGUAGE doc/YICES-LANGUAGE %license copyright.txt LICENSE.txt -%{_libdir}/libyices.so.2* +%{_libdir}/libyices.so.2.7* %files devel %{_includedir}/%{name}/ From 548580a5a3e209116902b1ba07d4379fbe0270c9 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Fri, 25 Jul 2025 21:12:24 +0000 Subject: [PATCH 46/54] Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild From a9b6193c7cea08c1ce27ef148c73a9085e0ef7a5 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 5 Dec 2025 11:54:10 -0700 Subject: [PATCH 47/54] Rebuild for cadical 2.2.0 --- yices.spec | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/yices.spec b/yices.spec index 8f5caac..e9c2542 100644 --- a/yices.spec +++ b/yices.spec @@ -40,15 +40,15 @@ BuildRequires: tex(latex) Provides: bundled(cudd) = 3.0.0 %description -Yices 2 is an efficient SMT solver that decides the satisfiability of -formulas containing uninterpreted function symbols with equality, linear -real and integer arithmetic, bitvectors, scalar types, and tuples. +Yices 2 is an efficient SMT solver that decides the satisfiability of formulas +containing uninterpreted function symbols with equality, linear real and +integer arithmetic, bitvectors, scalar types, and tuples. -Yices 2 can process input written in the SMT-LIB notation (both versions -2.0 and 1.2 are supported). +Yices 2 can process input written in the SMT-LIB notation (both versions 2.0 +and 1.2 are supported). -Alternatively, you can write specifications using the Yices 2 -specification language, which includes tuples and scalar types. +Alternatively, you can write specifications using the Yices 2 specification +language, which includes tuples and scalar types. Yices 2 can also be used as a library in other software. @@ -58,8 +58,8 @@ Requires: %{name}%{?_isa} = %{version}-%{release} Requires: gmp-devel%{?_isa} %description devel -This package contains the header files necessary for developing programs -which use yices. +This package contains the header files necessary for developing programs which +use yices. %package tools Summary: Command line tools that use the yices library From 341a656de73a66e73790936c8aac4b20ee2323ab Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 14 Jan 2026 08:53:19 -0700 Subject: [PATCH 48/54] Be more precise about globbing in %files --- yices.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/yices.spec b/yices.spec index e9c2542..bcdfb14 100644 --- a/yices.spec +++ b/yices.spec @@ -169,7 +169,7 @@ make check MODE=debug %files %doc doc/SMT-LIB-LANGUAGE doc/YICES-LANGUAGE %license copyright.txt LICENSE.txt -%{_libdir}/libyices.so.2.7* +%{_libdir}/libyices.so.2.7{,.*} %files devel %{_includedir}/%{name}/ From 56690d563979d72852a848956928eef9f1a415cc Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 17 Jan 2026 21:02:14 +0000 Subject: [PATCH 49/54] Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild From 2ecfd8c6fb46213e6541a84d55e3af42d93d369e Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 20 Feb 2026 08:27:32 -0700 Subject: [PATCH 50/54] Adapt to changes in TeXLive packaging --- yices.spec | 3 +++ 1 file changed, 3 insertions(+) diff --git a/yices.spec b/yices.spec index bcdfb14..0dcf297 100644 --- a/yices.spec +++ b/yices.spec @@ -35,6 +35,9 @@ BuildRequires: libtool BuildRequires: make BuildRequires: %{py3_dist sphinx} BuildRequires: tex(latex) +BuildRequires: texlive-courier +BuildRequires: texlive-helvetic +BuildRequires: texlive-times # See Source1 comment Provides: bundled(cudd) = 3.0.0 From a3e2b398052d9a04e035c4e0066edd08074a68d1 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 30 Apr 2026 12:18:22 -0600 Subject: [PATCH 51/54] Rebuild for cryptominisat 5.14.4 --- yices-cryptominisat.patch | 2 +- yices.spec | 10 ++++++++++ 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/yices-cryptominisat.patch b/yices-cryptominisat.patch index be1cc37..78d4a74 100644 --- a/yices-cryptominisat.patch +++ b/yices-cryptominisat.patch @@ -5,7 +5,7 @@ #ifdef HAVE_CADICAL -#include "ccadical.h" -+#include ++#include #endif #ifdef HAVE_CRYPTOMINISAT diff --git a/yices.spec b/yices.spec index 0dcf297..782983c 100644 --- a/yices.spec +++ b/yices.spec @@ -34,9 +34,19 @@ BuildRequires: libpoly-devel BuildRequires: libtool BuildRequires: make BuildRequires: %{py3_dist sphinx} +BuildRequires: tex(amsfonts.sty) +BuildRequires: tex(cite.sty) +BuildRequires: tex(listings.sty) +BuildRequires: tex(xcolor.sty) BuildRequires: tex(latex) +BuildRequires: texlive-bibtex +BuildRequires: texlive-cm BuildRequires: texlive-courier +BuildRequires: texlive-ec BuildRequires: texlive-helvetic +BuildRequires: texlive-makeindex +BuildRequires: texlive-metafont +BuildRequires: texlive-mfware BuildRequires: texlive-times # See Source1 comment From 307ef2eee4aa592e6b4eb02118c6a97e514e1230 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 30 Apr 2026 14:21:41 -0600 Subject: [PATCH 52/54] BR tex(epstopdf.sty) --- yices.spec | 1 + 1 file changed, 1 insertion(+) diff --git a/yices.spec b/yices.spec index 782983c..318bdd4 100644 --- a/yices.spec +++ b/yices.spec @@ -36,6 +36,7 @@ BuildRequires: make BuildRequires: %{py3_dist sphinx} BuildRequires: tex(amsfonts.sty) BuildRequires: tex(cite.sty) +BuildRequires: tex(epstopdf.sty) BuildRequires: tex(listings.sty) BuildRequires: tex(xcolor.sty) BuildRequires: tex(latex) From 577205dc10feeda512102e7982ba05575d775c38 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 14 Jul 2026 19:34:02 -0600 Subject: [PATCH 53/54] Reduce the number of TeXLive packages used to build --- yices.spec | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/yices.spec b/yices.spec index 318bdd4..7b990a7 100644 --- a/yices.spec +++ b/yices.spec @@ -39,15 +39,13 @@ BuildRequires: tex(cite.sty) BuildRequires: tex(epstopdf.sty) BuildRequires: tex(listings.sty) BuildRequires: tex(xcolor.sty) -BuildRequires: tex(latex) BuildRequires: texlive-bibtex BuildRequires: texlive-cm BuildRequires: texlive-courier BuildRequires: texlive-ec BuildRequires: texlive-helvetic +BuildRequires: texlive-latex BuildRequires: texlive-makeindex -BuildRequires: texlive-metafont -BuildRequires: texlive-mfware BuildRequires: texlive-times # See Source1 comment From a796b4116134d8960f2a60dd3fcf983ad0d833ea Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Fri, 17 Jul 2026 09:34:40 +0000 Subject: [PATCH 54/54] Rebuilt for https://fedoraproject.org/wiki/Fedora_45_Mass_Rebuild