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

Previous Next

Full log

View this message in rfc822 format

From: help-debbugs <at> gnu.org (GNU bug Tracking System)
To: Mathieu Othacehe <m.othacehe <at> gmail.com>
Cc: tracker <at> debbugs.gnu.org
Subject: bug#38214: closed ([PATCH] gnu: Add minisat.)
Date: Tue, 19 Nov 2019 16:33:02 +0000

[Message part 1 (text/plain, inline)]

Your message dated Tue, 19 Nov 2019 17:32:42 +0100
with message-id <87wobv3jyt.fsf <at> gmail.com>
and subject line Re: [PATCH v2] gnu: Add minisat.
has caused the debbugs.gnu.org bug report #38214,
regarding [PATCH] gnu: Add minisat.
to be marked as done.

(If you believe you have received this mail in error, please contact
help-debbugs <at> gnu.org.)


-- 
38214: http://debbugs.gnu.org/cgi/bugreport.cgi?bug=38214
GNU Bug Tracking System
Contact help-debbugs <at> gnu.org with problems

[Message part 2 (message/rfc822, inline)]

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 part 3 (message/rfc822, inline)]

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.