[cvc4] New upstream release.
Jerry James
jjames at fedoraproject.org
Fri Jan 2 23:58:16 UTC 2015
commit f624faa1705dc40eca4a531ea607bed904c85f35
Author: Jerry James <loganjerry at gmail.com>
Date: Fri Jan 2 16:57:48 2015 -0700
New upstream release.
Also:
- Drop updated test files, now included upstream
- Drop obsolete workarounds for glpk compatibility
- Drop lfsc BR/R, as it has been incorporated into cvc4
.gitignore | 2 +-
cvc4-abc.patch | 30 +++++
cvc4-doxygen.patch | 124 ++++++++++++---------
cvc4.spec | 98 ++++++++++------
sat.plf | 127 ---------------------
smt.plf | 313 ----------------------------------------------------
sources | 2 +-
th_base.plf | 107 ------------------
8 files changed, 166 insertions(+), 637 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index c0346c5..c4944a6 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1 @@
-/cvc4-1.3.tar.gz
+/cvc4-1.4.tar.gz
diff --git a/cvc4-abc.patch b/cvc4-abc.patch
new file mode 100644
index 0000000..e2f0dfa
--- /dev/null
+++ b/cvc4-abc.patch
@@ -0,0 +1,30 @@
+--- ./configure.orig 2014-07-13 11:47:37.469270988 -0600
++++ ./configure 2015-01-01 21:00:00.000000000 -0700
+@@ -19368,7 +19368,7 @@ See \`config.log' for more details" "$LI
+
+ fi
+
+- if ! test -d "$ABC_HOME" || ! test -x "$ABC_HOME/arch_flags"; then
++ if ! test -d "$ABC_HOME" ; then
+ { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
+ $as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
+ as_fn_error $? "either $ABC_HOME is not an abc source tree or it's not yet built
+@@ -19377,15 +19377,15 @@ See \`config.log' for more details" "$LI
+
+ { $as_echo "$as_me:${as_lineno-$LINENO}: checking for arch_flags to use with libabc" >&5
+ $as_echo_n "checking for arch_flags to use with libabc... " >&6; }
+- libabc_arch_flags="$("$ABC_HOME/arch_flags")"
++ libabc_arch_flags=""
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: $libabc_arch_flags" >&5
+ $as_echo "$libabc_arch_flags" >&6; }
+- CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$ABC_HOME/src $libabc_arch_flags"
++ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$ABC_HOME/include/abc"
+ ABC_LDFLAGS="-L$ABC_HOME"
+
+ cvc4_save_LDFLAGS="$LDFLAGS"
+ ABC_LIBS=
+- CPPFLAGS="$CPPFLAGS -I$ABC_HOME/src $libabc_arch_flags"
++ CPPFLAGS="$CPPFLAGS -I$ABC_HOME/include/abc"
+ LDFLAGS="$LDFLAGS $ABC_LDFLAGS"
+ ac_fn_c_check_header_mongrel "$LINENO" "base/abc/abc.h" "ac_cv_header_base_abc_abc_h" "$ac_includes_default"
+ if test "x$ac_cv_header_base_abc_abc_h" = xyes; then :
diff --git a/cvc4-doxygen.patch b/cvc4-doxygen.patch
index a572bc9..3c05327 100644
--- a/cvc4-doxygen.patch
+++ b/cvc4-doxygen.patch
@@ -1,5 +1,5 @@
---- ./src/decision/options.h.orig 2013-12-06 16:07:43.586866550 -0700
-+++ ./src/decision/options.h 2013-12-06 16:07:43.586866550 -0700
+--- ./src/decision/options.h.orig 2014-07-13 11:48:44.263172259 -0600
++++ ./src/decision/options.h 2014-07-13 11:48:44.263172259 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@@ -9,8 +9,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
---- ./src/expr/expr_manager_template.h.orig 2013-12-03 15:24:58.911994034 -0700
-+++ ./src/expr/expr_manager_template.h 2013-12-03 15:24:58.911994034 -0700
+--- ./src/expr/expr_manager_template.h.orig 2014-07-13 11:32:35.479585444 -0600
++++ ./src/expr/expr_manager_template.h 2014-07-13 11:32:35.479585444 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file expr_manager_template.h
@@ -18,8 +18,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: Dejan Jovanovic
---- ./src/expr/expr_template.h.orig 2013-11-27 09:42:59.916302990 -0700
-+++ ./src/expr/expr_template.h 2013-11-27 09:42:59.916302990 -0700
+--- ./src/expr/expr_template.h.orig 2014-07-13 11:32:35.479585444 -0600
++++ ./src/expr/expr_template.h 2014-07-13 11:32:35.479585444 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file expr_template.h
@@ -27,8 +27,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: Dejan Jovanovic
---- ./src/expr/kind_template.h.orig 2013-11-11 10:21:58.180347624 -0700
-+++ ./src/expr/kind_template.h 2013-11-11 10:21:58.180347624 -0700
+--- ./src/expr/kind_template.h.orig 2014-07-13 11:32:35.479585444 -0600
++++ ./src/expr/kind_template.h 2014-07-13 11:32:35.479585444 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file kind_template.h
@@ -36,8 +36,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: Dejan Jovanovic
---- ./src/expr/options.h.orig 2013-12-06 16:07:22.010279788 -0700
-+++ ./src/expr/options.h 2013-12-06 16:07:22.010279788 -0700
+--- ./src/expr/options.h.orig 2014-07-13 11:48:13.930308852 -0600
++++ ./src/expr/options.h 2014-07-13 11:48:13.930308852 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@@ -47,8 +47,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
---- ./src/main/options.h.orig 2013-12-06 16:07:45.234911367 -0700
-+++ ./src/main/options.h 2013-12-06 16:07:45.234911367 -0700
+--- ./src/main/options.h.orig 2014-07-13 11:48:47.275258010 -0600
++++ ./src/main/options.h 2014-07-13 11:48:47.275258010 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@@ -58,8 +58,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
---- ./src/options/base_options.h.orig 2013-12-06 16:07:21.118255532 -0700
-+++ ./src/options/base_options.h 2013-12-06 16:07:21.118255532 -0700
+--- ./src/options/base_options.h.orig 2014-07-13 11:48:12.830277541 -0600
++++ ./src/options/base_options.h 2014-07-13 11:48:12.830277541 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@@ -69,8 +69,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
---- ./src/options/base_options_template.h.orig 2013-11-11 10:21:58.276350312 -0700
-+++ ./src/options/base_options_template.h 2013-11-11 10:21:58.276350312 -0700
+--- ./src/options/base_options_template.h.orig 2014-07-13 11:32:35.579588292 -0600
++++ ./src/options/base_options_template.h 2014-07-13 11:32:35.579588292 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file base_options_template.h
@@ -78,8 +78,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
---- ./src/options/options.h.orig 2013-11-11 10:21:58.284350536 -0700
-+++ ./src/options/options.h 2013-11-11 10:21:58.284350536 -0700
+--- ./src/options/options.h.orig 2014-07-01 12:37:15.061881767 -0600
++++ ./src/options/options.h 2014-07-01 12:37:15.061881767 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file options.h
@@ -87,8 +87,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
---- ./src/parser/options.h.orig 2013-12-06 16:07:46.070934102 -0700
-+++ ./src/parser/options.h 2013-12-06 16:07:46.070934102 -0700
+--- ./src/parser/options.h.orig 2014-07-13 11:48:48.427290778 -0600
++++ ./src/parser/options.h 2014-07-13 11:48:48.427290778 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@@ -98,8 +98,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
---- ./src/printer/options.h.orig 2013-12-06 16:07:39.042742975 -0700
-+++ ./src/printer/options.h 2013-12-06 16:07:39.042742975 -0700
+--- ./src/printer/options.h.orig 2014-07-13 11:48:37.070967532 -0600
++++ ./src/printer/options.h 2014-07-13 11:48:37.070967532 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@@ -109,8 +109,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
---- ./src/proof/options.h.orig 2013-12-06 16:07:38.522728834 -0700
-+++ ./src/proof/options.h 2013-12-06 16:07:38.522728834 -0700
+--- ./src/proof/options.h.orig 2014-07-13 11:48:36.346946926 -0600
++++ ./src/proof/options.h 2014-07-13 11:48:36.346946926 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@@ -120,8 +120,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
---- ./src/prop/options.h.orig 2013-12-06 16:07:38.086716977 -0700
-+++ ./src/prop/options.h 2013-12-06 16:07:38.086716977 -0700
+--- ./src/prop/options.h.orig 2014-07-13 11:48:35.870933374 -0600
++++ ./src/prop/options.h 2014-07-13 11:48:35.870933374 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@@ -131,8 +131,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
---- ./src/smt/options.h.orig 2013-12-06 16:07:42.546838267 -0700
-+++ ./src/smt/options.h 2013-12-06 16:07:42.546838267 -0700
+--- ./src/smt/options.h.orig 2014-07-13 11:48:42.683127279 -0600
++++ ./src/smt/options.h 2014-07-13 11:48:42.683127279 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@@ -142,8 +142,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
---- ./src/theory/arith/options.h.orig 2013-12-06 16:07:28.406453727 -0700
-+++ ./src/theory/arith/options.h 2013-12-06 16:07:28.406453727 -0700
+--- ./src/theory/arith/options.h.orig 2014-07-13 11:48:23.866591680 -0600
++++ ./src/theory/arith/options.h 2014-07-13 11:48:23.866591680 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@@ -153,8 +153,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
---- ./src/theory/arrays/options.h.orig 2013-12-06 16:07:31.002524327 -0700
-+++ ./src/theory/arrays/options.h 2013-12-06 16:07:31.002524327 -0700
+--- ./src/theory/arrays/options.h.orig 2014-07-13 11:48:26.966679925 -0600
++++ ./src/theory/arrays/options.h 2014-07-13 11:48:26.966679925 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@@ -164,8 +164,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
---- ./src/theory/booleans/options.h.orig 2013-12-06 16:07:22.494292954 -0700
-+++ ./src/theory/booleans/options.h 2013-12-06 16:07:22.494292954 -0700
+--- ./src/theory/booleans/options.h.orig 2014-07-13 11:48:14.450323654 -0600
++++ ./src/theory/booleans/options.h 2014-07-13 11:48:14.450323654 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@@ -175,8 +175,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
---- ./src/theory/builtin/options.h.orig 2013-12-06 16:07:25.114364203 -0700
-+++ ./src/theory/builtin/options.h 2013-12-06 16:07:25.114364203 -0700
+--- ./src/theory/builtin/options.h.orig 2014-07-13 11:48:18.334434213 -0600
++++ ./src/theory/builtin/options.h 2014-07-13 11:48:18.334434213 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@@ -186,8 +186,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
---- ./src/theory/bv/options.h.orig 2013-12-06 16:07:24.114337006 -0700
-+++ ./src/theory/bv/options.h 2013-12-06 16:07:24.114337006 -0700
+--- ./src/theory/bv/options.h.orig 2014-07-13 11:48:17.270403926 -0600
++++ ./src/theory/bv/options.h 2014-07-13 11:48:17.270403926 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@@ -197,8 +197,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
---- ./src/theory/datatypes/options.h.orig 2013-12-06 16:07:24.714353323 -0700
-+++ ./src/theory/datatypes/options.h 2013-12-06 16:07:24.714353323 -0700
+--- ./src/theory/datatypes/options.h.orig 2014-07-13 11:48:17.930422713 -0600
++++ ./src/theory/datatypes/options.h 2014-07-13 11:48:17.930422713 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@@ -208,8 +208,19 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
---- ./src/theory/options.h.orig 2013-12-06 16:07:23.074308723 -0700
-+++ ./src/theory/options.h 2013-12-06 16:07:23.074308723 -0700
+--- ./src/theory/idl/options.h.orig 2014-07-13 11:48:49.099309909 -0600
++++ ./src/theory/idl/options.h 2014-07-13 11:48:49.099309909 -0600
+@@ -28,7 +28,7 @@
+ /* Edit the template file instead. */
+
+ /********************* */
+-/*! \file base_options_template.h
++/*! \file theory/idl/options.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+--- ./src/theory/options.h.orig 2014-07-13 11:48:15.082341645 -0600
++++ ./src/theory/options.h 2014-07-13 11:48:15.082341645 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@@ -219,8 +230,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
---- ./src/theory/quantifiers/options.h.orig 2013-12-06 16:07:35.278640613 -0700
-+++ ./src/theory/quantifiers/options.h 2013-12-06 16:07:35.278640613 -0700
+--- ./src/theory/quantifiers/options.h.orig 2014-07-13 11:48:32.886848435 -0600
++++ ./src/theory/quantifiers/options.h 2014-07-13 11:48:32.886848435 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@@ -230,19 +241,30 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
---- ./src/theory/rewriterules/options.h.orig 2013-12-06 16:07:35.926658235 -0700
-+++ ./src/theory/rewriterules/options.h 2013-12-06 16:07:35.926658235 -0700
+--- ./src/theory/sets/options.h.orig 2014-07-13 11:48:49.839330972 -0600
++++ ./src/theory/sets/options.h 2014-07-13 11:48:49.839330972 -0600
+@@ -28,7 +28,7 @@
+ /* Edit the template file instead. */
+
+ /********************* */
+-/*! \file base_options_template.h
++/*! \file theory/sets/options.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+--- ./src/theory/strings/options.h.orig 2014-07-13 11:48:34.382891021 -0600
++++ ./src/theory/strings/options.h 2014-07-13 11:48:34.382891021 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
-+/*! \file theory/rewriterules/options.h
++/*! \file theory/strings/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
---- ./src/theory/uf/options.h.orig 2013-12-06 16:07:30.142500939 -0700
-+++ ./src/theory/uf/options.h 2013-12-06 16:07:30.142500939 -0700
+--- ./src/theory/uf/options.h.orig 2014-07-13 11:48:25.926650321 -0600
++++ ./src/theory/uf/options.h 2014-07-13 11:48:25.926650321 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@@ -252,8 +274,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
---- ./src/util/tls.h.in.orig 2013-12-03 13:43:42.822811181 -0700
-+++ ./src/util/tls.h.in 2013-12-03 13:43:42.822811181 -0700
+--- ./src/util/tls.h.in.orig 2014-07-13 11:32:36.123603789 -0600
++++ ./src/util/tls.h.in 2014-07-13 11:32:36.123603789 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file tls.h.in
diff --git a/cvc4.spec b/cvc4.spec
index 3cba481..0961c46 100644
--- a/cvc4.spec
+++ b/cvc4.spec
@@ -1,10 +1,13 @@
+# CVC4 1.4 and later need a modified glpk, unavailable in Fedora. Therefore,
+# we currently build without glpk support.
+
%ifarch %{ix86} x86_64 ppc ppc64
%global have_perftools 1
%endif
Name: cvc4
-Version: 1.3
-Release: 7%{?dist}
+Version: 1.4
+Release: 1%{?dist}
Summary: Automatic theorem prover for SMT problems
# License breakdown:
@@ -12,19 +15,20 @@ Summary: Automatic theorem prover for SMT problems
# o src/util/channel.h
# o examples/hashsmt/sha1.hpp
# - Files containing code under the BSD license:
+# o proofs/lfsc_checker/*
# o src/parser/antlr_input_imports.cpp
# o src/parser/bounded_token_buffer.cpp
# - All other files are distributed under the MIT license
-License: MIT and BSD and Boost
+# But we link with readline, so it all gets subsumed by GPLv3+ anyway.
+License: GPLv3+
URL: http://cvc4.cs.nyu.edu/web/
Source0: http://cvc4.cs.nyu.edu/builds/src/%{name}-%{version}.tar.gz
-# Updated *.plf files from upstream. These are needed only for the self-tests.
-Source1: smt.plf
-Source2: sat.plf
-Source3: th_base.plf
# Fix some doxygen problems. Upstream plans to fix this differently.
Patch0: %{name}-doxygen.patch
+# Adapt to the way the Fedora ABC package is constructed.
+Patch1: %{name}-abc.patch
+BuildRequires: abc-devel
BuildRequires: antlr3-C-devel
BuildRequires: antlr3-tool
BuildRequires: boost-devel
@@ -32,21 +36,21 @@ BuildRequires: chrpath
BuildRequires: cxxtest
BuildRequires: doxygen-latex
BuildRequires: ghostscript
-BuildRequires: glpk-devel
BuildRequires: gmp-devel
%if 0%{?have_perftools}
BuildRequires: gperftools-devel
%endif
-BuildRequires: java-devel >= 1:1.6.0
+BuildRequires: java-devel
BuildRequires: jpackage-utils
-BuildRequires: lfsc
BuildRequires: perl
BuildRequires: python
BuildRequires: readline-devel
BuildRequires: swig
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
-Requires: lfsc
+
+Obsoletes: lfsc < 1.0-1%{?dist}
+Provides: lfsc = %{version}-%{release}
%description
CVC4 is an efficient open-source automatic theorem prover for
@@ -74,6 +78,7 @@ Header files and library links for developing applications that use %{name}.
%package doc
Summary: Interface documentation for %{name}
+Provides: bundled(jquery)
%description doc
Interface documentation for %{name}.
@@ -96,33 +101,51 @@ Java interface to %{name}.
%prep
%setup -q
-# The rpm patch macro doesn't understand -T, and we need to it to avoid
+# The rpm patch macro doesn't understand -T, and we need it to to avoid
# regenerating the very files we're trying to patch.
patch -p0 -T < %{PATCH0}
+%patch1
-# Don't change the build flags we want to use and avoid hardcoded rpaths
+# Don't change the build flags we want to use, avoid hardcoded rpaths, adapt to
+# antlr 3.5, and allow boost to use g++ 4.9.
sed -e '/^if test "$enable_debug_symbols"/,/fi/d' \
- -e 's|^hardcode_libdir_flag_spec=.*|hardcode_libdir_flag_spec=""|g' \
- -e 's|^runpath_var=LD_RUN_PATH|runpath_var=DIE_RPATH_DIE|g' \
+ -e 's,^hardcode_libdir_flag_spec=.*,hardcode_libdir_flag_spec="",g' \
+ -e 's,runpath_var=LD_RUN_PATH,runpath_var=DIE_RPATH_DIE,g' \
+ -e 's,\([^.]\)3\.4,\13.5,g' \
+ -e 's,\(__GNUC_MINOR__ == \)8\(.*\)gcc48,\19\2gcc49,' \
-i configure
# Change the Java installation paths for Fedora
sed -i "s|^\(javalibdir =.*\)jni|\1java/%{name}|" src/bindings/Makefile.in
+# Make lfsc documentation available
+cp -p proofs/lfsc_checker/AUTHORS AUTHORS.lfsc
+cp -p proofs/lfsc_checker/COPYING COPYING.lfsc
+cp -p proofs/lfsc_checker/NEWS NEWS.lfsc
+cp -p proofs/lfsc_checker/README README.lfsc
+
+# Preserve timestamps when installing
+for fil in $(find . -name Makefile\*); do
+ sed -i 's/$(install_sh) -c/$(install_sh) -p/' $fil
+done
+
%build
-%configure --enable-proof --enable-language-bindings=all --with-portfolio \
+export CPPFLAGS="-I%{_jvmdir}/java/include -I%{_jvmdir}/java/include/linux -I%{_includedir}/abc"
+%if %{__isa_bits} == 64
+CPPFLAGS+=" -DLIN64"
+%else
+CPPFLAGS+=" -DLIN"
+%endif
+%configure --enable-gpl --enable-proof --enable-language-bindings=all \
%if 0%{?have_perftools}
--with-google-perftools \
%endif
- --with-glpk --without-compat \
- CPPFLAGS="-I%{_jvmdir}/java/include -I%{_jvmdir}/java/include/linux -DFEDORA_GLPK_ITCNT -Dlpx_get_int_parm(x,y)=glp_get_it_cnt(x)" \
- LFSCARGS="%{_datadir}/lfsc/sat.plf"
+ --with-portfolio --with-abc --with-abc-dir=%{_prefix} --with-readline \
+ --without-compat
# Workaround libtool reordering -Wl,--as-needed after all the libraries
-sed -i 's/CC=.g../& -Wl,--as-needed/' builds/*-linux-gnu/default-proof/libtool
-
-# Workaround insufficiently quoted CPPFLAGS
-find builds -name Makefile | xargs sed -i 's/-Dlpx.*glp_get_it_cnt(x)/"&"/'
+sed -i 's/CC=.g../& -Wl,--as-needed/' \
+ builds/*-linux-gnu*/production-abc-proof/libtool
make %{?_smp_mflags}
make doc
@@ -150,14 +173,14 @@ chrpath -d %{buildroot}%{_bindir}/* \
%{buildroot}%{_jnidir}/%{name}/lib%{name}*.so.*.*.*
# Help the debuginfo generator
-BUILDS=builds/*-*-linux-gnu
+BUILDS=$(echo builds/*-*-linux-gnu*)
for dir in decision expr main parser printer prop smt theory theory/arith \
theory/arrays theory/booleans theory/bv theory/datatypes theory/idl \
theory/quantifiers theory/rewriterules theory/strings theory/uf; do
- ln -s $PWD/src/$dir/options $BUILDS/default-proof/src/$dir
+ ln -s $PWD/src/$dir/options $BUILDS/production-abc-proof/src/$dir
done
-ln -s default-proof/src $BUILDS
-ln -s $PWD/src/options/base_options $BUILDS/default-proof/src/options
+ln -s production-abc-proof/src $BUILDS
+ln -s $PWD/src/options/base_options $BUILDS/production-abc-proof/src/options
ln -s $PWD/src/options/base_options_template.cpp $BUILDS/src/options
ln -s $PWD/src/options/options_holder_template.h $BUILDS/src/options
ln -s $PWD/src/options/options_template.cpp $BUILDS/src/options
@@ -171,19 +194,14 @@ ln -s $PWD/src/smt/smt_options_template.cpp $BUILDS/src/smt
# The tests use a large amount of stack space
ulimit -s unlimited
-# The tests require unreleased *.plf files from upstream
-for mk in $(find builds/*-*-linux-gnu/default-proof/test -name Makefile)
-do
- sed -e 's,^\(LFSCARGS =\).*,\1 %{SOURCE1} %{SOURCE2} %{SOURCE3},' \
- -e 's,^\(TESTS_ENVIRONMENT = LFSC=\)".*",\1"lfsc %{SOURCE1} %{SOURCE2} %{SOURCE3}",' \
- -i $mk
-done
-
+export LD_LIBRARY_PATH=$PWD/builds%{_libdir}
make check
%files
-%doc AUTHORS NEWS README RELEASE-NOTES THANKS
+%doc AUTHORS AUTHORS.lfsc NEWS NEWS.lfsc README README.lfsc RELEASE-NOTES THANKS
+%license COPYING.lfsc
%{_bindir}/*
+%{_datadir}/%{name}/
%{_mandir}/man1/*
%{_mandir}/man5/*
@@ -191,7 +209,7 @@ make check
%doc doc/doxygen/*
%files libs
-%doc COPYING
+%license COPYING
%{_libdir}/lib%{name}*.so.*
%files devel
@@ -204,6 +222,12 @@ make check
%{_jnidir}/%{name}/
%changelog
+* Thu Jan 1 2015 Jerry James <loganjerry at gmail.com> - 1.4-1
+- New upstream release
+- Drop updated test files, now included upstream
+- Drop obsolete workarounds for glpk compatibility
+- Drop lfsc BR/R, as it has been incorporated into cvc4
+
* Fri Aug 22 2014 Jerry James <loganjerry at gmail.com> - 1.3-7
- Remove arm platforms from have_perftools due to bz 1109309
diff --git a/sources b/sources
index 7bf6add..e52e87d 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-a8c2bf10b7fa581a8de283072f4137b6 cvc4-1.3.tar.gz
+581c559c02b94fcb18b2e5b11432e009 cvc4-1.4.tar.gz
More information about the scm-commits
mailing list