From patchwork Tue Jun 21 08:16:25 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Zhu Zihao X-Patchwork-Id: 40205 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 33E4027BBEA; Tue, 21 Jun 2022 09:18:17 +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=-2.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,FREEMAIL_FROM,MAILING_LIST_MULTI,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 65DF527BBE9 for ; Tue, 21 Jun 2022 09:18:16 +0100 (BST) Received: from localhost ([::1]:41406 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1o3Z5T-0006tn-HV for patchwork@mira.cbaines.net; Tue, 21 Jun 2022 04:18:15 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:53864) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1o3Z5H-0006tP-5W for guix-patches@gnu.org; Tue, 21 Jun 2022 04:18:04 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:36945) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1o3Z5G-0002O4-Ni for guix-patches@gnu.org; Tue, 21 Jun 2022 04:18:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1o3Z5G-0002c2-Gv for guix-patches@gnu.org; Tue, 21 Jun 2022 04:18: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: Tue, 21 Jun 2022 08:18:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 56107 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Maxime Devos Cc: 56107@debbugs.gnu.org Received: via spool by 56107-submit@debbugs.gnu.org id=B56107.16557994469994 (code B ref 56107); Tue, 21 Jun 2022 08:18:02 +0000 Received: (at 56107) by debbugs.gnu.org; 21 Jun 2022 08:17:26 +0000 Received: from localhost ([127.0.0.1]:59075 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1o3Z4f-0002b7-Fp for submit@debbugs.gnu.org; Tue, 21 Jun 2022 04:17:26 -0400 Received: from mail-m975.mail.163.com ([123.126.97.5]:54434) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1o3Z4N-0002aF-Rb for 56107@debbugs.gnu.org; Tue, 21 Jun 2022 04:17:24 -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=7zjJL 6IjQ8yGKaVcKgA7yN1uWj2BJ9ofYXTcrR++Ofo=; b=RtwiLpfr0eN0X7FnsIUEb WlOQSR7+M/J2vxbfMuk5DspjthOG70Stz6DyYZU7x/3Se1+NwzbJsdBeJpeou5L/ Giwq1XixSriItJQ1Zm+v0ulzKOJmk6ARRdPfR2rptuIUkQa9wrxJfnHX/Tao3kYq yFg4DcWD7LL81aV6wXqkN8= Received: from asus-laptop (unknown [27.38.202.29]) by smtp5 (Coremail) with SMTP id HdxpCgAXH0t3frFi4KMLKQ--.5200S2; Tue, 21 Jun 2022 16:16:56 +0800 (CST) References: <86mte7v7jf.fsf@163.com> <81f29e686f5727d02c9924782d4adb9895369046.camel@telenet.be> User-agent: mu4e 1.6.10; emacs 27.2 From: Zhu Zihao Date: Tue, 21 Jun 2022 16:16:25 +0800 In-reply-to: <81f29e686f5727d02c9924782d4adb9895369046.camel@telenet.be> Message-ID: <86fsjyv3bc.fsf@163.com> MIME-Version: 1.0 X-CM-TRANSID: HdxpCgAXH0t3frFi4KMLKQ--.5200S2 X-Coremail-Antispam: 1Uf129KBjDUn29KB7ZKAUJUUUUU529EdanIXcx71UUUUU7v73 VFW2AGmfu7bjvjm3AaLaJ3UbIYCTnIWIevJa73UjIFyTuYvjxUjF4iDUUUU X-Originating-IP: [27.38.202.29] X-CM-SenderInfo: pdoosuxxwbztlvw6il2tof0z/1tbiTxknr1sGbmxBRAAAsE 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 Thanks, patches updated. From e1df674d84fe5a26a343a2ea68ea961d045dffe8 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..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 ") "")) - #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