Message ID | 86fsjyv3bc.fsf@163.com |
---|---|
State | Accepted |
Headers | show |
Series | [bug#56107] : Update z3 to 4.8.17 and use cmake to build the package. | expand |
Context | Check | Description |
---|---|---|
cbaines/applying patch | fail | View Laminar job |
cbaines/issue | success | View issue |
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’.
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