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

  • Done
  • quality assurance status badge
Details
3 participants
  • Zhu Zihao
  • Ludovic Courtès
  • Maxime Devos
Owner
unassigned
Submitted by
Zhu Zihao
Severity
normal
Z
Z
Zhu Zihao wrote on 20 Jun 2022 14:32
(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 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
--
Retrieve my PGP public key:

gpg --recv-keys D47A9C8B2AE3905B563D9135BE42B352A9F6821F

Zihao
M
M
Maxime Devos wrote on 20 Jun 2022 14:54
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 2022 10:16
(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 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
--
Retrieve my PGP public key:

gpg --recv-keys D47A9C8B2AE3905B563D9135BE42B352A9F6821F

Zihao
L
L
Ludovic Courtès wrote on 3 Jul 2022 01:40
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 2022 11:43
(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 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 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
--
Retrieve my PGP public key:

gpg --recv-keys D47A9C8B2AE3905B563D9135BE42B352A9F6821F

Zihao
L
L
Ludovic Courtès wrote on 4 Jul 2022 11:14
(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
?