GNU bug report logs - #57181
[PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat

Previous Next

Full log

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

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.