From patchwork Mon Jun 20 12:32:47 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Zhu Zihao X-Patchwork-Id: 40195 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id 7517C27BBEA; Mon, 20 Jun 2022 13:35:30 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-3.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,FREEMAIL_FROM,MAILING_LIST_MULTI,RCVD_IN_MSPIKE_H2, SPF_HELO_PASS,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id 590B027BBE9 for ; Mon, 20 Jun 2022 13:35:29 +0100 (BST) Received: from localhost ([::1]:59658 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1o3Gcq-0004qT-Eg for patchwork@mira.cbaines.net; Mon, 20 Jun 2022 08:35:28 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:60272) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1o3GcQ-0004lP-Du for guix-patches@gnu.org; Mon, 20 Jun 2022 08:35:03 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:60825) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1o3GcQ-0002lP-3X for guix-patches@gnu.org; Mon, 20 Jun 2022 08:35:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1o3GcQ-00016k-18 for guix-patches@gnu.org; Mon, 20 Jun 2022 08:35:02 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#56107] [PATCH]: Update z3 to 4.8.17 and use cmake to build the package. Resent-From: Zhu Zihao Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 20 Jun 2022 12:35:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 56107 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 56107@debbugs.gnu.org X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@debbugs.gnu.org id=B.16557284564204 (code B ref -1); Mon, 20 Jun 2022 12:35:01 +0000 Received: (at submit) by debbugs.gnu.org; 20 Jun 2022 12:34:16 +0000 Received: from localhost ([127.0.0.1]:54722 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1o3Gbb-00015e-Ld for submit@debbugs.gnu.org; Mon, 20 Jun 2022 08:34:16 -0400 Received: from lists.gnu.org ([209.51.188.17]:38030) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1o3GbS-00015M-8g for submit@debbugs.gnu.org; Mon, 20 Jun 2022 08:34:10 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:60142) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1o3GbS-0003nk-1y for guix-patches@gnu.org; Mon, 20 Jun 2022 08:34:02 -0400 Received: from mail-m973.mail.163.com ([123.126.97.3]:40066) by eggs.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1o3GbJ-0002FI-5Q for guix-patches@gnu.org; Mon, 20 Jun 2022 08:33:58 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=163.com; s=s110527; h=From:Subject:Date:Message-ID:MIME-Version; bh=ehyRC x1dVGKIzGXkHqmV4Mh4c7/O3wLLdtKQneBM+1E=; b=GhU9Api/kavzlN1aA1a+J vpxZ7wMVdTRUXW276Qhkn6/IMmy5LoyxJPGNpG2d5crC7iZcVe3HvGlHUBdBlyIo eJuWiHC1ZYgGqvDJnnB188vnHX6X9EvmXPYLyiEN39JcuxxAFHFsHYTocNyNFbM3 8U+x0sQozNxHjfPcHogOWw= Received: from asus-laptop (unknown [112.95.115.209]) by smtp3 (Coremail) with SMTP id G9xpCgCnPI4aabBiH6yiKw--.18775S2; Mon, 20 Jun 2022 20:33:39 +0800 (CST) User-agent: mu4e 1.6.10; emacs 27.2 From: Zhu Zihao Date: Mon, 20 Jun 2022 20:32:47 +0800 Message-ID: <86mte7v7jf.fsf@163.com> MIME-Version: 1.0 X-CM-TRANSID: G9xpCgCnPI4aabBiH6yiKw--.18775S2 X-Coremail-Antispam: 1Uf129KBjDUn29KB7ZKAUJUUUUU529EdanIXcx71UUUUU7v73 VFW2AGmfu7bjvjm3AaLaJ3UbIYCTnIWIevJa73UjIFyTuYvjxUIG-eUUUUU X-Originating-IP: [112.95.115.209] X-CM-SenderInfo: pdoosuxxwbztlvw6il2tof0z/1tbiKQMmr1Xl39XW9wAAs4 Received-SPF: pass client-ip=123.126.97.3; envelope-from=all_but_last@163.com; helo=mail-m973.mail.163.com X-Spam_score_int: -20 X-Spam_score: -2.1 X-Spam_bar: -- X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001, RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01 autolearn=ham autolearn_force=no X-Spam_action: no action X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches From 6bd6bda66d40782e2f269001d9bc53e3bf8a153f Mon Sep 17 00:00:00 2001 From: Zhu Zihao 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 ") "")) - #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