From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:470:142:3::10]:39110) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1iVRRw-0001iD-6t for guix-patches@gnu.org; Thu, 14 Nov 2019 21:35:05 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1iVRRu-0005ig-Nr for guix-patches@gnu.org; Thu, 14 Nov 2019 21:35:04 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:54864) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1iVRRu-0005ia-KY for guix-patches@gnu.org; Thu, 14 Nov 2019 21:35:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1iVRRu-0004Ik-Ed for guix-patches@gnu.org; Thu, 14 Nov 2019 21:35:02 -0500 Subject: [bug#38214] [PATCH] gnu: Add minisat. Resent-Message-ID: Received: from eggs.gnu.org ([2001:470:142:3::10]:39012) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1iVRRE-0001dv-8Y for guix-patches@gnu.org; Thu, 14 Nov 2019 21:34:21 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1iVRRC-0005GB-Fx for guix-patches@gnu.org; Thu, 14 Nov 2019 21:34:19 -0500 Received: from mout02.posteo.de ([185.67.36.66]:35009) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1iVRRB-0005FN-Uf for guix-patches@gnu.org; Thu, 14 Nov 2019 21:34:18 -0500 Received: from submission (posteo.de [89.146.220.130]) by mout02.posteo.de (Postfix) with ESMTPS id C302C2400FB for ; Fri, 15 Nov 2019 03:34:14 +0100 (CET) From: Robert Smith Date: Fri, 15 Nov 2019 03:34:01 +0100 Message-Id: <20191115023401.8126-1-robertsmith@posteo.net> MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable 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: 38214@debbugs.gnu.org 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+))) =20 +(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=3D" %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 h= elp +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/S= olverTypes.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 =3D false); ++ //friend Lit mkLit(Var var, bool sign =3D false); + + bool operator =3D=3D (Lit p) const { return x =3D=3D p.x; } + bool operator !=3D (Lit p) const { return x !=3D p.x; } +@@ -55,7 +55,7 @@ struct Lit { + }; + + +-inline Lit mkLit (Var var, bool sign) { Lit p; p.x =3D var + var = + (int)sign; return p; } ++inline Lit mkLit (Var var, bool sign =3D false) { Lit p; p.x =3D = var + var + (int)sign; return p; } + inline Lit operator ~(Lit p) { Lit q; q.x =3D p.x ^ 1; r= eturn q; } + inline Lit operator ^(Lit p, bool b) { Lit q; q.x =3D p.x ^ (uns= igned 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/p= ackages/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 =3D 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 --=20 2.24.0