* [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 external index https://git.savannah.gnu.org/cgit/guix.git This is an external index of several public inboxes, see mirroring instructions on how to clone and mirror all data and code used by this external index.