* [bug#38214] [PATCH] gnu: Add minisat.
@ 2019-11-15 2:34 Robert Smith
2019-11-15 15:03 ` Mathieu Othacehe
2019-11-16 15:18 ` [bug#38214] [PATCH v2] " Robert Smith
0 siblings, 2 replies; 7+ messages in thread
From: Robert Smith @ 2019-11-15 2:34 UTC (permalink / raw)
To: 38214; +Cc: Robert Smith
* 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
^ permalink raw reply related [flat|nested] 7+ messages in thread
* [bug#38214] [PATCH] gnu: Add minisat.
2019-11-15 2:34 [bug#38214] [PATCH] gnu: Add minisat Robert Smith
@ 2019-11-15 15:03 ` Mathieu Othacehe
2019-11-15 20:00 ` Robert Smith
2019-11-16 15:18 ` [bug#38214] [PATCH v2] " Robert Smith
1 sibling, 1 reply; 7+ messages in thread
From: Mathieu Othacehe @ 2019-11-15 15:03 UTC (permalink / raw)
To: 38214; +Cc: robertsmith
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
^ permalink raw reply [flat|nested] 7+ messages in thread
* [bug#38214] [PATCH] gnu: Add minisat.
2019-11-15 15:03 ` Mathieu Othacehe
@ 2019-11-15 20:00 ` Robert Smith
0 siblings, 0 replies; 7+ messages in thread
From: Robert Smith @ 2019-11-15 20:00 UTC (permalink / raw)
To: 38214; +Cc: m.othacehe
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
^ permalink raw reply [flat|nested] 7+ messages in thread
* [bug#38214] [PATCH v2] gnu: Add minisat.
2019-11-15 2:34 [bug#38214] [PATCH] gnu: Add minisat Robert Smith
2019-11-15 15:03 ` Mathieu Othacehe
@ 2019-11-16 15:18 ` Robert Smith
2019-11-16 15:34 ` [bug#38230] Oops Robert Smith
` (2 more replies)
1 sibling, 3 replies; 7+ messages in thread
From: Robert Smith @ 2019-11-16 15:18 UTC (permalink / raw)
To: m.othacehe; +Cc: robertsmith, 38214
* 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@gnu.org>
;;; Copyright © 2019 Nicolas Goaziou <mail@nicolasgoaziou.fr>
;;; Copyright © 2019 Steve Sprang <scs@stevesprang.com>
+;;; Copyright © 2019 Robert Smith <robertsmith@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
^ permalink raw reply related [flat|nested] 7+ messages in thread
end of thread, other threads:[~2019-11-19 16:33 UTC | newest]
Thread overview: 7+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2019-11-15 2:34 [bug#38214] [PATCH] gnu: Add minisat Robert Smith
2019-11-15 15:03 ` Mathieu Othacehe
2019-11-15 20:00 ` Robert Smith
2019-11-16 15:18 ` [bug#38214] [PATCH v2] " Robert Smith
2019-11-16 15:34 ` [bug#38230] Oops Robert Smith
2019-11-19 16:30 ` [bug#38214] [PATCH v2] gnu: Add minisat Mathieu Othacehe
2019-11-19 16:32 ` bug#38214: " Mathieu Othacehe
Code repositories for project(s) associated with this public inbox
https://git.savannah.gnu.org/cgit/guix.git
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).