Package: guix-patches;
Reported by: Zhu Zihao <all_but_last <at> 163.com>
Date: Mon, 20 Jun 2022 12:35:01 UTC
Severity: normal
Tags: patch
Done: Ludovic Courtès <ludo <at> gnu.org>
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 56107 in the body.
You can then email your comments to 56107 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#56107; Package guix-patches.
(Mon, 20 Jun 2022 12:35:01 GMT) Full text and rfc822 format available.Zhu Zihao <all_but_last <at> 163.com>:guix-patches <at> gnu.org.
(Mon, 20 Jun 2022 12:35:02 GMT) Full text and rfc822 format available.Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):
From: Zhu Zihao <all_but_last <at> 163.com> To: guix-patches <at> gnu.org Subject: [PATCH]: Update z3 to 4.8.17 and use cmake to build the package. Date: Mon, 20 Jun 2022 20:32:47 +0800
[Message part 1 (text/plain, inline)]
[signature.asc (application/pgp-signature, inline)]
[0001-gnu-z3-Use-G-expressions.patch (text/x-patch, inline)]
From a8ccfba4a1c5ef02618d81f3873912b28411092e Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last <at> 163.com>
Date: Mon, 20 Jun 2022 20:09:20 +0800
Subject: [PATCH 1/3] gnu: z3: Use G-expressions.
* gnu/packages/maths.scm (z3)[arguments]: Use G-expressions.
[native-inputs]: Use label-less style.
---
gnu/packages/maths.scm | 89 +++++++++++++++++++++---------------------
1 file changed, 45 insertions(+), 44 deletions(-)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 0ad14ba36e..b6d56e7467 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -50,6 +50,7 @@
;;; Copyright © 2021 Jean-Baptiste Volatier <jbv <at> pm.me>
;;; Copyright © 2021 Guillaume Le Vaillant <glv <at> posteo.net>
;;; Copyright © 2021 Pierre-Antoine Bouttier <pierre-antoine.bouttier <at> univ-grenoble-alpes.fr>
+;;; Copyright © 2022 Zhu Zihao <all_but_last <at> 163.com>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -5829,51 +5830,51 @@ (define-public z3
"1hnbzq10d23drd7ksm3c1n2611c3kd0q0yxgz8y78zaafwczvwxx"))))
(build-system gnu-build-system)
(arguments
- `(#:imported-modules ((guix build python-build-system)
- ,@%gnu-build-system-modules)
- #:modules (((guix build python-build-system) #:select (site-packages))
- (guix build gnu-build-system)
- (guix build utils))
- #:phases
- (modify-phases %standard-phases
- (add-after 'unpack 'enable-bytecode-determinism
- (lambda _
- (setenv "PYTHONHASHSEED" "0")
- #t))
- (add-after 'unpack 'fix-compatability
- ;; Versions after 4.8.3 have immintrin.h IFDEFed for Windows only.
- (lambda _
- (substitute* "src/util/mpz.cpp"
- (("#include <immintrin.h>") ""))
- #t))
- (add-before 'configure 'bootstrap
- (lambda _
- (invoke "python" "scripts/mk_make.py")))
- ;; work around gnu-build-system's setting --enable-fast-install
- ;; (z3's `configure' is a wrapper around the above python file,
- ;; which fails when passed --enable-fast-install)
- (replace 'configure
- (lambda* (#:key inputs outputs #:allow-other-keys)
- (invoke "./configure"
- "--python"
- (string-append "--prefix=" (assoc-ref outputs "out"))
- (string-append "--pypkgdir=" (site-packages inputs outputs)))))
- (add-after 'configure 'change-directory
- (lambda _
- (chdir "build")
- #t))
- (add-before 'check 'make-test-z3
- (lambda _
- ;; Build the test suite executable.
- (invoke "make" "test-z3" "-j"
- (number->string (parallel-job-count)))))
- (replace 'check
- (lambda _
- ;; Run all the tests that don't require arguments.
- (invoke "./test-z3" "/a"))))))
+ (list
+ #:imported-modules `((guix build python-build-system)
+ ,@%cmake-build-system-modules)
+ #:modules '((guix build cmake-build-system)
+ (guix build utils)
+ ((guix build python-build-system) #:select (site-packages)))
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'unpack 'enable-bytecode-determinism
+ (lambda _
+ (setenv "PYTHONHASHSEED" "0")
+ #t))
+ (add-after 'unpack 'fix-compatability
+ ;; Versions after 4.8.3 have immintrin.h IFDEFed for Windows only.
+ (lambda _
+ (substitute* "src/util/mpz.cpp"
+ (("#include <immintrin.h>") ""))
+ #t))
+ (add-before 'configure 'bootstrap
+ (lambda _
+ (invoke "python" "scripts/mk_make.py")))
+ ;; work around gnu-build-system's setting --enable-fast-install
+ ;; (z3's `configure' is a wrapper around the above python file,
+ ;; which fails when passed --enable-fast-install)
+ (replace 'configure
+ (lambda* (#:key inputs outputs #:allow-other-keys)
+ (invoke "./configure"
+ "--python"
+ (string-append "--prefix=" (assoc-ref outputs "out"))
+ (string-append "--pypkgdir=" (site-packages inputs outputs)))))
+ (add-after 'configure 'change-directory
+ (lambda _
+ (chdir "build")
+ #t))
+ (add-before 'check 'make-test-z3
+ (lambda _
+ ;; Build the test suite executable.
+ (invoke "make" "test-z3" "-j"
+ (number->string (parallel-job-count)))))
+ (replace 'check
+ (lambda _
+ ;; Run all the tests that don't require arguments.
+ (invoke "./test-z3" "/a"))))))
(native-inputs
- `(("which" ,which)
- ("python" ,python-wrapper)))
+ (list which python-wrapper))
(synopsis "Theorem prover")
(description "Z3 is a theorem prover and @dfn{satisfiability modulo
theories} (SMT) solver. It provides a C/C++ API, as well as Python bindings.")
--
2.36.1
[0002-gnu-z3-Update-to-4.8.17.patch (text/x-patch, inline)]
From 5ce1ec4c3c6d0a865645da9a6b0899f3596b5e3e Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last <at> 163.com>
Date: Mon, 20 Jun 2022 20:14:37 +0800
Subject: [PATCH 2/3] gnu: z3: Update to 4.8.17.
* gnu/packages/maths.scm (z3): Update to 4.8.17.
---
gnu/packages/maths.scm | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index b6d56e7467..2f1f731890 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -5818,7 +5818,7 @@ (define-public jacal
(define-public z3
(package
(name "z3")
- (version "4.8.9")
+ (version "4.8.17")
(home-page "https://github.com/Z3Prover/z3")
(source (origin
(method git-fetch)
@@ -5827,8 +5827,8 @@ (define-public z3
(file-name (git-file-name name version))
(sha256
(base32
- "1hnbzq10d23drd7ksm3c1n2611c3kd0q0yxgz8y78zaafwczvwxx"))))
(build-system gnu-build-system)
+ "1vvb09q7w7zd29qc4qjysrrhyylszm1wf6azkff004ixwn026b05"))))
(arguments
(list
#:imported-modules `((guix build python-build-system)
--
2.36.1
[0003-gnu-z3-Prefer-CMake-to-build-the-package.patch (text/x-patch, inline)]
From 6bd6bda66d40782e2f269001d9bc53e3bf8a153f Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last <at> 163.com>
Date: Mon, 20 Jun 2022 20:17:54 +0800
Subject: [PATCH 3/3] gnu: z3: Prefer CMake to build the package.
Z3 developer recommends to use CMake to build Z3 except the OCaml bindings.
Use CMake also enable us to cross compile z3.
* gnu/packages/maths.scm (z3)[build-system]: Use cmake-build-system.
[arguments]<#:configure-flags>: Add flags for CMake.
<#:phases>: Remove stale phase 'fix-compatability'.
In phase 'check', build the z3 test binary and don't test when cross
compiling.
Add phase 'compile-python-modules' phase to generate python bytecode cache for
z3 python binding.
Add phase 'fix-z3-library-path' to help z3 pythong binding to find the z3
shared library.
(ocaml-z3)[build-system]: Override the inherited value with 'gnu-build-system'.
---
gnu/packages/maths.scm | 64 ++++++++++++++++++++----------------------
1 file changed, 31 insertions(+), 33 deletions(-)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 2f1f731890..02809f5a63 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -5827,8 +5827,8 @@ (define-public z3
(file-name (git-file-name name version))
(sha256
(base32
- (build-system gnu-build-system)
"1vvb09q7w7zd29qc4qjysrrhyylszm1wf6azkff004ixwn026b05"))))
+ (build-system cmake-build-system)
(arguments
(list
#:imported-modules `((guix build python-build-system)
@@ -5836,43 +5836,40 @@ (define-public z3
#:modules '((guix build cmake-build-system)
(guix build utils)
((guix build python-build-system) #:select (site-packages)))
+ #:configure-flags
+ #~(list "-DZ3_BUILD_PYTHON_BINDINGS=ON"
+ "-DZ3_LINK_TIME_OPTIMIZATION=ON"
+ (string-append
+ "-DCMAKE_INSTALL_PYTHON_PKG_DIR="
+ #$output "/lib/python"
+ #$(version-major+minor (package-version python-wrapper))
+ "/site-packages"))
#:phases
#~(modify-phases %standard-phases
- (add-after 'unpack 'enable-bytecode-determinism
+ (replace 'check
+ (lambda* (#:key parallel-build? #:allow-other-keys)
+ (unless #$(%current-target-system)
+ (invoke "make" "test-z3"
+ (format #f "-j~a"
+ (if parallel-build?
+ (parallel-job-count)
+ 1)))
+ (invoke "./test-z3" "/a"))))
+ (add-after 'install 'compile-python-modules
(lambda _
(setenv "PYTHONHASHSEED" "0")
- #t))
- (add-after 'unpack 'fix-compatability
- ;; Versions after 4.8.3 have immintrin.h IFDEFed for Windows only.
- (lambda _
- (substitute* "src/util/mpz.cpp"
- (("#include <immintrin.h>") ""))
- #t))
- (add-before 'configure 'bootstrap
- (lambda _
- (invoke "python" "scripts/mk_make.py")))
- ;; work around gnu-build-system's setting --enable-fast-install
- ;; (z3's `configure' is a wrapper around the above python file,
- ;; which fails when passed --enable-fast-install)
- (replace 'configure
+
+ (invoke "python" "-m" "compileall"
+ "--invalidation-mode=unchecked-hash"
+ #$output)))
+ ;; This step is missing in the CMake build system, do it here.
+ (add-after 'compile-python-modules 'fix-z3-library-path
(lambda* (#:key inputs outputs #:allow-other-keys)
- (invoke "./configure"
- "--python"
- (string-append "--prefix=" (assoc-ref outputs "out"))
- (string-append "--pypkgdir=" (site-packages inputs outputs)))))
- (add-after 'configure 'change-directory
- (lambda _
- (chdir "build")
- #t))
- (add-before 'check 'make-test-z3
- (lambda _
- ;; Build the test suite executable.
- (invoke "make" "test-z3" "-j"
- (number->string (parallel-job-count)))))
- (replace 'check
- (lambda _
- ;; Run all the tests that don't require arguments.
- (invoke "./test-z3" "/a"))))))
+ (let* ((dest (string-append (site-packages inputs outputs)
+ "/z3/lib/libz3.so"))
+ (z3-lib (string-append #$output "/lib/libz3.so")))
+ (mkdir-p (dirname dest))
+ (symlink z3-lib dest)))))))
(native-inputs
(list which python-wrapper))
(synopsis "Theorem prover")
@@ -5884,6 +5881,7 @@ (define-public ocaml-z3
(package
(inherit z3)
(name "ocaml-z3")
+ (build-system gnu-build-system)
(arguments
`(#:imported-modules ((guix build python-build-system)
,@%gnu-build-system-modules)
--
2.36.1
[Message part 6 (text/plain, inline)]
-- Retrieve my PGP public key: gpg --recv-keys D47A9C8B2AE3905B563D9135BE42B352A9F6821F Zihao
guix-patches <at> gnu.org:bug#56107; Package guix-patches.
(Mon, 20 Jun 2022 12:55:01 GMT) Full text and rfc822 format available.Message #8 received at 56107 <at> debbugs.gnu.org (full text, mbox):
From: Maxime Devos <maximedevos <at> telenet.be> To: Zhu Zihao <all_but_last <at> 163.com>, 56107 <at> debbugs.gnu.org Subject: Re: [bug#56107] [PATCH]: Update z3 to 4.8.17 and use cmake to build the package. Date: Mon, 20 Jun 2022 14:54:30 +0200
[Message part 1 (text/plain, inline)]
Zhu Zihao schreef op ma 20-06-2022 om 20:32 [+0800]: > + (replace 'check > + (lambda* (#:key parallel-build? #:allow-other-keys) > + (unless #$(%current-target-system) That doesn't support --without-tests. I recommend doing the standard (when tests? [...]) construct instead, which supports the --without-tests package transformation and which will be accepted by "guix lint". Greetings, Maxime.
[signature.asc (application/pgp-signature, inline)]
guix-patches <at> gnu.org:bug#56107; Package guix-patches.
(Tue, 21 Jun 2022 08:18:02 GMT) Full text and rfc822 format available.Message #11 received at 56107 <at> debbugs.gnu.org (full text, mbox):
From: Zhu Zihao <all_but_last <at> 163.com> To: Maxime Devos <maximedevos <at> telenet.be> Cc: 56107 <at> debbugs.gnu.org Subject: Re: [bug#56107] [PATCH]: Update z3 to 4.8.17 and use cmake to build the package. Date: Tue, 21 Jun 2022 16:16:25 +0800
[Message part 1 (text/plain, inline)]
Thanks, patches updated.
[signature.asc (application/pgp-signature, inline)]
[0001-gnu-z3-Use-G-expressions.patch (text/x-patch, inline)]
From a8ccfba4a1c5ef02618d81f3873912b28411092e Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last <at> 163.com>
Date: Mon, 20 Jun 2022 20:09:20 +0800
Subject: [PATCH 1/3] gnu: z3: Use G-expressions.
* gnu/packages/maths.scm (z3)[arguments]: Use G-expressions.
[native-inputs]: Use label-less style.
---
gnu/packages/maths.scm | 89 +++++++++++++++++++++---------------------
1 file changed, 45 insertions(+), 44 deletions(-)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 0ad14ba36e..b6d56e7467 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -50,6 +50,7 @@
;;; Copyright © 2021 Jean-Baptiste Volatier <jbv <at> pm.me>
;;; Copyright © 2021 Guillaume Le Vaillant <glv <at> posteo.net>
;;; Copyright © 2021 Pierre-Antoine Bouttier <pierre-antoine.bouttier <at> univ-grenoble-alpes.fr>
+;;; Copyright © 2022 Zhu Zihao <all_but_last <at> 163.com>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -5829,51 +5830,51 @@ (define-public z3
"1hnbzq10d23drd7ksm3c1n2611c3kd0q0yxgz8y78zaafwczvwxx"))))
(build-system gnu-build-system)
(arguments
- `(#:imported-modules ((guix build python-build-system)
- ,@%gnu-build-system-modules)
- #:modules (((guix build python-build-system) #:select (site-packages))
- (guix build gnu-build-system)
- (guix build utils))
- #:phases
- (modify-phases %standard-phases
- (add-after 'unpack 'enable-bytecode-determinism
- (lambda _
- (setenv "PYTHONHASHSEED" "0")
- #t))
- (add-after 'unpack 'fix-compatability
- ;; Versions after 4.8.3 have immintrin.h IFDEFed for Windows only.
- (lambda _
- (substitute* "src/util/mpz.cpp"
- (("#include <immintrin.h>") ""))
- #t))
- (add-before 'configure 'bootstrap
- (lambda _
- (invoke "python" "scripts/mk_make.py")))
- ;; work around gnu-build-system's setting --enable-fast-install
- ;; (z3's `configure' is a wrapper around the above python file,
- ;; which fails when passed --enable-fast-install)
- (replace 'configure
- (lambda* (#:key inputs outputs #:allow-other-keys)
- (invoke "./configure"
- "--python"
- (string-append "--prefix=" (assoc-ref outputs "out"))
- (string-append "--pypkgdir=" (site-packages inputs outputs)))))
- (add-after 'configure 'change-directory
- (lambda _
- (chdir "build")
- #t))
- (add-before 'check 'make-test-z3
- (lambda _
- ;; Build the test suite executable.
- (invoke "make" "test-z3" "-j"
- (number->string (parallel-job-count)))))
- (replace 'check
- (lambda _
- ;; Run all the tests that don't require arguments.
- (invoke "./test-z3" "/a"))))))
+ (list
+ #:imported-modules `((guix build python-build-system)
+ ,@%cmake-build-system-modules)
+ #:modules '((guix build cmake-build-system)
+ (guix build utils)
+ ((guix build python-build-system) #:select (site-packages)))
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'unpack 'enable-bytecode-determinism
+ (lambda _
+ (setenv "PYTHONHASHSEED" "0")
+ #t))
+ (add-after 'unpack 'fix-compatability
+ ;; Versions after 4.8.3 have immintrin.h IFDEFed for Windows only.
+ (lambda _
+ (substitute* "src/util/mpz.cpp"
+ (("#include <immintrin.h>") ""))
+ #t))
+ (add-before 'configure 'bootstrap
+ (lambda _
+ (invoke "python" "scripts/mk_make.py")))
+ ;; work around gnu-build-system's setting --enable-fast-install
+ ;; (z3's `configure' is a wrapper around the above python file,
+ ;; which fails when passed --enable-fast-install)
+ (replace 'configure
+ (lambda* (#:key inputs outputs #:allow-other-keys)
+ (invoke "./configure"
+ "--python"
+ (string-append "--prefix=" (assoc-ref outputs "out"))
+ (string-append "--pypkgdir=" (site-packages inputs outputs)))))
+ (add-after 'configure 'change-directory
+ (lambda _
+ (chdir "build")
+ #t))
+ (add-before 'check 'make-test-z3
+ (lambda _
+ ;; Build the test suite executable.
+ (invoke "make" "test-z3" "-j"
+ (number->string (parallel-job-count)))))
+ (replace 'check
+ (lambda _
+ ;; Run all the tests that don't require arguments.
+ (invoke "./test-z3" "/a"))))))
(native-inputs
- `(("which" ,which)
- ("python" ,python-wrapper)))
+ (list which python-wrapper))
(synopsis "Theorem prover")
(description "Z3 is a theorem prover and @dfn{satisfiability modulo
theories} (SMT) solver. It provides a C/C++ API, as well as Python bindings.")
--
2.36.1
[0002-gnu-z3-Update-to-4.8.17.patch (text/x-patch, inline)]
From 5ce1ec4c3c6d0a865645da9a6b0899f3596b5e3e Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last <at> 163.com>
Date: Mon, 20 Jun 2022 20:14:37 +0800
Subject: [PATCH 2/3] gnu: z3: Update to 4.8.17.
* gnu/packages/maths.scm (z3): Update to 4.8.17.
---
gnu/packages/maths.scm | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index b6d56e7467..2f1f731890 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -5818,7 +5818,7 @@ (define-public jacal
(define-public z3
(package
(name "z3")
- (version "4.8.9")
+ (version "4.8.17")
(home-page "https://github.com/Z3Prover/z3")
(source (origin
(method git-fetch)
@@ -5827,8 +5827,8 @@ (define-public z3
(file-name (git-file-name name version))
(sha256
(base32
- "1hnbzq10d23drd7ksm3c1n2611c3kd0q0yxgz8y78zaafwczvwxx"))))
(build-system gnu-build-system)
+ "1vvb09q7w7zd29qc4qjysrrhyylszm1wf6azkff004ixwn026b05"))))
(arguments
(list
#:imported-modules `((guix build python-build-system)
--
2.36.1
[0003-gnu-z3-Prefer-CMake-to-build-the-package.patch (text/x-patch, inline)]
From e1df674d84fe5a26a343a2ea68ea961d045dffe8 Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last <at> 163.com>
Date: Mon, 20 Jun 2022 20:17:54 +0800
Subject: [PATCH 3/3] gnu: z3: Prefer CMake to build the package.
Z3 developer recommends to use CMake to build Z3 except the OCaml bindings.
Use CMake also enable us to cross compile z3.
* gnu/packages/maths.scm (z3)[build-system]: Use cmake-build-system.
[arguments]<#:configure-flags>: Add flags for CMake.
<#:phases>: Remove stale phase 'fix-compatability'.
In phase 'check', build the z3 test binary and don't test when cross
compiling.
Add phase 'compile-python-modules' phase to generate python bytecode cache for
z3 python binding.
Add phase 'fix-z3-library-path' to help z3 pythong binding to find the z3
shared library.
(ocaml-z3)[build-system]: Override the inherited value with 'gnu-build-system'.
---
gnu/packages/maths.scm | 64 ++++++++++++++++++++----------------------
1 file changed, 31 insertions(+), 33 deletions(-)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 2f1f731890..a73dfdb809 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -5827,8 +5827,8 @@ (define-public z3
(file-name (git-file-name name version))
(sha256
(base32
- (build-system gnu-build-system)
"1vvb09q7w7zd29qc4qjysrrhyylszm1wf6azkff004ixwn026b05"))))
+ (build-system cmake-build-system)
(arguments
(list
#:imported-modules `((guix build python-build-system)
@@ -5836,43 +5836,40 @@ (define-public z3
#:modules '((guix build cmake-build-system)
(guix build utils)
((guix build python-build-system) #:select (site-packages)))
+ #:configure-flags
+ #~(list "-DZ3_BUILD_PYTHON_BINDINGS=ON"
+ "-DZ3_LINK_TIME_OPTIMIZATION=ON"
+ (string-append
+ "-DCMAKE_INSTALL_PYTHON_PKG_DIR="
+ #$output "/lib/python"
+ #$(version-major+minor (package-version python-wrapper))
+ "/site-packages"))
#:phases
#~(modify-phases %standard-phases
- (add-after 'unpack 'enable-bytecode-determinism
+ (replace 'check
+ (lambda* (#:key parallel-build? tests? #:allow-other-keys)
+ (when tests?
+ (invoke "make" "test-z3"
+ (format #f "-j~a"
+ (if parallel-build?
+ (parallel-job-count)
+ 1)))
+ (invoke "./test-z3" "/a"))))
+ (add-after 'install 'compile-python-modules
(lambda _
(setenv "PYTHONHASHSEED" "0")
- #t))
- (add-after 'unpack 'fix-compatability
- ;; Versions after 4.8.3 have immintrin.h IFDEFed for Windows only.
- (lambda _
- (substitute* "src/util/mpz.cpp"
- (("#include <immintrin.h>") ""))
- #t))
- (add-before 'configure 'bootstrap
- (lambda _
- (invoke "python" "scripts/mk_make.py")))
- ;; work around gnu-build-system's setting --enable-fast-install
- ;; (z3's `configure' is a wrapper around the above python file,
- ;; which fails when passed --enable-fast-install)
- (replace 'configure
+
+ (invoke "python" "-m" "compileall"
+ "--invalidation-mode=unchecked-hash"
+ #$output)))
+ ;; This step is missing in the CMake build system, do it here.
+ (add-after 'compile-python-modules 'fix-z3-library-path
(lambda* (#:key inputs outputs #:allow-other-keys)
- (invoke "./configure"
- "--python"
- (string-append "--prefix=" (assoc-ref outputs "out"))
- (string-append "--pypkgdir=" (site-packages inputs outputs)))))
- (add-after 'configure 'change-directory
- (lambda _
- (chdir "build")
- #t))
- (add-before 'check 'make-test-z3
- (lambda _
- ;; Build the test suite executable.
- (invoke "make" "test-z3" "-j"
- (number->string (parallel-job-count)))))
- (replace 'check
- (lambda _
- ;; Run all the tests that don't require arguments.
- (invoke "./test-z3" "/a"))))))
+ (let* ((dest (string-append (site-packages inputs outputs)
+ "/z3/lib/libz3.so"))
+ (z3-lib (string-append #$output "/lib/libz3.so")))
+ (mkdir-p (dirname dest))
+ (symlink z3-lib dest)))))))
(native-inputs
(list which python-wrapper))
(synopsis "Theorem prover")
@@ -5884,6 +5881,7 @@ (define-public ocaml-z3
(package
(inherit z3)
(name "ocaml-z3")
+ (build-system gnu-build-system)
(arguments
`(#:imported-modules ((guix build python-build-system)
,@%gnu-build-system-modules)
--
2.36.1
[Message part 6 (text/plain, inline)]
-- Retrieve my PGP public key: gpg --recv-keys D47A9C8B2AE3905B563D9135BE42B352A9F6821F Zihao
guix-patches <at> gnu.org:bug#56107; Package guix-patches.
(Sat, 02 Jul 2022 23:41:01 GMT) Full text and rfc822 format available.Message #14 received at 56107 <at> debbugs.gnu.org (full text, mbox):
From: Ludovic Courtès <ludo <at> gnu.org> To: Zhu Zihao <all_but_last <at> 163.com> Cc: 56107 <at> debbugs.gnu.org, Maxime Devos <maximedevos <at> telenet.be> Subject: Re: bug#56107: [PATCH]: Update z3 to 4.8.17 and use cmake to build the package. Date: Sun, 03 Jul 2022 01:40:27 +0200
Hi! The series LGTM, but unfortunately the upgrade breaks one dependent, ‘solidity’: --8<---------------cut here---------------start------------->8--- --- SKIPPING ALL SEMANTICS TESTS --- Running 4839 test cases... 0% 10 20 30 40 50 60 70 80 90 100% |----|----|----|----|----|----|----|----|----|----| *********************************************/solidity/test/boostTest.cpp(114): error: in "smtCheckerTests/loops/while_loop_array_assignment_storage_storage": Test expectation mismatch. Expected result: Warning 6328: (290-309): CHC: Assertion violation happens here. Warning 6328: (313-332): CHC: Assertion violation happens here. Obtained result: Warning 6328: (290-309): CHC: Assertion violation happens here. Warning 6328: (313-332): CHC: Assertion violation happens here. Warning 4661: (266-286): BMC: Assertion violation happens here. /solidity/test/boostTest.cpp(114): error: in "smtCheckerTests/loops/for_1_false_positive": Test expectation mismatch. Expected result: Warning 2661: (176-181): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. Obtained result: Warning 2661: (176-181): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. Warning 4661: (296-309): BMC: Assertion violation happens here. */solidity/test/boostTest.cpp(114): error: in "smtCheckerTests/crypto/crypto_functions_compare_hashes": Test expectation mismatch. Expected result: Warning 6328: (183-197): CHC: Assertion violation happens here. Warning 6328: (201-215): CHC: Assertion violation happens here. Warning 6328: (219-233): CHC: Assertion violation happens here. Obtained result: Warning 1218: (183-197): CHC: Error trying to invoke SMT solver. Warning 1218: (201-215): CHC: Error trying to invoke SMT solver. Warning 1218: (219-233): CHC: Error trying to invoke SMT solver. Warning 4661: (183-197): BMC: Assertion violation happens here. Warning 4661: (201-215): BMC: Assertion violation happens here. Warning 4661: (219-233): BMC: Assertion violation happens here. /solidity/test/boostTest.cpp(114): error: in "smtCheckerTests/crypto/crypto_functions_not_same": Test expectation mismatch. Expected result: Warning 6328: (229-243): CHC: Assertion violation happens here. Obtained result: Warning 1218: (229-243): CHC: Error trying to invoke SMT solver. Warning 4661: (229-243): BMC: Assertion violation happens here. Warning 4661: (229-243): BMC: Assertion violation happens here. **/solidity/test/boostTest.cpp(114): error: in "smtCheckerTests/operators/compound_bitwise_or_uint_2": Test expectation mismatch. Expected result: Warning 7812: (173-192): BMC: Assertion violation might happen here. Obtained result: Warning 6328: (173-192): CHC: Assertion violation happens here. */solidity/test/boostTest.cpp(114): error: in "smtCheckerTests/operators/slice_default_start": Test expectation mismatch. Expected result: Warning 6328: (193-225): CHC: Assertion violation happens here. Warning 4661: (157-189): BMC: Assertion violation happens here. Obtained result: Warning 4661: (157-189): BMC: Assertion violation happens here. Warning 4661: (193-225): BMC: Assertion violation happens here. ** *** 6 failures are detected in the test module "SolidityTests" error: in phase 'check': uncaught exception: %exception #<&invoke-error program: "./scripts/tests.sh" arguments: () exit-status: 1 term-signal: #f stop-signal: #f> phase `check' failed after 656.5 seconds command "./scripts/tests.sh" failed with status 1 builder for `/gnu/store/g69say6c7vqvk15p8jark6l3m4k6z7bg-solidity-0.7.4.drv' failed with exit code 1 build of /gnu/store/g69say6c7vqvk15p8jark6l3m4k6z7bg-solidity-0.7.4.drv failed --8<---------------cut here---------------end--------------->8--- Thoughts? Ludo’.
guix-patches <at> gnu.org:bug#56107; Package guix-patches.
(Sun, 03 Jul 2022 09:46:01 GMT) Full text and rfc822 format available.Message #17 received at 56107 <at> debbugs.gnu.org (full text, mbox):
From: Zhu Zihao <all_but_last <at> 163.com> To: Ludovic Courtès <ludo <at> gnu.org> Cc: 56107 <at> debbugs.gnu.org, Maxime Devos <maximedevos <at> telenet.be> Subject: Re: bug#56107: [PATCH]: Update z3 to 4.8.17 and use cmake to build the package. Date: Sun, 03 Jul 2022 17:43:35 +0800
[Message part 1 (text/plain, inline)]
I update the solidity to 0.8.15 and now it can be built with z3 4.8.
[signature.asc (application/pgp-signature, inline)]
[0001-gnu-z3-Use-G-expressions.patch (text/x-patch, inline)]
From a8ccfba4a1c5ef02618d81f3873912b28411092e Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last <at> 163.com>
Date: Mon, 20 Jun 2022 20:09:20 +0800
Subject: [PATCH 1/6] gnu: z3: Use G-expressions.
* gnu/packages/maths.scm (z3)[arguments]: Use G-expressions.
[native-inputs]: Use label-less style.
---
gnu/packages/maths.scm | 89 +++++++++++++++++++++---------------------
1 file changed, 45 insertions(+), 44 deletions(-)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 0ad14ba36e..b6d56e7467 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -50,6 +50,7 @@
;;; Copyright © 2021 Jean-Baptiste Volatier <jbv <at> pm.me>
;;; Copyright © 2021 Guillaume Le Vaillant <glv <at> posteo.net>
;;; Copyright © 2021 Pierre-Antoine Bouttier <pierre-antoine.bouttier <at> univ-grenoble-alpes.fr>
+;;; Copyright © 2022 Zhu Zihao <all_but_last <at> 163.com>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -5829,51 +5830,51 @@ (define-public z3
"1hnbzq10d23drd7ksm3c1n2611c3kd0q0yxgz8y78zaafwczvwxx"))))
(build-system gnu-build-system)
(arguments
- `(#:imported-modules ((guix build python-build-system)
- ,@%gnu-build-system-modules)
- #:modules (((guix build python-build-system) #:select (site-packages))
- (guix build gnu-build-system)
- (guix build utils))
- #:phases
- (modify-phases %standard-phases
- (add-after 'unpack 'enable-bytecode-determinism
- (lambda _
- (setenv "PYTHONHASHSEED" "0")
- #t))
- (add-after 'unpack 'fix-compatability
- ;; Versions after 4.8.3 have immintrin.h IFDEFed for Windows only.
- (lambda _
- (substitute* "src/util/mpz.cpp"
- (("#include <immintrin.h>") ""))
- #t))
- (add-before 'configure 'bootstrap
- (lambda _
- (invoke "python" "scripts/mk_make.py")))
- ;; work around gnu-build-system's setting --enable-fast-install
- ;; (z3's `configure' is a wrapper around the above python file,
- ;; which fails when passed --enable-fast-install)
- (replace 'configure
- (lambda* (#:key inputs outputs #:allow-other-keys)
- (invoke "./configure"
- "--python"
- (string-append "--prefix=" (assoc-ref outputs "out"))
- (string-append "--pypkgdir=" (site-packages inputs outputs)))))
- (add-after 'configure 'change-directory
- (lambda _
- (chdir "build")
- #t))
- (add-before 'check 'make-test-z3
- (lambda _
- ;; Build the test suite executable.
- (invoke "make" "test-z3" "-j"
- (number->string (parallel-job-count)))))
- (replace 'check
- (lambda _
- ;; Run all the tests that don't require arguments.
- (invoke "./test-z3" "/a"))))))
+ (list
+ #:imported-modules `((guix build python-build-system)
+ ,@%cmake-build-system-modules)
+ #:modules '((guix build cmake-build-system)
+ (guix build utils)
+ ((guix build python-build-system) #:select (site-packages)))
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'unpack 'enable-bytecode-determinism
+ (lambda _
+ (setenv "PYTHONHASHSEED" "0")
+ #t))
+ (add-after 'unpack 'fix-compatability
+ ;; Versions after 4.8.3 have immintrin.h IFDEFed for Windows only.
+ (lambda _
+ (substitute* "src/util/mpz.cpp"
+ (("#include <immintrin.h>") ""))
+ #t))
+ (add-before 'configure 'bootstrap
+ (lambda _
+ (invoke "python" "scripts/mk_make.py")))
+ ;; work around gnu-build-system's setting --enable-fast-install
+ ;; (z3's `configure' is a wrapper around the above python file,
+ ;; which fails when passed --enable-fast-install)
+ (replace 'configure
+ (lambda* (#:key inputs outputs #:allow-other-keys)
+ (invoke "./configure"
+ "--python"
+ (string-append "--prefix=" (assoc-ref outputs "out"))
+ (string-append "--pypkgdir=" (site-packages inputs outputs)))))
+ (add-after 'configure 'change-directory
+ (lambda _
+ (chdir "build")
+ #t))
+ (add-before 'check 'make-test-z3
+ (lambda _
+ ;; Build the test suite executable.
+ (invoke "make" "test-z3" "-j"
+ (number->string (parallel-job-count)))))
+ (replace 'check
+ (lambda _
+ ;; Run all the tests that don't require arguments.
+ (invoke "./test-z3" "/a"))))))
(native-inputs
- `(("which" ,which)
- ("python" ,python-wrapper)))
+ (list which python-wrapper))
(synopsis "Theorem prover")
(description "Z3 is a theorem prover and @dfn{satisfiability modulo
theories} (SMT) solver. It provides a C/C++ API, as well as Python bindings.")
--
2.36.1
[0002-gnu-z3-Update-to-4.8.17.patch (text/x-patch, inline)]
From 5ce1ec4c3c6d0a865645da9a6b0899f3596b5e3e Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last <at> 163.com>
Date: Mon, 20 Jun 2022 20:14:37 +0800
Subject: [PATCH 2/6] gnu: z3: Update to 4.8.17.
* gnu/packages/maths.scm (z3): Update to 4.8.17.
---
gnu/packages/maths.scm | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index b6d56e7467..2f1f731890 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -5818,7 +5818,7 @@ (define-public jacal
(define-public z3
(package
(name "z3")
- (version "4.8.9")
+ (version "4.8.17")
(home-page "https://github.com/Z3Prover/z3")
(source (origin
(method git-fetch)
@@ -5827,8 +5827,8 @@ (define-public z3
(file-name (git-file-name name version))
(sha256
(base32
- "1hnbzq10d23drd7ksm3c1n2611c3kd0q0yxgz8y78zaafwczvwxx"))))
(build-system gnu-build-system)
+ "1vvb09q7w7zd29qc4qjysrrhyylszm1wf6azkff004ixwn026b05"))))
(arguments
(list
#:imported-modules `((guix build python-build-system)
--
2.36.1
[0003-gnu-z3-Prefer-CMake-to-build-the-package.patch (text/x-patch, inline)]
From e1df674d84fe5a26a343a2ea68ea961d045dffe8 Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last <at> 163.com>
Date: Mon, 20 Jun 2022 20:17:54 +0800
Subject: [PATCH 3/6] gnu: z3: Prefer CMake to build the package.
Z3 developer recommends to use CMake to build Z3 except the OCaml bindings.
Use CMake also enable us to cross compile z3.
* gnu/packages/maths.scm (z3)[build-system]: Use cmake-build-system.
[arguments]<#:configure-flags>: Add flags for CMake.
<#:phases>: Remove stale phase 'fix-compatability'.
In phase 'check', build the z3 test binary and don't test when cross
compiling.
Add phase 'compile-python-modules' phase to generate python bytecode cache for
z3 python binding.
Add phase 'fix-z3-library-path' to help z3 pythong binding to find the z3
shared library.
(ocaml-z3)[build-system]: Override the inherited value with 'gnu-build-system'.
---
gnu/packages/maths.scm | 64 ++++++++++++++++++++----------------------
1 file changed, 31 insertions(+), 33 deletions(-)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 2f1f731890..a73dfdb809 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -5827,8 +5827,8 @@ (define-public z3
(file-name (git-file-name name version))
(sha256
(base32
- (build-system gnu-build-system)
"1vvb09q7w7zd29qc4qjysrrhyylszm1wf6azkff004ixwn026b05"))))
+ (build-system cmake-build-system)
(arguments
(list
#:imported-modules `((guix build python-build-system)
@@ -5836,43 +5836,40 @@ (define-public z3
#:modules '((guix build cmake-build-system)
(guix build utils)
((guix build python-build-system) #:select (site-packages)))
+ #:configure-flags
+ #~(list "-DZ3_BUILD_PYTHON_BINDINGS=ON"
+ "-DZ3_LINK_TIME_OPTIMIZATION=ON"
+ (string-append
+ "-DCMAKE_INSTALL_PYTHON_PKG_DIR="
+ #$output "/lib/python"
+ #$(version-major+minor (package-version python-wrapper))
+ "/site-packages"))
#:phases
#~(modify-phases %standard-phases
- (add-after 'unpack 'enable-bytecode-determinism
+ (replace 'check
+ (lambda* (#:key parallel-build? tests? #:allow-other-keys)
+ (when tests?
+ (invoke "make" "test-z3"
+ (format #f "-j~a"
+ (if parallel-build?
+ (parallel-job-count)
+ 1)))
+ (invoke "./test-z3" "/a"))))
+ (add-after 'install 'compile-python-modules
(lambda _
(setenv "PYTHONHASHSEED" "0")
- #t))
- (add-after 'unpack 'fix-compatability
- ;; Versions after 4.8.3 have immintrin.h IFDEFed for Windows only.
- (lambda _
- (substitute* "src/util/mpz.cpp"
- (("#include <immintrin.h>") ""))
- #t))
- (add-before 'configure 'bootstrap
- (lambda _
- (invoke "python" "scripts/mk_make.py")))
- ;; work around gnu-build-system's setting --enable-fast-install
- ;; (z3's `configure' is a wrapper around the above python file,
- ;; which fails when passed --enable-fast-install)
- (replace 'configure
+
+ (invoke "python" "-m" "compileall"
+ "--invalidation-mode=unchecked-hash"
+ #$output)))
+ ;; This step is missing in the CMake build system, do it here.
+ (add-after 'compile-python-modules 'fix-z3-library-path
(lambda* (#:key inputs outputs #:allow-other-keys)
- (invoke "./configure"
- "--python"
- (string-append "--prefix=" (assoc-ref outputs "out"))
- (string-append "--pypkgdir=" (site-packages inputs outputs)))))
- (add-after 'configure 'change-directory
- (lambda _
- (chdir "build")
- #t))
- (add-before 'check 'make-test-z3
- (lambda _
- ;; Build the test suite executable.
- (invoke "make" "test-z3" "-j"
- (number->string (parallel-job-count)))))
- (replace 'check
- (lambda _
- ;; Run all the tests that don't require arguments.
- (invoke "./test-z3" "/a"))))))
+ (let* ((dest (string-append (site-packages inputs outputs)
+ "/z3/lib/libz3.so"))
+ (z3-lib (string-append #$output "/lib/libz3.so")))
+ (mkdir-p (dirname dest))
+ (symlink z3-lib dest)))))))
(native-inputs
(list which python-wrapper))
(synopsis "Theorem prover")
@@ -5884,6 +5881,7 @@ (define-public ocaml-z3
(package
(inherit z3)
(name "ocaml-z3")
+ (build-system gnu-build-system)
(arguments
`(#:imported-modules ((guix build python-build-system)
,@%gnu-build-system-modules)
--
2.36.1
[0004-gnu-solidity-Use-G-expressions.patch (text/x-patch, inline)]
From 7ec422d6f592a129f2e03fa57cfe3afb95febf29 Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last <at> 163.com>
Date: Sun, 3 Jul 2022 13:10:43 +0800
Subject: [PATCH 4/6] gnu: solidity: Use G-expressions.
* gnu/packages/solidity.scm (solidity)[arguments]: Use G-expressions.
[native-inputs]: Use label-less style inputs.
---
gnu/packages/solidity.scm | 69 ++++++++++++++++++++-------------------
1 file changed, 35 insertions(+), 34 deletions(-)
diff --git a/gnu/packages/solidity.scm b/gnu/packages/solidity.scm
index a5b5002ce8..606e078e42 100644
--- a/gnu/packages/solidity.scm
+++ b/gnu/packages/solidity.scm
@@ -1,4 +1,5 @@
;;; Copyright © 2020 Martin Becze <mjbecze <at> riseup.net>
+;;; Copyright © 2022 Zhu Zihao <all_but_last <at> 163.com>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -23,6 +24,7 @@ (define-module (gnu packages solidity)
#:use-module (gnu packages python)
#:use-module (gnu packages ncurses)
#:use-module (guix packages)
+ #:use-module (guix gexp)
#:use-module (guix git-download)
#:use-module (guix build-system cmake)
#:use-module ((guix licenses) #:prefix license:))
@@ -44,43 +46,42 @@ (define-public solidity
(base32 "1mswhjymiwnd3n7h3sjvjx5x8223yih0yvfcr0zpqr4aizpfx5z8"))))
(build-system cmake-build-system)
(arguments
- `(#:phases
- (modify-phases %standard-phases
- (add-after 'unpack 'create-commit_hash.txt
- (lambda _
- (with-output-to-file "commit_hash.txt"
- (lambda _
- (display
- (substring ,commit 0 8))))))
- (delete 'configure)
- (delete 'install)
- (replace 'build
- (lambda* (#:key outputs #:allow-other-keys)
- ;; Unbundle jsoncpp
- (delete-file "./cmake/jsoncpp.cmake")
- (substitute* "CMakeLists.txt"
- (("include\\(jsoncpp\\)") ""))
- ;; Bug list is always sorted since we only build releases
- (substitute* "./test/cmdlineTests.sh"
- (("\"\\$REPO_ROOT\"/scripts/update_bugs_by_version\\.py") ""))
- (substitute* "./scripts/build.sh"
- (("sudo\\ make\\ install") "make install")
- (("cmake\\ ..")
- (string-append "cmake .. -DCMAKE_INSTALL_PREFIX="
- (assoc-ref outputs "out"))))
- (setenv "CIRCLECI" "1")
- (invoke "./scripts/build.sh")
- #t))
- (replace 'check
- (lambda _
- (invoke "./scripts/tests.sh")
- #t)))))
+ (list
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'unpack 'create-commit_hash.txt
+ (lambda _
+ (with-output-to-file "commit_hash.txt"
+ (lambda _
+ (display
+ (substring #$commit 0 8))))))
+ (delete 'configure)
+ (delete 'install)
+ (replace 'build
+ (lambda* (#:key outputs #:allow-other-keys)
+ ;; Unbundle jsoncpp
+ (delete-file "./cmake/jsoncpp.cmake")
+ (substitute* "CMakeLists.txt"
+ (("include\\(jsoncpp\\)") ""))
+ ;; Bug list is always sorted since we only build releases
+ (substitute* "./test/cmdlineTests.sh"
+ (("\"\\$REPO_ROOT\"/scripts/update_bugs_by_version\\.py") ""))
+ (substitute* "./scripts/build.sh"
+ (("sudo\\ make\\ install") "make install")
+ (("cmake\\ ..")
+ (string-append "cmake .. -DCMAKE_INSTALL_PREFIX="
+ (assoc-ref outputs "out"))))
+ (setenv "CIRCLECI" "1")
+ (invoke "./scripts/build.sh")
+ #t))
+ (replace 'check
+ (lambda _
+ (invoke "./scripts/tests.sh")
+ #t)))))
(inputs
(list boost-static jsoncpp z3))
(native-inputs
- `(("python" ,python)
- ("tput" ,ncurses)
- ("xargs" ,findutils)))
+ (list python ncurses findutils))
(home-page "https://solidity.readthedocs.io")
(synopsis "Contract-Oriented Programming Language")
(description
--
2.36.1
[0005-gnu-Add-fmt-for-solidity.patch (text/x-patch, inline)]
From 5f7384a382124c46b77bd9537ae643caba4fea8f Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last <at> 163.com>
Date: Sun, 3 Jul 2022 17:37:35 +0800
Subject: [PATCH 5/6] gnu: Add fmt-for-solidity.
* gnu/packages/pretty-print.scm (fmt-for-solidity): New variable.
---
gnu/packages/pretty-print.scm | 14 ++++++++++++++
1 file changed, 14 insertions(+)
diff --git a/gnu/packages/pretty-print.scm b/gnu/packages/pretty-print.scm
index 4ee46b4e89..9745a9ba10 100644
--- a/gnu/packages/pretty-print.scm
+++ b/gnu/packages/pretty-print.scm
@@ -8,6 +8,7 @@
;;; Copyright © 2020 Paul Garlick <pgarlick <at> tourbillion-technology.com>
;;; Copyright © 2020 Vincent Legoll <vincent.legoll <at> gmail.com>
;;; Copyright © 2021 Greg Hogan <code <at> greghogan.com>
+;;; Copyright © 2022 Zhu Zihao <all_but_last <at> 163.com>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -187,6 +188,19 @@ (define-public fmt
;; The library is bsd-2, but documentation and tests include other licenses.
(license (list bsd-2 bsd-3 psfl))))
+(define-public fmt-for-solidity
+ (package
+ (inherit fmt)
+ (name "fmt-for-solidity")
+ (version "8.0.1")
+ (source
+ (origin
+ (method url-fetch)
+ (uri (string-append "https://github.com/fmtlib/fmt/releases/download/"
+ version "/fmt-" version ".zip"))
+ (sha256
+ (base32 "1gqmsk4r93x65cqs8w7zhfiv70w5fv8279nrblggqm4mmdpaa9x6"))))))
+
(define-public fmt-7
(package (inherit fmt)
(version "7.1.3")
--
2.36.1
[0006-gnu-solidity-Update-to-0.8.15.patch (text/x-patch, inline)]
From dca38a7c446f38417ae914d2f71c0568fba2cb8a Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last <at> 163.com>
Date: Sun, 3 Jul 2022 17:39:27 +0800
Subject: [PATCH 6/6] gnu: solidity: Update to 0.8.15.
* gnu/packages/solidity.scm (solidity): Update to 0.8.15.
[source]: Use Github release.
[arguments]<#:phases>: Remove phase 'create-commit_hash.txt'.
Restore phase 'configure' and phase 'install'.
Remove modifications applied to the phase 'build' and phase 'check'.
Add phase 'unbundle-3rd-party-dependencies'.
[inputs]: Add fmt-for-solidity, range-v3.
---
gnu/packages/solidity.scm | 94 +++++++++++++++------------------------
1 file changed, 37 insertions(+), 57 deletions(-)
diff --git a/gnu/packages/solidity.scm b/gnu/packages/solidity.scm
index 606e078e42..8e0bd91205 100644
--- a/gnu/packages/solidity.scm
+++ b/gnu/packages/solidity.scm
@@ -19,73 +19,53 @@
(define-module (gnu packages solidity)
#:use-module (gnu packages base)
#:use-module (gnu packages boost)
+ #:use-module (gnu packages cpp)
#:use-module (gnu packages maths)
#:use-module (gnu packages serialization)
+ #:use-module (gnu packages pretty-print)
#:use-module (gnu packages python)
#:use-module (gnu packages ncurses)
#:use-module (guix packages)
#:use-module (guix gexp)
+ #:use-module (guix download)
#:use-module (guix git-download)
#:use-module (guix build-system cmake)
#:use-module ((guix licenses) #:prefix license:))
(define-public solidity
- (let ((commit "3f05b770bdbf60eca866382049ea191dd701409a"))
- (package
- (name "solidity")
- (version "0.7.4")
- (source
- (origin
- (method git-fetch)
- (uri
- (git-reference
- (url "https://github.com/ethereum/solidity")
- (commit commit)))
- (file-name (git-file-name name version))
- (sha256
- (base32 "1mswhjymiwnd3n7h3sjvjx5x8223yih0yvfcr0zpqr4aizpfx5z8"))))
- (build-system cmake-build-system)
- (arguments
- (list
- #:phases
- #~(modify-phases %standard-phases
- (add-after 'unpack 'create-commit_hash.txt
- (lambda _
- (with-output-to-file "commit_hash.txt"
- (lambda _
- (display
- (substring #$commit 0 8))))))
- (delete 'configure)
- (delete 'install)
- (replace 'build
- (lambda* (#:key outputs #:allow-other-keys)
- ;; Unbundle jsoncpp
- (delete-file "./cmake/jsoncpp.cmake")
- (substitute* "CMakeLists.txt"
- (("include\\(jsoncpp\\)") ""))
- ;; Bug list is always sorted since we only build releases
- (substitute* "./test/cmdlineTests.sh"
- (("\"\\$REPO_ROOT\"/scripts/update_bugs_by_version\\.py") ""))
- (substitute* "./scripts/build.sh"
- (("sudo\\ make\\ install") "make install")
- (("cmake\\ ..")
- (string-append "cmake .. -DCMAKE_INSTALL_PREFIX="
- (assoc-ref outputs "out"))))
- (setenv "CIRCLECI" "1")
- (invoke "./scripts/build.sh")
- #t))
- (replace 'check
- (lambda _
- (invoke "./scripts/tests.sh")
- #t)))))
- (inputs
- (list boost-static jsoncpp z3))
- (native-inputs
- (list python ncurses findutils))
- (home-page "https://solidity.readthedocs.io")
- (synopsis "Contract-Oriented Programming Language")
- (description
- "Solidity is a statically-typed curly-braces programming language
+ (package
+ (name "solidity")
+ (version "0.8.15")
+ (source
+ (origin
+ (method url-fetch)
+ (uri
+ (string-append "https://github.com/ethereum/solidity/releases/download/v"
+ version "/solidity_" version ".tar.gz"))
+ (sha256
+ (base32 "0j9a8y5fizarl9yhbnwvd0x1nm6qsbskqb7j1fwsyqx47w5sa82p"))))
+ (build-system cmake-build-system)
+ (arguments
+ (list
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'unpack 'unbundle-3rd-party-dependencies
+ (lambda _
+ (substitute* "CMakeLists.txt"
+ (("include\\(fmtlib\\)")
+ "find_package(fmt)")
+ (("include\\(range-v3\\)")
+ "find_package(range-v3)")
+ (("include\\(jsoncpp\\)")
+ "find_package(jsoncpp)")))))))
+ (inputs
+ (list boost-static fmt-for-solidity jsoncpp range-v3 z3))
+ (native-inputs
+ (list python ncurses findutils))
+ (home-page "https://solidity.readthedocs.io")
+ (synopsis "Contract-Oriented Programming Language")
+ (description
+ "Solidity is a statically-typed curly-braces programming language
designed for developing smart contracts that run on the Ethereum Virtual
Machine.")
- (license license:gpl3+))))
+ (license license:gpl3+)))
--
2.36.1
[Message part 9 (text/plain, inline)]
-- Retrieve my PGP public key: gpg --recv-keys D47A9C8B2AE3905B563D9135BE42B352A9F6821F Zihao
Ludovic Courtès <ludo <at> gnu.org>:Zhu Zihao <all_but_last <at> 163.com>:Message #22 received at 56107-done <at> debbugs.gnu.org (full text, mbox):
From: Ludovic Courtès <ludo <at> gnu.org> To: Zhu Zihao <all_but_last <at> 163.com> Cc: 56107-done <at> debbugs.gnu.org, Maxime Devos <maximedevos <at> telenet.be> Subject: Re: bug#56107: [PATCH]: Update z3 to 4.8.17 and use cmake to build the package. Date: Mon, 04 Jul 2022 11:14:21 +0200
Hi, Zhu Zihao <all_but_last <at> 163.com> skribis: > I update the solidity to 0.8.15 and now it can be built with z3 4.8. Perfect; applied, thanks! Ludo’.
Debbugs Internal Request <help-debbugs <at> gnu.org>
to internal_control <at> debbugs.gnu.org.
(Mon, 01 Aug 2022 11:24:04 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.