Package: guix-patches;
Reported by: Maximilian Heisinger <mail <at> maxheisinger.at>
Date: Sat, 13 Aug 2022 16:57:03 UTC
Severity: normal
Tags: patch
Done: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
Bug is archived. No further changes may be made.
To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 57181 in the body.
You can then email your comments to 57181 AT debbugs.gnu.org in the normal way.
Toggle the display of automated, internal messages from the tracker.
View this report as an mbox folder, status mbox, maintainer mbox
guix-patches <at> gnu.org:bug#57181; Package guix-patches.
(Sat, 13 Aug 2022 16:57:03 GMT) Full text and rfc822 format available.Maximilian Heisinger <mail <at> maxheisinger.at>:guix-patches <at> gnu.org.
(Sat, 13 Aug 2022 16:57:03 GMT) Full text and rfc822 format available.Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):
From: Maximilian Heisinger <mail <at> maxheisinger.at> To: "guix-patches <at> gnu.org" <guix-patches <at> gnu.org> Subject: [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat Date: Sat, 13 Aug 2022 17:34:49 +0200 (CEST)
[Message part 1 (text/plain, inline)]
From dea29e40c0cfb5eaac49060082fe63c0ed1e08b7 Mon Sep 17 00:00:00 2001
From: Maximilian Heisinger <mail <at> maxheisinger.at>
Date: Sat, 13 Aug 2022 17:23:59 +0200
Subject: [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat
* gnu/packages/maths.scm (cryptominisat5): Add package.
* gnu/packages/maths.scm (kissat): Add package.
---
gnu/packages/maths.scm | 64 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 64 insertions(+)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index c79058ab42..4a58b9eb3f 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -7311,6 +7311,70 @@ (define-public minisat
"http://minisat.se/MiniSat.html")
(license license:expat))))
+(define-public cryptominisat5
+ (package
+ (name "cryptominisat5")
+ (version "5.8.0")
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/msoos/cryptominisat")
+ (commit version)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "00hmxdlyhn7pwk9jlvc5g0l5z5xqfchjzf5jgn3pkj9xhl8yqq50"))))
+ (build-system cmake-build-system)
+ (arguments `(#:tests? #false))
+ (inputs (list zlib boost))
+ (synopsis "Advanced incremental SAT solver")
+ (description
+ "Provides CryptoMiniSat, an advanced incremental SAT solver. The system
+has 3 interfaces: command-line, C++ library and python. The command-line
+interface takes a cnf as an input in the DIMACS format with the extension of
+XOR clauses. The C++ and python interface mimics this and also allows for
+incremental use: assumptions and multiple solve calls. A C compatible wrapper
+is also provided.")
+ (home-page "https://github.com/msoos/cryptominisat")
+ (license license:expat)))
+
+(define-public kissat
+ (package
+ (name "kissat")
+ (version "3.0.0")
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/arminbiere/kissat")
+ (commit (string-append "rel-" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "04x4w760srbdi4zci0s747qxk717x5d2x59ixraxh5104s9nyn8b"))))
+ (build-system gnu-build-system)
+ (arguments
+ `(#:tests? #f
+ #:phases
+ (modify-phases %standard-phases
+ (replace 'configure
+ (lambda* (#:key outputs #:allow-other-keys)
+ (invoke "./configure")))
+ (replace 'install
+ (lambda* (#:key inputs outputs #:allow-other-keys)
+ (install-file
+ "build/kissat"
+ (string-append (assoc-ref outputs "out") "/bin")))))))
+ (home-page "https://github.com/arminbiere/kissat")
+ (synopsis "Bare-metal SAT solver after the KISS principle principle
+written in C")
+ (description
+ "Kissat is a \"keep it simple and clean bare metal SAT solver\" written
+in C. It is a port of CaDiCaL back to C with improved data structures, better
+scheduling of inprocessing and optimized algorithms and implementation.")
+ (license license:gpl3+)))
+
(define-public libqalculate
(package
(name "libqalculate")
--
2.37.1
[signature.asc (application/pgp-signature, attachment)]
guix-patches <at> gnu.org:bug#57181; Package guix-patches.
(Sat, 13 Aug 2022 20:06:02 GMT) Full text and rfc822 format available.Message #8 received at 57181 <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: Maximilian Heisinger <mail <at> maxheisinger.at> Cc: 57181 <at> debbugs.gnu.org Subject: Re: [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat Date: Sat, 13 Aug 2022 22:05:02 +0200
Hi, Am Samstag, dem 13.08.2022 um 17:23 +0200 schrieb Maximilian Heisinger: > * gnu/packages/maths.scm (cryptominisat5): Add package. > * gnu/packages/maths.scm (kissat): Add package. Split into two patches, one for cryptominisat and one for kissat. > --- > gnu/packages/maths.scm | 64 > ++++++++++++++++++++++++++++++++++++++++++ > 1 file changed, 64 insertions(+) > > diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm > index c79058ab42..4a58b9eb3f 100644 > --- a/gnu/packages/maths.scm > +++ b/gnu/packages/maths.scm > @@ -7311,6 +7311,70 @@ (define-public minisat > "http://minisat.se/MiniSat.html") > (license license:expat)))) > > +(define-public cryptominisat5 > + (package > + (name "cryptominisat5") > + (version "5.8.0") > + (source > + (origin > + (method git-fetch) > + (uri (git-reference > + (url "https://github.com/msoos/cryptominisat") > + (commit version))) > + (file-name (git-file-name name version)) > + (sha256 > + (base32 > + "00hmxdlyhn7pwk9jlvc5g0l5z5xqfchjzf5jgn3pkj9xhl8yqq50")))) > + (build-system cmake-build-system) > + (arguments `(#:tests? #false)) Always state why tests are disabled. > + (inputs (list zlib boost)) > + (synopsis "Advanced incremental SAT solver") "Incremental SAT solver" is probably enough. > + (description > + "Provides CryptoMiniSat, an advanced incremental SAT solver. > The system > +has 3 interfaces: command-line, C++ library and python. I'd shorten this to "CryptoMiniSat is an incremental SAT solver with three interfaces: command-line, C++ library and Python". > The command-line > +interface takes a cnf as an input in the DIMACS format with the > extension of Use @abbrev for CNF (also capitalize). > +XOR clauses. The C++ and python interface mimics this and also > allows for > +incremental use: assumptions and multiple solve calls. A C > compatible wrapper > +is also provided.") Doesn't that technically make it a fourth interface? > + (home-page "https://github.com/msoos/cryptominisat") > + (license license:expat))) > +(define-public kissat > + (package > + (name "kissat") > + (version "3.0.0") > + (source > + (origin > + (method git-fetch) > + (uri (git-reference > + (url "https://github.com/arminbiere/kissat") > + (commit (string-append "rel-" version)))) > + (file-name (git-file-name name version)) > + (sha256 > + (base32 > + "04x4w760srbdi4zci0s747qxk717x5d2x59ixraxh5104s9nyn8b")))) > + (build-system gnu-build-system) > + (arguments > + `(#:tests? #f Specify why. > + #:phases > + (modify-phases %standard-phases > + (replace 'configure > + (lambda* (#:key outputs #:allow-other-keys) > + (invoke "./configure"))) You probably want to (apply invoke "./configure" configure-flags). > + (replace 'install > + (lambda* (#:key inputs outputs #:allow-other-keys) > + (install-file > + "build/kissat" > + (string-append (assoc-ref outputs "out") "/bin"))))))) Is this the only thing to install? > + (home-page "https://github.com/arminbiere/kissat") > + (synopsis "Bare-metal SAT solver after the KISS principle > principle > +written in C") "Bare-metal SAT solver" probably suffices. > + (description > + "Kissat is a \"keep it simple and clean bare metal SAT solver\" > written "bare metal SAT solver" again probably suffices. If you want to be generous with advertising terms, clean may be added, but I don't think it adds useful information. > +in C. It is a port of CaDiCaL back to C with improved data > structures, better > +scheduling of inprocessing and optimized algorithms and > implementation.") > + (license license:gpl3+))) > + Cheers
guix-patches <at> gnu.org:bug#57181; Package guix-patches.
(Sun, 14 Aug 2022 22:08:02 GMT) Full text and rfc822 format available.Message #11 received at 57181 <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: Maximilian Heisinger <mail <at> maxheisinger.at> Cc: 57181 <at> debbugs.gnu.org Subject: Re: [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat Date: Mon, 15 Aug 2022 00:07:42 +0200
Hi, Don't forget to CC the mailing list. Am Sonntag, dem 14.08.2022 um 21:27 +0200 schrieb Maximilian Heisinger: > gnu: maths: Add modern SAT solver cryptominisat5 Should simply be "gnu: Add cryptominisat5. > + (uri (git-reference > + (url "https://github.com/msoos/cryptominisat") > + (commit version) > + (recursive? #t))) Recursive checkout doesn't really sound "mini". > > + (description > + "Incremental SAT solver with four interfaces: command-line, C++ > library, > +C interface, and Python. I forgot this, but the description should consist of full sentences. Also, while I (jokingly) referred to the C interface as a separate interface, you should probably phrase this a little differently. > gnu: maths: Add modern SAT solver kissat As above. > + ;; One test fails in the guix build container: "main". > The cause > + ;; is not clear yet and this test is not enabled in the > tissat > + ;; test step. Kissat (called by tissat) just does not > finish. > + ;; Could be an issue with kissat. This could probably be shortened to something like "XXX: main test fails in build container". > + ;; Kissat has no `make install` step, so files are > installed > + ;; manually. This installs the (static) library, the > header and > + ;; the executable. Don't comment the obvious, but more importantly, could we try to make this a shared library? > Kissat is a bare-metal and clean SAT-solver written in C. I wouldn't use "and" as a joiner here. Both "clean, bare-metal SAT solver" and "bare-metal SAT solver" sound a little cleaner 🙂️ Cheers
guix-patches <at> gnu.org:bug#57181; Package guix-patches.
(Mon, 15 Aug 2022 13:28:02 GMT) Full text and rfc822 format available.Message #14 received at 57181 <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: Maximilian Heisinger <mail <at> maxheisinger.at> Cc: 57181 <at> debbugs.gnu.org Subject: Re: [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat Date: Mon, 15 Aug 2022 15:27:11 +0200
Hi, I've pushed kissat with some heavy edits. In particular, I - fixed the commit message, - hard-coded the compression binaries (and made them regular inputs), - fixed the actual test failure, - used G-Expressions rather than quasiquoting. See 9ddd37d6ab59e2519bbcefad15ce62561128f0ee. Am Montag, dem 15.08.2022 um 12:50 +0200 schrieb Maximilian Heisinger: > Hi, > > sorry, doing the correct CC now. > > > Recursive checkout doesn't really sound "mini". > > Oh, there's some history behind the mini... CryptoMiniSat adds some > stuff commonly needed in cryptography to MiniSat, which is a common > base for many other SAT solvers. I know about the existence of Minisat, but the problem here is rather that cryptominisat seems to pull in lots of stuff that we'd rather have packaged separately instead of vendored (e.g. googletest). Could you try unvendoring those things and place the remaining parts in the right location without a recursive checkout? > The library interfaces mimic this and also > +allow IPASIR-esque incremental use, including assumptions. "Incremental solving" sounds easier to understand. > + (inputs (list zlib boost)) > + (native-inputs (list python python-lit)) If you have a Python interface, you probably also need python in inputs, no? Cheers
guix-patches <at> gnu.org:bug#57181; Package guix-patches.
(Mon, 15 Aug 2022 15:46:02 GMT) Full text and rfc822 format available.Message #17 received at 57181 <at> debbugs.gnu.org (full text, mbox):
From: Maximilian Heisinger <mail <at> maxheisinger.at> To: Liliana Marie Prikler <liliana.prikler <at> gmail.com> Cc: 57181 <at> debbugs.gnu.org Subject: Re: [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat Date: Mon, 15 Aug 2022 12:50:30 +0200 (CEST)
[Message part 1 (text/plain, inline)]
Hi, sorry, doing the correct CC now. > Recursive checkout doesn't really sound "mini". Oh, there's some history behind the mini... CryptoMiniSat adds some stuff commonly needed in cryptography to MiniSat, which is a common base for many other SAT solvers. Kissat is "clean" mainly because it is a new solver that completely breaks with the old MiniSat codebase (and it cleans up some stuff, that was done in CaDiCaL, which I also intend to add later, as some features are still missing from Kissat). And MiniSat itself was a nice and minimal implementation containing (back then) the state-of-the-art optimizations. > could we try to make this a shared library? Done. Also updated the text and the commit messages :) Best regards, Max
[0002-PATCH-gnu-Add-modern-SAT-solver-kissat.patch (text/x-patch, attachment)]
[0001-PATCH-gnu-Add-modern-SAT-solver-cryptominisat5.patch (text/x-patch, attachment)]
[signature.asc (application/pgp-signature, attachment)]
guix-patches <at> gnu.org:bug#57181; Package guix-patches.
(Wed, 17 Aug 2022 07:47:01 GMT) Full text and rfc822 format available.Message #20 received at 57181 <at> debbugs.gnu.org (full text, mbox):
From: mail <at> maxheisinger.at To: liliana.prikler <at> gmail.com Cc: 57181 <at> debbugs.gnu.org Subject: Re: [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat Date: Wed, 17 Aug 2022 08:26:52 +0200
[Message part 1 (text/plain, inline)]
Hi,
> - fixed the commit message,
> - hard-coded the compression binaries (and made them regular inputs),
> - fixed the actual test failure,
> - used G-Expressions rather than quasiquoting.
>
> See 9ddd37d6ab59e2519bbcefad15ce62561128f0ee.
Thank you very much! This really is clearer, better, and gives me more
pointers to research about Guix.
> the problem here is rather that cryptominisat seems to pull in lots of
> stuff that we'd rather have packaged separately instead of vendored
> (e.g. googletest). Could you try unvendoring those things and place
> the remaining parts in the right location without a recursive
> checkout?
Yes, that would be better... Then we have two choices now I think:
1. Try to unvendor everything and add minisat as transformed package
with different sources + lingeling as a new package. This would
also still require to download the external test files as additional
source repositories.
2. Or we rely on using the ~ONLY_SIMPLE~ CMake option CryptoMiniSat
offers that is meant to build a simpler binary, but also deactivates
more complex tests. We still build a complex binary (i.e. Boost
program options for options parsing) by not setting it, but instead
substitute the query for the option in the ~test/CMakeLists.txt~
file. Additionally, we substitute some other issues away.
The second option loses some scripts and the more comprehensive tests.
I would argue though, that these would be better suited for developing
the solver and less for such a package management situation. What is
your opinion about this trade-off?
> "Incremental solving" sounds easier to understand.
Changed it.
> If you have a Python interface, you probably also need python in
> inputs, no?
True - it is better to directly expose it. I also took another look at
the solver's capabilities and output in more detail and added
python-numpy (required dependency for the py API) and sqlite (optional
dependency used for collecting statistics).
Thank you again for your patience and effort! You find my updated patch
attached.
Best regards (now even written from an Emacs mail client),
Max
[0001-gnu-Add-cryptominisat5.patch (text/x-patch, inline)]
From 5541a0aeb7660eacd5dbec8ef88db42af7b3b7b5 Mon Sep 17 00:00:00 2001
From: Maximilian Heisinger <mail <at> maxheisinger.at>
Date: Tue, 16 Aug 2022 20:59:06 +0200
Subject: [PATCH] gnu: Add cryptominisat5
* gnu/packages/maths.scm (cryptominisat5): Add package.
---
gnu/packages/maths.scm | 50 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 50 insertions(+)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 72d5e9a83a..a01f386831 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -55,6 +55,7 @@
;;; Copyright © 2022 Philip McGrath <philip <at> philipmcgrath.com>
;;; Copyright © 2022 Marek Felšöci <marek <at> felsoci.sk>
;;; Copyright © 2022 vicvbcun <guix <at> ikherbers.com>
+;;; Copyright © 2022 Maximilian Heisinger <mail <at> maxheisinger.at>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -159,6 +160,7 @@ (define-module (gnu packages maths)
#:use-module (gnu packages shells)
#:use-module (gnu packages sphinx)
#:use-module (gnu packages swig)
+ #:use-module (gnu packages sqlite)
#:use-module (gnu packages tcl)
#:use-module (gnu packages texinfo)
#:use-module (gnu packages tex)
@@ -7317,6 +7319,54 @@ (define-public minisat
"http://minisat.se/MiniSat.html")
(license license:expat))))
+(define-public cryptominisat5
+ (package
+ (name "cryptominisat5")
+ (version "5.8.0")
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/msoos/cryptominisat")
+ (commit version)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "00hmxdlyhn7pwk9jlvc5g0l5z5xqfchjzf5jgn3pkj9xhl8yqq50"))))
+ (build-system cmake-build-system)
+ (arguments
+ (list #:build-type "Release"
+ #:test-target "test"
+ #:configure-flags
+ #~(list "-DENABLE_TESTING=ON" "-DSTATS=ON")
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'unpack 'patch-source
+ (lambda* (#:key inputs #:allow-other-keys)
+ (substitute* "CMakeLists.txt"
+ (("add_subdirectory\\(utils/lingeling-ala\\)") ""))
+ ;; Transitively included in vendored gtest.h. Fixed in
+ ;; upstream:
+ ;; https://github.com/msoos/cryptominisat/pull/686
+ (substitute* "tests/assump_test.cpp"
+ (("#include <vector>")
+ "#include <vector>\n#include <algorithm>"))
+ (substitute* "tests/CMakeLists.txt"
+ (("add_subdirectory\\(\\$\\{GTEST_PREFIX\\} gtest\\)")
+ "find_package(GTest REQUIRED)")
+ (("if\\(NOT ONLY_SIMPLE\\)") "if(FALSE)")))))))
+ (inputs (list zlib boost sqlite python python-numpy))
+ (native-inputs (list python-lit googletest))
+ (synopsis "Incremental SAT solver")
+ (description
+ "CryptoMiniSat is an incremental SAT solver with both command line and
+library (C++, C, Python) interfaces. The command-line interface takes a
+@acronym{CNF, Conjunctive Normal Form} as an input in the DIMACS format with
+the extension of XOR clauses. The library interfaces mimic this and also
+allow incremental solving, including assumptions.")
+ (home-page "https://github.com/msoos/cryptominisat")
+ (license license:expat)))
+
(define-public kissat
(package
(name "kissat")
--
2.37.2
guix-patches <at> gnu.org:bug#57181; Package guix-patches.
(Wed, 17 Aug 2022 20:17:02 GMT) Full text and rfc822 format available.Message #23 received at 57181 <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: mail <at> maxheisinger.at Cc: 57181 <at> debbugs.gnu.org Subject: Re: [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat Date: Wed, 17 Aug 2022 22:16:03 +0200
Hi, Am Mittwoch, dem 17.08.2022 um 08:26 +0200 schrieb mail <at> maxheisinger.at: > [...] [W]e have two choices now I think: > > 1. Try to unvendor everything and add minisat as transformed package > with different sources + lingeling as a new package. This would > also still require to download the external test files as > additional source repositories. > 2. Or we rely on using the ~ONLY_SIMPLE~ CMake option CryptoMiniSat > offers that is meant to build a simpler binary, but also > deactivates more complex tests. We still build a complex binary > (i.e. Boost program options for options parsing) by not setting > it, but instead substitute the query for the option in the > ~test/CMakeLists.txt~ file. Additionally, we substitute some > other issues away. > > The second option loses some scripts and the more comprehensive > tests. I would argue though, that these would be better suited for > developing the solver and less for such a package management > situation. What is your opinion about this trade-off? Only running simple tests is preferable to running no tests at all. If you think that unvendoring everything is an unreasonable amount of work, that's a viable solution. However, we do strive to offer complete packages, so feel free to do 1. :) If you need some pointers as for the test files, ppsspp includes both another package's source (not so great, needs better unvendoring) and test files, and there's probably some other packages you could consult as well. > > "Incremental solving" sounds easier to understand. > > Changed it. LGTM. > > If you have a Python interface, you probably also need python in > > inputs, no? > > True - it is better to directly expose it. I also took another look > at the solver's capabilities and output in more detail and added > python-numpy (required dependency for the py API) and sqlite > (optional dependency used for collecting statistics). Note that python is now missing from native-inputs, but python-lit is in there. I suppose you need python both as input (for linking) and native-input (to run whatever python-lit is supposed to do). Cheers
guix-patches <at> gnu.org:bug#57181; Package guix-patches.
(Sat, 15 Oct 2022 14:56:02 GMT) Full text and rfc822 format available.Message #26 received at 57181 <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: 57181 <at> debbugs.gnu.org Cc: mail <at> maxheisinger.at Subject: [PATCH v2 2/4] gnu: Add lingeling. Date: Sat, 15 Oct 2022 16:45:44 +0200
* gnu/packages/maths.scm (lingeling): New variable.
---
gnu/packages/maths.scm | 82 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 82 insertions(+)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 1e9d7b8be8..5c8a0fe2ef 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -7429,6 +7429,88 @@ (define-public aiger
(license (list license:expat
license:bsd-3)))) ; blif2aig
+(define-public lingeling
+ (let ((commit "72d2b13eea5fbd95557a3d0d199cd98dfbdc76ee")
+ (revision "1"))
+ (package
+ (name "lingeling")
+ (version (git-version "sc2022" revision commit))
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/arminbiere/lingeling")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "16s30x8s2cw6icchwm65zj56ph4qwz6i07g3hwkknvajisvjq85c"))))
+ (build-system gnu-build-system)
+ (arguments
+ (list #:test-target "test"
+ #:modules `((ice-9 match)
+ ,@%gnu-build-system-modules)
+ #:configure-flags #~(list "--aiger=.")
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'unpack 'unpack-aiger
+ (lambda* (#:key inputs #:allow-other-keys)
+ (invoke #$(ar-for-target) "x"
+ (search-input-file inputs "lib/libaiger.a")
+ "aiger.o")
+ (copy-file
+ (search-input-file inputs "include/aiger/aiger.h")
+ "aiger.h")))
+ (add-after 'unpack 'hard-code-commit
+ (lambda _
+ (substitute* "mkconfig.sh"
+ (("`\\./getgitid`") #$commit))))
+ (add-after 'unpack 'patch-source
+ (lambda* (#:key inputs #:allow-other-keys)
+ (substitute* (list "treengeling.c" "lgldimacs.c")
+ (("\"(gunzip|xz|bzcat|7z)" all cmd)
+ (string-append
+ "\""
+ (search-input-file inputs (string-append "bin/" cmd)))))))
+ (replace 'configure
+ (lambda* (#:key configure-flags #:allow-other-keys)
+ (apply invoke "./configure.sh" configure-flags)))
+ (replace 'install
+ (lambda* (#:key outputs #:allow-other-keys)
+ (let ((bin (string-append (assoc-ref outputs "out")
+ "/bin")))
+ (mkdir-p bin)
+ (for-each
+ (lambda (file)
+ (install-file file bin))
+ '("blimc" "ilingeling" "lglddtrace" "lglmbt"
+ "lgluntrace" "lingeling" "plingeling"
+ "treengeling")))))
+ (add-after 'install 'wrap-path
+ (lambda* (#:key outputs #:allow-other-keys)
+ (with-directory-excursion (string-append
+ (assoc-ref outputs "out")
+ "/bin")
+ (for-each
+ (lambda (file)
+ (wrap-program
+ file
+ '("PATH" suffix
+ #$(map (lambda (input)
+ (file-append (this-package-input input) "/bin"))
+ '("gzip" "bzip2" "xz" "p7zip")))))
+ ;; These programs use sprintf on buffers with magic
+ ;; values to construct commands (yes, eww), so we
+ ;; can't easily substitute* them.
+ '("lglddtrace" "lgluntrace" "lingeling" "plingeling"))))))))
+ (inputs (list `(,aiger "static") gzip bzip2 xz p7zip))
+ (home-page "http://fmv.jku.at/lingeling")
+ (synopsis "SAT solver")
+ (description "This package provides a range of SAT solvers, including
+the sequential @command{lingeling} and its parallel variants
+@command{plingeling} and @command{treengeling}. A bounded model checker is
+also included.")
+ (license license:expat))))
+
(define-public libqalculate
(package
(name "libqalculate")
--
2.38.0
guix-patches <at> gnu.org:bug#57181; Package guix-patches.
(Sat, 15 Oct 2022 14:56:02 GMT) Full text and rfc822 format available.Message #29 received at 57181 <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: 57181 <at> debbugs.gnu.org Cc: mail <at> maxheisinger.at Subject: [PATCH v2 1/4] gnu: Add aiger. Date: Sat, 15 Oct 2022 16:45:33 +0200
* gnu/packages/maths.scm (aiger): New variable.
---
gnu/packages/maths.scm | 54 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 54 insertions(+)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index ffd2a89d2f..1e9d7b8be8 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -55,6 +55,7 @@
;;; Copyright © 2022 Philip McGrath <philip <at> philipmcgrath.com>
;;; Copyright © 2022 Marek Felšöci <marek <at> felsoci.sk>
;;; Copyright © 2022 vicvbcun <guix <at> ikherbers.com>
+;;; Copyright © 2022 Liliana Marie Prikler <liliana.prikler <at> gmail.com>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -7375,6 +7376,59 @@ (define-public kissat
optimized algorithms and implementation.")
(license license:expat)))
+(define-public aiger
+ (package
+ (name "aiger")
+ (version "1.9.9")
+ (source (origin
+ (method url-fetch)
+ (uri (string-append "http://fmv.jku.at/aiger/aiger-"
+ version ".tar.gz"))
+ (sha256
+ (base32
+ "1ish0dw0nf9gyghxsdhpy1jjiy5wp54c993swp85xp7m6vdx6l0y"))))
+ (outputs (list "out" "static"))
+ (build-system gnu-build-system)
+ (arguments
+ (list #:tests? #f ; no check target
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'unpack 'patch-source
+ (lambda* (#:key inputs #:allow-other-keys)
+ (substitute* "aiger.c"
+ (("\"(gzip|gunzip)" all cmd)
+ (string-append
+ "\""
+ (search-input-file inputs (string-append "bin/" cmd)))))))
+ (add-after 'unpack 'patch-build-files
+ (lambda* (#:key outputs #:allow-other-keys)
+ (substitute* "makefile.in"
+ (("test -d .*") "true")
+ (("/usr/local") (assoc-ref outputs "out")))))
+ (replace 'configure
+ (lambda* (#:key configure-flags #:allow-other-keys)
+ (apply invoke "./configure.sh" configure-flags)))
+ (add-after 'install 'install-static
+ (lambda* (#:key outputs #:allow-other-keys)
+ (apply invoke #$(ar-for-target) "rcs" "libaiger.a"
+ (find-files "." "\\.o$"))
+ (let* ((static (assoc-ref outputs "static"))
+ (lib (string-append static "/lib"))
+ (incl (string-append static "/include/aiger")))
+ (mkdir-p lib)
+ (mkdir-p incl)
+ (install-file "libaiger.a" lib)
+ (for-each (lambda (f) (install-file f incl))
+ (find-files "." "\\.h$"))))))))
+ (inputs (list gzip))
+ (home-page "http://fmv.jku.at/aiger")
+ (synopsis "Utilities for And-Inverter Graphs")
+ (description "AIGER is a format, library and set of utilities for
+@acronym{AIG, And-Inverter Graphs}s. The focus is on conversion utilities and a
+generic reader and writer API.")
+ (license (list license:expat
+ license:bsd-3)))) ; blif2aig
+
(define-public libqalculate
(package
(name "libqalculate")
--
2.38.0
guix-patches <at> gnu.org:bug#57181; Package guix-patches.
(Sat, 15 Oct 2022 14:56:03 GMT) Full text and rfc822 format available.Message #32 received at 57181 <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: 57181 <at> debbugs.gnu.org Cc: mail <at> maxheisinger.at Subject: [PATCH v2 3/4] gnu: Add louvain-community. Date: Sat, 15 Oct 2022 16:46:40 +0200
* gnu/packages/maths.scm (louvain-community): New variable.
---
gnu/packages/maths.scm | 31 +++++++++++++++++++++++++++++++
1 file changed, 31 insertions(+)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 5c8a0fe2ef..58faa6674b 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -7511,6 +7511,37 @@ (define-public lingeling
also included.")
(license license:expat))))
+(define-public louvain-community
+ (let ((commit "8cc5382d4844af127b1c1257373740d7e6b76f1e")
+ (revision "1"))
+ (package
+ (name "louvain-community")
+ (version (git-version "1.0.0" revision commit))
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/meelgroup/louvain-community")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "1ss00hkdvr9bdkd355hxf8zd7xycb3nm8qpy7s75gjjf6yng0bfj"))))
+ (build-system cmake-build-system)
+ (arguments
+ (list #:tests? #f ; tests appear to require missing files
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'unpack 'encode-git-hash
+ (lambda _
+ (substitute* "CMakeLists.txt"
+ (("GIT-hash-notfound") #$commit)))))))
+ (native-inputs (list python))
+ (home-page "https://github.com/meelgroup/louvain-communities")
+ (synopsis "Multi-criteria community detection")
+ (description "This package provides a C++ implementation of the Louvain
+community detection algorithm.")
+ (license license:lgpl3+))))
+
(define-public libqalculate
(package
(name "libqalculate")
--
2.38.0
guix-patches <at> gnu.org:bug#57181; Package guix-patches.
(Sat, 15 Oct 2022 14:56:03 GMT) Full text and rfc822 format available.Message #35 received at 57181 <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: 57181 <at> debbugs.gnu.org Cc: mail <at> maxheisinger.at Subject: [PATCH v2 4/4] gnu: Add cryptominisat. Date: Sat, 15 Oct 2022 16:47:03 +0200
* gnu/packages/maths.scm (cryptominisat): New variable.
Co-authored-by: Maximilian Heisinger <mail <at> maxheisinger.at>
---
gnu/packages/maths.scm | 51 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 51 insertions(+)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 58faa6674b..9db28239fd 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -56,6 +56,7 @@
;;; Copyright © 2022 Marek Felšöci <marek <at> felsoci.sk>
;;; Copyright © 2022 vicvbcun <guix <at> ikherbers.com>
;;; Copyright © 2022 Liliana Marie Prikler <liliana.prikler <at> gmail.com>
+;;; Copyright © 2022 Maximilian Heisinger <mail <at> maxheisinger.at>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -159,6 +160,7 @@ (define-module (gnu packages maths)
#:use-module (gnu packages serialization)
#:use-module (gnu packages shells)
#:use-module (gnu packages sphinx)
+ #:use-module (gnu packages sqlite)
#:use-module (gnu packages swig)
#:use-module (gnu packages tcl)
#:use-module (gnu packages texinfo)
@@ -7542,6 +7544,55 @@ (define-public louvain-community
community detection algorithm.")
(license license:lgpl3+))))
+(define-public cryptominisat
+ (package
+ (name "cryptominisat")
+ (version "5.11.4")
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/msoos/cryptominisat")
+ (commit version)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "1izjn44phjp9670s7bxrdx4p0r59idqwv3bm6sr0qnlqlha5z4zc"))))
+ (build-system cmake-build-system)
+ (arguments
+ (list
+ #:build-type "Release"
+ #:test-target "test"
+ #:configure-flags #~(list "-DENABLE_TESTING=ON" "-DSTATS=ON")
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'unpack 'patch-source
+ (lambda* (#:key inputs #:allow-other-keys)
+ (substitute* "CMakeLists.txt"
+ (("add_subdirectory\\(utils/lingeling-ala\\)") ""))
+ ;; Transitively included in vendored gtest.h. Fixed in
+ ;; upstream:
+ ;; https://github.com/msoos/cryptominisat/pull/686
+ (substitute* "tests/assump_test.cpp"
+ (("#include <vector>")
+ "#include <vector>\n#include <algorithm>"))
+ (substitute* "tests/CMakeLists.txt"
+ (("add_subdirectory\\(\\$\\{GTEST_PREFIX\\} gtest\\)")
+ "find_package(GTest REQUIRED)")
+ (("add_subdirectory\\(\\$\\{PROJECT_SOURCE_DIR\\}/utils/.*\\)")
+ "")))))))
+ (inputs (list boost louvain-community python python-numpy sqlite zlib))
+ (native-inputs (list googletest lingeling python python-wrapper python-lit))
+ (synopsis "Incremental SAT solver")
+ (description
+ "CryptoMiniSat is an incremental SAT solver with both command line and
+library (C++, C, Python) interfaces. The command-line interface takes a
+@acronym{CNF, Conjunctive Normal Form} as an input in the DIMACS format with
+the extension of XOR clauses. The library interfaces mimic this and also
+allow incremental solving, including assumptions.")
+ (home-page "https://github.com/msoos/cryptominisat")
+ (license license:expat)))
+
(define-public libqalculate
(package
(name "libqalculate")
--
2.38.0
Liliana Marie Prikler <liliana.prikler <at> gmail.com>:Maximilian Heisinger <mail <at> maxheisinger.at>:Message #40 received at 57181-done <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: 57181-done <at> debbugs.gnu.org Cc: mail <at> maxheisinger.at Subject: Re: [PATCH v2 4/4] gnu: Add cryptominisat. Date: Sat, 26 Nov 2022 14:15:35 +0100
Am Samstag, dem 15.10.2022 um 16:47 +0200 schrieb Liliana Marie Prikler: > * gnu/packages/maths.scm (cryptominisat): New variable. > > Co-authored-by: Maximilian Heisinger <mail <at> maxheisinger.at> Aaaand it's pushed.
guix-patches <at> gnu.org:bug#57181; Package guix-patches.
(Sun, 27 Nov 2022 17:53:02 GMT) Full text and rfc822 format available.Message #43 received at 57181 <at> debbugs.gnu.org (full text, mbox):
From: Maximilian Heisinger <mail <at> maxheisinger.at> To: Liliana Marie Prikler <liliana.prikler <at> gmail.com>, "57181 <at> debbugs.gnu.org" <57181 <at> debbugs.gnu.org> Subject: Re: [PATCH v2 4/4] gnu: Add cryptominisat. Date: Sun, 27 Nov 2022 18:48:37 +0100 (CET)
[Message part 1 (text/plain, inline)]
> Liliana Marie Prikler <liliana.prikler <at> gmail.com> hat am 26.11.2022 14:15 CET geschrieben: > > Aaaand it's pushed. Thank you so much! Sorry for not working on the patch in the meantime, I started doing this while at a conference and was completely wrapped up in other issues and some deadlines after coming back... This is a beautiful patch series and I am looking forward to being able to coming up with such constructs myself. Integrating libraries like this is really interesting and opens up quite a few possibilities for research, especially with preserving old releases and making them comparable. Thanks again, and I'm looking forward to future submissions! They will be bottom-up next time :) Best regards, Max
[signature.asc (application/pgp-signature, attachment)]
Debbugs Internal Request <help-debbugs <at> gnu.org>
to internal_control <at> debbugs.gnu.org.
(Mon, 26 Dec 2022 12:24:11 GMT) Full text and rfc822 format available.
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997,2003 nCipher Corporation Ltd,
1994-97 Ian Jackson.