GNU bug report logs - #38230
[PATCH v2] gnu: Add minisat.

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 38230 in the body.
You can then email your comments to 38230 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Robert Smith <robertsmith <at> posteo.net>
To: m.othacehe <at> gmail.com
Cc: Robert Smith <robertsmith <at> posteo.net>, 38214 <at> debbugs.gnu.org,
 guix-patches <at> gnu.org
Subject: [PATCH v2] gnu: Add minisat.
Date: Sat, 16 Nov 2019 16:18:43 +0100

* gnu/packages/maths.scm (minisat): New variable.
---
I updated the source to the latest commit available, which unfortunately
only gets us from 2010 to 2013. Although the minisat-friend-declaration
patch was written by the original author in 2014, they never committed
it to the repo. Additionally an install patch is still needed to avoid a
dependency on our own shared library. Hopefully all style issues have
been fixed, and a copyright line was added.

 gnu/packages/maths.scm                        | 42 +++++++++++++++++++
 .../patches/minisat-friend-declaration.patch  | 25 +++++++++++
 gnu/packages/patches/minisat-install.patch    | 19 +++++++++
 3 files changed, 86 insertions(+)
 create mode 100644 gnu/packages/patches/minisat-friend-declaration.patch
 create mode 100644 gnu/packages/patches/minisat-install.patch

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 16a9d97a47..42a72737da 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -32,6 +32,7 @@
 ;;; Copyright © 2018 Amin Bandali <bandali <at> gnu.org>
 ;;; Copyright © 2019 Nicolas Goaziou <mail <at> nicolasgoaziou.fr>
 ;;; Copyright © 2019 Steve Sprang <scs <at> stevesprang.com>
+;;; Copyright © 2019 Robert Smith <robertsmith <at> posteo.net>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -5242,3 +5243,44 @@ 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 with good documentation")
+      (description
+       "MiniSat is a minimalistic, open-source SAT solver, developed to help
+researchers and developers alike to get started on SAT.  It is released under
+the MIT licence, and is currently used in a number of projects.")
+      (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 0000000000..14a886ae2f
--- /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 0000000000..23cde89bec
--- /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)) \
-- 
2.24.0

Message #8 received at 38230 <at> debbugs.gnu.org (full text, mbox):

From: Robert Smith <robertsmith <at> posteo.net>
To: 38230 <at> debbugs.gnu.org
Subject: Oops
Date: Sat, 16 Nov 2019 16:34:06 +0100

Apologies, I didn't intend to create a new issue.
My email-foo is still weak :(

-Robert

Message #13 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Mathieu Othacehe <m.othacehe <at> gmail.com>
To: Robert Smith <robertsmith <at> posteo.net>
Cc: 38214 <at> debbugs.gnu.org, guix-patches <at> gnu.org
Subject: Re: [PATCH v2] gnu: Add minisat.
Date: Tue, 19 Nov 2019 17:30:52 +0100

Hello Robert,

I fixed a small indentation issue, added both patches to local.mk, 
edited commit message accordingly and pushed!

Thanks,

Mathieu

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.