[PATCH]: Update z3 to 4.8.17 and use cmake to build the package.

DoneSubmitted by Zhu Zihao.
Details
3 participants
  • Zhu Zihao
  • Ludovic Courtès
  • Maxime Devos
Owner
unassigned
Severity
normal
Z
Z
Zhu Zihao wrote on 20 Jun 14:32 +0200
(address . guix-patches@gnu.org)
86mte7v7jf.fsf@163.com
-----BEGIN PGP SIGNATURE-----

iIsEARYIADMWIQRefA5qkqvnKdl/GTlmOX+E92aT+QUCYrBpFBUcYWxsX2J1dF9s
YXN0QDE2My5jb20ACgkQZjl/hPdmk/luBQEA7KJ+Z1VmHgVG3PdSUz8sj10prIQ3
TEUm42dmZNqRIuYBAMfEvCmg23ORDCxqvnqkKswLcLNkLhWMCpM0d7LG7MIP
=bwv+
-----END PGP SIGNATURE-----

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(-)

Toggle diff (110 lines)
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
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(-)

Toggle diff (25 lines)
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
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(-)

Toggle diff (97 lines)
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
--
Retrieve my PGP public key:

gpg --recv-keys D47A9C8B2AE3905B563D9135BE42B352A9F6821F

Zihao
M
M
Maxime Devos wrote on 20 Jun 14:54 +0200
81f29e686f5727d02c9924782d4adb9895369046.camel@telenet.be
Zhu Zihao schreef op ma 20-06-2022 om 20:32 [+0800]:
Toggle quote (4 lines)
> +          (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.
-----BEGIN PGP SIGNATURE-----

iI0EABYKADUWIQTB8z7iDFKP233XAR9J4+4iGRcl7gUCYrBuBhccbWF4aW1lZGV2
b3NAdGVsZW5ldC5iZQAKCRBJ4+4iGRcl7qbXAQDY2+sjTgoM7ZhsMwaBBjLpLqlH
caRWH8ULRii8FSX9KgEAi1fY3YBmoBGmVU1nOk8q5jhc2+QyG7Hah8rgovxHHwM=
=CN2z
-----END PGP SIGNATURE-----


Z
Z
Zhu Zihao wrote on 21 Jun 10:16 +0200
(name . Maxime Devos)(address . maximedevos@telenet.be)(address . 56107@debbugs.gnu.org)
86fsjyv3bc.fsf@163.com
Thanks, patches updated.
-----BEGIN PGP SIGNATURE-----

iIsEARYIADMWIQRefA5qkqvnKdl/GTlmOX+E92aT+QUCYrF+dxUcYWxsX2J1dF9s
YXN0QDE2My5jb20ACgkQZjl/hPdmk/nEFQD/XOddUEUHlJJJW/JVEA8bn458Ioo2
LZfy0c1ilveMJGABAK8m8LSW9Ah7uzViZHuPR14o2mODTl4PraD7ey38uukA
=rcI1
-----END PGP SIGNATURE-----

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(-)

Toggle diff (110 lines)
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
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(-)

Toggle diff (25 lines)
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
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(-)

Toggle diff (97 lines)
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
--
Retrieve my PGP public key:

gpg --recv-keys D47A9C8B2AE3905B563D9135BE42B352A9F6821F

Zihao
L
L
Ludovic Courtès wrote on 3 Jul 01:40 +0200
Re: bug#56107: [PATCH]: Update z3 to 4.8.17 and use cmake to build the package.
(name . Zhu Zihao)(address . all_but_last@163.com)
87k08v13tg.fsf_-_@gnu.org
Hi!

The series LGTM, but unfortunately the upgrade breaks one dependent,
‘solidity’:

Toggle snippet (68 lines)
--- 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

Thoughts?

Ludo’.
Z
Z
Zhu Zihao wrote on 3 Jul 11:43 +0200
(name . Ludovic Courtès)(address . ludo@gnu.org)
86fsji7con.fsf@163.com
I update the solidity to 0.8.15 and now it can be built with z3 4.8.
-----BEGIN PGP SIGNATURE-----

iIsEARYIADMWIQRefA5qkqvnKdl/GTlmOX+E92aT+QUCYsFlCBUcYWxsX2J1dF9s
YXN0QDE2My5jb20ACgkQZjl/hPdmk/kjeQD/X57vlLBHHNZ01c5fi4UUjncfcKHx
LFWR9yBqBgb1deIBAPh1deLujMXIlz1KM6l7BW3ddEdYqA9EeP+smn7wfWoP
=2DmI
-----END PGP SIGNATURE-----

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(-)

Toggle diff (110 lines)
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
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(-)

Toggle diff (25 lines)
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
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(-)

Toggle diff (97 lines)
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
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(-)

Toggle diff (97 lines)
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
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(+)

Toggle diff (34 lines)
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
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(-)

Toggle diff (117 lines)
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
--
Retrieve my PGP public key:

gpg --recv-keys D47A9C8B2AE3905B563D9135BE42B352A9F6821F

Zihao
L
L
Ludovic Courtès wrote on 4 Jul 11:14 +0200
(name . Zhu Zihao)(address . all_but_last@163.com)
87y1x9fdea.fsf@gnu.org
Hi,

Zhu Zihao <all_but_last@163.com> skribis:

Toggle quote (2 lines)
> I update the solidity to 0.8.15 and now it can be built with z3 4.8.

Perfect; applied, thanks!

Ludo’.
Closed
?
Your comment

This issue is archived.

To comment on this conversation send email to 56107@debbugs.gnu.org