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/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/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/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/sources b/sources index 5efcc73..5aa08fc 100644 --- a/sources +++ b/sources @@ -1,2 +1,2 @@ -SHA512 (Yices-2.6.2.tar.gz) = 58990cff2a70d4fae797efdf3c52a15772eb824bc6865682fa64e63b571054eb042a252e52b67b2f89fb191444543f0ad55f9b34086bdd8bcd083ef10422d388 +SHA512 (yices-2.7.0.tar.gz) = 0ed9811bfc505793078aa87afd86177a79bb5b9a4ec579fa0c43076cc997ff432d66588e996c1303d91bfb2163110312f30f1fc75a4d2f60d5786499bdd26b92 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..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 @@ -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) { @@ -68,15 +68,15 @@ 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; } } -@@ -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.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 f17f7a9..7b990a7 100644 --- a/yices.spec +++ b/yices.spec @@ -1,24 +1,26 @@ +%global giturl https://github.com/SRI-CSL/yices2 + Name: yices -Version: 2.6.2 -Release: 3%{?dist} +Version: 2.7.0 +Release: %autorelease 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 +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 -# 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 +Patch: %{name}-cryptominisat.patch +# Get rid of an implicit-int function declaration in a configure check. +Patch: implicit-int.patch + +# See https://fedoraproject.org/wiki/Changes/EncourageI686LeafRemoval +ExcludeArch: %{ix86} BuildRequires: cadical-devel BuildRequires: cryptominisat-devel @@ -26,25 +28,39 @@ BuildRequires: gcc BuildRequires: gcc-c++ BuildRequires: gmp-devel BuildRequires: gperf +BuildRequires: kissat-devel BuildRequires: latexmk BuildRequires: libpoly-devel BuildRequires: libtool -BuildRequires: python3dist(sphinx) -BuildRequires: tex(latex) +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: texlive-bibtex +BuildRequires: texlive-cm +BuildRequires: texlive-courier +BuildRequires: texlive-ec +BuildRequires: texlive-helvetic +BuildRequires: texlive-latex +BuildRequires: texlive-makeindex +BuildRequires: texlive-times # 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 -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. @@ -54,8 +70,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 @@ -65,6 +81,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.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.3a AND AGPL-3.0-only Summary: Documentation for yices BuildArch: noarch @@ -72,17 +117,24 @@ 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 +%conf # Do not try to avoid -fstack-protector 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 +# 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 +autoreconf -fi +cd - # Fix end of line encodings sed -i 's/\r//' examples/{jinpeng,problem_with_input}.ys @@ -93,16 +145,13 @@ 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 - -#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" +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' %configure --enable-mcsat guess=$(./config.guess) @@ -126,79 +175,31 @@ 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 %license copyright.txt LICENSE.txt -%{_libdir}/*.so.2* +%{_libdir}/libyices.so.2.7{,.*} %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 -* 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