* [bug#56107] [PATCH]: Update z3 to 4.8.17 and use cmake to build the package.
@ 2022-06-20 12:32 Zhu Zihao
2022-06-20 12:54 ` Maxime Devos
0 siblings, 1 reply; 6+ messages in thread
From: Zhu Zihao @ 2022-06-20 12:32 UTC (permalink / raw)
To: 56107
[-- Attachment #1.1: Type: text/plain, Size: 0 bytes --]
[-- Attachment #1.2: signature.asc --]
[-- Type: application/pgp-signature, Size: 255 bytes --]
[-- Attachment #2: 0001-gnu-z3-Use-G-expressions.patch --]
[-- Type: text/x-patch, Size: 5381 bytes --]
From a8ccfba4a1c5ef02618d81f3873912b28411092e Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last@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@pm.me>
;;; Copyright © 2021 Guillaume Le Vaillant <glv@posteo.net>
;;; Copyright © 2021 Pierre-Antoine Bouttier <pierre-antoine.bouttier@univ-grenoble-alpes.fr>
+;;; Copyright © 2022 Zhu Zihao <all_but_last@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
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #3: 0002-gnu-z3-Update-to-4.8.17.patch --]
[-- Type: text/x-patch, Size: 1164 bytes --]
From 5ce1ec4c3c6d0a865645da9a6b0899f3596b5e3e Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last@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
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #4: 0003-gnu-z3-Prefer-CMake-to-build-the-package.patch --]
[-- Type: text/x-patch, Size: 5174 bytes --]
From 6bd6bda66d40782e2f269001d9bc53e3bf8a153f Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last@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
[-- Attachment #5: Type: text/plain, Size: 100 bytes --]
--
Retrieve my PGP public key:
gpg --recv-keys D47A9C8B2AE3905B563D9135BE42B352A9F6821F
Zihao
^ permalink raw reply related [flat|nested] 6+ messages in thread
* [bug#56107] [PATCH]: Update z3 to 4.8.17 and use cmake to build the package.
2022-06-20 12:32 [bug#56107] [PATCH]: Update z3 to 4.8.17 and use cmake to build the package Zhu Zihao
@ 2022-06-20 12:54 ` Maxime Devos
2022-06-21 8:16 ` Zhu Zihao
0 siblings, 1 reply; 6+ messages in thread
From: Maxime Devos @ 2022-06-20 12:54 UTC (permalink / raw)
To: Zhu Zihao, 56107
[-- Attachment #1: Type: text/plain, Size: 477 bytes --]
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.
[-- Attachment #2: This is a digitally signed message part --]
[-- Type: application/pgp-signature, Size: 260 bytes --]
^ permalink raw reply [flat|nested] 6+ messages in thread
* [bug#56107] [PATCH]: Update z3 to 4.8.17 and use cmake to build the package.
2022-06-20 12:54 ` Maxime Devos
@ 2022-06-21 8:16 ` Zhu Zihao
2022-07-02 23:40 ` Ludovic Courtès
0 siblings, 1 reply; 6+ messages in thread
From: Zhu Zihao @ 2022-06-21 8:16 UTC (permalink / raw)
To: Maxime Devos; +Cc: 56107
[-- Attachment #1.1: Type: text/plain, Size: 26 bytes --]
Thanks, patches updated.
[-- Attachment #1.2: signature.asc --]
[-- Type: application/pgp-signature, Size: 255 bytes --]
[-- Attachment #2: 0001-gnu-z3-Use-G-expressions.patch --]
[-- Type: text/x-patch, Size: 5381 bytes --]
From a8ccfba4a1c5ef02618d81f3873912b28411092e Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last@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@pm.me>
;;; Copyright © 2021 Guillaume Le Vaillant <glv@posteo.net>
;;; Copyright © 2021 Pierre-Antoine Bouttier <pierre-antoine.bouttier@univ-grenoble-alpes.fr>
+;;; Copyright © 2022 Zhu Zihao <all_but_last@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
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #3: 0002-gnu-z3-Update-to-4.8.17.patch --]
[-- Type: text/x-patch, Size: 1164 bytes --]
From 5ce1ec4c3c6d0a865645da9a6b0899f3596b5e3e Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last@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
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #4: 0003-gnu-z3-Prefer-CMake-to-build-the-package.patch --]
[-- Type: text/x-patch, Size: 5159 bytes --]
From e1df674d84fe5a26a343a2ea68ea961d045dffe8 Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last@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
[-- Attachment #5: Type: text/plain, Size: 100 bytes --]
--
Retrieve my PGP public key:
gpg --recv-keys D47A9C8B2AE3905B563D9135BE42B352A9F6821F
Zihao
^ permalink raw reply related [flat|nested] 6+ messages in thread
* [bug#56107] [PATCH]: Update z3 to 4.8.17 and use cmake to build the package.
2022-06-21 8:16 ` Zhu Zihao
@ 2022-07-02 23:40 ` Ludovic Courtès
2022-07-03 9:43 ` Zhu Zihao
0 siblings, 1 reply; 6+ messages in thread
From: Ludovic Courtès @ 2022-07-02 23:40 UTC (permalink / raw)
To: Zhu Zihao; +Cc: 56107, Maxime Devos
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’.
^ permalink raw reply [flat|nested] 6+ messages in thread
* [bug#56107] [PATCH]: Update z3 to 4.8.17 and use cmake to build the package.
2022-07-02 23:40 ` Ludovic Courtès
@ 2022-07-03 9:43 ` Zhu Zihao
2022-07-04 9:14 ` bug#56107: " Ludovic Courtès
0 siblings, 1 reply; 6+ messages in thread
From: Zhu Zihao @ 2022-07-03 9:43 UTC (permalink / raw)
To: Ludovic Courtès; +Cc: 56107, Maxime Devos
[-- Attachment #1.1: Type: text/plain, Size: 72 bytes --]
I update the solidity to 0.8.15 and now it can be built with z3 4.8.
[-- Attachment #1.2: signature.asc --]
[-- Type: application/pgp-signature, Size: 255 bytes --]
[-- Attachment #2: 0001-gnu-z3-Use-G-expressions.patch --]
[-- Type: text/x-patch, Size: 5381 bytes --]
From a8ccfba4a1c5ef02618d81f3873912b28411092e Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last@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@pm.me>
;;; Copyright © 2021 Guillaume Le Vaillant <glv@posteo.net>
;;; Copyright © 2021 Pierre-Antoine Bouttier <pierre-antoine.bouttier@univ-grenoble-alpes.fr>
+;;; Copyright © 2022 Zhu Zihao <all_but_last@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
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #3: 0002-gnu-z3-Update-to-4.8.17.patch --]
[-- Type: text/x-patch, Size: 1164 bytes --]
From 5ce1ec4c3c6d0a865645da9a6b0899f3596b5e3e Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last@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
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #4: 0003-gnu-z3-Prefer-CMake-to-build-the-package.patch --]
[-- Type: text/x-patch, Size: 5159 bytes --]
From e1df674d84fe5a26a343a2ea68ea961d045dffe8 Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last@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
[-- Attachment #5: 0004-gnu-solidity-Use-G-expressions.patch --]
[-- Type: text/x-patch, Size: 4501 bytes --]
From 7ec422d6f592a129f2e03fa57cfe3afb95febf29 Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last@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@riseup.net>
+;;; Copyright © 2022 Zhu Zihao <all_but_last@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
[-- Attachment #6: 0005-gnu-Add-fmt-for-solidity.patch --]
[-- Type: text/x-patch, Size: 1549 bytes --]
From 5f7384a382124c46b77bd9537ae643caba4fea8f Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last@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@tourbillion-technology.com>
;;; Copyright © 2020 Vincent Legoll <vincent.legoll@gmail.com>
;;; Copyright © 2021 Greg Hogan <code@greghogan.com>
+;;; Copyright © 2022 Zhu Zihao <all_but_last@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
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #7: 0006-gnu-solidity-Update-to-0.8.15.patch --]
[-- Type: text/x-patch, Size: 5088 bytes --]
From dca38a7c446f38417ae914d2f71c0568fba2cb8a Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last@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
[-- Attachment #8: Type: text/plain, Size: 100 bytes --]
--
Retrieve my PGP public key:
gpg --recv-keys D47A9C8B2AE3905B563D9135BE42B352A9F6821F
Zihao
^ permalink raw reply related [flat|nested] 6+ messages in thread
* bug#56107: [PATCH]: Update z3 to 4.8.17 and use cmake to build the package.
2022-07-03 9:43 ` Zhu Zihao
@ 2022-07-04 9:14 ` Ludovic Courtès
0 siblings, 0 replies; 6+ messages in thread
From: Ludovic Courtès @ 2022-07-04 9:14 UTC (permalink / raw)
To: Zhu Zihao; +Cc: 56107-done, Maxime Devos
Hi,
Zhu Zihao <all_but_last@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’.
^ permalink raw reply [flat|nested] 6+ messages in thread
end of thread, other threads:[~2022-07-04 9:15 UTC | newest]
Thread overview: 6+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-06-20 12:32 [bug#56107] [PATCH]: Update z3 to 4.8.17 and use cmake to build the package Zhu Zihao
2022-06-20 12:54 ` Maxime Devos
2022-06-21 8:16 ` Zhu Zihao
2022-07-02 23:40 ` Ludovic Courtès
2022-07-03 9:43 ` Zhu Zihao
2022-07-04 9:14 ` bug#56107: " Ludovic Courtès
Code repositories for project(s) associated with this public inbox
https://git.savannah.gnu.org/cgit/guix.git
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).