GNU bug report logs - #78246
[PATCH 0/3] gnu: Add bitwuzla.

Previous Next

Full log

View this message in rfc822 format

From: help-debbugs <at> gnu.org (GNU bug Tracking System)
To: soeren <at> soeren-tempel.net
Subject: bug#78246: closed (Re: [PATCH v2] gnu: Add symfpu.)
Date: Wed, 14 May 2025 12:57:07 +0000

[Message part 1 (text/plain, inline)]

Your bug report

#78246: [PATCH 0/3] gnu: Add bitwuzla.

which was filed against the guix-patches package, has been closed.

The explanation is attached below, along with your original report.
If you require more details, please reply to 78246 <at> debbugs.gnu.org.

-- 
78246: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=78246
GNU Bug Tracking System
Contact help-debbugs <at> gnu.org with problems

[Message part 2 (message/rfc822, inline)]

From: Andreas Enge <andreas <at> enge.fr>
To: soeren <at> soeren-tempel.net
Cc: 78246-done <at> debbugs.gnu.org, liliana.prikler <at> gmail.com
Subject: Re: [PATCH v2] gnu: Add symfpu.
Date: Wed, 14 May 2025 14:56:40 +0200

Hello Sören,

thanks a lot for your patch, which I have modified a little bit and
pushed. Next time when you send a v2, could you send the complete patch
set, even those which have (seemingly) not changed? Here for instance
the bitwuzla patch did not apply any more as such, since the context had
changed (the previous line from symfpu ended in "gpl3+))))" instead of
"gpl3))))"). And I think this will also help QA to apply all patches of
the v2.

I have also expanded a bit the descriptions and in particular made them
full sentences. And added a copyright line for you.

For bitwuzla, many of the native-inputs should instead be just regular
inputs (rule of thumb: everything that is just needed during the build,
such as pkg-config for configuring or googletest for the tests, should
be native; when cross-compiling, it is run on the build machine;
whereas libraries against which the project is linked should be regular,
they will be used during, well, the use of the package).

(To be honest, I am not totally sure my split between native and normal
inputs is correct; maybe the header only library symfpu should be a
native input? I have also removed python as an input; the build works
without, and I did not see python related in the output.)

I am closing this issue; please feel free to reopen it if something does
not work as expected.

Andreas

[Message part 3 (message/rfc822, inline)]

From: soeren <at> soeren-tempel.net
To: guix-patches <at> gnu.org
Cc: liliana.prikler <at> gmail.com
Subject: [PATCH 0/3] gnu: Add bitwuzla.
Date: Sun,  4 May 2025 19:34:41 +0200

From: Sören Tempel <soeren <at> soeren-tempel.net>

This patchsets adds bitwuzla <https://bitwuzla.github.io/> an SMT solver
which is especially efficent for bitvector theory and can be used with
the already packaged BINSEC symbolic executor.

While packaging bitwuzla, I also noticed and fixed a bug regarding the
installed header files for cadical (CC: liliana.prikler@) and added a
package for symfpu, which is a dependency of bitwuzla.

Sören Tempel (3):
  gnu: cadical: also install C++ header file to /usr/include
  gnu: Add symfpu.
  gnu: Add bitwuzla.

 gnu/packages/maths.scm | 96 +++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 95 insertions(+), 1 deletion(-)


base-commit: 415e3d98d6faf5fd3d1b7b3daa2f20636e4ff822

Previous Next

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