From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:470:142:3::10]:51467) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1iVzro-0006eg-Cv for guix-patches@gnu.org; Sat, 16 Nov 2019 10:20:05 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1iVzrm-00085y-Un for guix-patches@gnu.org; Sat, 16 Nov 2019 10:20:04 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:58988) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1iVzrm-00085r-Re for guix-patches@gnu.org; Sat, 16 Nov 2019 10:20:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1iVzrm-0005n9-Hm for guix-patches@gnu.org; Sat, 16 Nov 2019 10:20:02 -0500 Subject: [bug#38214] [PATCH v2] gnu: Add minisat. References: <20191115023401.8126-1-robertsmith@posteo.net> In-Reply-To: <20191115023401.8126-1-robertsmith@posteo.net> Resent-Message-ID: From: Robert Smith Date: Sat, 16 Nov 2019 16:18:43 +0100 Message-Id: <20191116151843.30150-1-robertsmith@posteo.net> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+kyle=kyleam.com@gnu.org Sender: "Guix-patches" To: m.othacehe@gmail.com Cc: robertsmith@posteo.net, 38214@debbugs.gnu.org * 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 ;;; Copyright © 2019 Nicolas Goaziou ;;; Copyright © 2019 Steve Sprang +;;; Copyright © 2019 Robert Smith ;;; ;;; 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