[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[bug#57181] [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and
From: |
Liliana Marie Prikler |
Subject: |
[bug#57181] [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat |
Date: |
Mon, 15 Aug 2022 00:07:42 +0200 |
User-agent: |
Evolution 3.42.1 |
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