[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
01/01: gnu: Add minisat.
|
From: |
guix-commits |
|
Subject: |
01/01: gnu: Add minisat. |
|
Date: |
Tue, 19 Nov 2019 11:29:13 -0500 (EST) |
mothacehe pushed a commit to branch master
in repository guix.
commit 3b7828cc7f938fcb369976cbe75d9c85f22583a1
Author: Robert Smith <address@hidden>
Date: Sat Nov 16 16:18:43 2019 +0100
gnu: Add minisat.
* gnu/packages/patches/minisat-friend-declaration.patch: New file.
* gnu/packages/patches/minisat-install.patch: New file.
* gnu/local.mk (dist_patch_DATA): Add both files above.
* gnu/packages/maths.scm (minisat): New exported variable.
Signed-off-by: Mathieu Othacehe <address@hidden>
---
gnu/local.mk | 2 ++
gnu/packages/maths.scm | 40 ++++++++++++++++++++++
.../patches/minisat-friend-declaration.patch | 25 ++++++++++++++
gnu/packages/patches/minisat-install.patch | 19 ++++++++++
4 files changed, 86 insertions(+)
diff --git a/gnu/local.mk b/gnu/local.mk
index 8a52e98..bb4dcbb 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -1131,6 +1131,8 @@ dist_patch_DATA =
\
%D%/packages/patches/metabat-fix-compilation.patch \
%D%/packages/patches/mhash-keygen-test-segfault.patch \
%D%/packages/patches/mingw-w64-6.0.0-gcc.patch \
+ %D%/packages/patches/minisat-friend-declaration.patch \
+ %D%/packages/patches/minisat-install.patch \
%D%/packages/patches/mpc123-initialize-ao.patch \
%D%/packages/patches/module-init-tools-moduledir.patch \
%D%/packages/patches/monero-use-system-miniupnpc.patch
\
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 16a9d97..32608ea 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -32,6 +32,7 @@
;;; Copyright © 2018 Amin Bandali <address@hidden>
;;; Copyright © 2019 Nicolas Goaziou <address@hidden>
;;; Copyright © 2019 Steve Sprang <address@hidden>
+;;; Copyright © 2019 Robert Smith <address@hidden>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -5242,3 +5243,42 @@ fields of knowledge.")
(home-page "http://speedcrunch.org/";)
(license license:gpl2+)))
+(define-public minisat
+ ;; This is the last commit which is available upstream, no
+ ;; release happened since 2010.
+ (let ((commit "37dc6c67e2af26379d88ce349eb9c4c6160e8543")
+ (revision "1"))
+ (package
+ (name "minisat")
+ (version (string-append "2.2.0-" revision "." (string-take commit 7)))
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/niklasso/minisat.git";)
+ (commit commit)))
+ (file-name (string-append name "-" version "-checkout"))
+ (sha256
+ (base32
+ "091hf3qkm197s5r7xcr3m07xsdwyz2rqk1hc9kj0hn13imz09irq"))
+ (patches
+ (search-patches "minisat-friend-declaration.patch"
+ "minisat-install.patch"))))
+ (build-system gnu-build-system)
+ (arguments
+ '(#:make-flags (list (string-append "prefix=" %output))
+ #:tests? #f ;no check target
+ #:phases
+ (modify-phases %standard-phases
+ (delete 'configure))))
+ (inputs
+ `(("zlib:static" ,zlib "static")
+ ("zlib" ,zlib)))
+ (synopsis
+ "Small, yet efficient, SAT solver")
+ (description
+ "MiniSat is a minimalistic, open-source SAT solver, developed to help
+researchers and developers alike to get started on SAT.")
+ (home-page
+ "http://minisat.se/MiniSat.html";)
+ (license license:expat))))
diff --git a/gnu/packages/patches/minisat-friend-declaration.patch
b/gnu/packages/patches/minisat-friend-declaration.patch
new file mode 100644
index 0000000..14a886a
--- /dev/null
+++ b/gnu/packages/patches/minisat-friend-declaration.patch
@@ -0,0 +1,25 @@
+See https://groups.google.com/forum/#!topic/minisat/FCocZsC8oMQ
+This seems to only be a problem with newer versions of g++, and
+upstream development seems to have stopped in 2013.
+
+diff -rupN minisat-2.2.0/core/SolverTypes.h
minisat-2.2.0.patched/core/SolverTypes.h
+--- a/minisat/core/SolverTypes.h 2010-07-10 17:07:36.000000000 +0100
++++ b/minisat/core/SolverTypes.h 2014-03-29 11:57:49.000000000 +0000
+@@ -47,7 +47,7 @@ struct Lit {
+ int x;
+
+ // Use this as a constructor:
+- friend Lit mkLit(Var var, bool sign = false);
++ //friend Lit mkLit(Var var, bool sign = false);
+
+ bool operator == (Lit p) const { return x == p.x; }
+ bool operator != (Lit p) const { return x != p.x; }
+@@ -55,7 +55,7 @@ struct Lit {
+ };
+
+
+-inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var +
(int)sign; return p; }
++inline Lit mkLit (Var var, bool sign = false) { Lit p; p.x = var + var
+ (int)sign; return p; }
+ inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q;
}
+ inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned
int)b; return q; }
+ inline bool sign (Lit p) { return p.x & 1; }
diff --git a/gnu/packages/patches/minisat-install.patch
b/gnu/packages/patches/minisat-install.patch
new file mode 100644
index 0000000..23cde89
--- /dev/null
+++ b/gnu/packages/patches/minisat-install.patch
@@ -0,0 +1,19 @@
+Avoid the default dynamic executable, which depends on minisat.so
+Instead install the release version, which is statically linked.
+
+diff --git a/Makefile b/Makefile
+index ceb9d77..7b91906 100644
+--- a/Makefile
++++ b/Makefile
+@@ -191,9 +191,9 @@ install-lib: $(BUILD_DIR)/release/lib/$(MINISAT_SLIB)
$(BUILD_DIR)/dynamic/lib/$
+ ln -sf $(MINISAT_DLIB).$(SOMAJOR) $(DESTDIR)$(libdir)/$(MINISAT_DLIB)
+ $(INSTALL) -m 644 $(BUILD_DIR)/release/lib/$(MINISAT_SLIB)
$(DESTDIR)$(libdir)
+
+-install-bin: $(BUILD_DIR)/dynamic/bin/$(MINISAT)
++install-bin: $(BUILD_DIR)/release/bin/$(MINISAT)
+ $(INSTALL) -d $(DESTDIR)$(bindir)
+- $(INSTALL) -m 755 $(BUILD_DIR)/dynamic/bin/$(MINISAT)
$(DESTDIR)$(bindir)
++ $(INSTALL) -m 755 $(BUILD_DIR)/release/bin/$(MINISAT)
$(DESTDIR)$(bindir)
+
+ clean:
+ rm -f $(foreach t, release debug profile dynamic, $(foreach o,
$(SRCS:.cc=.o), $(BUILD_DIR)/$t/$o)) \