rpms/yices
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Compare commits

base: rpms:rawhide
Branches Tags
rpms:rawhide
rpms:f45
rpms:main
rpms:f44
rpms:f43
rpms:f42
rpms:f41
rpms:f40
rpms:f39
rpms:f38
rpms:f37
rpms:f36
rpms:f35
rpms:f34
rpms:f33
rpms:f32
rpms:f31
rpms:f30
rpms:f29
rpms:f28
rpms:f27
..
compare: rpms:f33
Branches Tags
rpms:f45
rpms:main
rpms:rawhide
rpms:f44
rpms:f43
rpms:f42
rpms:f41
rpms:f40
rpms:f39
rpms:f38
rpms:f37
rpms:f36
rpms:f35
rpms:f34
rpms:f33
rpms:f32
rpms:f31
rpms:f30
rpms:f29
rpms:f28
rpms:f27

No commits in common. "rawhide" and "f33" have entirely different histories.
rawhide ... f33

10 changed files with 249 additions and 230 deletions
Download patch file Download diff file Expand all files Collapse all files

1
.gitignore vendored
View file

@ -1,3 +1,2 @@
/Yices-*.tar.gz
/yices-*.tar.gz
/cudd-*.tar.gz

11
README.md
View file

@ -1,11 +0,0 @@
# 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.

109
changelog
View file

@ -1,109 +0,0 @@
* Tue Feb 20 2024 Jerry James <loganjerry@gmail.com> - 2.6.4-12
- Fix the SPDX expression
* Fri Feb 9 2024 Jerry James <loganjerry@gmail.com> - 2.6.4-11
- Rebuild for cryptominisat 5.11.21
* Wed Jan 31 2024 Jerry James <loganjerry@gmail.com> - 2.6.4-10
- Rebuild for cryptominisat 5.11.15
* Sat Jan 27 2024 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.4-9
- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild
* Wed Jan 10 2024 Jerry James <loganjerry@gmail.com> - 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 <releng@fedoraproject.org> - 2.6.4-7
- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild
* Sat Jan 21 2023 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.4-6
- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild
* Mon Nov 28 2022 Jerry James <loganjerry@gmail.com> - 2.6.4-5
- Regenerate the cudd configure script to fix FTBFS
- Convert License tag to SPDX
* Mon Nov 28 2022 Timm Bäder <tbaeder@redhat.com> - 2.6.4-5
- Get rid of an implicit int function declaration in a configure check
* Sat Jul 23 2022 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.4-4
- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild
* Sat Jan 22 2022 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.4-3
- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild
* Tue Jan 11 2022 Jerry James <loganjerry@gmail.com> - 2.6.4-2
- Build with kissat support
* Mon Oct 25 2021 Jerry James <loganjerry@gmail.com> - 2.6.4-1
- Version 2.6.4
- Drop upstreamed -big-endian and -sphinx3 patches
- Enable tests on 32-bit platforms
* Fri Jul 23 2021 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.2-8
- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild
* Thu Jan 28 2021 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.2-7
- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild
* Fri Nov 27 2020 Jerry James <loganjerry@gmail.com> - 2.6.2-6
- Rebuild for cryptominisat 5.8.0
* Mon Aug 3 2020 Jerry James <loganjerry@gmail.com> - 2.6.2-5
- Rebuild for cadical 1.3.0
* Wed Jul 29 2020 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.2-4
- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild
* Sat Apr 25 2020 Jerry James <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 2.6.2-2
- Use native sphinx 3 support for enum instead of cenum extension (bz 1823515)
* Thu Mar 26 2020 Jerry James <loganjerry@gmail.com> - 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 <releng@fedoraproject.org> - 2.6.1-6
- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild
* Thu Jan 23 2020 Jerry James <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 2.6.1-4
- Add -fwrapv to build flags; thanks to Jeff Law for the diagnosis
* Sat Jul 27 2019 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.1-3
- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild
* Sun Feb 03 2019 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.1-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild
* Tue Oct 30 2018 Jerry James <loganjerry@gmail.com> - 2.6.1-1
- New upstream version
* Sat Jul 14 2018 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.0-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
* Wed Jul 4 2018 Jerry James <loganjerry@gmail.com> - 2.6.0-1
- New upstream version
* Fri Feb 09 2018 Fedora Release Engineering <releng@fedoraproject.org> - 2.5.4-3
- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
* Tue Jan 2 2018 Jerry James <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 2.5.4-1
- Initial RPM

12
implicit-int.patch
View file

