diff mbox series

[bug#38214] gnu: Add minisat.

Message ID 20191115023401.8126-1-robertsmith@posteo.net
State Accepted
Headers show
Series [bug#38214] gnu: Add minisat. | expand

Commit Message

Robert Smith Nov. 15, 2019, 2:34 a.m. UTC 
* 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

Comments

Mathieu Othacehe Nov. 15, 2019, 3:03 p.m. UTC | #1 
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
Robert Smith Nov. 15, 2019, 8 p.m. UTC | #2 
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
diff mbox series

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