From debbugs-submit-bounces@debbugs.gnu.org Sat Dec 15 23:36:19 2018 Received: (at submit) by debbugs.gnu.org; 16 Dec 2018 04:36:19 +0000 Received: from localhost ([127.0.0.1]:49831 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gYOA7-00040H-04 for submit@debbugs.gnu.org; Sat, 15 Dec 2018 23:36:19 -0500 Received: from eggs.gnu.org ([208.118.235.92]:56323) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gYNhf-0003H2-BH for submit@debbugs.gnu.org; Sat, 15 Dec 2018 23:06:55 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gYNhX-0002ZM-Vq for submit@debbugs.gnu.org; Sat, 15 Dec 2018 23:06:49 -0500 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=0.8 required=5.0 tests=BAYES_50 autolearn=disabled version=3.3.2 Received: from lists.gnu.org ([2001:4830:134:3::11]:40624) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1gYNhW-0002Y5-3p for submit@debbugs.gnu.org; Sat, 15 Dec 2018 23:06:47 -0500 Received: from eggs.gnu.org ([2001:4830:134:3::10]:37690) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gYNhR-0001VE-WA for guix-patches@gnu.org; Sat, 15 Dec 2018 23:06:45 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gYNhO-0002Sz-5m for guix-patches@gnu.org; Sat, 15 Dec 2018 23:06:40 -0500 Received: from fencepost.gnu.org ([2001:4830:134:3::e]:60138) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gYNhH-0002HY-Le; Sat, 15 Dec 2018 23:06:31 -0500 Received: from wn-res-nat-129-97-125-0.dynamic.uwaterloo.ca ([129.97.125.0]:9828 helo=localhost.localdomain) by fencepost.gnu.org with esmtpsa (TLS1.2:DHE_RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1gYNhH-0004Ug-GA; Sat, 15 Dec 2018 23:06:31 -0500 From: Amin Bandali To: guix-patches@gnu.org Subject: [PATCH] gnu: z3: Update to 4.8.3 and add python{,2}-z3 bindings. Date: Sat, 15 Dec 2018 23:05:30 -0500 Message-Id: <20181216040528.29880-1-bandali@gnu.org> X-Mailer: git-send-email 2.20.0 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6.x X-Received-From: 2001:4830:134:3::11 X-Spam-Score: -5.0 (-----) X-Debbugs-Envelope-To: submit X-Mailman-Approved-At: Sat, 15 Dec 2018 23:36:17 -0500 Cc: Amin Bandali X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -6.0 (------) * gnu/packages/maths.scm (z3): Update to 4.8.3. [build-system]: Switch from cmake to make, and use the current scripts/mk_make.py build script instead of the now-deprecated contrib/cmake/bootstrap.py. * gnu/packages/python.scm (python-z3, python2-z3): New public variables. --- gnu/packages/maths.scm | 31 +++++++++++++++++++------------ gnu/packages/python.scm | 10 ++++++++++ 2 files changed, 29 insertions(+), 12 deletions(-) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index ad6aacf9c..7996c3211 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -29,6 +29,7 @@ ;;; Copyright © 2018 Marius Bakke ;;; Copyright © 2018 Eric Brown ;;; Copyright © 2018 Julien Lepiller +;;; Copyright © 2018 Amin Bandali ;;; ;;; This file is part of GNU Guix. ;;; @@ -3965,7 +3966,7 @@ as equations, scalars, vectors, and matrices.") (define-public z3 (package (name "z3") - (version "4.8.1") + (version "4.8.3") (home-page "https://github.com/Z3Prover/z3") (source (origin (method git-fetch) @@ -3973,21 +3974,26 @@ as equations, scalars, vectors, and matrices.") (commit (string-append "z3-" version)))) (sha256 (base32 - "1vr57bwx40sd5riijyrhy70i2wnv9xrdihf6y5zdz56yq88rl48f")))) - (build-system cmake-build-system) + "0p5gdmhd32x6zwmx7j5cgwh4jyfxa9yapym95nlmyfaqzak92qar")))) + (build-system gnu-build-system) (arguments - `(#:configure-flags - (list "-DBUILD_PYTHON_BINDINGS=true" - "-DINSTALL_PYTHON_BINDINGS=true" - (string-append "-DCMAKE_INSTALL_PYTHON_PKG_DIR=" - %output - "/lib/python2.7/site-packages")) - #:phases + `(#:phases (modify-phases %standard-phases (add-before 'configure 'bootstrap (lambda _ (zero? - (system* "python" "contrib/cmake/bootstrap.py" "create")))) + (system* "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" + (string-append "--prefix=" (assoc-ref outputs "out"))))) + (add-after 'configure 'change-directory + (lambda _ + (chdir "build") + #t)) (add-before 'check 'make-test-z3 (lambda _ ;; Build the test suite executable. @@ -3998,7 +4004,8 @@ as equations, scalars, vectors, and matrices.") ;; Run all the tests that don't require arguments. (zero? (system* "./test-z3" "/a"))))))) (native-inputs - `(("python" ,python-2))) + `(("which" ,(@ (gnu packages base) which)) + ("python" ,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 bindings.") diff --git a/gnu/packages/python.scm b/gnu/packages/python.scm index fd13339cc..5db3c438e 100644 --- a/gnu/packages/python.scm +++ b/gnu/packages/python.scm @@ -56,6 +56,7 @@ ;;; Copyright © 2018 Clément Lassieur ;;; Copyright © 2018 Maxim Cournoyer ;;; Copyright © 2018 Luther Thompson +;;; Copyright © 2018 Amin Bandali ;;; ;;; This file is part of GNU Guix. ;;; @@ -14989,3 +14990,12 @@ RFC 8265 and RFC 8266.") (description "Simple decorator to set attributes of target function or class in a @acronym{DRY, Don't Repeat Yourself} way.") (license license:expat))) + +(define-public python-z3 z3) + +(define-public python2-z3 + (package (inherit python-z3) + (name "python2-z3") + (native-inputs + `(("which" ,which) + ("python" ,python-2))))) -- 2.20.0 From debbugs-submit-bounces@debbugs.gnu.org Sun Dec 16 10:18:30 2018 Received: (at 33764) by debbugs.gnu.org; 16 Dec 2018 15:18:30 +0000 Received: from localhost ([127.0.0.1]:50494 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gYYBa-0005nw-3N for submit@debbugs.gnu.org; Sun, 16 Dec 2018 10:18:30 -0500 Received: from eggs.gnu.org ([208.118.235.92]:38091) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gYYBY-0005nj-Kc for 33764@debbugs.gnu.org; Sun, 16 Dec 2018 10:18:29 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gYYBS-0005nb-LQ for 33764@debbugs.gnu.org; Sun, 16 Dec 2018 10:18:23 -0500 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=0.8 required=5.0 tests=BAYES_50 autolearn=disabled version=3.3.2 Received: from fencepost.gnu.org ([2001:4830:134:3::e]:41121) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gYYBN-0005fP-LV; Sun, 16 Dec 2018 10:18:18 -0500 Received: from [2a01:e0a:1d:7270:af76:b9b:ca24:c465] (port=59878 helo=ribbon) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1gYYBN-0004Uy-DJ; Sun, 16 Dec 2018 10:18:17 -0500 From: =?utf-8?Q?Ludovic_Court=C3=A8s?= To: Amin Bandali Subject: Re: [bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings. References: <20181216040528.29880-1-bandali@gnu.org> Date: Sun, 16 Dec 2018 16:18:16 +0100 In-Reply-To: <20181216040528.29880-1-bandali@gnu.org> (Amin Bandali's message of "Sat, 15 Dec 2018 23:05:30 -0500") Message-ID: <87bm5lv6tj.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.1 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 2001:4830:134:3::e X-Spam-Score: -5.0 (-----) X-Debbugs-Envelope-To: 33764 Cc: 33764@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -6.0 (------) Hello Amin, Amin Bandali skribis: > * gnu/packages/maths.scm (z3): Update to 4.8.3. > [build-system]: Switch from cmake to make, and use the current > scripts/mk_make.py build script instead of the now-deprecated > contrib/cmake/bootstrap.py. > > * gnu/packages/python.scm (python-z3, python2-z3): New public > variables. Overall LGTM. Some comments: > (native-inputs > - `(("python" ,python-2))) > + `(("which" ,(@ (gnu packages base) which)) > + ("python" ,python-wrapper))) Please add #:use-module (gnu packages which) so you don=E2=80=99t have to r= esort to the @ notation. > --- a/gnu/packages/python.scm > +++ b/gnu/packages/python.scm > @@ -56,6 +56,7 @@ > ;;; Copyright =C2=A9 2018 Cl=C3=A9ment Lassieur > ;;; Copyright =C2=A9 2018 Maxim Cournoyer > ;;; Copyright =C2=A9 2018 Luther Thompson > +;;; Copyright =C2=A9 2018 Amin Bandali > ;;; > ;;; This file is part of GNU Guix. > ;;; > @@ -14989,3 +14990,12 @@ RFC 8265 and RFC 8266.") > (description "Simple decorator to set attributes of target function = or > class in a @acronym{DRY, Don't Repeat Yourself} way.") > (license license:expat))) > + > +(define-public python-z3 z3) Is this variable necessary? Note that this does not create a =E2=80=9Cpython-z3=E2=80=9D package. > +(define-public python2-z3 > + (package (inherit python-z3) This definition cannot be in python.scm; it must be in the same file as =E2=80=98z3=E2=80=99 or we can get =E2=80=9Cunbound variable=E2=80=9D error= s while loading either of these two modules. Also, as we=E2=80=99re approaching end-of-life upstream for Python 2.x, we = now avoid creating =E2=80=9Cpython2-=E2=80=9D packages, unless we cannot avoid = it for some reason. Do you think we could do without this =E2=80=9Cpython2-z3=E2=80=9D= package? Could you send an updated patch? If you think we really need =E2=80=9Cpython2-z3=E2=80=9D, please make it a separate patch. Thank you! Ludo=E2=80=99. From debbugs-submit-bounces@debbugs.gnu.org Mon Dec 17 02:29:30 2018 Received: (at 33764) by debbugs.gnu.org; 17 Dec 2018 07:29:30 +0000 Received: from localhost ([127.0.0.1]:50783 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gYnLG-0000vn-GG for submit@debbugs.gnu.org; Mon, 17 Dec 2018 02:29:30 -0500 Received: from flashner.co.il ([178.62.234.194]:48166) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gYnLE-0000vZ-NJ for 33764@debbugs.gnu.org; Mon, 17 Dec 2018 02:29:29 -0500 Received: from localhost (unknown [141.226.9.73]) by flashner.co.il (Postfix) with ESMTPSA id D829740041; Mon, 17 Dec 2018 07:29:22 +0000 (UTC) Date: Mon, 17 Dec 2018 09:29:21 +0200 From: Efraim Flashner To: Ludovic =?utf-8?Q?Court=C3=A8s?= Subject: Re: [bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings. Message-ID: <20181217072921.GG3468@macbook41> References: <20181216040528.29880-1-bandali@gnu.org> <87bm5lv6tj.fsf@gnu.org> MIME-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha512; protocol="application/pgp-signature"; boundary="LZFKeWUZP29EKQNE" Content-Disposition: inline In-Reply-To: <87bm5lv6tj.fsf@gnu.org> User-Agent: Mutt/1.11.0 (2018-11-25) X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 33764 Cc: 33764@debbugs.gnu.org, Amin Bandali X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) --LZFKeWUZP29EKQNE Content-Type: text/plain; charset=utf-8 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable On Sun, Dec 16, 2018 at 04:18:16PM +0100, Ludovic Court=C3=A8s wrote: > Hello Amin, >=20 > Amin Bandali skribis: >=20 > > * gnu/packages/maths.scm (z3): Update to 4.8.3. > > [build-system]: Switch from cmake to make, and use the current > > scripts/mk_make.py build script instead of the now-deprecated > > contrib/cmake/bootstrap.py. > > > > * gnu/packages/python.scm (python-z3, python2-z3): New public > > variables. >=20 > Overall LGTM. Some comments: >=20 > > (native-inputs > > - `(("python" ,python-2))) > > + `(("which" ,(@ (gnu packages base) which)) > > + ("python" ,python-wrapper))) >=20 > Please add #:use-module (gnu packages which) so you don=E2=80=99t have to= resort > to the @ notation. >=20 > > --- a/gnu/packages/python.scm > > +++ b/gnu/packages/python.scm > > @@ -56,6 +56,7 @@ > > ;;; Copyright =C2=A9 2018 Cl=C3=A9ment Lassieur > > ;;; Copyright =C2=A9 2018 Maxim Cournoyer > > ;;; Copyright =C2=A9 2018 Luther Thompson > > +;;; Copyright =C2=A9 2018 Amin Bandali > > ;;; > > ;;; This file is part of GNU Guix. > > ;;; > > @@ -14989,3 +14990,12 @@ RFC 8265 and RFC 8266.") > > (description "Simple decorator to set attributes of target functio= n or > > class in a @acronym{DRY, Don't Repeat Yourself} way.") > > (license license:expat))) > > + > > +(define-public python-z3 z3) >=20 > Is this variable necessary? Note that this does not create a > =E2=80=9Cpython-z3=E2=80=9D package. >=20 > > +(define-public python2-z3 > > + (package (inherit python-z3) >=20 > This definition cannot be in python.scm; it must be in the same file as > =E2=80=98z3=E2=80=99 or we can get =E2=80=9Cunbound variable=E2=80=9D err= ors while loading either of > these two modules. >=20 > Also, as we=E2=80=99re approaching end-of-life upstream for Python 2.x, w= e now > avoid creating =E2=80=9Cpython2-=E2=80=9D packages, unless we cannot avoi= d it for some > reason. Do you think we could do without this =E2=80=9Cpython2-z3=E2=80= =9D package? >=20 Currently our z3 package builds python2 bindings > Could you send an updated patch? If you think we really need > =E2=80=9Cpython2-z3=E2=80=9D, please make it a separate patch. >=20 > Thank you! >=20 > Ludo=E2=80=99. >=20 We should also check that the other packages that use z3 aren't expecting the python2 bindings when built with the python3 bindings. --=20 Efraim Flashner =D7=90=D7=A4=D7=A8=D7=99=D7=9D = =D7=A4=D7=9C=D7=A9=D7=A0=D7=A8 GPG key =3D A28B F40C 3E55 1372 662D 14F7 41AA E7DC CA3D 8351 Confidentiality cannot be guaranteed on emails sent or received unencrypted --LZFKeWUZP29EKQNE Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQIzBAABCgAdFiEEoov0DD5VE3JmLRT3Qarn3Mo9g1EFAlwXUE4ACgkQQarn3Mo9 g1Epmg/+OY6XPruJUoAszNT7g6kHTUA5Cl4RCLnRMnw1fR+rR7ZRZV1GL8sd+Z20 xjN1vbbQjSnKYBgiRQeHZmRok5fkbjpT7b2WjUtm9AC50Ci4nKYWeyrJQWhdOM3P Nvck5I0c/nI4sV9go3Okcf0+uge+nMBu67Gnq805SnC6zgQXXjT1luErafvSe0cw D91YJxAZZJXj2m7J3F5WIZTe6gwgRd8E63N31uP+9iGfAav6ObWoQfofdXKja/2E 7R/izZG8MpRW0amj1kJNbZNUK7jleZ8iP34QaRPPzzSAYwDWHE3JeXqcwlC2VVdO 2RtAAK7r5FeHoQWLohxl6CAyWzrb+7xHqwHY1NRdtTizJU1Oc137OXtlayrDdBUe AaXsFHG6qfQNvIwoyOGm6f4UC7m8ePrU2dtsp3KqZU8ZPxmyJ2H95B3CKf0JAbMp CPqCmRdeqoFaB86qSq7rf8SJUrRVVnXauJVcvGt8I7XPdjIk/L2lEhqrA8734W9I mB5hS+Lh9oJJ2EXJii+R7U5mrqQGJNn7jR0CprDmqrF2btwVN/iEGdp4nhEj8yxD aPbpr4OSqyR4fRqQbNJwZXO9Qqro5NWFObhphcTIEyPmiJVaTJURysbXE06xBD+7 LIuT71YV8sbTsJiVI3YnLn0nixHogsfltwYV8FTt4KpiSyZ18Ng= =F9/1 -----END PGP SIGNATURE----- --LZFKeWUZP29EKQNE-- From debbugs-submit-bounces@debbugs.gnu.org Mon Dec 17 09:34:30 2018 Received: (at 33764) by debbugs.gnu.org; 17 Dec 2018 14:34:31 +0000 Received: from localhost ([127.0.0.1]:50996 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gYtyY-0007HK-K3 for submit@debbugs.gnu.org; Mon, 17 Dec 2018 09:34:30 -0500 Received: from eggs.gnu.org ([208.118.235.92]:37080) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gYtyV-0007H4-WB for 33764@debbugs.gnu.org; Mon, 17 Dec 2018 09:34:29 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gYtyP-0002Ok-O6 for 33764@debbugs.gnu.org; Mon, 17 Dec 2018 09:34:22 -0500 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=-0.0 required=5.0 tests=BAYES_40 autolearn=disabled version=3.3.2 Received: from fencepost.gnu.org ([2001:4830:134:3::e]:36876) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gYtyG-0002Hj-Ne; Mon, 17 Dec 2018 09:34:12 -0500 Received: from cpe00fc8db93e03-cm00fc8db93e00.cpe.net.cable.rogers.com ([99.228.14.66]:34050 helo=localhost) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1gYtyG-0007mH-IW; Mon, 17 Dec 2018 09:34:12 -0500 From: Amin Bandali To: Efraim Flashner Subject: Re: [bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings. References: <20181216040528.29880-1-bandali@gnu.org> <87bm5lv6tj.fsf@gnu.org> <20181217072921.GG3468@macbook41> Date: Mon, 17 Dec 2018 09:34:11 -0500 In-Reply-To: <20181217072921.GG3468@macbook41> (Efraim Flashner's message of "Mon, 17 Dec 2018 09:29:21 +0200") Message-ID: <87efag6x3w.fsf@aminb.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.0.50 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 2001:4830:134:3::e X-Spam-Score: -5.0 (-----) X-Debbugs-Envelope-To: 33764 Cc: Ludovic =?utf-8?Q?Court=C3=A8s?= , 33764@debbugs.gnu.org, Marius Bakke X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -6.0 (------) Hi Ludo=E2=80=99, Efraim, Thank you both for the feedback. I=E2=80=99ve responded below. On 2018-12-17 9:29 AM, Efraim Flashner wrote: > On Sun, Dec 16, 2018 at 04:18:16PM +0100, Ludovic Court=C3=A8s wrote: >> > (native-inputs >> > - `(("python" ,python-2))) >> > + `(("which" ,(@ (gnu packages base) which)) >> > + ("python" ,python-wrapper))) >>=20 >> Please add #:use-module (gnu packages which) so you don=E2=80=99t have t= o resort >> to the @ notation. Will do for the next version of the patch, thanks. >> > +(define-public python-z3 z3) >>=20 >> Is this variable necessary? Note that this does not create a >> =E2=80=9Cpython-z3=E2=80=9D package. I see! I thought that it /would/ create a python-z3 package; but then again I=E2=80=99m very much a Guix newb :) Since I added a python2-z3, I th= ought I would also add a python-z3 for =E2=80=98symmetry=E2=80=99 in case someone= expects it. Should I then add a (define-public python-z3 (package inherit z3)) if we decide to add the python2-z3 bindings? >> > +(define-public python2-z3 >> > + (package (inherit python-z3) >>=20 >> This definition cannot be in python.scm; it must be in the same file as >> =E2=80=98z3=E2=80=99 or we can get =E2=80=9Cunbound variable=E2=80=9D er= rors while loading either of >> these two modules. Oh I see. If we choose to keep it (add it), I=E2=80=99ll move it to maths.= scm. >> Also, as we=E2=80=99re approaching end-of-life upstream for Python 2.x, = we now >> avoid creating =E2=80=9Cpython2-=E2=80=9D packages, unless we cannot avo= id it for some >> reason. Do you think we could do without this =E2=80=9Cpython2-z3=E2=80= =9D package? >>=20 > > Currently our z3 package builds python2 bindings What Efraim said. Since the current z3 provides python2 bindings, I thought I would preserve that option by adding a python2-z3 in case anyone wants to continue to use the python2 bindings. I=E2=80=99m Cc=E2=80=99ing Marius who=E2=80=99s one of the recent committer= s to the z3 package definition. Marius, any thoughts on whether we should keep the python2 bindings around or do away with them? >> Could you send an updated patch? If you think we really need >> =E2=80=9Cpython2-z3=E2=80=9D, please make it a separate patch. Sure. I=E2=80=99ll send an update patch (or patches) once we figure out wh= ether we should keep the python2 bindings around. > > We should also check that the other packages that use z3 aren't > expecting the python2 bindings when built with the python3 bindings. > Right. grepping through the codebase, I see that only two other packages depend on z3: cubicle (in maths.scm) and yosys (in fpga.scm). cubicle is an ocaml package and doesn=E2=80=99t seem to use the python bind= ings of z3, and yosys seems to only use z3 as an executable, not a library. So, it appears to me that as of now, there are no packages that depend on the python2 bindings of z3. If so, do we drop python2-z3 (and also python-z3) altogether and just switch z3 to python3? Best, amin From debbugs-submit-bounces@debbugs.gnu.org Fri Dec 21 12:02:26 2018 Received: (at 33764) by debbugs.gnu.org; 21 Dec 2018 17:02:26 +0000 Received: from localhost ([127.0.0.1]:58747 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gaOBu-0002Jy-5m for submit@debbugs.gnu.org; Fri, 21 Dec 2018 12:02:26 -0500 Received: from eggs.gnu.org ([208.118.235.92]:33524) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gaOBt-0002G3-8G for 33764@debbugs.gnu.org; Fri, 21 Dec 2018 12:02:25 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gaOBj-0003pN-Qf for 33764@debbugs.gnu.org; Fri, 21 Dec 2018 12:02:19 -0500 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=disabled version=3.3.2 Received: from fencepost.gnu.org ([2001:4830:134:3::e]:45794) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gaOBZ-0003hV-VG; Fri, 21 Dec 2018 12:02:06 -0500 Received: from [2a01:e0a:1d:7270:af76:b9b:ca24:c465] (port=55404 helo=ribbon) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1gaOBY-0005bi-SB; Fri, 21 Dec 2018 12:02:05 -0500 From: =?utf-8?Q?Ludovic_Court=C3=A8s?= To: Amin Bandali Subject: Re: [bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings. References: <20181216040528.29880-1-bandali@gnu.org> <87bm5lv6tj.fsf@gnu.org> <20181217072921.GG3468@macbook41> <87efag6x3w.fsf@aminb.org> Date: Fri, 21 Dec 2018 18:02:02 +0100 In-Reply-To: <87efag6x3w.fsf@aminb.org> (Amin Bandali's message of "Mon, 17 Dec 2018 09:34:11 -0500") Message-ID: <87k1k2olth.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.1 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 2001:4830:134:3::e X-Spam-Score: -5.0 (-----) X-Debbugs-Envelope-To: 33764 Cc: Marius Bakke , 33764@debbugs.gnu.org, Efraim Flashner X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -6.0 (------) Hello! Amin Bandali skribis: > On 2018-12-17 9:29 AM, Efraim Flashner wrote: >> On Sun, Dec 16, 2018 at 04:18:16PM +0100, Ludovic Court=C3=A8s wrote: [...] >>> > +(define-public python2-z3 >>> > + (package (inherit python-z3) >>>=20 >>> This definition cannot be in python.scm; it must be in the same file as >>> =E2=80=98z3=E2=80=99 or we can get =E2=80=9Cunbound variable=E2=80=9D e= rrors while loading either of >>> these two modules. > > Oh I see. If we choose to keep it (add it), I=E2=80=99ll move it to math= s.scm. > >>> Also, as we=E2=80=99re approaching end-of-life upstream for Python 2.x,= we now >>> avoid creating =E2=80=9Cpython2-=E2=80=9D packages, unless we cannot av= oid it for some >>> reason. Do you think we could do without this =E2=80=9Cpython2-z3=E2= =80=9D package? >>>=20 >> >> Currently our z3 package builds python2 bindings > > What Efraim said. Since the current z3 provides python2 bindings, I > thought I would preserve that option by adding a python2-z3 in case > anyone wants to continue to use the python2 bindings. > > I=E2=80=99m Cc=E2=80=99ing Marius who=E2=80=99s one of the recent committ= ers to the z3 package > definition. Marius, any thoughts on whether we should keep the python2 > bindings around or do away with them? Marius, WDYT? Ludo=E2=80=99. From debbugs-submit-bounces@debbugs.gnu.org Fri Dec 21 15:41:03 2018 Received: (at 33764) by debbugs.gnu.org; 21 Dec 2018 20:41:03 +0000 Received: from localhost ([127.0.0.1]:58838 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gaRbS-0008AD-Ui for submit@debbugs.gnu.org; Fri, 21 Dec 2018 15:41:03 -0500 Received: from out1-smtp.messagingengine.com ([66.111.4.25]:49449) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gaRbR-00089b-4x for 33764@debbugs.gnu.org; Fri, 21 Dec 2018 15:41:01 -0500 Received: from compute5.internal (compute5.nyi.internal [10.202.2.45]) by mailout.nyi.internal (Postfix) with ESMTP id 9783121F51; Fri, 21 Dec 2018 15:40:55 -0500 (EST) Received: from mailfrontend1 ([10.202.2.162]) by compute5.internal (MEProxy); Fri, 21 Dec 2018 15:40:55 -0500 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=fastmail.com; h= from:to:cc:subject:in-reply-to:references:date:message-id :mime-version:content-type; s=fm1; bh=Ad+Ex9Dfk7SSxoLMzObm48G10c xpE9qXikGZ1dOj8FM=; b=Zw4GpwVijK4RbanSDAHfRegtjoGjMqLjFlsLgvet22 bGWB/1m0BK2alwHzsDsjWmyXanAU680mcJIUTsrZTCgxLjFFVFg+asucxfELRRIY 009bWuNgv0woGfysgijUFFpxIbB2CDd3aKNcOZ8qlr7kAu1BBt6IloORmgoJEWPW vTZvIvfjqXP9hdRJQSNCa1iQ6xZZb/bw47By3P8a/AkoxaUDEOMzwGuvHjra6O4X HsACjrF+15+oioDzm8jNqhz/gLHBCu08bCOBTe4enCox5DqpadLCY9nGWzmgnS3Q uDffplVA2rS87oGAN7MRgXWIx8BNTFOBuf/MYbmdyYxw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d= messagingengine.com; h=cc:content-type:date:from:in-reply-to :message-id:mime-version:references:subject:to:x-me-proxy :x-me-proxy:x-me-sender:x-me-sender:x-sasl-enc; s=fm1; bh=Ad+Ex9 Dfk7SSxoLMzObm48G10cxpE9qXikGZ1dOj8FM=; b=Qq6P3RLf1lfL8XrivnRN1j 641FJa3UPV0EeuL9lDQmwfENOyXGFFQZH/yZZMBrBA4l3YFJmQKXH+5/OV5axZsa Nv4WSwtkVxlLVUL6tuLGKVshmPH9JvXulfsJ0RewqfpPesvKR5lHNVPtnBc6TYxP jdtOxK0N+qB8kbnWxSbiWZiUWbrCErcBdmWtV+NYq4OncIWsrSDx3/YXTIoxldRg 7XZ83p25AD5WOfzG6tFUMK5zg9QxaQXDfuqzDOD4L3f+aCaASzAX2WYgjVXKJ189 EdquzeIvVpqLeoFnGJk3nb5dKmRmzX3vOcDUzZ/ZIwX2N7D9GKCqcZIufsf3EM9w == X-ME-Sender: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedtkedrudejhedgudegudcutefuodetggdotefrod ftvfcurfhrohhfihhlvgemucfhrghsthforghilhdpqfhuthenuceurghilhhouhhtmecu fedttdenucesvcftvggtihhpihgvnhhtshculddquddttddmnecujfgurhephffvufgjfh gffffkgggtsehgtderredtreejnecuhfhrohhmpeforghrihhushcuuegrkhhkvgcuoehm sggrkhhkvgesfhgrshhtmhgrihhlrdgtohhmqeenucffohhmrghinhepphihthhhohhnrd horhhgnecukfhppeeivddrudeirddvvdeirddugedtnecurfgrrhgrmhepmhgrihhlfhhr ohhmpehmsggrkhhkvgesfhgrshhtmhgrihhlrdgtohhmnecuvehluhhsthgvrhfuihiivg eptd X-ME-Proxy: Received: from localhost (140.226.16.62.customer.cdi.no [62.16.226.140]) by mail.messagingengine.com (Postfix) with ESMTPA id 97819E436E; Fri, 21 Dec 2018 15:40:54 -0500 (EST) From: Marius Bakke To: Ludovic =?utf-8?Q?Court=C3=A8s?= , Amin Bandali Subject: Re: [bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings. In-Reply-To: <87k1k2olth.fsf@gnu.org> References: <20181216040528.29880-1-bandali@gnu.org> <87bm5lv6tj.fsf@gnu.org> <20181217072921.GG3468@macbook41> <87efag6x3w.fsf@aminb.org> <87k1k2olth.fsf@gnu.org> User-Agent: Notmuch/0.28 (https://notmuchmail.org) Emacs/26.1 (x86_64-pc-linux-gnu) Date: Fri, 21 Dec 2018 21:40:47 +0100 Message-ID: <874lb6aa0g.fsf@fastmail.com> MIME-Version: 1.0 Content-Type: multipart/signed; boundary="=-=-="; micalg=pgp-sha512; protocol="application/pgp-signature" X-Spam-Score: -0.7 (/) X-Debbugs-Envelope-To: 33764 Cc: 33764@debbugs.gnu.org, Efraim Flashner X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.7 (-) --=-=-= Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Ludovic Court=C3=A8s writes: > Hello! > > Amin Bandali skribis: > >> On 2018-12-17 9:29 AM, Efraim Flashner wrote: >>> On Sun, Dec 16, 2018 at 04:18:16PM +0100, Ludovic Court=C3=A8s wrote: > > [...] > >>>> > +(define-public python2-z3 >>>> > + (package (inherit python-z3) >>>>=20 >>>> This definition cannot be in python.scm; it must be in the same file as >>>> =E2=80=98z3=E2=80=99 or we can get =E2=80=9Cunbound variable=E2=80=9D = errors while loading either of >>>> these two modules. >> >> Oh I see. If we choose to keep it (add it), I=E2=80=99ll move it to mat= hs.scm. >> >>>> Also, as we=E2=80=99re approaching end-of-life upstream for Python 2.x= , we now >>>> avoid creating =E2=80=9Cpython2-=E2=80=9D packages, unless we cannot a= void it for some >>>> reason. Do you think we could do without this =E2=80=9Cpython2-z3=E2= =80=9D package? >>>>=20 >>> >>> Currently our z3 package builds python2 bindings >> >> What Efraim said. Since the current z3 provides python2 bindings, I >> thought I would preserve that option by adding a python2-z3 in case >> anyone wants to continue to use the python2 bindings. >> >> I=E2=80=99m Cc=E2=80=99ing Marius who=E2=80=99s one of the recent commit= ters to the z3 package >> definition. Marius, any thoughts on whether we should keep the python2 >> bindings around or do away with them? > > Marius, WDYT? Hello! I don't actually know z3 at all, I just updated it to fix the build on core-updates :-) In any case dropping python2 bindings seems sensible, seeing as Python 2 is EOL in a year[1]. So please go ahead, thank you Amin! [1]: https://www.python.org/dev/peps/pep-0373/ --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQEzBAEBCgAdFiEEu7At3yzq9qgNHeZDoqBt8qM6VPoFAlwdT88ACgkQoqBt8qM6 VPrw4Qf+O5a19rZwuURvfrI2jJ+Ncn/xi8cRywuv+++sPWMp3gC1Ult2QxXDao+T ttupksN2uERD2KKj//+MfQUcE3bRPJuqU5hsoitN/ca/br7903AKmeXJUwLf6PbG BY4gIQRdMpvlyE3I0Ex4JZJLz5VIjeuYmSeBjy2l4UAoil1N5W9LjKh3aZ8LkA6T YVIrtXOPvpSxOBXLE0MMmZjnPWFuavrobDfYl4MCaSfX8fceGTlDBKTYFrsbuK+d VKEHOtHDdO2xeTCWfQ9rGrN1nsuqvSztnB49z9rpEvd2hbCFgiPXBou8t/ywL1Jy Amn9StJp3qa6a8Eoy3vUpRldDwDguQ== =dzxn -----END PGP SIGNATURE----- --=-=-=-- From debbugs-submit-bounces@debbugs.gnu.org Fri Dec 21 18:42:14 2018 Received: (at 33764) by debbugs.gnu.org; 21 Dec 2018 23:42:14 +0000 Received: from localhost ([127.0.0.1]:58989 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gaUQk-00061u-VW for submit@debbugs.gnu.org; Fri, 21 Dec 2018 18:42:14 -0500 Received: from eggs.gnu.org ([208.118.235.92]:35815) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gaUQj-00061i-Fi for 33764@debbugs.gnu.org; Fri, 21 Dec 2018 18:42:09 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gaUQd-0004B3-CP for 33764@debbugs.gnu.org; Fri, 21 Dec 2018 18:42:04 -0500 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=disabled version=3.3.2 Received: from fencepost.gnu.org ([2001:4830:134:3::e]:53951) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gaUQS-00041B-SV; Fri, 21 Dec 2018 18:41:53 -0500 Received: from [2607:fea8:3ba0:f85::5] (port=41766 helo=localhost) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1gaUQS-0001hF-Ni; Fri, 21 Dec 2018 18:41:52 -0500 From: Amin Bandali To: Marius Bakke Subject: Re: [bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings. References: <20181216040528.29880-1-bandali@gnu.org> <87bm5lv6tj.fsf@gnu.org> <20181217072921.GG3468@macbook41> <87efag6x3w.fsf@aminb.org> <87k1k2olth.fsf@gnu.org> <874lb6aa0g.fsf@fastmail.com> Date: Fri, 21 Dec 2018 18:41:51 -0500 In-Reply-To: <874lb6aa0g.fsf@fastmail.com> (Marius Bakke's message of "Fri, 21 Dec 2018 21:40:47 +0100") Message-ID: <87h8f6curk.fsf@aminb.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.0.50 (gnu/linux) MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="=-=-=" X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 2001:4830:134:3::e X-Spam-Score: -5.0 (-----) X-Debbugs-Envelope-To: 33764 Cc: Ludovic =?utf-8?Q?Court=C3=A8s?= , 33764@debbugs.gnu.org, Efraim Flashner X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -6.0 (------) --=-=-= Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Hello! On 2018-12-21 9:40 PM, Marius Bakke wrote: > Ludovic Court=C3=A8s writes: > >> Hello! >> >> [...] >> >> Marius, WDYT? > > Hello! > > I don't actually know z3 at all, I just updated it to fix the build on > core-updates :-) > > In any case dropping python2 bindings seems sensible, seeing as Python 2 > is EOL in a year[1]. So please go ahead, thank you Amin! > > [1]: https://www.python.org/dev/peps/pep-0373/ > Thanks for the reply, Marius. I=E2=80=99ve attached a new version of the p= atch with only Python 3 bindings and with Ludo=E2=80=99s feedback about =E2=80= =98which=E2=80=99. Best, amin --=-=-= Content-Type: text/x-patch; charset=utf-8 Content-Disposition: attachment; filename=0001-gnu-z3-Update-to-4.8.3-and-provide-python3-bindings.patch Content-Transfer-Encoding: quoted-printable >From ed80a156cd0aa3d7839e49bd6ebdd5e2911067ae Mon Sep 17 00:00:00 2001 From: Amin Bandali Date: Fri, 21 Dec 2018 18:27:11 -0500 Subject: [PATCH v2] gnu: z3: Update to 4.8.3 and provide python3 bindings * gnu/packages/maths.scm (z3): Update to 4.8.3. [build-system]: Switch from cmake to make, and use the current scripts/mk_make.py build script instead of the now-deprecated contrib/cmake/bootstrap.py. --- gnu/packages/maths.scm | 32 ++++++++++++++++++++------------ 1 file changed, 20 insertions(+), 12 deletions(-) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 9fb02b738..f49b50c23 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -29,6 +29,7 @@ ;;; Copyright =C2=A9 2018 Marius Bakke ;;; Copyright =C2=A9 2018 Eric Brown ;;; Copyright =C2=A9 2018 Julien Lepiller +;;; Copyright =C2=A9 2018 Amin Bandali ;;; ;;; This file is part of GNU Guix. ;;; @@ -116,6 +117,7 @@ #:use-module (gnu packages tex) #:use-module (gnu packages tls) #:use-module (gnu packages version-control) + #:use-module (gnu packages which) #:use-module (gnu packages wxwidgets) #:use-module (gnu packages xml) #:use-module (srfi srfi-1)) @@ -3965,7 +3967,7 @@ as equations, scalars, vectors, and matrices.") (define-public z3 (package (name "z3") - (version "4.8.1") + (version "4.8.3") (home-page "https://github.com/Z3Prover/z3") (source (origin (method git-fetch) @@ -3974,16 +3976,10 @@ as equations, scalars, vectors, and matrices.") (file-name (git-file-name name version)) (sha256 (base32 - "1vr57bwx40sd5riijyrhy70i2wnv9xrdihf6y5zdz56yq88rl48f")))) - (build-system cmake-build-system) + "0p5gdmhd32x6zwmx7j5cgwh4jyfxa9yapym95nlmyfaqzak92qar")))) + (build-system gnu-build-system) (arguments - `(#:configure-flags - (list "-DBUILD_PYTHON_BINDINGS=3Dtrue" - "-DINSTALL_PYTHON_BINDINGS=3Dtrue" - (string-append "-DCMAKE_INSTALL_PYTHON_PKG_DIR=3D" - %output - "/lib/python2.7/site-packages")) - #:phases + `(#:phases (modify-phases %standard-phases (add-after 'unpack 'fix-compatability ;; Versions after 4.8.3 have immintrin.h IFDEFed for Windows on= ly. @@ -3994,7 +3990,18 @@ as equations, scalars, vectors, and matrices.") (add-before 'configure 'bootstrap (lambda _ (zero? - (system* "python" "contrib/cmake/bootstrap.py" "create")))) + (system* "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" + (string-append "--prefix=3D" (assoc-ref outputs "out"= ))))) + (add-after 'configure 'change-directory + (lambda _ + (chdir "build") + #t)) (add-before 'check 'make-test-z3 (lambda _ ;; Build the test suite executable. @@ -4005,7 +4012,8 @@ as equations, scalars, vectors, and matrices.") ;; Run all the tests that don't require arguments. (zero? (system* "./test-z3" "/a"))))))) (native-inputs - `(("python" ,python-2))) + `(("which" ,(@ (gnu packages base) which)) + ("python" ,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.20.1 --=-=-=-- From debbugs-submit-bounces@debbugs.gnu.org Sat Dec 22 10:21:34 2018 Received: (at 33764) by debbugs.gnu.org; 22 Dec 2018 15:21:34 +0000 Received: from localhost ([127.0.0.1]:60133 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gaj5m-00087m-T0 for submit@debbugs.gnu.org; Sat, 22 Dec 2018 10:21:34 -0500 Received: from eggs.gnu.org ([208.118.235.92]:48956) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gaj5l-00087V-49 for 33764@debbugs.gnu.org; Sat, 22 Dec 2018 10:21:29 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gaj5d-0007bB-PP for 33764@debbugs.gnu.org; Sat, 22 Dec 2018 10:21:23 -0500 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=-0.0 required=5.0 tests=BAYES_20 autolearn=disabled version=3.3.2 Received: from fencepost.gnu.org ([2001:4830:134:3::e]:41546) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gaj5E-0006kk-Ix; Sat, 22 Dec 2018 10:20:58 -0500 Received: from [2607:fea8:3ba0:f85::5] (port=49314 helo=localhost) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1gaj5E-0000NG-E7; Sat, 22 Dec 2018 10:20:56 -0500 From: Amin Bandali To: Marius Bakke Subject: Re: [bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings. References: <20181216040528.29880-1-bandali@gnu.org> <87bm5lv6tj.fsf@gnu.org> <20181217072921.GG3468@macbook41> <87efag6x3w.fsf@aminb.org> <87k1k2olth.fsf@gnu.org> <874lb6aa0g.fsf@fastmail.com> <87h8f6curk.fsf@aminb.org> Date: Sat, 22 Dec 2018 10:20:55 -0500 In-Reply-To: <87h8f6curk.fsf@aminb.org> (Amin Bandali's message of "Fri, 21 Dec 2018 18:41:51 -0500") Message-ID: <87d0ptfuzs.fsf@aminb.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.0.50 (gnu/linux) MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="=-=-=" X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 2001:4830:134:3::e X-Spam-Score: -5.0 (-----) X-Debbugs-Envelope-To: 33764 Cc: Ludovic =?utf-8?Q?Court=C3=A8s?= , 33764@debbugs.gnu.org, Efraim Flashner X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -6.0 (------) --=-=-= Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Apologies, I just realized that I forgot to remove my use of the @ notation in my v2 patch submitted earlier. I=E2=80=99ve attached an update= d one that doesn=E2=80=99t. --=-=-= Content-Type: text/x-patch; charset=utf-8 Content-Disposition: attachment; filename=0001-gnu-z3-Update-to-4.8.3-and-provide-python3-bindings.patch Content-Transfer-Encoding: quoted-printable >From ad9433c11ebba672db3ca75689ebee92ea9da7de Mon Sep 17 00:00:00 2001 From: Amin Bandali Date: Sat, 22 Dec 2018 10:16:57 -0500 Subject: [PATCH v3] gnu: z3: Update to 4.8.3 and provide python3 bindings * gnu/packages/maths.scm (z3): Update to 4.8.3. [build-system]: Switch from cmake to make, and use the current scripts/mk_make.py build script instead of the now-deprecated contrib/cmake/bootstrap.py. --- gnu/packages/maths.scm | 32 ++++++++++++++++++++------------ 1 file changed, 20 insertions(+), 12 deletions(-) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 9fb02b738..1b6127e9f 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -29,6 +29,7 @@ ;;; Copyright =C2=A9 2018 Marius Bakke ;;; Copyright =C2=A9 2018 Eric Brown ;;; Copyright =C2=A9 2018 Julien Lepiller +;;; Copyright =C2=A9 2018 Amin Bandali ;;; ;;; This file is part of GNU Guix. ;;; @@ -116,6 +117,7 @@ #:use-module (gnu packages tex) #:use-module (gnu packages tls) #:use-module (gnu packages version-control) + #:use-module (gnu packages which) #:use-module (gnu packages wxwidgets) #:use-module (gnu packages xml) #:use-module (srfi srfi-1)) @@ -3965,7 +3967,7 @@ as equations, scalars, vectors, and matrices.") (define-public z3 (package (name "z3") - (version "4.8.1") + (version "4.8.3") (home-page "https://github.com/Z3Prover/z3") (source (origin (method git-fetch) @@ -3974,16 +3976,10 @@ as equations, scalars, vectors, and matrices.") (file-name (git-file-name name version)) (sha256 (base32 - "1vr57bwx40sd5riijyrhy70i2wnv9xrdihf6y5zdz56yq88rl48f")))) - (build-system cmake-build-system) + "0p5gdmhd32x6zwmx7j5cgwh4jyfxa9yapym95nlmyfaqzak92qar")))) + (build-system gnu-build-system) (arguments - `(#:configure-flags - (list "-DBUILD_PYTHON_BINDINGS=3Dtrue" - "-DINSTALL_PYTHON_BINDINGS=3Dtrue" - (string-append "-DCMAKE_INSTALL_PYTHON_PKG_DIR=3D" - %output - "/lib/python2.7/site-packages")) - #:phases + `(#:phases (modify-phases %standard-phases (add-after 'unpack 'fix-compatability ;; Versions after 4.8.3 have immintrin.h IFDEFed for Windows on= ly. @@ -3994,7 +3990,18 @@ as equations, scalars, vectors, and matrices.") (add-before 'configure 'bootstrap (lambda _ (zero? - (system* "python" "contrib/cmake/bootstrap.py" "create")))) + (system* "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" + (string-append "--prefix=3D" (assoc-ref outputs "out"= ))))) + (add-after 'configure 'change-directory + (lambda _ + (chdir "build") + #t)) (add-before 'check 'make-test-z3 (lambda _ ;; Build the test suite executable. @@ -4005,7 +4012,8 @@ as equations, scalars, vectors, and matrices.") ;; Run all the tests that don't require arguments. (zero? (system* "./test-z3" "/a"))))))) (native-inputs - `(("python" ,python-2))) + `(("which" ,which) + ("python" ,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.20.1 --=-=-=-- From debbugs-submit-bounces@debbugs.gnu.org Sun Dec 23 12:34:03 2018 Received: (at 33764-done) by debbugs.gnu.org; 23 Dec 2018 17:34:03 +0000 Received: from localhost ([127.0.0.1]:33985 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gb7db-0006Xl-5k for submit@debbugs.gnu.org; Sun, 23 Dec 2018 12:34:03 -0500 Received: from hera.aquilenet.fr ([185.233.100.1]:52446) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gb7dZ-0006XQ-Kn for 33764-done@debbugs.gnu.org; Sun, 23 Dec 2018 12:34:02 -0500 Received: from localhost (localhost [127.0.0.1]) by hera.aquilenet.fr (Postfix) with ESMTP id 2A5091282; Sun, 23 Dec 2018 18:34:01 +0100 (CET) X-Virus-Scanned: Debian amavisd-new at aquilenet.fr Received: from hera.aquilenet.fr ([127.0.0.1]) by localhost (hera.aquilenet.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id Gq87bDfWpAn7; Sun, 23 Dec 2018 18:34:00 +0100 (CET) Received: from ribbon (unknown [IPv6:2a01:e0a:1d:7270:af76:b9b:ca24:c465]) by hera.aquilenet.fr (Postfix) with ESMTPSA id 0E148123E; Sun, 23 Dec 2018 18:33:59 +0100 (CET) From: =?utf-8?Q?Ludovic_Court=C3=A8s?= To: Amin Bandali Subject: Re: [bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings. References: <20181216040528.29880-1-bandali@gnu.org> <87bm5lv6tj.fsf@gnu.org> <20181217072921.GG3468@macbook41> <87efag6x3w.fsf@aminb.org> <87k1k2olth.fsf@gnu.org> <874lb6aa0g.fsf@fastmail.com> <87h8f6curk.fsf@aminb.org> <87d0ptfuzs.fsf@aminb.org> X-URL: http://www.fdn.fr/~lcourtes/ X-Revolutionary-Date: 3 =?utf-8?Q?Niv=C3=B4se?= an 227 de la =?utf-8?Q?R?= =?utf-8?Q?=C3=A9volution?= X-PGP-Key-ID: 0x090B11993D9AEBB5 X-PGP-Key: http://www.fdn.fr/~lcourtes/ludovic.asc X-PGP-Fingerprint: 3CE4 6455 8A84 FDC6 9DB4 0CFB 090B 1199 3D9A EBB5 X-OS: x86_64-pc-linux-gnu Date: Sun, 23 Dec 2018 18:33:59 +0100 In-Reply-To: <87d0ptfuzs.fsf@aminb.org> (Amin Bandali's message of "Sat, 22 Dec 2018 10:20:55 -0500") Message-ID: <878t0gi1vc.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.1 (gnu/linux) MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="=-=-=" X-Spam-Score: 1.0 (+) X-Debbugs-Envelope-To: 33764-done Cc: Marius Bakke , 33764-done@debbugs.gnu.org, Efraim Flashner X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.0 (/) --=-=-= Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Hi Amin, Amin Bandali skribis: > From ad9433c11ebba672db3ca75689ebee92ea9da7de Mon Sep 17 00:00:00 2001 > From: Amin Bandali > Date: Sat, 22 Dec 2018 10:16:57 -0500 > Subject: [PATCH v3] gnu: z3: Update to 4.8.3 and provide python3 bindings > > * gnu/packages/maths.scm (z3): Update to 4.8.3. > [build-system]: Switch from cmake to make, and use the current > scripts/mk_make.py build script instead of the now-deprecated > contrib/cmake/bootstrap.py. Applied with the fixes below for =E2=80=98which=E2=80=99. Thank you! Ludo=E2=80=99. --=-=-= Content-Type: text/x-patch Content-Disposition: inline diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 1b6127e9f7..448d9e373b 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -54,7 +54,7 @@ #:use-module (guix download) #:use-module (guix git-download) #:use-module (guix utils) - #:use-module (guix build utils) + #:use-module ((guix build utils) #:select (alist-replace)) #:use-module (guix build-system cmake) #:use-module (guix build-system gnu) #:use-module (guix build-system ocaml) @@ -64,6 +64,7 @@ #:use-module (gnu packages algebra) #:use-module (gnu packages audio) #:use-module (gnu packages autotools) + #:use-module (gnu packages base) #:use-module (gnu packages bison) #:use-module (gnu packages boost) #:use-module (gnu packages check) @@ -117,7 +118,6 @@ #:use-module (gnu packages tex) #:use-module (gnu packages tls) #:use-module (gnu packages version-control) - #:use-module (gnu packages which) #:use-module (gnu packages wxwidgets) #:use-module (gnu packages xml) #:use-module (srfi srfi-1)) --=-=-=-- From unknown Tue Sep 09 06:48:51 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Mon, 21 Jan 2019 12:24:05 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # bug archived. thanks # This fakemail brought to you by your local debbugs # administrator