From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp10.migadu.com ([2001:41d0:2:bcc0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms5.migadu.com with LMTPS id QAE5IZRpsGJ9HgAAbAwnHQ (envelope-from ) for ; Mon, 20 Jun 2022 14:35:32 +0200 Received: from aspmx1.migadu.com ([2001:41d0:2:bcc0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp10.migadu.com with LMTPS id WDJLIJRpsGJ2wAAAG6o9tA (envelope-from ) for ; Mon, 20 Jun 2022 14:35:32 +0200 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by aspmx1.migadu.com (Postfix) with ESMTPS id C5BAA30020 for ; Mon, 20 Jun 2022 14:35:30 +0200 (CEST) Received: from localhost ([::1]:59658 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1o3Gcr-0004qT-GN for larch@yhetil.org; Mon, 20 Jun 2022 08:35:29 -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 Content-Type: multipart/mixed; boundary="=-=-=" 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+larch=yhetil.org@gnu.org Sender: "Guix-patches" X-Migadu-Flow: FLOW_IN X-Migadu-To: larch@yhetil.org X-Migadu-Country: US ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1655728532; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:mime-version:mime-version: content-type:content-type:resent-cc:resent-from:resent-sender: resent-message-id:list-id:list-help:list-unsubscribe:list-subscribe: list-post:dkim-signature; bh=ehyRCx1dVGKIzGXkHqmV4Mh4c7/O3wLLdtKQneBM+1E=; b=rrEFjc4dlLGMmF+HiWYnjeAJsqR/u+Q4EvcDHWimdpZQ4fAdw3q3iCtw3HR/u5GsUF0FYL bF4hsYl0+R9VAJduSOJaMMCGt8dyaqSElcgdPTwG1f0ElkrBS/azPizG41GMd6J65+IVg4 a+4NNQCLMHmvTH+n/AGR29FDsHEjwX4gAQ4ZDYWuqcE3zJocQdF/19vMOBZyJoPkT23HkO lJIn0zjiolo/p4hCkVHMBgmeRckN74FVp+e3o2gikXa+tcbOSbhpMor+9w+CfY5CbasnoL uOpoJbMhAgj8znsU33ptxA1bKA4SCSk2nzHmh4S6iTiHpXgpDKedFEfi05sVVA== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1655728532; a=rsa-sha256; cv=none; b=C4kJOIcVHAySttEHtmpQcfDvTqEQER5nBLs3si59w1HWxJ1A0B9InkT1JsujWSUc4MZFhP dAQmvWc/AUWT6d005UuTb7yRBGOXfDXGSFSR+XSlQyhQfFJpyvKcnfkbRSRPKlIH3lrt3y 2YlDYCZb33pKd36/XkbgMFKVlyE1d3rA51w8aStcQ+UsMnG8kRBqj73MUXRh7nhyKrc3B4 ymL4jFlCIn2QUszeomho2+Y9qfUv6l//QfVqjJbuQfzcqaFta91IQxLOPkui6wU5tVIWd1 27I+nj/K9hrp9MMYsk1CthGdVoz3vR7tF9eHNsSDHEHPBaUH1JzMTZX7DLEr/w== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=163.com header.s=s110527 header.b="GhU9Api/"; dmarc=fail reason="SPF not aligned (relaxed)" header.from=163.com (policy=none); spf=pass (aspmx1.migadu.com: domain of "guix-patches-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-patches-bounces+larch=yhetil.org@gnu.org" X-Migadu-Spam-Score: 3.23 Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=163.com header.s=s110527 header.b="GhU9Api/"; dmarc=fail reason="SPF not aligned (relaxed)" header.from=163.com (policy=none); spf=pass (aspmx1.migadu.com: domain of "guix-patches-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-patches-bounces+larch=yhetil.org@gnu.org" X-Migadu-Queue-Id: C5BAA30020 X-Spam-Score: 3.23 X-Migadu-Scanner: scn0.migadu.com X-TUID: Rx+XUdp31zFV --=-=-= Content-Type: multipart/signed; boundary="==-=-="; micalg=pgp-sha256; protocol="application/pgp-signature" --==-=-= Content-Type: text/plain --==-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iIsEARYIADMWIQRefA5qkqvnKdl/GTlmOX+E92aT+QUCYrBpFBUcYWxsX2J1dF9s YXN0QDE2My5jb20ACgkQZjl/hPdmk/luBQEA7KJ+Z1VmHgVG3PdSUz8sj10prIQ3 TEUm42dmZNqRIuYBAMfEvCmg23ORDCxqvnqkKswLcLNkLhWMCpM0d7LG7MIP =bwv+ -----END PGP SIGNATURE----- --==-=-=-- --=-=-= Content-Type: text/x-patch; charset=utf-8 Content-Disposition: inline; filename=0001-gnu-z3-Use-G-expressions.patch Content-Transfer-Encoding: quoted-printable >From a8ccfba4a1c5ef02618d81f3873912b28411092e Mon Sep 17 00:00:00 2001 From: Zhu Zihao 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(-) 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 =C2=A9 2021 Jean-Baptiste Volatier ;;; Copyright =C2=A9 2021 Guillaume Le Vaillant ;;; Copyright =C2=A9 2021 Pierre-Antoine Bouttier +;;; Copyright =C2=A9 2022 Zhu Zihao ;;; ;;; 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-package= s)) - (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 on= ly. - (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 - (lambda* (#:key inputs outputs #:allow-other-keys) - (invoke "./configure" - "--python" - (string-append "--prefix=3D" (assoc-ref outputs "out"= )) - (string-append "--pypkgdir=3D" (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-package= s))) + #: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 o= nly. + (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 + (lambda* (#:key inputs outputs #:allow-other-keys) + (invoke "./configure" + "--python" + (string-append "--prefix=3D" (assoc-ref outputs "out= ")) + (string-append "--pypkgdir=3D" (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 bindin= gs.") --=20 2.36.1 --=-=-= Content-Type: text/x-patch Content-Disposition: inline; filename=0002-gnu-z3-Update-to-4.8.17.patch >From 5ce1ec4c3c6d0a865645da9a6b0899f3596b5e3e Mon Sep 17 00:00:00 2001 From: Zhu Zihao 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(-) 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 --=-=-= Content-Type: text/x-patch Content-Disposition: inline; filename=0003-gnu-z3-Prefer-CMake-to-build-the-package.patch >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 --=-=-= Content-Type: text/plain -- Retrieve my PGP public key: gpg --recv-keys D47A9C8B2AE3905B563D9135BE42B352A9F6821F Zihao --=-=-=--