Package: guix-patches;
Reported by: soeren <at> soeren-tempel.net
Date: Sun, 4 May 2025 17:38:05 UTC
Severity: normal
Tags: patch
Done: Andreas Enge <andreas <at> enge.fr>
To reply to this bug, email your comments to 78246 AT debbugs.gnu.org.
There is no need to reopen the bug first.
Toggle the display of automated, internal messages from the tracker.
View this report as an mbox folder, status mbox, maintainer mbox
andreas <at> enge.fr, bavier <at> posteo.net, sharlatanus <at> gmail.com, guix-patches <at> gnu.org:bug#78246; Package guix-patches.
(Sun, 04 May 2025 17:38:05 GMT) Full text and rfc822 format available.soeren <at> soeren-tempel.net:andreas <at> enge.fr, bavier <at> posteo.net, sharlatanus <at> gmail.com, guix-patches <at> gnu.org.
(Sun, 04 May 2025 17:38:05 GMT) Full text and rfc822 format available.Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):
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
andreas <at> enge.fr, bavier <at> posteo.net, sharlatanus <at> gmail.com, guix-patches <at> gnu.org:bug#78246; Package guix-patches.
(Sun, 04 May 2025 17:41:02 GMT) Full text and rfc822 format available.Message #8 received at 78246 <at> debbugs.gnu.org (full text, mbox):
From: soeren <at> soeren-tempel.net To: 78246 <at> debbugs.gnu.org Subject: [PATCH 1/3] gnu: cadical: also install C++ header file to /usr/include Date: Sun, 4 May 2025 19:40:26 +0200
From: Sören Tempel <soeren <at> soeren-tempel.net>
* gnu/packages/maths.scm (cadical)[arguments]: Install cadical.hpp.
---
gnu/packages/maths.scm | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index eb23a375b4..53f726f620 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9840,7 +9840,7 @@ (define-public cadical
#:install-plan
`(("build" "bin" #:include ("cadical" "mobical"))
("build" "lib" #:include-regexp ("libcadical\\.(a|so)$"))
- ("src" "include" #:include ("cadical.h"))
+ ("src" "include" #:include ("cadical.h" "cadical.hpp"))
;; Internal headers used by cadiback.
("src" "include/cadical" #:include-regexp ("\\.hpp$")))
args))))))
andreas <at> enge.fr, bavier <at> posteo.net, sharlatanus <at> gmail.com, guix-patches <at> gnu.org:bug#78246; Package guix-patches.
(Sun, 04 May 2025 17:41:02 GMT) Full text and rfc822 format available.Message #11 received at 78246 <at> debbugs.gnu.org (full text, mbox):
From: soeren <at> soeren-tempel.net To: 78246 <at> debbugs.gnu.org Subject: [PATCH 2/3] gnu: Add symfpu. Date: Sun, 4 May 2025 19:40:27 +0200
From: Sören Tempel <soeren <at> soeren-tempel.net>
* gnu/packages/maths.scm (symfpu): New variable.
---
gnu/packages/maths.scm | 56 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 56 insertions(+)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 53f726f620..572912ca82 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -8218,6 +8218,62 @@ (define-public yices
s-expression-based format.")
(license license:gpl3+)))
+(define-public symfpu
+ (let ((commit "22d993d880f66b2e470c3928e0e61bdf61419702"))
+ (package
+ (name "symfpu")
+ (version (git-version "20220910" "0" commit))
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/martin-cs/symfpu")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "1h20zzkyi225290kc6mzg8i4dwkj0p1vlwfgc9ycs61snlyd8gr8"))))
+ (build-system copy-build-system)
+ (arguments
+ (list
+ #:phases
+ #~(modify-phases %standard-phases
+ (delete 'configure)
+ (replace 'install
+ (lambda* (#:key outputs #:allow-other-keys)
+ (let* ((outdir (assoc-ref outputs "out"))
+ (incdir (string-append outdir "/include/symfpu"))
+ (libdir (string-append outdir "/lib"))
+
+ (coredir (string-append incdir "/core"))
+ (utilsdir (string-append incdir "/utils")))
+ (mkdir-p coredir)
+ (mkdir-p utilsdir)
+ (copy-recursively "core" coredir)
+ (copy-recursively "utils" utilsdir)
+ (mkdir-p (string-append libdir "/pkgconfig"))
+ (with-output-to-file (string-append libdir
+ "/pkgconfig/symfpu.pc")
+ (lambda _
+ (format #t
+ "prefix=~a~@
+ exec_prefix=${prefix}~@
+ includedir=${prefix}/include~@
+ ~@
+ ~@
+ Name: symfpu~@
+ Version: ~a~@
+ Description: library for IEEE-754 floats~@
+ Cflags: -I${includedir}~%"
+ outdir
+ #$version)))))))))
+ (synopsis
+ "Concrete and symbolic implementation of IEEE-754 floating-point numbers")
+ (description
+ "This library provides a C++ implementation of concrete and symbolic semantics
+for floating point numbers as defined in IEEE Standard for Floating-Point Arithmetic.")
+ (home-page "https://github.com/martin-cs/symfpu")
+ (license license:gpl3))))
+
(define-public z3
(package
(name "z3")
andreas <at> enge.fr, bavier <at> posteo.net, sharlatanus <at> gmail.com, guix-patches <at> gnu.org:bug#78246; Package guix-patches.
(Sun, 04 May 2025 17:41:03 GMT) Full text and rfc822 format available.Message #14 received at 78246 <at> debbugs.gnu.org (full text, mbox):
From: soeren <at> soeren-tempel.net To: 78246 <at> debbugs.gnu.org Subject: [PATCH 3/3] gnu: Add bitwuzla. Date: Sun, 4 May 2025 19:40:28 +0200
From: Sören Tempel <soeren <at> soeren-tempel.net>
* gnu/packages/maths.scm (bitwuzla): New variable.
---
gnu/packages/maths.scm | 38 ++++++++++++++++++++++++++++++++++++++
1 file changed, 38 insertions(+)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 572912ca82..09ce6bcb7c 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -8274,6 +8274,44 @@ (define-public symfpu
(home-page "https://github.com/martin-cs/symfpu")
(license license:gpl3))))
+(define-public bitwuzla
+ (package
+ (name "bitwuzla")
+ (version "0.7.0")
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/bitwuzla/bitwuzla")
+ (commit version)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "1fpd1kgb5xdbcjiqbbc6j0b8g2ly9bp9m3la78fiayl4qlmsvh2b"))))
+ (build-system meson-build-system)
+ (arguments
+ `(#:configure-flags '("-Dtesting=enabled" "-Ddefault_library=shared"
+ "-Dkissat=true")
+ #:phases (modify-phases %standard-phases
+ (add-after 'unpack 'make-git-optional
+ (lambda _
+ (substitute* "src/meson.build"
+ (("run_command\\('git',")
+ "run_command('sh', '-c', 'git',")))))))
+ (native-inputs (list pkg-config
+ googletest
+ python
+ gmp
+ cadical
+ symfpu
+ kissat))
+ (synopsis "SMT solver optimized for the theory of bit-vectors")
+ (description
+ "@acronym{SMT, Satisfiability Modulo Theories} solver for the
+theories of fixed-size bit-vectors, floating-point arithmetic, arrays,
+uninterpreted functions and their combinations.")
+ (home-page "https://bitwuzla.github.io/")
+ (license license:expat)))
+
(define-public z3
(package
(name "z3")
guix-patches <at> gnu.org:bug#78246; Package guix-patches.
(Mon, 05 May 2025 07:34:01 GMT) Full text and rfc822 format available.Message #17 received at 78246 <at> debbugs.gnu.org (full text, mbox):
From: Liliana Marie Prikler <liliana.prikler <at> gmail.com> To: soeren <at> soeren-tempel.net, 78246 <at> debbugs.gnu.org Subject: Re: [PATCH 2/3] gnu: Add symfpu. Date: Mon, 05 May 2025 09:32:58 +0200
Am Sonntag, dem 04.05.2025 um 19:40 +0200 schrieb
soeren <at> soeren-tempel.net:
> From: Sören Tempel <soeren <at> soeren-tempel.net>
>
> * gnu/packages/maths.scm (symfpu): New variable.
> ---
> gnu/packages/maths.scm | 56
> ++++++++++++++++++++++++++++++++++++++++++
> 1 file changed, 56 insertions(+)
>
> diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
> index 53f726f620..572912ca82 100644
> --- a/gnu/packages/maths.scm
> +++ b/gnu/packages/maths.scm
> @@ -8218,6 +8218,62 @@ (define-public yices
> s-expression-based format.")
> (license license:gpl3+)))
>
> +(define-public symfpu
> + (let ((commit "22d993d880f66b2e470c3928e0e61bdf61419702"))
Commit and revision should both be let-bound.
> + (package
> + (name "symfpu")
> + (version (git-version "20220910" "0" commit))
Whence cometh the base version?
> + (source
> + (origin
> + (method git-fetch)
> + (uri (git-reference
> + (url "https://github.com/martin-cs/symfpu")
> + (commit commit)))
> + (file-name (git-file-name name version))
> + (sha256
> + (base32
> "1h20zzkyi225290kc6mzg8i4dwkj0p1vlwfgc9ycs61snlyd8gr8"))))
> + (build-system copy-build-system)
> + (arguments
> + (list
> + #:phases
> + #~(modify-phases %standard-phases
> + (delete 'configure)
> + (replace 'install
> + (lambda* (#:key outputs #:allow-other-keys)
> + (let* ((outdir (assoc-ref outputs "out"))
> + (incdir (string-append outdir
> "/include/symfpu"))
> + (libdir (string-append outdir "/lib"))
> +
> + (coredir (string-append incdir "/core"))
> + (utilsdir (string-append incdir "/utils")))
> + (mkdir-p coredir)
> + (mkdir-p utilsdir)
> + (copy-recursively "core" coredir)
> + (copy-recursively "utils" utilsdir)
This should be an install plan.
> + (mkdir-p (string-append libdir "/pkgconfig"))
> + (with-output-to-file (string-append libdir
> +
> "/pkgconfig/symfpu.pc")
> + (lambda _
> + (format #t
> + "prefix=~a~@
> + exec_prefix=${prefix}~@
> + includedir=${prefix}/include~@
> + ~@
> + ~@
> + Name: symfpu~@
> + Version: ~a~@
> + Description: library for IEEE-754 floats~@
> + Cflags: -I${includedir}~%"
> + outdir
> + #$version)))))))))
Consider writing this to the current directory and refering to it in
the install plan.
> + (synopsis
> + "Concrete and symbolic implementation of IEEE-754 floating-
> point numbers")
> + (description
> + "This library provides a C++ implementation of concrete and
> symbolic semantics
> +for floating point numbers as defined in IEEE Standard for Floating-
> Point Arithmetic.")
> + (home-page "https://github.com/martin-cs/symfpu")
> + (license license:gpl3))))
> +
Should probably be gpl3+
Cheers
andreas <at> enge.fr, bavier <at> posteo.net, sharlatanus <at> gmail.com, guix-patches <at> gnu.org:bug#78246; Package guix-patches.
(Mon, 05 May 2025 16:41:02 GMT) Full text and rfc822 format available.Message #20 received at 78246 <at> debbugs.gnu.org (full text, mbox):
From: soeren <at> soeren-tempel.net To: 78246 <at> debbugs.gnu.org Cc: liliana.prikler <at> gmail.com Subject: [PATCH v2] gnu: Add symfpu. Date: Mon, 5 May 2025 18:39:30 +0200
From: Sören Tempel <soeren <at> soeren-tempel.net>
* gnu/packages/maths.scm (symfpu): New variable.
---
Change since v2:
* Make revision let-bound
* Fix git-version
* Use an install-plan
* Change license to gpl3+
gnu/packages/maths.scm | 48 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 48 insertions(+)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index eb23a375b4..c139d46fee 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -8218,6 +8218,54 @@ (define-public yices
s-expression-based format.")
(license license:gpl3+)))
+(define-public symfpu
+ (let ((commit "22d993d880f66b2e470c3928e0e61bdf61419702")
+ (revision "0"))
+ (package
+ (name "symfpu")
+ (version (git-version "0" revision commit))
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/martin-cs/symfpu")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "1h20zzkyi225290kc6mzg8i4dwkj0p1vlwfgc9ycs61snlyd8gr8"))))
+ (build-system copy-build-system)
+ (arguments
+ (list
+ #:install-plan
+ #~`(("symfpu.pc" "lib/pkgconfig/symfpu.pc")
+ ("core" "include/symfpu/core")
+ ("utils" "include/symfpu/utils"))
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-before 'install 'build-pkgconfig
+ (lambda* (#:key outputs #:allow-other-keys)
+ (with-output-to-file "symfpu.pc"
+ (lambda _
+ (format #t
+ "prefix=~a~@
+ exec_prefix=${prefix}~@
+ includedir=${prefix}/include~@
+ ~@
+ ~@
+ Name: symfpu~@
+ Version: ~a~@
+ Description: library for IEEE-754 floats~@
+ Cflags: -I${includedir}~%"
+ (assoc-ref outputs "out")
+ #$version))))))))
+ (synopsis
+ "Concrete and symbolic implementation of IEEE-754 floating-point numbers")
+ (description
+ "This library provides a C++ implementation of concrete and symbolic semantics
+for floating point numbers as defined in IEEE Standard for Floating-Point Arithmetic.")
+ (home-page "https://github.com/martin-cs/symfpu")
+ (license license:gpl3+))))
+
(define-public z3
(package
(name "z3")
base-commit: 415e3d98d6faf5fd3d1b7b3daa2f20636e4ff822
Andreas Enge <andreas <at> enge.fr>:soeren <at> soeren-tempel.net:Message #25 received at 78246-done <at> debbugs.gnu.org (full text, mbox):
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
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997,2003 nCipher Corporation Ltd,
1994-97 Ian Jackson.