GNU bug report logs - #38214
[PATCH] 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 38214 in the body.
You can then email your comments to 38214 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: guix-patches <at> gnu.org
Cc: Robert Smith <robertsmith <at> posteo.net>
Subject: [PATCH] gnu: Add minisat.
Date: Fri, 15 Nov 2019 03:34:01 +0100

* gnu/packages/maths.scm (minisat): New variable.
---
 gnu/packages/maths.scm                        | 41 +++++++++++++++++++
 .../patches/minisat-friend-declaration.patch  | 23 +++++++++++
 .../patches/minisat-mroot-and-install.patch   | 30 ++++++++++++++
 3 files changed, 94 insertions(+)
 create mode 100644 gnu/packages/patches/minisat-friend-declaration.patch
 create mode 100644 gnu/packages/patches/minisat-mroot-and-install.patch

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 16a9d97a47..9271609843 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -5242,3 +5242,44 @@ fields of knowledge.")
     (home-page "http://speedcrunch.org/")
     (license license:gpl2+)))
 
+(define-public minisat
+  (package
+    (name "minisat")
+    (version "2.2.0")
+    (source
+      (origin
+        (method url-fetch)
+        (uri (string-append "http://minisat.se/downloads/minisat-"
+                            version ".tar.gz"))
+        (sha256
+          (base32
+            "023qdnsb6i18yrrawlhckm47q8x0sl7chpvvw3gssfyw3j2pv5cj"))
+        (patches
+          (search-patches "minisat-friend-declaration.patch"
+                          "minisat-mroot-and-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)
+           (add-before 'build 'mroot
+             (lambda* (#:key inputs #:allow-other-keys)
+                      (setenv "MROOT" (getcwd))
+                      (chdir "simp")
+                      #t)))))
+    (inputs
+      `(("zlib:static" ,zlib "static")
+        ("zlib" ,zlib)
+        ("kernel-headers" ,linux-libre-headers)))
+    (home-page
+      "http://minisat.se/MiniSat.html")
+    (synopsis
+      "Small, yet efficient, SAT solver with good documentation")
+    (license license:expat)
+    (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.")))
+
diff --git a/gnu/packages/patches/minisat-friend-declaration.patch b/gnu/packages/patches/minisat-friend-declaration.patch
new file mode 100644
index 0000000000..8283084086
--- /dev/null
+++ b/gnu/packages/patches/minisat-friend-declaration.patch
@@ -0,0 +1,23 @@
+See https://groups.google.com/forum/#!topic/minisat/FCocZsC8oMQ
+
+diff -rupN minisat-2.2.0/core/SolverTypes.h minisat-2.2.0.patched/core/SolverTypes.h
+--- a/core/SolverTypes.h	2010-07-10 17:07:36.000000000 +0100
++++ b/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-mroot-and-install.patch b/gnu/packages/patches/minisat-mroot-and-install.patch
new file mode 100644
index 0000000000..7862314f75
--- /dev/null
+++ b/gnu/packages/patches/minisat-mroot-and-install.patch
@@ -0,0 +1,30 @@
+Add install target, change default
+
+ * rs now default build target
+
+--- a/simp/Makefile
++++ b/simp/Makefile
+@@ -2,3 +2,8 @@
+ DEPDIR    = mtl utils core
+
+ include $(MROOT)/mtl/template.mk
++
++install:
++	mkdir -p $(DESTDIR)$(PREFIX)/bin
++	cp -f $(EXEC)_static $(DESTDIR)$(PREFIX)/bin/minisat
++
+--- a/mtl/template.mk
++++ b/mtl/template.mk
+@@ -29,11 +29,11 @@
+
+ .PHONY : s p d r rs clean
+
++rs:	$(EXEC)_static
+ s:	$(EXEC)
+ p:	$(EXEC)_profile
+ d:	$(EXEC)_debug
+ r:	$(EXEC)_release
+-rs:	$(EXEC)_static
+
+ libs:	lib$(LIB)_standard.a
+ libp:	lib$(LIB)_profile.a
-- 
2.24.0

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

From: Mathieu Othacehe <m.othacehe <at> gmail.com>
To: guix-patches <at> gnu.org
Cc: Robert Smith <robertsmith <at> posteo.net>, 38214 <at> debbugs.gnu.org
Subject: Re: [bug#38214] [PATCH] gnu: Add minisat.
Date: Fri, 15 Nov 2019 16:03:35 +0100

Hello Robert,

Thanks for your patch, a few remarks below.

> +          (search-patches "minisat-friend-declaration.patch"
> +                          "minisat-mroot-and-install.patch"))))

Why are these patch needed? It seems that the last release was a long
time ago, maybe we should package it from a git commit?

> +        ("kernel-headers" ,linux-libre-headers)))
                      ^
                      Is this really useful? It seems to build without.

> +    (synopsis
> +      "Small, yet efficient, SAT solver with good documentation")
> +    (license license:expat)

It's a tacit agreement, but the order of package fields is often:

- synopsis
- description
- home-page
- license.

Could you re-order those fields?

Do not forget to add your copyright on top of the file, and to indent
your code properly (see:
https://guix.gnu.org/manual/en/html_node/Formatting-Code.html).

Could you send an updated patch?

Thanks,

Mathieu

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

From: "Robert Smith" <robertsmith <at> posteo.net>
To: <guix-patches <at> gnu.org>
Cc: Mathieu Othacehe <m.othacehe <at> gmail.com>, 38214 <at> debbugs.gnu.org
Subject: Re: [bug#38214] [PATCH] gnu: Add minisat.
Date: Fri, 15 Nov 2019 21:00:27 +0100

On Fri Nov 15, 2019 at 4:03 PM Mathieu Othacehe wrote:
> > +          (search-patches "minisat-friend-declaration.patch"
> > +                          "minisat-mroot-and-install.patch"))))
> 
> Why are these patch needed? It seems that the last release was a long
> time ago, maybe we should package it from a git commit?

Thanks for the catch, I didn't realize that the git repo was so far
ahead of the last release.

> > +        ("kernel-headers" ,linux-libre-headers)))
>                       ^
>                       Is this really useful? It seems to build without.

I could have sworn that it refused to build without them, but testing
it now seems to work fine. I must have either been confused or it was
some other problem that I fixed.

Thanks for the feedback, I'll work on making the changes and submitting
a new patch.

-Robert

Message #20 received at 38214 <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 #25 received at 38214 <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

Message #30 received at 38214-done <at> debbugs.gnu.org (full text, mbox):

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

And closing!

Previous Next

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