From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp12.migadu.com ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms5.migadu.com with LMTPS id 2M05Fsp+sWItbQAAbAwnHQ (envelope-from ) for ; Tue, 21 Jun 2022 10:18:18 +0200 Received: from aspmx1.migadu.com ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp12.migadu.com with LMTPS id sDjPFcp+sWJHegAAauVa8A (envelope-from ) for ; Tue, 21 Jun 2022 10:18:18 +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 C2DCE2118A for ; Tue, 21 Jun 2022 10:18:17 +0200 (CEST) Received: from localhost ([::1]:41406 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1o3Z5U-0006tn-Ci for larch@yhetil.org; Tue, 21 Jun 2022 04:18:16 -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 Content-Type: multipart/mixed; boundary="=-=-=" 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+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=1655799498; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:cc:mime-version:mime-version: content-type:content-type:resent-cc:resent-from:resent-sender: resent-message-id:in-reply-to:in-reply-to:references:references: list-id:list-help:list-unsubscribe:list-subscribe:list-post: dkim-signature; bh=7zjJL6IjQ8yGKaVcKgA7yN1uWj2BJ9ofYXTcrR++Ofo=; b=XGBdpRhAkjU93CBqLZIk4yZ2V4Xpgg3BHRflUeI1pvItE4U6jrTFMbh6FQu1QI7+aMGn1M p5vMbkBttIsupbJNKfP3D5rrp7iFHbfzQEUZEZbkxBh2YVSw6tk+rhu6XhCcoz026ngH4C n7pViSPir2XnZzD7IR/b2Ml8MTzzI4emaAKMDYjcv2TnkjTLe8/GVZyg467v+TCqUTqhtr hSr0djLhCi/woMV0qXoTkaKbKZLMehkvIrjJx9fkflbomqJO0pmC0mRhVLqcNE01P7/45h +Y6PM6ExAJM05E1W3QbkO4a4/SPdxtwoiqvh46QailvM2m5np85xWBuQ9sV+6Q== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1655799498; a=rsa-sha256; cv=none; b=DKOXODl7iPCv/pLrK3x0KnE3HKiLkgZKTKYcP+QWPVG/3wAAyReuWF2m8gKNEN5+P5YFIX ZBEJrhdmM69mSvCuBVLpy4l5dVaaTHPuTGjYgb1lr5xm+/9FvAAYp6Men8VdZXNGWfdmk5 6FXczgJTXNwX3fgavnpLCf52fpPAjoj73EY6I6eC3ilqLoZEBdmtRBpquWqA9O2hXSFJNZ cyT4hSPSr9LaDV4XhtiDxOgkhyHRwJJWrqNmYS+gMyv0LfEjNigzWZNVuiYzfSG1KLLaGW 1uULu1cX/jXeizBfnTu4U5UbNnQDFD8KjM+CF9AhogNmNtdHmR4R9FFfoylovg== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=163.com header.s=s110527 header.b=RtwiLpfr; 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.43 Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=163.com header.s=s110527 header.b=RtwiLpfr; 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: C2DCE2118A X-Spam-Score: 3.43 X-Migadu-Scanner: scn0.migadu.com X-TUID: 4tCUGLinG7ud --=-=-= Content-Type: multipart/signed; boundary="==-=-="; micalg=pgp-sha256; protocol="application/pgp-signature" --==-=-= Content-Type: text/plain Thanks, patches updated. --==-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iIsEARYIADMWIQRefA5qkqvnKdl/GTlmOX+E92aT+QUCYrF+dxUcYWxsX2J1dF9s YXN0QDE2My5jb20ACgkQZjl/hPdmk/nEFQD/XOddUEUHlJJJW/JVEA8bn458Ioo2 LZfy0c1ilveMJGABAK8m8LSW9Ah7uzViZHuPR14o2mODTl4PraD7ey38uukA =rcI1 -----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 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 --=-=-= Content-Type: text/plain -- Retrieve my PGP public key: gpg --recv-keys D47A9C8B2AE3905B563D9135BE42B352A9F6821F Zihao --=-=-=--