[calligra] 2.7.1
by Rex Dieter
commit 3ead173f8afd3ccc824c506b39f280cb63fec1e5
Author: Rex Dieter <rdieter(a)math.unl.edu>
Date: Wed Jul 31 18:16:08 2013 -0500
2.7.1
.gitignore | 3 +--
calligra-2.7.0-krita_mime_install.patch | 11 -----------
calligra.spec | 16 ++++++----------
qreal_double.patch | 21 ---------------------
sources | 2 +-
5 files changed, 8 insertions(+), 45 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index a20751d..83417c2 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1 @@
-/calligra-2.6.4.tar.bz2
-/calligra-2.7.0.tar.bz2
+/calligra-2.7.1.tar.xz
diff --git a/calligra.spec b/calligra.spec
index 9f118bb..64c18aa 100644
--- a/calligra.spec
+++ b/calligra.spec
@@ -14,8 +14,8 @@
%global _changelog_trimtime %(date +%s -d "1 year ago")
Name: calligra
-Version: 2.7.0
-Release: 3%{?dist}
+Version: 2.7.1
+Release: 1%{?dist}
Summary: An integrated office suite
License: GPLv2+ and LGPLv2+
@@ -26,15 +26,11 @@ URL: http://www.calligra-suite.org/
%else
%global stable stable
%endif
-Source0: http://download.kde.org/%{stable}/calligra-%{version}/calligra-%{version}...
+Source0: http://download.kde.org/%{stable}/calligra-%{version}/calligra-%{version}...
## upstreamable patches
-# arm qreal vs float patch courtesy of kubuntu
-# http://bazaar.launchpad.net/~kubuntu-packagers/kubuntu-packaging/calligra...
-Patch50: qreal_double.patch
## upstream patches
-Patch100: calligra-2.7.0-krita_mime_install.patch
BuildRequires: boost-devel
BuildRequires: bzip2-devel bzip2
@@ -468,9 +464,6 @@ Requires: okular%{?_kde4_version: >= %{_kde4_version}}
%prep
%setup -q
-%patch50 -p1 -b .qreal_double
-%patch100 -p1 -b .krita_mime_install
-
## kdchart munging begin
pushd 3rdparty/kdchart
mv src kdchart
@@ -1163,6 +1156,9 @@ fi
%changelog
+* Wed Jul 31 2013 Rex Dieter <rdieter(a)fedoraproject.org> 2.7.1-1
+- 2.7.1
+
* Tue Jul 30 2013 Petr Machata <pmachata(a)redhat.com> - 2.7.0-3
- Rebuild for boost 1.54.0
diff --git a/sources b/sources
index e9981a5..bfc1b46 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-ae154d84e3745bfd170020066f6086e8 calligra-2.7.0.tar.bz2
+9cf909ddf57ecb16d4370cc1062d0f7f calligra-2.7.1.tar.xz
9Â years, 6Â months
[undertaker] Add -picosat patch to adapt to new reentrant picosat API. Fix bogus changelog date.
by Jerry James
commit 10db322d6189204b89f2777a9563e4f2141a5733
Author: Jerry James <jamesjer(a)betterlinux.com>
Date: Wed Jul 31 16:51:08 2013 -0600
Add -picosat patch to adapt to new reentrant picosat API.
Fix bogus changelog date.
undertaker-boost_mt.patch | 12 +++---
undertaker-picosat.patch | 91 +++++++++++++++++++++++++++++++++++++++++++++
undertaker.spec | 17 +++++---
3 files changed, 107 insertions(+), 13 deletions(-)
---
diff --git a/undertaker-boost_mt.patch b/undertaker-boost_mt.patch
index 65b049e..2c8f06a 100644
--- a/undertaker-boost_mt.patch
+++ b/undertaker-boost_mt.patch
@@ -1,6 +1,6 @@
-diff -up vamos-1.2/undertaker/Makefile~ vamos-1.2/undertaker/Makefile
---- vamos-1.2/undertaker/Makefile~ 2011-08-30 12:11:34.000000000 +0200
-+++ vamos-1.2/undertaker/Makefile 2013-07-28 00:56:25.617959197 +0200
+diff -up ./undertaker/Makefile~ ./undertaker/Makefile
+--- ./undertaker/Makefile~ 2011-08-30 12:11:34.000000000 +0200
++++ ./undertaker/Makefile 2013-07-28 00:56:25.000000000 +0200
@@ -13,7 +13,7 @@ CXXFLAGS = $(CFLAGS)
LDFLAGS =
@@ -10,9 +10,9 @@ diff -up vamos-1.2/undertaker/Makefile~ vamos-1.2/undertaker/Makefile
PARSEROBJ = RsfReader.o KconfigWhitelist.o ConfigurationModel.o \
ModelContainer.o SatChecker.o BlockDefectAnalyzer.o \
-diff -up vamos-1.2/ziz/Makefile~ vamos-1.2/ziz/Makefile
---- vamos-1.2/ziz/Makefile~ 2011-08-24 17:05:15.000000000 +0200
-+++ vamos-1.2/ziz/Makefile 2013-07-28 00:56:36.850027021 +0200
+diff -up ./ziz/Makefile~ ./ziz/Makefile
+--- ./ziz/Makefile~ 2011-08-24 17:05:15.000000000 +0200
++++ ./ziz/Makefile 2013-07-28 00:56:36.000000000 +0200
@@ -3,7 +3,7 @@ LDXX=g++
DEBUG = -g3
CFLAGS = -Wall -Wextra -O2 $(DEBUG)
diff --git a/undertaker-picosat.patch b/undertaker-picosat.patch
new file mode 100644
index 0000000..58b3a0a
--- /dev/null
+++ b/undertaker-picosat.patch
@@ -0,0 +1,91 @@
+--- ./undertaker/SatChecker.h.orig 2011-08-24 09:05:15.000000000 -0600
++++ ./undertaker/SatChecker.h 2013-07-31 16:34:25.000000000 -0600
+@@ -48,7 +48,7 @@ namespace Picosat {
+
+ /* Include the Limmat library header as C */
+ extern "C" {
+-#include <picosat/picosat.h>
++#include <picosat.h>
+ }
+ };
+
+@@ -202,6 +202,8 @@ private:
+ const std::string _sat;
+ clock_t _runtime;
+
++ Picosat::PicoSAT *picosat_inst;
++
+ int stringToSymbol(const std::string &key);
+ int newSymbol(void);
+ void addClause(int *clause);
+--- ./undertaker/SatChecker.cpp.orig 2011-08-24 09:05:15.000000000 -0600
++++ ./undertaker/SatChecker.cpp 2013-07-31 16:32:06.000000000 -0600
+@@ -70,13 +70,13 @@ int SatChecker::stringToSymbol(const std
+ }
+
+ int SatChecker::newSymbol(void) {
+- return Picosat::picosat_inc_max_var();
++ return Picosat::picosat_inc_max_var(picosat_inst);
+ }
+
+ void SatChecker::addClause(int *clause) {
+ for (int *x = clause; *x; x++)
+- Picosat::picosat_add(*x);
+- Picosat::picosat_add(0);
++ Picosat::picosat_add(picosat_inst, *x);
++ Picosat::picosat_add(picosat_inst, 0);
+ }
+
+ int SatChecker::notClause(int inner_clause) {
+@@ -299,7 +299,8 @@ void SatChecker::fillSatChecker(std::str
+ std::cout << std::string(expression.begin(), expression.begin()
+ + info.length) << endl;
+ */
+- Picosat::picosat_reset();
++ Picosat::picosat_reset(picosat_inst);
++ picosat_inst = NULL;
+ throw SatCheckerError("SatChecker: Couldn't parse: " + expression);
+ }
+ }
+@@ -308,7 +309,7 @@ void SatChecker::fillSatChecker(tree_par
+ iter_t expression = info.trees.begin()->children.begin();
+ int top_clause = transform_bool_rec(expression);
+ /* This adds the last clause */
+- Picosat::picosat_assume(top_clause);
++ Picosat::picosat_assume(picosat_inst, top_clause);
+ }
+
+ SatChecker::SatChecker(const char *sat, int debug)
+@@ -325,26 +326,26 @@ bool SatChecker::operator()() throw (Sat
+ debug_parser_indent = 0;
+
+ try {
+- Picosat::picosat_init();
++ picosat_inst = Picosat::picosat_init();
+ // try to enable as many features as possible
+- Picosat::picosat_set_global_default_phase(1);
++ Picosat::picosat_set_global_default_phase(picosat_inst, 1);
+
+ fillSatChecker(_sat);
+
+- int res = Picosat::picosat_sat(-1);
++ int res = Picosat::picosat_sat(picosat_inst, -1);
+
+ if (res == PICOSAT_SATISFIABLE) {
+ /* Let's get the assigment out of picosat, because we have to
+ reset the sat solver afterwards */
+ std::map<std::string, int>::const_iterator it;
+ for (it = symbolTable.begin(); it != symbolTable.end(); ++it) {
+- bool selected = Picosat::picosat_deref(it->second) == 1;
++ bool selected = Picosat::picosat_deref(picosat_inst, it->second) == 1;
+ assignmentTable.insert(std::make_pair(it->first, selected));
+ }
+ }
+
+- Picosat::picosat_reset();
+-
++ Picosat::picosat_reset(picosat_inst);
++ picosat_inst = NULL;
+
+ if (res == PICOSAT_UNSATISFIABLE)
+ return false;
diff --git a/undertaker.spec b/undertaker.spec
index 5b2c34f..80e51f4 100644
--- a/undertaker.spec
+++ b/undertaker.spec
@@ -1,6 +1,6 @@
Name: undertaker
Version: 1.2
-Release: 10%{?dist}
+Release: 11%{?dist}
Summary: Find always-on and always-off conditional C code
Group: Development/Languages
@@ -8,7 +8,9 @@ License: GPLv2 and GPLv3+
URL: http://vamos.informatik.uni-erlangen.de/trac/undertaker
Source0: http://vamos.informatik.uni-erlangen.de/files/%{name}-%{version}.tar.gz
# As of F20, Boost doesn't ship -mt DSO's anymore.
-Patch0: undertaker-boost_mt.patch
+Patch0: %{name}-boost_mt.patch
+# Adapt to new picosat API
+Patch1: %{name}-picosat.patch
BuildRequires: boost-devel
BuildRequires: emacs
@@ -70,10 +72,8 @@ Source Elisp code for XEmacs support for %{name}.
%prep
%setup -q -n vamos-%{version}
-%patch0 -p1
-
-# Fix up one include path
-sed -i 's|picosat/picosat.h|picosat.h|' undertaker/SatChecker.h
+%patch0
+%patch1
# Fix a python path
sed -i "s|^PYTHONPATH=.*|PYTHONPATH=\""%{python2_sitelib}"\"|" \
@@ -162,6 +162,9 @@ cd $RPM_BUILD_ROOT%{_emacs_sitelispdir}/%{name}
%{_xemacs_sitelispdir}/%{name}/*.el
%changelog
+* Wed Jul 31 2013 Jerry James <loganjerry(a)gmail.com> - 1.2-11
+- Add -picosat patch to adapt to new reentrant picosat API
+
* Sat Jul 27 2013 Petr Machata <pmachata(a)redhat.com> - 1.2-10
- Rebuild for boost 1.54.0
- Boost.Wave and Boost.System DSO's do not include -mt suffix anymore
@@ -187,7 +190,7 @@ cd $RPM_BUILD_ROOT%{_emacs_sitelispdir}/%{name}
- Drop unnecessary BRs
- Ensure correct LDFLAGS
-* Mon Jan 6 2012 Jerry James <loganjerry(a)gmail.com> - 1.2-3
+* Mon Jan 9 2012 Jerry James <loganjerry(a)gmail.com> - 1.2-3
- Rebuild for GCC 4.7
* Sun Nov 20 2011 Jerry James <loganjerry(a)gmail.com> - 1.2-2
9Â years, 6Â months
[csisat] Rebuild for new glpk and new picosat.
by Jerry James
commit 1232bbad68a899de4a45365987e8673a540de171
Author: Jerry James <jamesjer(a)betterlinux.com>
Date: Wed Jul 31 16:50:07 2013 -0600
Rebuild for new glpk and new picosat.
csisat-glpk.patch | 469 ++++++++++++++++++++++++++++++++++++++++++++++++++
csisat-picosat.patch | 127 ++++++++++++++
csisat.spec | 17 ++-
3 files changed, 611 insertions(+), 2 deletions(-)
---
diff --git a/csisat-glpk.patch b/csisat-glpk.patch
new file mode 100644
index 0000000..5e3f617
--- /dev/null
+++ b/csisat-glpk.patch
@@ -0,0 +1,469 @@
+--- ./glpk_ml_wrapper/src/camlglpk.c.orig 2008-07-08 22:38:04.000000000 -0600
++++ ./glpk_ml_wrapper/src/camlglpk.c 2013-07-31 15:57:11.000000000 -0600
+@@ -60,14 +60,14 @@ void to_std_out()
+ value lp_create(value unit)
+ {
+ CAMLparam1(unit);
+- LPX* lp = lpx_create_prob();
++ glp_prob* lp = glp_create_prob();
+ CAMLreturn ((value)lp);
+ }
+
+ value lp_delete(value lp)
+ {
+ CAMLparam1(lp);
+- lpx_delete_prob((LPX*)lp);
++ glp_delete_prob((glp_prob*)lp);
+ CAMLreturn (Val_unit);
+ }
+
+@@ -75,105 +75,105 @@ value lp_delete(value lp)
+ value lp_set_maximize(value lp)
+ {
+ CAMLparam1(lp);
+- lpx_set_obj_dir((LPX*)lp, LPX_MAX);
++ glp_set_obj_dir((glp_prob*)lp, GLP_MAX);
+ CAMLreturn (Val_unit);
+ }
+
+ value lp_set_minimize(value lp)
+ {
+ CAMLparam1(lp);
+- lpx_set_obj_dir((LPX*)lp, LPX_MIN);
++ glp_set_obj_dir((glp_prob*)lp, GLP_MIN);
+ CAMLreturn (Val_unit);
+ }
+
+ value lp_add_row(value lp, value i)
+ {
+ CAMLparam2(lp,i);
+- lpx_add_rows((LPX*)lp, Int_val(i));
++ glp_add_rows((glp_prob*)lp, Int_val(i));
+ CAMLreturn (Val_unit);
+ }
+
+ value lp_add_col(value lp, value i)
+ {
+ CAMLparam2(lp,i);
+- lpx_add_cols((LPX*)lp, Int_val(i));
++ glp_add_cols((glp_prob*)lp, Int_val(i));
+ CAMLreturn (Val_unit);
+ }
+
+ value lp_set_row_bnd_free(value lp, value i)
+ {
+ CAMLparam2(lp,i);
+- lpx_set_row_bnds((LPX*)lp, Int_val(i) + 1, LPX_FR, 0.0, 0.0 );
++ glp_set_row_bnds((glp_prob*)lp, Int_val(i) + 1, GLP_FR, 0.0, 0.0 );
+ CAMLreturn (Val_unit);
+ }
+
+ value lp_set_row_bnd_lower(value lp, value i, value lo)
+ {
+ CAMLparam3(lp,i,lo);
+- lpx_set_row_bnds((LPX*)lp, Int_val(i) + 1, LPX_LO, Double_val(lo), 0.0 );
++ glp_set_row_bnds((glp_prob*)lp, Int_val(i) + 1, GLP_LO, Double_val(lo), 0.0 );
+ CAMLreturn (Val_unit);
+ }
+
+ value lp_set_row_bnd_upper(value lp, value i, value up)
+ {
+ CAMLparam3(lp,i,up);
+- lpx_set_row_bnds((LPX*)lp, Int_val(i) + 1, LPX_UP, 0.0, Double_val(up) );
++ glp_set_row_bnds((glp_prob*)lp, Int_val(i) + 1, GLP_UP, 0.0, Double_val(up) );
+ CAMLreturn (Val_unit);
+ }
+
+ value lp_set_row_bnd_double(value lp, value i, value lo, value up)
+ {
+ CAMLparam4(lp,i,lo,up);
+- lpx_set_row_bnds((LPX*)lp, Int_val(i) + 1, LPX_DB, Double_val(lo), Double_val(up) );
++ glp_set_row_bnds((glp_prob*)lp, Int_val(i) + 1, GLP_DB, Double_val(lo), Double_val(up) );
+ CAMLreturn (Val_unit);
+ }
+
+ value lp_set_row_bnd_fixed(value lp, value i, value x)
+ {
+ CAMLparam3(lp,i,x);
+- lpx_set_row_bnds((LPX*)lp, Int_val(i) + 1, LPX_FX, Double_val(x), Double_val(x) );
++ glp_set_row_bnds((glp_prob*)lp, Int_val(i) + 1, GLP_FX, Double_val(x), Double_val(x) );
+ CAMLreturn (Val_unit);
+ }
+
+ value lp_set_col_bnd_free(value lp, value i)
+ {
+ CAMLparam2(lp,i);
+- lpx_set_col_bnds((LPX*)lp, Int_val(i) + 1, LPX_FR, 0.0, 0.0 );
++ glp_set_col_bnds((glp_prob*)lp, Int_val(i) + 1, GLP_FR, 0.0, 0.0 );
+ CAMLreturn (Val_unit);
+ }
+
+ value lp_set_col_bnd_lower(value lp, value i, value lo)
+ {
+ CAMLparam3(lp,i,lo);
+- lpx_set_col_bnds((LPX*)lp, Int_val(i) + 1, LPX_LO, Double_val(lo), 0.0 );
++ glp_set_col_bnds((glp_prob*)lp, Int_val(i) + 1, GLP_LO, Double_val(lo), 0.0 );
+ CAMLreturn (Val_unit);
+ }
+
+ value lp_set_col_bnd_upper(value lp, value i, value up)
+ {
+ CAMLparam3(lp,i,up);
+- lpx_set_col_bnds((LPX*)lp, Int_val(i) + 1, LPX_UP, 0.0, Double_val(up) );
++ glp_set_col_bnds((glp_prob*)lp, Int_val(i) + 1, GLP_UP, 0.0, Double_val(up) );
+ CAMLreturn (Val_unit);
+ }
+
+ value lp_set_col_bnd_double(value lp, value i, value lo, value up)
+ {
+ CAMLparam4(lp,i,lo,up);
+- lpx_set_col_bnds((LPX*)lp, Int_val(i) + 1, LPX_DB, Double_val(lo), Double_val(up) );
++ glp_set_col_bnds((glp_prob*)lp, Int_val(i) + 1, GLP_DB, Double_val(lo), Double_val(up) );
+ CAMLreturn (Val_unit);
+ }
+
+ value lp_set_col_bnd_fixed(value lp, value i, value x)
+ {
+ CAMLparam3(lp,i,x);
+- lpx_set_col_bnds((LPX*)lp, Int_val(i) + 1, LPX_FX, Double_val(x), Double_val(x) );
++ glp_set_col_bnds((glp_prob*)lp, Int_val(i) + 1, GLP_FX, Double_val(x), Double_val(x) );
+ CAMLreturn (Val_unit);
+ }
+
+ value lp_set_obj_coef(value lp, value i, value coeff)
+ {
+ CAMLparam3(lp,i,coeff);
+- lpx_set_obj_coef((LPX*)lp, Int_val(i) + 1, Double_val(coeff));
++ glp_set_obj_coef((glp_prob*)lp, Int_val(i) + 1, Double_val(coeff));
+ CAMLreturn (Val_unit);
+ }
+
+@@ -194,7 +194,7 @@ value lp_set_mat_row(value lp, value i,
+ }
+ }
+ if(non_zero > 0){
+- lpx_set_mat_row((LPX*)lp, Int_val(i) + 1, non_zero, indexes, val);
++ glp_set_mat_row((glp_prob*)lp, Int_val(i) + 1, non_zero, indexes, val);
+ }
+ free(indexes);
+ free(val);
+@@ -218,7 +218,7 @@ value lp_set_mat_col(value lp, value i,
+ }
+ }
+ if(non_zero > 0){
+- lpx_set_mat_col((LPX*)lp, Int_val(i) + 1, non_zero, indexes, val);
++ glp_set_mat_col((glp_prob*)lp, Int_val(i) + 1, non_zero, indexes, val);
+ }
+ free(indexes);
+ free(val);
+@@ -229,32 +229,30 @@ value lp_set_mat_col(value lp, value i,
+ value lp_simplex(value lp, value presolve)
+ {
+ CAMLparam2(lp,presolve);
+- if(Bool_val(presolve)){
+- lpx_set_int_parm((LPX*)lp, LPX_K_PRESOL, 1);
+- }else{
+- lpx_set_int_parm((LPX*)lp, LPX_K_PRESOL, 0);
+- }
++ glp_smcp params;
++ glp_init_smcp(¶ms);
++ params.presolve = (Bool_val(presolve)) ? GLP_ON : GLP_OFF;
+ to_dev_null();
+- int status = lpx_simplex((LPX*)lp);
++ int status = glp_simplex((glp_prob*)lp, ¶ms);
+ to_std_out();
+ value val = Val_false;
+- if(status == LPX_E_OK){
++ if(status == 0){
+ val = Val_true;
+- }else if (status == LPX_E_FAULT){
++ }else if (status == GLP_EBADB || status == GLP_ECOND || status == GLP_EBOUND){
+ //fprintf(stderr, "solving failed \n");
+- }else if (status == LPX_E_OBJLL){
++ }else if (status == GLP_EOBJLL){
+ //fprintf(stderr, "unbounded (lower)\n");
+- }else if (status == LPX_E_OBJUL){
++ }else if (status == GLP_EOBJUL){
+ //fprintf(stderr, "unbounded (upper)\n");
+- }else if (status == LPX_E_ITLIM){
++ }else if (status == GLP_EITLIM){
+ //fprintf(stderr, "iteration limit reached\n");
+- }else if (status == LPX_E_TMLIM){
++ }else if (status == GLP_ETMLIM){
+ //fprintf(stderr, "time limit reached\n");
+- }else if (status == LPX_E_SING){
++ }else if (status == GLP_ESING){
+ fprintf(stderr, "singular or ill-conditionned matrix\n");
+- }else if (status == LPX_E_NOPFS){
++ }else if (status == GLP_ENOPFS){
+ //fprintf(stderr, "no primal solution\n");
+- }else if (status == LPX_E_NODFS){
++ }else if (status == GLP_ENODFS){
+ //fprintf(stderr, "no dual solution\n");
+ }else{
+ fprintf(stderr, "unknown status: %d\n", status);
+@@ -265,28 +263,30 @@ value lp_simplex(value lp, value presolv
+ value lp_simplex_exact(value lp)
+ {
+ CAMLparam1(lp);
++ glp_smcp params;
++ glp_init_smcp(¶ms);
+ to_dev_null();
+- lpx_simplex((LPX*)lp);
+- int status = lpx_exact((LPX*)lp);
++ glp_simplex((glp_prob*)lp, ¶ms);
++ int status = glp_exact((glp_prob*)lp, ¶ms);
+ to_std_out();
+ value val = Val_false;
+- if(status == LPX_E_OK){
++ if(status == 0){
+ val = Val_true;
+- }else if (status == LPX_E_FAULT){
++ }else if (status == GLP_EBADB || status == GLP_ECOND || status == GLP_EBOUND){
+ //fprintf(stderr, "solving failed \n");
+- }else if (status == LPX_E_OBJLL){
++ }else if (status == GLP_EOBJLL){
+ //fprintf(stderr, "unbounded (lower)\n");
+- }else if (status == LPX_E_OBJUL){
++ }else if (status == GLP_EOBJUL){
+ //fprintf(stderr, "unbounded (upper)\n");
+- }else if (status == LPX_E_ITLIM){
++ }else if (status == GLP_EITLIM){
+ //fprintf(stderr, "iteration limit reached\n");
+- }else if (status == LPX_E_TMLIM){
++ }else if (status == GLP_ETMLIM){
+ //fprintf(stderr, "time limit reached\n");
+- }else if (status == LPX_E_SING){
++ }else if (status == GLP_ESING){
+ fprintf(stderr, "singular or ill-conditionned matrix\n");
+- }else if (status == LPX_E_NOPFS){
++ }else if (status == GLP_ENOPFS){
+ //fprintf(stderr, "no primal solution\n");
+- }else if (status == LPX_E_NODFS){
++ }else if (status == GLP_ENODFS){
+ //fprintf(stderr, "no dual solution\n");
+ }else{
+ fprintf(stderr, "unknown status: %d\n", status);
+@@ -296,7 +296,7 @@ value lp_simplex_exact(value lp)
+ value lp_get_stat(value lp)
+ {
+ CAMLparam1(lp);
+- int status = lpx_get_status((LPX*)lp);
++ int status = glp_get_status((glp_prob*)lp);
+ CAMLreturn (Val_int(status));
+ }
+
+@@ -304,21 +304,21 @@ value lp_get_stat(value lp)
+ value lp_get_obj_val(value lp)
+ {
+ CAMLparam1(lp);
+- double status = lpx_get_obj_val((LPX*)lp);
++ double status = glp_get_obj_val((glp_prob*)lp);
+ CAMLreturn (caml_copy_double(status));
+ }
+
+ value lp_get_row_stat(value lp, value i)
+ {
+ CAMLparam2(lp,i);
+- int status = lpx_get_row_stat((LPX*)lp, Int_val(i) + 1);
++ int status = glp_get_row_stat((glp_prob*)lp, Int_val(i) + 1);
+ CAMLreturn (Val_int(status));
+ }
+
+ value lp_get_row_primal(value lp, value i)
+ {
+ CAMLparam2(lp,i);
+- double val = lpx_get_row_prim((LPX*)lp, Int_val(i) + 1);
++ double val = glp_get_row_prim((glp_prob*)lp, Int_val(i) + 1);
+ CAMLreturn (caml_copy_double(val));
+ }
+
+@@ -327,7 +327,7 @@ value lp_get_rows_primal(value lp, value
+ CAMLparam3(lp,length,array);
+ int i;
+ for(i = 0; i < Int_val(length); ++i){
+- double val = lpx_get_row_prim((LPX*)lp, i + 1);
++ double val = glp_get_row_prim((glp_prob*)lp, i + 1);
+ Store_double_field(array, i, val);
+ }
+ CAMLreturn (Val_unit);
+@@ -337,7 +337,7 @@ value lp_get_rows_primal(value lp, value
+ value lp_get_row_dual(value lp, value i)
+ {
+ CAMLparam2(lp,i);
+- double val = lpx_get_row_dual((LPX*)lp, Int_val(i) + 1);
++ double val = glp_get_row_dual((glp_prob*)lp, Int_val(i) + 1);
+ CAMLreturn (caml_copy_double(val));
+ }
+
+@@ -346,7 +346,7 @@ value lp_get_rows_dual(value lp, value l
+ CAMLparam3(lp,length,array);
+ int i;
+ for(i = 0; i < Int_val(length); ++i){
+- double val = lpx_get_row_dual((LPX*)lp, i + 1);
++ double val = glp_get_row_dual((glp_prob*)lp, i + 1);
+ Store_double_field(array, i, val);
+ }
+ CAMLreturn (Val_unit);
+@@ -355,14 +355,14 @@ value lp_get_rows_dual(value lp, value l
+ value lp_get_col_stat(value lp, value i)
+ {
+ CAMLparam2(lp,i);
+- int status = lpx_get_col_stat((LPX*)lp, Int_val(i) + 1);
++ int status = glp_get_col_stat((glp_prob*)lp, Int_val(i) + 1);
+ CAMLreturn (Val_int(status));
+ }
+
+ value lp_get_col_primal(value lp, value i)
+ {
+ CAMLparam2(lp,i);
+- double val = lpx_get_col_prim((LPX*)lp, Int_val(i) + 1);
++ double val = glp_get_col_prim((glp_prob*)lp, Int_val(i) + 1);
+ CAMLreturn (caml_copy_double(val));
+ }
+
+@@ -371,7 +371,7 @@ value lp_get_cols_primal(value lp, value
+ CAMLparam3(lp,length,array);
+ int i;
+ for(i = 0; i < Int_val(length); ++i){
+- double val = lpx_get_col_prim((LPX*)lp, i + 1);
++ double val = glp_get_col_prim((glp_prob*)lp, i + 1);
+ Store_double_field(array, i, val);
+ }
+ CAMLreturn (Val_unit);
+@@ -380,7 +380,7 @@ value lp_get_cols_primal(value lp, value
+ value lp_get_col_dual(value lp, value i)
+ {
+ CAMLparam2(lp,i);
+- double val = lpx_get_col_dual((LPX*)lp, Int_val(i) + 1);
++ double val = glp_get_col_dual((glp_prob*)lp, Int_val(i) + 1);
+ CAMLreturn (caml_copy_double(val));
+ }
+
+@@ -389,7 +389,7 @@ value lp_get_cols_dual(value lp, value l
+ CAMLparam3(lp,length,array);
+ int i;
+ for(i = 0; i < Int_val(length); ++i){
+- double val = lpx_get_col_dual((LPX*)lp, i + 1);
++ double val = glp_get_col_dual((glp_prob*)lp, i + 1);
+ Store_double_field(array, i, val);
+ }
+ CAMLreturn (Val_unit);
+@@ -399,20 +399,20 @@ value lp_interior(value lp)
+ {
+ CAMLparam1(lp);
+ to_dev_null();
+- int status = lpx_interior((LPX*)lp);
++ int status = glp_interior((glp_prob*)lp, NULL);
+ to_std_out();
+ value val = Val_false;
+- if(status == LPX_E_OK){
++ if(status == 0){
+ val = Val_true;
+- }else if (status == LPX_E_FAULT){
++ }else if (status == GLP_EFAIL){
+ //fprintf(stderr, "solving failed \n");
+- }else if (status == LPX_E_NOFEAS){
++ }else if (status == GLP_ENOFEAS){
+ //fprintf(stderr, "unfeasible system\n");
+- }else if (status == LPX_E_NOCONV){
++ }else if (status == GLP_ENOCVG){
+ fprintf(stderr, "slow convergence (or diverge)\n");
+- }else if (status == LPX_E_ITLIM){
++ }else if (status == GLP_EITLIM){
+ fprintf(stderr, "iteration limit reached\n");
+- }else if (status == LPX_E_INSTAB){
++ }else if (status == GLP_EINSTAB){
+ fprintf(stderr, "numerical instability\n");
+ }else{
+ fprintf(stderr, "unknown status: %d\n", status);
+@@ -423,14 +423,14 @@ value lp_interior(value lp)
+ value lp_ipt_obj_val(value lp)
+ {
+ CAMLparam1(lp);
+- double status = lpx_ipt_obj_val((LPX*)lp);
++ double status = glp_ipt_obj_val((glp_prob*)lp);
+ CAMLreturn (caml_copy_double(status));
+ }
+
+ value lp_ipt_row_primal(value lp, value i)
+ {
+ CAMLparam2(lp,i);
+- double val = lpx_ipt_row_prim((LPX*)lp, Int_val(i) + 1);
++ double val = glp_ipt_row_prim((glp_prob*)lp, Int_val(i) + 1);
+ CAMLreturn (caml_copy_double(val));
+ }
+
+@@ -439,7 +439,7 @@ value lp_ipt_rows_primal(value lp, value
+ CAMLparam3(lp,length,array);
+ int i;
+ for(i = 0; i < Int_val(length); ++i){
+- double val = lpx_ipt_row_prim((LPX*)lp, i + 1);
++ double val = glp_ipt_row_prim((glp_prob*)lp, i + 1);
+ Store_double_field(array, i, val);
+ }
+ CAMLreturn (Val_unit);
+@@ -448,7 +448,7 @@ value lp_ipt_rows_primal(value lp, value
+ value lp_ipt_row_dual(value lp, value i)
+ {
+ CAMLparam2(lp,i);
+- double val = lpx_ipt_row_dual((LPX*)lp, Int_val(i) + 1);
++ double val = glp_ipt_row_dual((glp_prob*)lp, Int_val(i) + 1);
+ CAMLreturn (caml_copy_double(val));
+ }
+
+@@ -457,7 +457,7 @@ value lp_ipt_rows_dual(value lp, value l
+ CAMLparam3(lp,length,array);
+ int i;
+ for(i = 0; i < Int_val(length); ++i){
+- double val = lpx_ipt_row_dual((LPX*)lp, i + 1);
++ double val = glp_ipt_row_dual((glp_prob*)lp, i + 1);
+ Store_double_field(array, i, val);
+ }
+ CAMLreturn (Val_unit);
+@@ -466,7 +466,7 @@ value lp_ipt_rows_dual(value lp, value l
+ value lp_ipt_col_primal(value lp, value i)
+ {
+ CAMLparam2(lp,i);
+- double val = lpx_ipt_col_prim((LPX*)lp, Int_val(i) + 1);
++ double val = glp_ipt_col_prim((glp_prob*)lp, Int_val(i) + 1);
+ CAMLreturn (caml_copy_double(val));
+ }
+
+@@ -475,7 +475,7 @@ value lp_ipt_cols_primal(value lp, value
+ CAMLparam3(lp,length,array);
+ int i;
+ for(i = 0; i < Int_val(length); ++i){
+- double val = lpx_ipt_col_prim((LPX*)lp, i + 1);
++ double val = glp_ipt_col_prim((glp_prob*)lp, i + 1);
+ Store_double_field(array, i, val);
+ }
+ CAMLreturn (Val_unit);
+@@ -484,7 +484,7 @@ value lp_ipt_cols_primal(value lp, value
+ value lp_ipt_col_dual(value lp, value i)
+ {
+ CAMLparam2(lp,i);
+- double val = lpx_ipt_col_dual((LPX*)lp, Int_val(i) + 1);
++ double val = glp_ipt_col_dual((glp_prob*)lp, Int_val(i) + 1);
+ CAMLreturn (caml_copy_double(val));
+ }
+
+@@ -493,7 +493,7 @@ value lp_ipt_cols_dual(value lp, value l
+ CAMLparam3(lp,length,array);
+ int i;
+ for(i = 0; i < Int_val(length); ++i){
+- double val = lpx_ipt_col_dual((LPX*)lp, i + 1);
++ double val = glp_ipt_col_dual((glp_prob*)lp, i + 1);
+ Store_double_field(array, i, val);
+ }
+ CAMLreturn (Val_unit);
+@@ -502,7 +502,7 @@ value lp_ipt_cols_dual(value lp, value l
+ value lp_dump_problem(value lp)
+ {
+ CAMLparam1(lp);
+- lpx_print_prob((LPX*)lp, "lp_error.debug");
+- lpx_write_cpxlp((LPX*)lp, "cpxlp_error.debug");
++ glp_write_lp((glp_prob*)lp, NULL, "lp_error.debug");
++ glp_write_lp((glp_prob*)lp, NULL, "cpxlp_error.debug");
+ CAMLreturn (Val_unit);
+ }
diff --git a/csisat-picosat.patch b/csisat-picosat.patch
new file mode 100644
index 0000000..1bfa6b0
--- /dev/null
+++ b/csisat-picosat.patch
@@ -0,0 +1,127 @@
+--- ./pico_ml_wrapper/src/camlpico.c.orig 2008-07-08 22:38:01.000000000 -0600
++++ ./pico_ml_wrapper/src/camlpico.c 2013-07-31 16:11:40.000000000 -0600
+@@ -26,6 +26,8 @@
+ #include <caml/memory.h>
+ #include <picosat.h>
+
++static PicoSAT *my_picosat;
++
+ /* the methods comment were directly taken from 'picosat.h' */
+
+ CAMLprim value unknown(){ return Val_int(PICOSAT_UNKNOWN);}
+@@ -35,13 +37,14 @@ CAMLprim value unsatisfiable(){ return V
+
+ CAMLprim value init(value unit)
+ {
+- picosat_init();
++ my_picosat = picosat_init();
+ return Val_unit;
+ }
+
+ CAMLprim value reset(value unit)
+ {
+- picosat_reset();
++ picosat_reset(my_picosat);
++ my_picosat = NULL;
+ return Val_unit;
+ }
+
+@@ -55,7 +58,7 @@ CAMLprim value reset(value unit)
+ */
+ CAMLprim value set_seed(value seed)
+ {
+- picosat_set_seed(Unsigned_int_val(seed));
++ picosat_set_seed(my_picosat, Unsigned_int_val(seed));
+ return Val_unit;
+ }
+
+@@ -65,7 +68,7 @@ CAMLprim value set_seed(value seed)
+ */
+ CAMLprim value enable_trace(value unit)
+ {
+- picosat_enable_trace_generation();
++ picosat_enable_trace_generation(my_picosat);
+ return Val_unit;
+ }
+
+@@ -76,7 +79,7 @@ CAMLprim value enable_trace(value unit)
+ */
+ CAMLprim value adjust(value n)
+ {
+- picosat_adjust(Int_val(n));
++ picosat_adjust(my_picosat, Int_val(n));
+ return Val_unit;
+ }
+
+@@ -85,7 +88,7 @@ CAMLprim value adjust(value n)
+ */
+ CAMLprim value second(value unit)
+ {
+- return caml_copy_double(picosat_seconds());
++ return caml_copy_double(picosat_seconds(my_picosat));
+ }
+
+ /*------------------------------------------------------------------------*/
+@@ -95,7 +98,7 @@ CAMLprim value second(value unit)
+ */
+ CAMLprim value add(value i)
+ {
+- picosat_add(Int_val(i));
++ picosat_add(my_picosat, Int_val(i));
+ return Val_unit;
+ }
+
+@@ -106,7 +109,7 @@ CAMLprim value add(value i)
+ */
+ CAMLprim value assume(value i)
+ {
+- picosat_assume(Int_val(i));
++ picosat_assume(my_picosat, Int_val(i));
+ return Val_unit;
+ }
+
+@@ -117,7 +120,7 @@ CAMLprim value assume(value i)
+ */
+ CAMLprim value sat(value limit)
+ {
+- return Val_int(picosat_sat(Int_val(limit)));
++ return Val_int(picosat_sat(my_picosat, Int_val(limit)));
+ }
+
+ /* After 'picosat_sat' was called and returned 'PICOSAT_SATISFIABLE', then
+@@ -127,7 +130,7 @@ CAMLprim value sat(value limit)
+ */
+ CAMLprim value deref(value lit)
+ {
+- return Val_int(picosat_deref(Int_val(lit)));
++ return Val_int(picosat_deref(my_picosat, Int_val(lit)));
+ }
+
+ /* A cheap way of determining an over-approximation of a variable core is to
+@@ -138,7 +141,7 @@ CAMLprim value deref(value lit)
+ */
+ CAMLprim value usedlit(value lit)
+ {
+- return Val_int(picosat_usedlit(Int_val(lit)));
++ return Val_int(picosat_usedlit(my_picosat, Int_val(lit)));
+ }
+
+ /*------------------------------------------------------------------------*/
+@@ -155,7 +158,7 @@ CAMLprim value usedlit(value lit)
+ */
+ CAMLprim value corelit(value lit)
+ {
+- return Val_int(picosat_corelit(Int_val(lit)));
++ return Val_int(picosat_corelit(my_picosat, Int_val(lit)));
+ }
+
+ //#include <stdio.h>
+@@ -165,7 +168,7 @@ value get_proof(value unit)
+ {
+ CAMLparam0();
+ CAMLlocal1 (array);
+- int* proof = picosat_get_proof();
++ int* proof = picosat_get_proof(my_picosat);
+ int size = 0;
+ while(proof[size] != EOP){
+ size++;
diff --git a/csisat.spec b/csisat.spec
index b3c896c..76fa4a1 100644
--- a/csisat.spec
+++ b/csisat.spec
@@ -1,6 +1,6 @@
Name: csisat
Version: 1.2
-Release: 11%{?dist}
+Release: 12%{?dist}
Summary: Tool for LA+EUF Interpolation
Group: Applications/Engineering
@@ -10,7 +10,11 @@ Source0: http://csisat.googlecode.com/files/%{name}-%{version}.zip
# This patch has not been sent upstream. Upstream wishes to distribute the
# picosat sources with their code. This patch builds with the system picosat
# instead, and also adds missing dependencies so that parallel make works.
-Patch0: csisat-makefile.patch
+Patch0: %{name}-makefile.patch
+# Adapt to new glpk API
+Patch1: %{name}-glpk.patch
+# Adapt to new picosat API
+Patch2: %{name}-picosat.patch
BuildRequires: glpk-devel, ocaml, picosat-devel, subversion
@@ -32,10 +36,16 @@ efficiency of a SAT solver to reason about the boolean structure.
%prep
%setup -q
%patch0
+%patch1
+%patch2
# Make sure we don't use the bundled version of picosat
rm -fr picosat-*
+# We need the picosat version with trace enabled
+sed -i 's/lpicosat/lpicosat-trace/' \
+ Makefile pico_ml_wrapper/Makefile pico_ml_wrapper/compile.sh
+
# Get rid of inappropriate executable bits
chmod a-x *.txt
find . -name \*.c | xargs chmod a-x
@@ -54,6 +64,9 @@ cp -p bin/* $RPM_BUILD_ROOT%{_bindir}
%{_bindir}/csisatServer
%changelog
+* Wed Jul 31 2013 Jerry James <loganjerry(a)gmail.com> - 1.2-12
+- Rebuild for new glpk and new picosat
+
* Sat Feb 2 2013 Jerry James <loganjerry(a)gmail.com> - 1.2-11
- Rebuild for new glpk
9Â years, 6Â months
[picosat] New upstream release. Remove comment that was being pulled into postun.
by Jerry James
commit 4d9d514952450eb08a3f48a5927359b75182cebb
Author: Jerry James <jamesjer(a)betterlinux.com>
Date: Wed Jul 31 16:49:06 2013 -0600
New upstream release.
Remove comment that was being pulled into postun.
.gitignore | 2 +-
picosat-alias.patch | 24 +++++++++--------
picosat-proof-access.patch | 59 ++++++++++++++++++++++---------------------
picosat-trace.patch | 24 +++++++++---------
picosat.spec | 11 ++++---
sources | 2 +-
6 files changed, 63 insertions(+), 59 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index a08d939..3757868 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1 @@
-/picosat-951.tar.gz
+/picosat-957.tar.gz
diff --git a/picosat-alias.patch b/picosat-alias.patch
index 271b754..bea34a9 100644
--- a/picosat-alias.patch
+++ b/picosat-alias.patch
@@ -1,37 +1,39 @@
---- ./picosat.c.orig 2012-08-20 14:56:30.236102928 -0600
-+++ ./picosat.c 2012-08-20 15:02:03.774695361 -0600
-@@ -1283,8 +1283,10 @@ new_clause (unsigned size, unsigned lear
+--- ./picosat.c.orig 2013-07-31 14:41:10.000000000 -0600
++++ ./picosat.c 2013-07-31 14:48:29.000000000 -0600
+@@ -1321,8 +1321,10 @@ new_clause (PS * ps, unsigned size, unsi
res->collected = 0;
#endif
- if (learned && size > 2)
-- *CLS2ACT (res) = cinc;
+- *CLS2ACT (res) = ps->cinc;
+ if (learned && size > 2) {
+ Act *act = CLS2ACT (res);
-+ *act = cinc;
++ *act = ps->cinc;
+ }
return res;
}
-@@ -5504,14 +5506,17 @@ iteration (void)
+@@ -5611,8 +5613,8 @@ iteration (PS * ps)
static int
- cmp_activity (Cls * c, Cls * d)
+ cmp_glue_activity_size (PS * ps, Cls * c, Cls * d)
{
- Act a;
- Act b;
+ Act a, *aptr;
+ Act b, *bptr;
- assert (c->learned);
- assert (d->learned);
+ (void) ps;
+
+@@ -5625,8 +5627,10 @@ cmp_glue_activity_size (PS * ps, Cls * c
+ if (c->glue > d->glue)
+ return -1;
- a = *CLS2ACT (c);
- b = *CLS2ACT (d);
+ aptr = CLS2ACT (c);
+ bptr = CLS2ACT (d);
-+
+ a = *aptr;
+ b = *bptr;
- if (a < b)
+ if (a < b) // then higher activity
return -1;
diff --git a/picosat-proof-access.patch b/picosat-proof-access.patch
index 0bdc039..ec04dc0 100644
--- a/picosat-proof-access.patch
+++ b/picosat-proof-access.patch
@@ -1,7 +1,7 @@
---- ./picosat.c.orig 2012-08-20 14:53:10.101697229 -0600
-+++ ./picosat.c 2012-08-20 14:55:28.099997470 -0600
-@@ -6362,6 +6362,168 @@ write_trace (FILE * file, int fmt)
- #endif
+--- ./picosat.c.orig 2013-07-31 14:26:09.000000000 -0600
++++ ./picosat.c 2013-07-31 14:41:10.000000000 -0600
+@@ -6383,6 +6383,168 @@ trace_zhain (PS * ps, unsigned idx, Zhn
+ fputs (" 0\n", file);
}
+/**
@@ -25,13 +25,13 @@
+}
+
+static int
-+my_write_idx (unsigned idx)
++my_write_idx (PS * ps, unsigned idx)
+{
+ return EXPORTIDX (idx);
+}
+
+static void
-+my_trace_lits (Cls * cls)
++my_trace_lits (PS * ps, Cls * cls)
+{
+ Lit **p, **eol = end_of_lits (cls);
+
@@ -48,7 +48,7 @@
+}
+
+static void
-+my_trace_zhain (unsigned idx, Zhn * zhain)
++my_trace_zhain (PS * ps, unsigned idx, Zhn * zhain)
+{
+ unsigned prev, this, delta, i;
+ Znt *p, byte;
@@ -57,12 +57,12 @@
+ assert (zhain);
+ assert (zhain->core);
+
-+ int id = my_write_idx (idx);
++ int id = my_write_idx (ps, idx);
+ add_int_to_proof(id);
+
+ cls = IDX2CLS (idx);
+ assert (cls);
-+ my_trace_lits (cls);
++ my_trace_lits (ps, cls);
+
+ i = 0;
+ delta = 0;
@@ -78,7 +78,7 @@
+
+ this = prev + delta;
+
-+ id = my_write_idx (this);
++ id = my_write_idx (ps, this);
+ add_int_to_proof(id);
+
+ prev = this;
@@ -90,23 +90,23 @@
+}
+
+static void
-+my_trace_clause (unsigned idx, Cls * cls)
++my_trace_clause (PS * ps, unsigned idx, Cls * cls)
+{
+ assert (cls);
+ assert (cls->core);
+ assert (!cls->learned);
+ assert (CLS2IDX (cls) == idx);
+
-+ add_int_to_proof (my_write_idx (idx));
++ add_int_to_proof (my_write_idx (ps, idx));
+
-+ my_trace_lits (cls);
++ my_trace_lits (ps, cls);
+
+ add_int_to_proof(0);
+
+}
+
+static int*
-+get_proof ()
++get_proof (PS * ps)
+{
+ Cls *cls, ** p;
+ Zhn *zhain;
@@ -119,21 +119,21 @@
+ current_size = PROOF_BLOCK;
+ cursor = 0;
+
-+ core ();
++ core (ps);
+
+ for (p = SOC; p != EOC; p = NXC (p))
+ {
+ cls = *p;
+
-+ if (oclauses <= p && p < eoo)
++ if (ps->oclauses <= p && p < ps->eoo)
+ {
-+ i = OIDX2IDX (p - oclauses);
++ i = OIDX2IDX (p - ps->oclauses);
+ assert (!cls || CLS2IDX (cls) == i);
+ }
+ else
+ {
-+ assert (lclauses <= p && p < eol);
-+ i = LIDX2IDX (p - lclauses);
++ assert (ps->lclauses <= p && p < eol);
++ i = LIDX2IDX (p - ps->lclauses);
+ }
+
+ zhain = IDX2ZHN (i);
@@ -142,12 +142,12 @@
+ {
+ if (zhain->core)
+ {
-+ my_trace_zhain (i, zhain);
++ my_trace_zhain (ps, i, zhain);
+ }
+ }
+ else if (cls && cls->core)
+ {
-+ my_trace_clause (i, cls);
++ my_trace_clause (ps, i, cls);
+ }
+ }
+ add_int_to_proof(EOP);
@@ -157,30 +157,31 @@
+#endif
+
+int *
-+picosat_get_proof ()
++picosat_get_proof (PS * ps)
+{
+#ifdef TRACE
-+ return get_proof();
++ return get_proof(ps);
+#else
+ return NULL;
+#endif
+}
+
static void
- write_core_wrapper (FILE * file, int fmt)
+ write_core (PS * ps, FILE * file)
{
---- ./picosat.h.orig 2012-08-12 08:06:23.000000000 -0600
-+++ ./picosat.h 2012-08-20 14:55:28.116997497 -0600
-@@ -251,6 +251,12 @@ void picosat_simplify (void);
+--- ./picosat.h.orig 2013-06-01 07:35:00.000000000 -0600
++++ ./picosat.h 2013-07-31 14:44:24.000000000 -0600
+@@ -275,6 +275,13 @@ void picosat_simplify (PicoSAT *);
*/
- void picosat_adjust (int max_idx);
+ void picosat_adjust (PicoSAT *, int max_idx);
+/* Return an array of int where every cell is the next value of the proof in
+ * EXTENDED_TRACECHECK_TRACE_FMT format.
+ * The proof finishes by EOP.
+ */
+#define EOP ((int)(1 << 31)) /* 2^31 -1, max caml int32*/
-+int* picosat_get_proof();
++int* picosat_get_proof(PicoSAT *);
++
/*------------------------------------------------------------------------*/
/* Statistics.
*/
diff --git a/picosat-trace.patch b/picosat-trace.patch
index bdfaddb..80de5d7 100644
--- a/picosat-trace.patch
+++ b/picosat-trace.patch
@@ -1,5 +1,5 @@
---- ./makefile.in.orig 2012-08-12 08:06:23.000000000 -0600
-+++ ./makefile.in 2012-08-20 14:52:17.942652233 -0600
+--- ./makefile.in.orig 2013-06-01 07:35:00.000000000 -0600
++++ ./makefile.in 2013-07-31 14:26:09.000000000 -0600
@@ -12,16 +12,16 @@ clean:
analyze:
clang --analyze $(CFLAGS) *.c *.h
@@ -21,7 +21,7 @@
$(CC) $(CFLAGS) -o $@ picogcnf.o -L. -lpicosat
app.o: app.c picosat.h makefile
-@@ -37,10 +37,10 @@ main.o: main.c picosat.h makefile
+@@ -40,10 +40,10 @@ main.o: main.c picosat.h makefile
$(CC) $(CFLAGS) -c $<
picosat.o: picosat.c picosat.h makefile
@@ -34,7 +34,7 @@
config.h: makefile VERSION mkconfig # and actually picosat.c
rm -f $@; ./mkconfig > $@
-@@ -51,6 +51,6 @@ libpicosat.a: picosat.o version.o
+@@ -54,6 +54,6 @@ libpicosat.a: picosat.o version.o
SONAME=-Xlinker -soname -Xlinker libpicosat.so
libpicosat.so: picosat.o version.o
@@ -42,9 +42,9 @@
+ $(CC) $(CFLAGS) -fPIC -shared -o $@ picosat.o version.o $(SONAME)
.PHONY: all clean
---- ./picosat.c.orig 2012-08-12 08:06:23.000000000 -0600
-+++ ./picosat.c 2012-08-20 14:53:10.101697229 -0600
-@@ -6564,7 +6564,7 @@ check_trace_support_and_execute (FILE *
+--- ./picosat.c.orig 2013-06-01 07:35:00.000000000 -0600
++++ ./picosat.c 2013-07-31 14:26:09.000000000 -0600
+@@ -6673,7 +6673,7 @@ check_trace_support_and_execute (PS * ps
(void) file;
(void) fmt;
(void) f;
@@ -53,7 +53,7 @@
#endif
}
-@@ -7214,7 +7214,7 @@ picosat_corelit (int int_lit)
+@@ -7360,7 +7360,7 @@ picosat_corelit (PS * ps, int int_lit)
return res;
}
#else
@@ -62,7 +62,7 @@
return 0;
#endif
}
-@@ -7250,7 +7250,7 @@ picosat_coreclause (int ocls)
+@@ -7396,7 +7396,7 @@ picosat_coreclause (PS * ps, int ocls)
return res;
}
#else
@@ -71,9 +71,9 @@
return 0;
#endif
}
---- ./picomus.c.orig 2012-08-12 08:06:23.000000000 -0600
-+++ ./picomus.c 2012-08-20 14:54:41.645922533 -0600
-@@ -193,9 +193,8 @@ int main (int argc, char ** argv) {
+--- ./picomus.c.orig 2013-06-01 07:35:00.000000000 -0600
++++ ./picomus.c 2013-07-31 14:26:09.000000000 -0600
+@@ -195,9 +195,8 @@ int main (int argc, char ** argv) {
"\n"
"This typically slows down this MUS extractor, since\n"
"it only relies on clause selector variables and\n"
diff --git a/picosat.spec b/picosat.spec
index 3658461..efa8b72 100644
--- a/picosat.spec
+++ b/picosat.spec
@@ -1,6 +1,6 @@
Name: picosat
-Version: 951
-Release: 2%{?dist}
+Version: 957
+Release: 1%{?dist}
Summary: A SAT solver
Group: Applications/Engineering
@@ -107,9 +107,6 @@ cp -p %{SOURCE1} %{SOURCE2} %{SOURCE3} $RPM_BUILD_ROOT%{_mandir}/man1
%postun libs -p /sbin/ldconfig
-# The LICENSE file is placed in the -libs package rather than the base package,
-# because the -libs package is always installed when the base package is
-# installed, but not vice versa.
%files
%{_bindir}/pico*
%{_mandir}/man1/picosat*
@@ -126,6 +123,10 @@ cp -p %{SOURCE1} %{SOURCE2} %{SOURCE3} $RPM_BUILD_ROOT%{_mandir}/man1
%{_libdir}/libpicosat.so
%changelog
+* Wed Jul 31 2013 Jerry James <loganjerry(a)gmail.com> - 957-1
+- New upstream release
+- Remove comment that was being pulled into postun
+
* Thu Feb 14 2013 Fedora Release Engineering <rel-eng(a)lists.fedoraproject.org> - 951-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild
diff --git a/sources b/sources
index a1e0ad7..f06e750 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-eab092f83bcb083bce42e1a8873531b4 picosat-951.tar.gz
+6cb7d32a61b19e450961c689841aaccb picosat-957.tar.gz
9Â years, 6Â months
[pykde4] use %{_target_cpu}, it's shorter
by Rex Dieter
commit 4357acf7f536484c91ce3b8f6576c65768894177
Author: Rex Dieter <rdieter(a)math.unl.edu>
Date: Wed Jul 31 17:38:23 2013 -0500
use %{_target_cpu}, it's shorter
arm is FTBFS due to odd
CMake Error: : System Error: File name too long
pykde4.spec | 12 ++++++------
1 files changed, 6 insertions(+), 6 deletions(-)
---
diff --git a/pykde4.spec b/pykde4.spec
index 3a9e25b..b136300 100644
--- a/pykde4.spec
+++ b/pykde4.spec
@@ -167,8 +167,8 @@ Provides: python3-PyKDE4-devel%{?_isa} = %{version}-%{release}
%build
%if 0%{?python3}
-mkdir -p %{_target_platform}-python3
-pushd %{_target_platform}-python3
+mkdir -p %{_target_cpu}-python3
+pushd %{_target_cpu}-python3
%{cmake_kde4} \
-DPYTHON_EXECUTABLE:PATH=%{__python3} \
-DPYTHON_LIBRARY:PATH=%{_libdir}/libpython%{python3_version}%{?python3_abiflags}.so.1.0 \
@@ -178,8 +178,8 @@ make %{?_smp_mflags}
popd
%endif
-mkdir -p %{_target_platform}
-pushd %{_target_platform}
+mkdir -p %{_target_cpu}
+pushd %{_target_cpu}
%{cmake_kde4} \
-DPYKDEUIC4_ALTINSTALL:BOOL=ON \
-DPYTHON_EXECUTABLE:PATH=%{__python} \
@@ -192,7 +192,7 @@ popd
%install
%if 0%{?python3}
-make install/fast DESTDIR=%{buildroot} -C %{_target_platform}-python3
+make install/fast DESTDIR=%{buildroot} -C %{_target_cpu}-python3
# not python3 compat yet
rm -fv %{buildroot}%{_kde4_libdir}/kde4/kpythonpluginfactory.so
@@ -210,7 +210,7 @@ rm -fv %{buildroot}%{_kde4_appsdir}/pykde4/examples/*.py?
mv %{buildroot}%{_kde4_appsdir}/pykde4/examples/ %{buildroot}%{_docdir}/python3-pykde4/
%endif
-make install/fast DESTDIR=%{buildroot} -C %{_target_platform}
+make install/fast DESTDIR=%{buildroot} -C %{_target_cpu}
# HACK: fix multilib conflict, similar to PyQt4's http://bugzilla.redhat.com/509415
rm -fv %{buildroot}%{_bindir}/pykdeuic4{,-%{python_version}}
9Â years, 6Â months
[gdl] Disable failing tests on arm for now
by Orion Poplawski
commit cd7186d045225cdf78a76c00b5063d380a26462e
Author: Orion Poplawski <orion(a)nwra.com>
Date: Wed Jul 31 16:10:42 2013 -0600
Disable failing tests on arm for now
gdl.spec | 6 ++++++
1 files changed, 6 insertions(+), 0 deletions(-)
---
diff --git a/gdl.spec b/gdl.spec
index 9240b64..e73ebb7 100644
--- a/gdl.spec
+++ b/gdl.spec
@@ -167,7 +167,13 @@ cd build
# - https://sourceforge.net/p/gnudatalanguage/bugs/521/
# test_matrix_multiply is causing problems - hangs
# - https://sourceforge.net/p/gnudatalanguage/bugs/556/
+%ifarch %{arm}
+# test_finite and test_fix fail currently on arm
+# https://bugzilla.redhat.com/show_bug.cgi?id=990749
+make check ARGS="-V -E 'test_bug_3104326|test_bug_3300626|test_ce|test_dicom|test_execute|test_str_sep|test_matrix_multiply|test_finite|test_fix'"
+%else
make check ARGS="-V -E 'test_bug_3104326|test_bug_3300626|test_ce|test_dicom|test_execute|test_str_sep|test_matrix_multiply'"
+%endif
%clean
rm -rf $RPM_BUILD_ROOT
9Â years, 6Â months