@ -1,12 +0,0 @@
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 <math.h>
-main(void)
+int main(void)
{
if (HUGE_VAL != HUGE_VAL * 3 || HUGE_VAL != HUGE_VAL / 3) return 1;
return 0;

2
sources
View file

@ -1,2 +1,2 @@
SHA512 (yices-2.7.0.tar.gz) = 0ed9811bfc505793078aa87afd86177a79bb5b9a4ec579fa0c43076cc997ff432d66588e996c1303d91bfb2163110312f30f1fc75a4d2f60d5786499bdd26b92
SHA512 (Yices-2.6.2.tar.gz) = 58990cff2a70d4fae797efdf3c52a15772eb824bc6865682fa64e63b571054eb042a252e52b67b2f89fb191444543f0ad55f9b34086bdd8bcd083ef10422d388
SHA512 (cudd-3.0.0.tar.gz) = a26728fedc3033ae2a842000f43f215b4abc914cd00fe0097fd483e59dc630568bfa6a115baa93af94b2f70f3d538761a12143fdb757167e90395c9fd244318c

78
yices-big-endian.patch Normal file
View file

@ -0,0 +1,78 @@
--- 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

18
yices-cryptominisat.patch
View file

@ -5,7 +5,7 @@
#ifdef HAVE_CADICAL
-#include "ccadical.h"
+#include <cadical/ccadical.h>
+#include <ccadical.h>
#endif
#ifdef HAVE_CRYPTOMINISAT
@ -13,8 +13,8 @@
+#include <cryptominisat5/cryptominisat_c.h>
#endif
#ifdef HAVE_KISSAT
@@ -308,44 +308,44 @@ static void cadical_as_delegate(delegate
#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) {
@ -68,15 +68,15 @@
static smt_status_t cryptominisat_check(void *solver) {
- switch (cmsat_solve(solver)) {
- case CMSAT_SAT: return YICES_STATUS_SAT;
- case CMSAT_UNSAT: return YICES_STATUS_UNSAT;
- case CMSAT_SAT: return STATUS_SAT;
- case CMSAT_UNSAT: return STATUS_UNSAT;
+ switch (cmsat_solve((SATSolver *)solver).x) {
+ case L_TRUE: return YICES_STATUS_SAT;
+ case L_FALSE: return YICES_STATUS_UNSAT;
default: return YICES_STATUS_UNKNOWN;
+ case L_TRUE: return STATUS_SAT;
+ case L_FALSE: return STATUS_UNSAT;
default: return STATUS_UNKNOWN;
}
}
@@ -356,28 +356,23 @@ static smt_status_t cryptominisat_check(
@@ -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) {

57
yices-sphinx3.patch Normal file
View file

@ -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;
}

8
yices.rpmlintrc Normal file
View file

@ -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')

183
yices.spec
View file

@ -1,26 +1,24 @@
%global giturl https://github.com/SRI-CSL/yices2
Name: yices
Version: 2.7.0
Release: %autorelease
Version: 2.6.2
Release: 6%{?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
# The yices code is GPLv3+. The cudd code is BSD.
License: GPLv3+ and BSD
URL: http://yices.csl.sri.com/
VCS : git:%{giturl}.git
Source0: %{giturl}/archive/yices-%{version}.tar.gz
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
# 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
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}
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
@ -28,39 +26,26 @@ BuildRequires: gcc
BuildRequires: gcc-c++
BuildRequires: gmp-devel
BuildRequires: gperf
BuildRequires: kissat-devel
BuildRequires: latexmk
BuildRequires: libpoly-devel
BuildRequires: libtool
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
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 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.
@ -70,8 +55,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
@ -81,35 +66,6 @@ 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
@ -117,24 +73,17 @@ BuildArch: noarch
This package contains yices documentation.
%prep
%autosetup -n yices2-yices-%{version} -a 1 -p1
%autosetup -n yices2-Yices-%{version} -p1
%setup -q -n yices2-Yices-%{version} -T -D -a 1
%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
# 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
# Generate the configure script
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
@ -145,13 +94,16 @@ 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="%{optflags} -fPIC" CXXFLAGS="%{optflags} -fPIC"
%make_build
cd -
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'
#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
guess=$(./config.guess)
@ -175,31 +127,88 @@ 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}/libyices.so.2.7{,.*}
%{_libdir}/*.so.2*
%files devel
%{_includedir}/%{name}/
%{_libdir}/libyices.so
%{_libdir}/*.so
%files tools
%{_bindir}/yices
%{_bindir}/yices-sat
%{_bindir}/yices-smt
%{_bindir}/yices-smt2
%{_mandir}/man1/yices.1*
%{_mandir}/man1/yices-sat.1*
%{_mandir}/man1/yices-smt.1*
%{_mandir}/man1/yices-smt2.1*
%{_mandir}/man1/*
%files doc
%doc doc/manual/manual.pdf doc/sphinx/build/html examples
%license copyright.txt LICENSE.txt
%changelog
%autochangelog
* Fri Nov 27 2020 Jerry James <loganjerry@gmail.com> - 2.6.2-6
- Rebuild for cryptominisat 5.8.0
* Mon Aug 3 2020 Jerry James <loganjerry@gmail.com> - 2.6.2-5
- Rebuild for cadical 1.3.0
* Wed Jul 29 2020 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.2-4
- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild
* Sat Apr 25 2020 Jerry James <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 2.6.2-2
- Use native sphinx 3 support for enum instead of cenum extension (bz 1823515)
* Thu Mar 26 2020 Jerry James <loganjerry@gmail.com> - 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 <releng@fedoraproject.org> - 2.6.1-6
- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild
* Thu Jan 23 2020 Jerry James <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 2.6.1-4
- Add -fwrapv to build flags; thanks to Jeff Law for the diagnosis
* Sat Jul 27 2019 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.1-3
- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild
* Sun Feb 03 2019 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.1-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild
* Tue Oct 30 2018 Jerry James <loganjerry@gmail.com> - 2.6.1-1
- New upstream version
* Sat Jul 14 2018 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.0-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
* Wed Jul 4 2018 Jerry James <loganjerry@gmail.com> - 2.6.0-1
- New upstream version
* Fri Feb 09 2018 Fedora Release Engineering <releng@fedoraproject.org> - 2.5.4-3
- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
* Tue Jan 2 2018 Jerry James <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 2.5.4-1
- Initial RPM